You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I think the solution is to give an explicit type to any term that isn't applied to a quantified variable (variables always get types when bound in the lambda.)
The text was updated successfully, but these errors were encountered:
Reopening, because this is also an issue when printing equations in "normal" mode.
I think if we want to solve this in all cases, we have to take the generated equation (without type annotations) and do type inference on it. Then add extra type annotations so that the inferred type matches up with the actual type of the discovered law.
Consider the following signature:
which produces the following output:
But uh oh! This code is ambiguous in
a
!I think the solution is to give an explicit type to any term that isn't applied to a quantified variable (variables always get types when bound in the lambda.)
The text was updated successfully, but these errors were encountered: