Getting valid substitutions to work for subsumption

[Richard Eisenberg]

Hi Matthías,

This is going to be challenging to fix, I'm afraid.

When GHC sees a definition with a polymorphic type signature, it *skolemizes* the signature before ever looking at the definition. In this context, skolemizing means that GHC will fix the type variable a (in your trace, it becomes the skolem a_a1D1[sk:2]; the "sk" there means skolem) and assume `Num a`. (This action takes place in TcBinds.tcPolyCheck.) GHC then goes about trying to typecheck the definition against the skolemized type. That's why the "expected types" in your trace just mention skolems, with no `Num a_a1D1` in sight.

The way that GHC assumes a constraint is this: it typechecks the code over which the constraint is assumed, producing some residual WantedConstraints. GHC then builds an implication over these WantedConstraints, where the implication marks the assumed constraint as a Given. This action is in TcUnify.checkConstraints and buildImplication. Note that tcPolyCheck calls checkConstraints.

The problem is that it seems you need to access the assumed constraints even before you're done typechecking the enclosed expression. GHC simply isn't set up for that. I think your best bet is to modify CHoleCan or make a new constructor of Ct (in TcRnTypes) that stores the information you need to produce the output you would like. Then, in your tcSubsumes, you will still need to emit any residual wanteds, all the way to the top level. Then GHC will run the solver, and TcErrors can format suggestions appropriately.

I hope this makes some sense!
Richard