Differences in constraint language between implementation and formalisation

[jstolarek]

Relevant differences between current implementation and formalisation:

• there is no implementation of forall constraints ∀a.C
• there is no implementation of def constraints. Def constraint exist in original inferno implementation but they got dropped from our prototype at some point.
• due to above the client generates let mono constraints for abstractions instead of def constraints (cf. C-Abs and C-AbsAscribe rules in the paper).
• in addition to above, there is currently no support for restrictions on existentially quantified variables, so there is no way to generate a monomorphicaly-restricted existentials in C-Abs rule. Instead, variables are temporarily monomorphised by the solver when handling monomorphic lets.

Additionally:

• there's a subtle difference in how C-AbsAscribe is implemented. In the paper we use a concrete type B corresponding to annotation. In the code we introduce an existential providing it with a concrete structure corresponding to type annotation. This is a technicality. I don't think any action needs to be taken here. Perhaps it makes sense to mention this in Implementation section of the paper but I think this is an uninteresting implementation detail.