Proposal: support for constrained existential type variables in record fields

[arossato]

Currently mhs doesn't allow data type constructors with constrained existentially quantified type variables in record fields. For example:

data T = forall a . Show a => T { field :: a }
main = pure ()

produces an error:

Cannot satisfy constraint: (a#310 ~ a)

This happens because mhs generates top-level functions and HasField instances for field selectors, which may expose the existential type outside its intended scope. For instance:

data T = forall a . T { field :: [a] }
myT = T [1..10]
main = print $ length $ field myT

This works in mhs, which prints 10, whereas ghc would reject it:

Cannot use record selector ‘field’ as a function due to escaped type variables

I don't know if ghc is correct or not, but I'm sure that enforcing the ghc policy would break ghc-compat, and I believe this would be unacceptable. So this proposal will only affect constrained existential records.

Proposed changes:

1. The first commit will suppress the generation of top level functions and HasField instances for constrained existential record fields.

2. The second commit addresses some issues in pattern matching when the type constructor is wrapped in a dictionary application, thus enabling punning and record wildcards with constrained record fields.

3. The third commit is the most invasive: updates of constrained existential records will be desugared into a case expression, without using setField.

4. The last commit adds some tests for the changes I'm proposing.

[augustss]

Thank you! I will merge this soon

[augustss]

This doesn't quite work. If you remove the export list from the ExistField test the compiler gets an impossible, because a field is missing when generating the export.

Don't worry about it. I'm taking your code and changing it a little instead of a direct merge.

[augustss]

Another problem is that constructing records with T{a=1, b=2} no longer seems to work. I'll fix that too.

[arossato]

Another problem is that constructing records with T{a=1, b=2} no longer seems to work. I'll fix that too.

This is a bit embarrassing, because I thought that correctly handling the case where multiple fields share the same existential type variable was crucial — that’s why the first test was exactly about T. Yet I still missed that point. And I didn't test it, which is worse.

Clearly I underestimated the subtleties of the issue. A good lesson for me, though: when something looks simple, you’re probably overlooking something important.

I’m sure you already have a solution in mind, but I’ll try to understand and solve it myself as well — time to go back to studying!

[arossato]

This doesn't quite work. If you remove the export list from the ExistField test the compiler gets an impossible, because a field is missing when generating the export.

Don't worry about it. I'm taking your code and changing it a little instead of a direct merge.

I've suppressed the creation of field selectors in the type-checker without thinking that maybe that could have other consequences... see my previous comment.