Greetings, I'm working on improving the valid substitution feature that I implemented a few weeks ago, but I'm having a problem making it work with subsumption, i.e. if the types are not exactly equal. You can find all the code on a branch on my fork of GHC on GitHub, with the subsumption checker being the following function: -- Reports whether one type subsumes another, discarding any errors tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool tcSubsumes hole_ty ty = discardErrs $ do { (_, wanted, _) <- pushLevelAndCaptureConstraints $ tcSubType_NC ExprSigCtxt ty hole_ty ; (rem, _) <- runTcS (simpl_top wanted) ; return (isEmptyWC rem) } The current example I'm working with is module T3 where ps3 :: Num a => a -> a -> a ps3 = (+) ps4 :: Num a => a -> a -> a ps4 = _ Which should of course include (+) as a suggestion. However, when it checks for (+), it does not report it as a match. What could be going wrong here? Could someone more familiar with the underlying machinery give some guidance on what could be going wrong here? Dumping the traceTc (i.e. running ./inplace/bin/ghc-stage2 -o test t3.hs -ddump-tc-trace) gives the following relevant output in the dump: Checking for substitution + parent:Num imported from ‘Prelude’ at t3.hs:1:8-9 (and originally defined in ‘GHC.Num’) tcSubType_NC an expression type signature forall a. Num a => a -> a -> a a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] tc_sub_tc_type (general case) ty_actual = forall a. Num a => a -> a -> a ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] tcSkolemise tc_sub_type_ds ty_actual = forall a. Num a => a -> a -> a ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] instCallConstraints [$dNum_a4eI] Instantiating all tyvars? True origin arising from a type equality forall a. Num a => a -> a -> a ~ a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] type forall a. Num a => a -> a -> a theta [Num a_a19t] leave_bndrs [] with [a_a4eH[tau:3]] theta: [Num a0_a4eH[tau:3]] tc_sub_type_ds ty_actual = a0_a4eH[tau:3] -> a0_a4eH[tau:3] -> a0_a4eH[tau:3] ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] tc_sub_type_ds ty_actual = a0_a4eH[tau:3] -> a0_a4eH[tau:3] ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] tc_sub_type_ds ty_actual = a0_a4eH[tau:3] ty_expected = a_a1D1[sk:2] u_tys tclvl 3 a0_a4eH[tau:3] ~ a_a1D1[sk:2] arising from a type equality a0_a4eH[tau:3] -> a0_a4eH[tau:3] -> a0_a4eH[tau:3] ~ a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] u_tys tclvl 3 * ~ * arising from a kind equality arising from a0_a4eH[tau:3] ~ a_a1D1[sk:2] u_tys tclvl 3 'GHC.Types.LiftedRep ~ 'GHC.Types.LiftedRep arising from a kind equality arising from a0_a4eH[tau:3] ~ a_a1D1[sk:2] u_tys yields no coercion u_tys yields no coercion writeMetaTyVar a_a4eH[tau:3] :: * := a_a1D1[sk:2] u_tys yields no coercion tc_sub_tc_type (general case) ty_actual = a_a1D1[sk:2] ty_expected = a0_a4eH[tau:3] tcSkolemise tc_sub_type_ds ty_actual = a_a1D1[sk:2] ty_expected = a0_a4eH[tau:3] u_tys tclvl 3 a_a1D1[sk:2] ~ a0_a4eH[tau:3] arising from a type equality a0_a4eH[tau:3] -> a0_a4eH[tau:3] -> a0_a4eH[tau:3] ~ a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] u_tys yields no coercion tc_sub_tc_type (general case) ty_actual = a_a1D1[sk:2] ty_expected = a0_a4eH[tau:3] tcSkolemise tc_sub_type_ds ty_actual = a_a1D1[sk:2] ty_expected = a0_a4eH[tau:3] u_tys tclvl 3 a_a1D1[sk:2] ~ a0_a4eH[tau:3] arising from a type equality a0_a4eH[tau:3] -> a0_a4eH[tau:3] -> a0_a4eH[tau:3] ~ a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2] u_tys yields no coercion newTcEvBinds unique = a4eJ solveWanteds { WC {wc_simple = [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical)} solveSimpleWanteds { {[WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical)} ----------------------------- Start solver pipeline { work item = [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical) inerts = {Unsolved goals = 0} rest of worklist = WL {} runStage canonicalization { workitem = [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical) canonicalize (non-canonical) [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical) canEvNC:cls Num [a0_a4eH[tau:3]] flatten_many { a0_a4eH[tau:3] Following filled tyvar a_a4eH[tau:3] = a_a1D1[sk:2] Unfilled tyvar a_a1D1[sk:2] flatten } a_a1D1[sk:2] canClass [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] Num a_a1D1[sk:2] ContinueWith [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] end stage canonicalization } runStage interact with inerts { workitem = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) end stage interact with inerts } runStage top-level reactions { workitem = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) doTopReact [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) matchClassInst pred = Num a_a1D1[sk:2] { matchClass not matching dict Num a_a1D1[sk:2] } matchClassInst result NoInstance try_fundeps [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) end stage top-level reactions } insertInertCan { Trying to insert new non-eq inert item: [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) addInertCan } Step 1[l:2,d:0] Kept as inert: [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] End solver pipeline (kept as inert) } final_item = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan) getUnsolvedInerts tv eqs = {} fun eqs = {} insols = {} others = {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)} implics = {} Unflattening {Funeqs = Tv eqs =} Unflattening 1 {} Unflattening 2 {} Unflattening 3 {} Unflattening done {} zonkSimples done: {} solveSimpleWanteds end } iterations = 1 residual = WC {wc_simple = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)} expandSuperClasses { End expandSuperClasses no-op } solveWanteds middle simples1 = {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)} simples2 = {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)} solveWanteds } final wc = WC {wc_simple = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)} current evbinds = {} zonkSimples done: {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan(psc))} zonkSimples done: {} applyDefaultingRules { wanteds = WC {wc_simple = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan(psc))} groups = [] info = ([Integer, Double], (False, False)) applyDefaultingRules } [] Constraint solver steps = 1 -- Matthías Páll Gissurarson _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
| 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:[hidden email]] On Behalf Of Richard | Eisenberg | Sent: 18 May 2017 14:21 | To: Matthías Páll Gissurarson <[hidden email]> | Cc: [hidden email] | 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 | [hidden email] | 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 _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
> On May 18, 2017, at 5:27 PM, Simon Peyton Jones <[hidden email]> wrote: > > I don't agree. If you call (tcSubsumes hole_ty ty) with closed types > hole_ty, ty, it should return True if I agree here. But it looks like Matthías's function gets the expected type as pushed down by bidirectional typechecking. This type will always be deeply skolemized before tcSubsumes can get a hold of it, so it won't be closed. Richard _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Free forum by Nabble | Edit this page |