System F Omega: Type Errors Are Broken

[DylanMoss1]

I may be mistaken, but I believe that type errors are currently broken in system F omega.

A minimal example that type checks when it shouldn't:

main :: Unit
main = 1;

I believe the issue is in the function solve_evar(self, name, ty). If the evar is already solved then we immediately return Ok. Whereas, we should first check that ty and evar do not conflict (e.g. they are not both concrete types containing different values).

I have added type conflict checks, and a new new error: TypeUnificationError, to cover these cases. The previous example now fails to type check as expected.

Please let me know if this makes sense, and if there are any other cases I might be missing?

[sdiehl]

This is a good solution. So now we have:

• Two concrete types (Con) must be identical
• Existential type variables can still be unified with anything
• Structural types recurse to check compatibility

I'll just do some checks and merge this and update some of the prose.

[sdiehl]

All merged, thanks for looking into this bug. Appreciate it. 😄