Getting valid substitutions to work for subsumption

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Getting valid substitutions to work for subsumption

Matthías Páll Gissurarson
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
Reply | Threaded
Open this post in threaded view
|

Re: Getting valid substitutions to work for subsumption

Richard Eisenberg-4
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
Reply | Threaded
Open this post in threaded view
|

RE: Getting valid substitutions to work for subsumption

GHC - devs mailing list
| 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
Reply | Threaded
Open this post in threaded view
|

Re: Getting valid substitutions to work for subsumption

Richard Eisenberg-4

> 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