Getting valid substitutions to work for subsumption

[Simon Peyton Jones]

| 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 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: ghc-devs 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
| _______________________________________________
| ghc-devs mailing list
| ghc-devs at 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