Getting valid substitutions to work for subsumption
Simon Peyton Jones
simonpj at microsoft.com
Thu May 18 21:27:47 UTC 2017
 This is going to be challenging to fix, I'm afraid.
I don't agree. If you call (tcSubsumes hole_ty ty) with closed types
hole_ty, ty, it should return True if
ty is more polymorphic than hole_ty.
For example
tcSubsumes (forall a. [a] > [a])
(forall b. b > b)
should return True.
Ditto
tcSubsumes (Int > Int)
(forall a. [a] > [a])
And
tcSubsumes (forall a. Ord a => a > a)
(forall b. Eq b => b > b)
I'm not sure what arguments you are actually giving it.
S
 Original Message
 From: ghcdevs [mailto:ghcdevsbounces at haskell.org] On Behalf Of Richard
 Eisenberg
 Sent: 18 May 2017 14:21
 To: Matthías Páll Gissurarson <mpg at mpg.is>
 Cc: ghcdevs at haskell.org
 Subject: Re: Getting valid substitutions to work for subsumption

 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
 _______________________________________________
 ghcdevs mailing list
 ghcdevs at haskell.org
 https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.hask
 ell.org%2Fcgibin%2Fmailman%2Flistinfo%2Fghc
 devs&data=02%7C01%7Csimonpj%40microsoft.com%7C8149f8440a30449d9f4a08d49df
 0d915%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636307105156540750&sda
 ta=OadpZcPB44wsFF6A93YpftNR5364BN7SleqhsMuNCeo%3D&reserved=0
More information about the ghcdevs
mailing list