At the moment monomorphic constraints perform generalisation and then mark all the quantifiers and free variables as being monomorphic. At first glance I thought this achieves the desired semantics, but it actually doesn't. For example this program should be rejected but isn't:
At the moment monomorphic constraints perform generalisation and then mark all the quantifiers and free variables as being monomorphic. At first glance I thought this achieves the desired semantics, but it actually doesn't. For example this program should be rejected but isn't:
because
fshould not have a quantified type, but it does if we don't discard the quantifiers. See also: https://github.com/jstolarek/inferno/pull/33#issuecomment-768596865