Getting valid substitutions to work for subsumption

Matthías Páll Gissurarson mpg at mpg.is
Thu May 18 12:55:11 UTC 2017


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
<https://github.com/Tritlo/ghc/tree/show-valid-substitutions-subsumes>,
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170518/f620da90/attachment.html>


More information about the ghc-devs mailing list