unison
unison copied to clipboard
Badly formatted type error in this case
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