This PR overhauls our representation of types, and reimplements HM-style type inference using the unification-fd library. It fixes known soundness issues with references (using value restriction) and pattern matches (with smarter unification of type variables), and adds support for using type annotations to restrict the type of polymorphic terms. This rewrite makes heavy use of PatternSynonyms and ViewPatterns for an easier time with builtin types.
A few things remain:
[x] segment let definition blocks that aren't actually mutually recursive, to increase polymorphism
[ ] actually unroll pattern annotations rather than discarding them
[ ] typecheck type definitions, i.e., check the kind of each type constructor
[ ] document everything lmao
[x] fix test suite lmao
At this point, there is very little in the way of proper support for builtin tuples and even lists; perhaps I will bake these in somewhere too.
Since this is a pretty big change, I don't want to let this sit and become stale. All tests are passing as is so I'm going merge this in now and address remaining issues with inference in a subsequent PR.
This PR overhauls our representation of types, and reimplements HM-style type inference using the unification-fd library. It fixes known soundness issues with references (using value restriction) and pattern matches (with smarter unification of type variables), and adds support for using type annotations to restrict the type of polymorphic terms. This rewrite makes heavy use of PatternSynonyms and ViewPatterns for an easier time with builtin types.
A few things remain:
At this point, there is very little in the way of proper support for builtin tuples and even lists; perhaps I will bake these in somewhere too.