unison icon indicating copy to clipboard operation
unison copied to clipboard

Badly formatted type error in this case

Open pchiusano opened this issue 6 months ago • 0 comments

ability Ask2 a where
  ask2 : a

Ask2.provide : a -> '{Ask2 a, g} x -> x
Ask2.provide a thunk = handle thunk() with cases
  { x } -> x
  { Ask2.ask2 -> k } -> Ask2.provide a do k a

Hits:

  Sorry, you hit an error we didn't make a nice message for yet.
  
  Here is a summary of the Note:
  
    simple cause:
      TypeMismatch
    context:
    Γ
      |start1|
      |let-rec-marker2|
      Ask1.provide3 : a -> (Unit ->{Ask1 a, g} x) ->{g} x
      |let-rec-marker76|
      |𝕩78|
      'Inference Ability-79
      'Inference Ability-138
      '𝕖139 = 𝕖79
      'User "g"-140
      '𝕖80 = 𝕖138, 𝕖79, g140
      Ask2.provide77 : a ->{𝕖79} (Unit ->{Ask2 a, g} x) ->{𝕖138, 𝕖79, g140} x
      |a82|
      @a83
      |g85|
      @g86
      |x88|
      @x89
      |a91|
      @a92
      |g94|
      @g95
      |x97|
      @x98
      |a100|
      a99 : a92
      |thunk102|
      thunk101 : Unit ->{Ask2 a92, g95} x98
      '𝕧112 = x98
      'Inference Ability-115
      'a118 = a92
      '𝕗117 = Ask2
      '𝕖116 = Ask2 a92
      '𝕦114 = 𝕖115, Ask2 a92
      '𝕗113 = Request
      '𝕗111 = Request {𝕖115, Ask2 a92}
      'roev5vjvom1104 = Request {𝕖115, Ask2 a92} x98
      '𝕖134 = 
      '𝕖135 = 𝕖79
      '𝕖136 = 𝕖138, 𝕖79, g140
      '𝕖105 = 𝕖79, 𝕖138, 𝕖79, g140
      '𝕣106 = x98
      roev5vjvom1103 : Request {𝕖115, Ask2 a92} x98
      'a107 = a92
      '𝕖109 = 𝕖115
      '𝕧108 = x98
      'Inference Ability-110
      'User "a"-133
      'Inference Ability-137
  

Changing to this fixes it and causes it to compile

Ask2.provide : a -> '{Ask2 a, g} x ->{g} x
Ask2.provide a thunk = handle thunk() with cases
  { x } -> x
  { Ask2.ask2 -> k } -> Ask2.provide a do k a

pchiusano avatar Apr 15 '25 17:04 pchiusano