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