| 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: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Richard
| Eisenberg
| Sent: 18 May 2017 14:21
| To: Matthías Páll Gissurarson
| Cc: ghc-devs@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
| _______________________________________________
| ghc-devs mailing list
| ghc-devs@haskell.org
| https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.hask
| ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
| devs&data=02%7C01%7Csimonpj%40microsoft.com%7C8149f8440a30449d9f4a08d49df
| 0d915%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636307105156540750&sda
| ta=OadpZcPB44wsFF6A93YpftNR5364BN7SleqhsMuNCeo%3D&reserved=0
