Better type error messages when there are unification variables involved #1318
Conversation
- Rename `expect` to `unify` - Add a `Syntax` argument to all `decomposeXXX` functions - Add `Source` and `Join` machinery to properly keep track of which type is "expected" and which is "actual"
This helps with error messages for multi-argument polymorphic function application (e.g. `if`).
Co-authored-by: Restyled.io <commits@restyled.io>
Co-authored-by: Restyled.io <commits@restyled.io>
test/unit/TestLanguagePipeline.hs
Outdated
| "definition with wrong result" | ||
| ( process | ||
| "def m : int -> int -> int = \\x. \\y. {3} end" | ||
| "1:37: Type mismatch:\n From context, expected `{3}` to have type `int`,\n but it is actually a delayed expression" |
There was a problem hiding this comment.
Could you please add a test case for two functions?
It seems to be handled based on the cmd test case above, but it would be nice to be sure we don't say:
expected
fto be a function, but it is actually a function!
There was a problem hiding this comment.
I added a couple test cases involving incompatible functions to show what happens. We will never say "expected f to be a function, but it is actually a function", for two reasons: first, if we are trying to unify two types and they are both function types, then we will proceed to unifying their input and output types, so we would never fail at the point where we have two function types. Second, we only say "blah is a function" when it specifically has a type of the form u1 -> u2 where u1 and u2 are unification variables. Any two such types will be guaranteed to be unifiable.
Say things like "expecting
xyzto be a function" instead of "expectingxyzto have typeu3 -> u4". Closes #1313.