<div dir="ltr">Greetings,<br><br>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 href="https://github.com/Tritlo/ghc/tree/show-valid-substitutions-subsumes">a branch on my fork of GHC on GitHub</a>, with the subsumption checker being the following function:<div><br></div><div><div><font face="monospace">  -- Reports whether one type subsumes another, discarding any errors</font></div><div><font face="monospace">  tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool</font></div><div><font face="monospace">  tcSubsumes hole_ty ty = discardErrs $</font></div><div><font face="monospace">   do {  (_, wanted, _) <- pushLevelAndCaptureConstraints $</font></div><div><font face="monospace">                             tcSubType_NC ExprSigCtxt ty hole_ty</font></div><div><font face="monospace">      ; (rem, _) <- runTcS (simpl_top wanted)</font></div><div><font face="monospace">      ; return (isEmptyWC rem)</font></div><div><font face="monospace">      }</font><br><br></div></div><div>The current example I'm working with is<div>  </div><div><font face="monospace">  module T3 where</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">  ps3 :: Num a => a -> a -> a</font></div><div><font face="monospace">  ps3 = (+)</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">  ps4 :: Num a => a -> a -> a</font></div><div><font face="monospace">  ps4 = _</font></div><div><br></div><div><br></div><div>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?</div><div><br></div><div>Dumping the traceTc (i.e. running .<font face="monospace">/inplace/bin/ghc-stage2 -o test t3.hs -ddump-tc-trace</font>) gives the following relevant output in the dump:<br><br><div><div><font face="monospace">    Checking for substitution</font></div><div><font face="monospace">    + parent:Num</font></div><div><font face="monospace">        imported from ‘Prelude’ at t3.hs:1:8-9</font></div><div><font face="monospace">        (and originally defined in ‘GHC.Num’)</font></div><div><font face="monospace">    tcSubType_NC</font></div><div><font face="monospace">    an expression type signature</font></div><div><font face="monospace">    forall a. Num a => a -> a -> a</font></div><div><font face="monospace">    a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2]</font></div><div><font face="monospace">    tc_sub_tc_type (general case)</font></div><div><font face="monospace">    ty_actual   = forall a. Num a => a -> a -> a</font></div><div><font face="monospace">    ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2]</font></div><div><font face="monospace">    tcSkolemise</font></div><div><font face="monospace">    tc_sub_type_ds</font></div><div><font face="monospace">    ty_actual   = forall a. Num a => a -> a -> a</font></div><div><font face="monospace">    ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2]</font></div><div><font face="monospace">    instCallConstraints [$dNum_a4eI]</font></div><div><font face="monospace">    Instantiating</font></div><div><font face="monospace">    all tyvars? True</font></div><div><font face="monospace">    origin arising from a type equality forall a. Num a => a -> a -> a</font></div><div><font face="monospace">                                        ~</font></div><div><font face="monospace">                                        a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2]</font></div><div><font face="monospace">    type forall a. Num a => a -> a -> a</font></div><div><font face="monospace">    theta [Num a_a19t]</font></div><div><font face="monospace">    leave_bndrs []</font></div><div><font face="monospace">    with [a_a4eH[tau:3]]</font></div><div><font face="monospace">    theta: [Num a0_a4eH[tau:3]]</font></div><div><font face="monospace">    tc_sub_type_ds</font></div><div><font face="monospace">    ty_actual   = a0_a4eH[tau:3] -> a0_a4eH[tau:3] -> a0_a4eH[tau:3]</font></div><div><font face="monospace">    ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2]</font></div><div><font face="monospace">    tc_sub_type_ds</font></div><div><font face="monospace">    ty_actual   = a0_a4eH[tau:3] -> a0_a4eH[tau:3]</font></div><div><font face="monospace">    ty_expected = a_a1D1[sk:2] -> a_a1D1[sk:2]</font></div><div><font face="monospace">    tc_sub_type_ds</font></div><div><font face="monospace">    ty_actual   = a0_a4eH[tau:3]</font></div><div><font face="monospace">    ty_expected = a_a1D1[sk:2]</font></div><div><font face="monospace">    u_tys</font></div><div><font face="monospace">    tclvl 3</font></div><div><font face="monospace">    a0_a4eH[tau:3] ~ a_a1D1[sk:2]</font></div><div><font face="monospace">    arising from a type equality a0_a4eH[tau:3]</font></div><div><font face="monospace">                                -> a0_a4eH[tau:3] -> a0_a4eH[tau:3]</font></div><div><font face="monospace">                                ~</font></div><div><font face="monospace">                                a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2]</font></div><div><font face="monospace">    u_tys</font></div><div><font face="monospace">    tclvl 3</font></div><div><font face="monospace">    * ~ *</font></div><div><font face="monospace">    arising from a kind equality arising from</font></div><div><font face="monospace">        a0_a4eH[tau:3] ~ a_a1D1[sk:2]</font></div><div><font face="monospace">    u_tys</font></div><div><font face="monospace">    tclvl 3</font></div><div><font face="monospace">    'GHC.Types.LiftedRep ~ 'GHC.Types.LiftedRep</font></div><div><font face="monospace">    arising from a kind equality arising from</font></div><div><font face="monospace">        a0_a4eH[tau:3] ~ a_a1D1[sk:2]</font></div><div><font face="monospace">    u_tys yields no coercion</font></div><div><font face="monospace">    u_tys yields no coercion</font></div><div><font face="monospace">    writeMetaTyVar a_a4eH[tau:3] :: * := a_a1D1[sk:2]</font></div><div><font face="monospace">    u_tys yields no coercion</font></div><div><font face="monospace">    tc_sub_tc_type (general case)</font></div><div><font face="monospace">    ty_actual   = a_a1D1[sk:2]</font></div><div><font face="monospace">    ty_expected = a0_a4eH[tau:3]</font></div><div><font face="monospace">    tcSkolemise</font></div><div><font face="monospace">    tc_sub_type_ds</font></div><div><font face="monospace">    ty_actual   = a_a1D1[sk:2]</font></div><div><font face="monospace">    ty_expected = a0_a4eH[tau:3]</font></div><div><font face="monospace">    u_tys</font></div><div><font face="monospace">    tclvl 3</font></div><div><font face="monospace">    a_a1D1[sk:2] ~ a0_a4eH[tau:3]</font></div><div><font face="monospace">    arising from a type equality a0_a4eH[tau:3]</font></div><div><font face="monospace">                                -> a0_a4eH[tau:3] -> a0_a4eH[tau:3]</font></div><div><font face="monospace">                                ~</font></div><div><font face="monospace">                                a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2]</font></div><div><font face="monospace">    u_tys yields no coercion</font></div><div><font face="monospace">    tc_sub_tc_type (general case)</font></div><div><font face="monospace">    ty_actual   = a_a1D1[sk:2]</font></div><div><font face="monospace">    ty_expected = a0_a4eH[tau:3]</font></div><div><font face="monospace">    tcSkolemise</font></div><div><font face="monospace">    tc_sub_type_ds</font></div><div><font face="monospace">    ty_actual   = a_a1D1[sk:2]</font></div><div><font face="monospace">    ty_expected = a0_a4eH[tau:3]</font></div><div><font face="monospace">    u_tys</font></div><div><font face="monospace">    tclvl 3</font></div><div><font face="monospace">    a_a1D1[sk:2] ~ a0_a4eH[tau:3]</font></div><div><font face="monospace">    arising from a type equality a0_a4eH[tau:3]</font></div><div><font face="monospace">                                -> a0_a4eH[tau:3] -> a0_a4eH[tau:3]</font></div><div><font face="monospace">                                ~</font></div><div><font face="monospace">                                a_a1D1[sk:2] -> a_a1D1[sk:2] -> a_a1D1[sk:2]</font></div><div><font face="monospace">    u_tys yields no coercion</font></div><div><font face="monospace">    newTcEvBinds unique = a4eJ</font></div><div><font face="monospace">    solveWanteds {</font></div><div><font face="monospace">    WC {wc_simple =</font></div><div><font face="monospace">            [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical)}</font></div><div><font face="monospace">    solveSimpleWanteds {</font></div><div><font face="monospace">    {[WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical)}</font></div><div><font face="monospace">    ----------------------------- </font></div><div><font face="monospace">    Start solver pipeline {</font></div><div><font face="monospace">    work item = [WD] $dNum_a4eI {0}:: Num</font></div><div><font face="monospace">                                        a0_a4eH[tau:3] (CNonCanonical)</font></div><div><font face="monospace">    inerts = {Unsolved goals = 0}</font></div><div><font face="monospace">    rest of worklist = WL {}</font></div><div><font face="monospace">    runStage canonicalization {</font></div><div><font face="monospace">    workitem   =  [WD] $dNum_a4eI {0}:: Num</font></div><div><font face="monospace">                                            a0_a4eH[tau:3] (CNonCanonical)</font></div><div><font face="monospace">    canonicalize (non-canonical)</font></div><div><font face="monospace">    [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3] (CNonCanonical)</font></div><div><font face="monospace">    canEvNC:cls Num [a0_a4eH[tau:3]]</font></div><div><font face="monospace">    flatten_many { a0_a4eH[tau:3]</font></div><div><font face="monospace">    Following filled tyvar a_a4eH[tau:3] = a_a1D1[sk:2]</font></div><div><font face="monospace">    Unfilled tyvar a_a1D1[sk:2]</font></div><div><font face="monospace">    flatten } a_a1D1[sk:2]</font></div><div><font face="monospace">    canClass</font></div><div><font face="monospace">    [WD] $dNum_a4eI {0}:: Num a0_a4eH[tau:3]</font></div><div><font face="monospace">    Num a_a1D1[sk:2]</font></div><div><font face="monospace">    ContinueWith [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2]</font></div><div><font face="monospace">    end stage canonicalization }</font></div><div><font face="monospace">    runStage interact with inerts {</font></div><div><font face="monospace">    workitem   =  [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)</font></div><div><font face="monospace">    end stage interact with inerts }</font></div><div><font face="monospace">    runStage top-level reactions {</font></div><div><font face="monospace">    workitem   =  [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)</font></div><div><font face="monospace">    doTopReact [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)</font></div><div><font face="monospace">    matchClassInst pred = Num a_a1D1[sk:2] {</font></div><div><font face="monospace">    matchClass not matching dict Num a_a1D1[sk:2]</font></div><div><font face="monospace">    } matchClassInst result NoInstance</font></div><div><font face="monospace">    try_fundeps [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)</font></div><div><font face="monospace">    end stage top-level reactions }</font></div><div><font face="monospace">    insertInertCan {</font></div><div><font face="monospace">    Trying to insert new non-eq inert item: [WD] $dNum_a4eI {0}:: Num</font></div><div><font face="monospace">                                                                    a_a1D1[sk:2] (CDictCan)</font></div><div><font face="monospace">    addInertCan }</font></div><div><font face="monospace">    Step 1[l:2,d:0] Kept as inert:</font></div><div><font face="monospace">        [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2]</font></div><div><font face="monospace">    End solver pipeline (kept as inert) }</font></div><div><font face="monospace">    final_item = [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)</font></div><div><font face="monospace">    getUnsolvedInerts</font></div><div><font face="monospace">    tv eqs = {}</font></div><div><font face="monospace">    fun eqs = {}</font></div><div><font face="monospace">    insols = {}</font></div><div><font face="monospace">    others = {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)}</font></div><div><font face="monospace">    implics = {}</font></div><div><font face="monospace">    Unflattening</font></div><div><font face="monospace">    {Funeqs =</font></div><div><font face="monospace">    Tv eqs =}</font></div><div><font face="monospace">    Unflattening 1 {}</font></div><div><font face="monospace">    Unflattening 2 {}</font></div><div><font face="monospace">    Unflattening 3 {}</font></div><div><font face="monospace">    Unflattening done {}</font></div><div><font face="monospace">    zonkSimples done: {}</font></div><div><font face="monospace">    solveSimpleWanteds end }</font></div><div><font face="monospace">    iterations = 1</font></div><div><font face="monospace">    residual = WC {wc_simple =</font></div><div><font face="monospace">                    [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)}</font></div><div><font face="monospace">    expandSuperClasses {</font></div><div><font face="monospace">    End expandSuperClasses no-op }</font></div><div><font face="monospace">    solveWanteds middle</font></div><div><font face="monospace">    simples1 = {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)}</font></div><div><font face="monospace">    simples2 = {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)}</font></div><div><font face="monospace">    solveWanteds }</font></div><div><font face="monospace">    final wc = WC {wc_simple =</font></div><div><font face="monospace">                    [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan)}</font></div><div><font face="monospace">    current evbinds  = {}</font></div><div><font face="monospace">    zonkSimples done:</font></div><div><font face="monospace">    {[WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan(psc))}</font></div><div><font face="monospace">    zonkSimples done: {}</font></div><div><font face="monospace">    applyDefaultingRules {</font></div><div><font face="monospace">    wanteds = WC {wc_simple =</font></div><div><font face="monospace">                    [WD] $dNum_a4eI {0}:: Num a_a1D1[sk:2] (CDictCan(psc))}</font></div><div><font face="monospace">    groups  = []</font></div><div><font face="monospace">    info    = ([Integer, Double], (False, False))</font></div><div><font face="monospace">    applyDefaultingRules } []</font></div><div><font face="monospace">    Constraint solver steps = 1</font></div></div></div><div><br></div><div><br></div></div></div><div dir="ltr">-- <br></div><div data-smartmail="gmail_signature"><div dir="ltr">Matthías Páll Gissurarson<br></div></div>