| 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 <mpg@mpg.is> | 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