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
_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Reply via email to