Commit fae672f6 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix constraint solving for forall-types

Trac #13879 showed that when we were trying to solve

  (forall z1 (y1::z1). ty1)  ~  (forall z2 (y2:z2). ty2)

we'd end up spitting out z1~z2 with no binding site for them.
Those kind equalities need to be inside the implication.

I ended up re-factoring the code for solving forall-equalities.
It's quite nice now.
parent c80920d2
......@@ -23,6 +23,8 @@ import Coercion
import FamInstEnv ( FamInstEnvs )
import FamInst ( tcTopNormaliseNewTypeTF_maybe )
import Var
import VarEnv( mkInScopeSet )
import VarSet( extendVarSetList )
import Outputable
import DynFlags( DynFlags )
import NameSet
......@@ -589,27 +591,7 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
can_eq_nc' _flat _rdr_env _envs ev eq_rel
s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
| CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev
= do { let (bndrs1,body1) = tcSplitForAllTyVarBndrs s1
(bndrs2,body2) = tcSplitForAllTyVarBndrs s2
; if not (equalLength bndrs1 bndrs2)
then do { traceTcS "Forall failure" $
vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
, ppr (map binderArgFlag bndrs1)
, ppr (map binderArgFlag bndrs2) ]
; canEqHardFailure ev s1 s2 }
else
do { traceTcS "Creating implication for polytype equality" $ ppr ev
; kind_cos <- zipWithM (unifyWanted loc Nominal)
(map binderKind bndrs1) (map binderKind bndrs2)
; all_co <- deferTcSForAllEq (eqRelRole eq_rel) loc
kind_cos (bndrs1,body1) (bndrs2,body2)
; setWantedEq orig_dest all_co
; stopWith ev "Deferred polytype equality" } }
| otherwise
= do { traceTcS "Omitting decomposition of given polytype equality" $
pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
; stopWith ev "Discard given polytype equality" }
= can_eq_nc_forall ev eq_rel s1 s2
-- See Note [Canonicalising type applications] about why we require flat types
can_eq_nc' True _rdr_env _envs ev eq_rel (AppTy t1 s1) _ ty2 _
......@@ -640,6 +622,77 @@ can_eq_nc' True _rdr_env _envs ev _eq_rel _ ps_ty1 _ ps_ty2
= do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
; canEqHardFailure ev ps_ty1 ps_ty2 }
---------------------------------
can_eq_nc_forall :: CtEvidence -> EqRel
-> Type -> Type -- LHS and RHS
-> TcS (StopOrContinue Ct)
-- (forall as. phi1) ~ (forall bs. phi2)
-- Check for length match of as, bs
-- Then build an implication constraint: forall as. phi1 ~ phi2[as/bs]
-- But remember also to unify the kinds of as and bs
-- (this is the 'go' loop), and actually substitute phi2[as |> cos / bs]
-- Remember also that we might have forall z (a:z). blah
-- so we must proceed one binder at a time (Trac #13879)
can_eq_nc_forall ev eq_rel s1 s2
| CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev
= do { let free_tvs1 = tyCoVarsOfType s1
free_tvs2 = tyCoVarsOfType s2
(bndrs1, phi1) = tcSplitForAllTyVarBndrs s1
(bndrs2, phi2) = tcSplitForAllTyVarBndrs s2
; if not (equalLength bndrs1 bndrs2)
then do { traceTcS "Forall failure" $
vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
, ppr (map binderArgFlag bndrs1)
, ppr (map binderArgFlag bndrs2) ]
; canEqHardFailure ev s1 s2 }
else
do { traceTcS "Creating implication for polytype equality" $ ppr ev
; let empty_subst1 = mkEmptyTCvSubst $ mkInScopeSet free_tvs1
; (subst1, skol_tvs) <- tcInstSkolTyVarsX empty_subst1 $
binderVars bndrs1
; let skol_info = UnifyForAllSkol phi1
phi1' = substTy subst1 phi1
-- Unify the kinds, extend the substitution
go (skol_tv:skol_tvs) subst (bndr2:bndrs2)
= do { let tv2 = binderVar bndr2
; kind_co <- unifyWanted loc Nominal
(tyVarKind skol_tv)
(substTy subst (tyVarKind tv2))
; let subst' = extendTvSubst subst tv2
(mkCastTy (mkTyVarTy skol_tv) kind_co)
; co <- go skol_tvs subst' bndrs2
; return (mkForAllCo skol_tv kind_co co) }
-- Done: unify phi1 ~ phi2
go [] subst bndrs2
= ASSERT( null bndrs2 )
unifyWanted loc (eqRelRole eq_rel)
phi1' (substTy subst phi2)
go _ _ _ = panic "cna_eq_nc_forall" -- case (s:ss) []
empty_subst2 = mkEmptyTCvSubst $ mkInScopeSet $
free_tvs2 `extendVarSetList` skol_tvs
; (implic, _ev_binds, all_co) <- buildImplication skol_info skol_tvs [] $
go skol_tvs empty_subst2 bndrs2
-- We have nowhere to put these bindings
-- but TcSimplify.setImplicationStatus
-- checks that we don't actually use them
-- when skol_info = UnifyForAllSkol
; updWorkListTcS (extendWorkListImplic implic)
; setWantedEq orig_dest all_co
; stopWith ev "Deferred polytype equality" } }
| otherwise
= do { traceTcS "Omitting decomposition of given polytype equality" $
pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
; stopWith ev "Discard given polytype equality" }
---------------------------------
-- | Compare types for equality, while zonking as necessary. Gives up
-- as soon as it finds that two types are not equal.
......
......@@ -7,7 +7,7 @@ module TcSMonad (
WorkList(..), isEmptyWorkList, emptyWorkList,
extendWorkListNonEq, extendWorkListCt, extendWorkListDerived,
extendWorkListCts, extendWorkListEq, extendWorkListFunEq,
appendWorkList,
appendWorkList, extendWorkListImplic,
selectNextWorkItem,
workListSize, workListWantedCount,
getWorkList, updWorkListTcS,
......@@ -16,9 +16,9 @@ module TcSMonad (
TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
failTcS, warnTcS, addErrTcS,
runTcSEqualities,
nestTcS, nestImplicTcS, setEvBindsTcS,
nestTcS, nestImplicTcS, setEvBindsTcS, buildImplication,
runTcPluginTcS, addUsedGRE, addUsedGREs, deferTcSForAllEq,
runTcPluginTcS, addUsedGRE, addUsedGREs,
-- Tracing etc
panicTcS, traceTcS,
......@@ -93,7 +93,7 @@ module TcSMonad (
-- MetaTyVars
newFlexiTcSTy, instFlexi, instFlexiX,
cloneMetaTyVar, demoteUnfilledFmv,
tcInstType,
tcInstType, tcInstSkolTyVarsX,
TcLevel, isTouchableMetaTyVarTcS,
isFilledMetaTyVar_maybe, isFilledMetaTyVar,
......@@ -277,8 +277,8 @@ extendWorkListDeriveds loc evs wl
| isDroppableDerivedLoc loc = wl { wl_deriv = evs ++ wl_deriv wl }
| otherwise = extendWorkListEqs (map mkNonCanonical evs) wl
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
extendWorkListImplic :: Bag Implication -> WorkList -> WorkList
extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
......@@ -2530,6 +2530,45 @@ nestTcS (TcS thing_inside)
; return res }
buildImplication :: SkolemInfo
-> [TcTyVar] -- Skolems
-> [EvVar] -- Givens
-> TcS result
-> TcS (Bag Implication, TcEvBinds, result)
-- Just like TcUnify.buildImplication, but in the TcS monnad,
-- using the work-list to gather the constraints
buildImplication skol_info skol_tvs givens (TcS thing_inside)
= TcS $ \ env ->
do { new_wl_var <- TcM.newTcRef emptyWorkList
; tc_lvl <- TcM.getTcLevel
; let new_tclvl = pushTcLevel tc_lvl
; res <- TcM.setTcLevel new_tclvl $
thing_inside (env { tcs_worklist = new_wl_var })
; wl@WL { wl_eqs = eqs } <- TcM.readTcRef new_wl_var
; if null eqs
then return (emptyBag, emptyTcEvBinds, res)
else
do { env <- TcM.getLclEnv
; ev_binds_var <- TcM.newTcEvBinds
; let wc = ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) &&
null (wl_deriv wl) && null (wl_implics wl), ppr wl )
WC { wc_simple = listToCts eqs
, wc_impl = emptyBag
, wc_insol = emptyCts }
imp = Implic { ic_tclvl = new_tclvl
, ic_skols = skol_tvs
, ic_no_eqs = True
, ic_given = givens
, ic_wanted = wc
, ic_status = IC_Unsolved
, ic_binds = ev_binds_var
, ic_env = env
, ic_needed = emptyVarSet
, ic_info = skol_info }
; return (unitBag imp, TcEvBinds ev_binds_var, res) } }
{-
Note [Propagate the solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -2925,7 +2964,8 @@ tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
-- (type vars, preds (incl equalities), rho)
tcInstType inst_tyvars id = wrapTcS (TcM.tcInstType inst_tyvars id)
tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX subst tvs
-- Creating and setting evidence variables and CtFlavors
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -3144,47 +3184,3 @@ from which we get the implication
See TcSMonad.deferTcSForAllEq
-}
-- Deferring forall equalities as implications
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
deferTcSForAllEq :: Role -- Nominal or Representational
-> CtLoc -- Original wanted equality flavor
-> [Coercion] -- among the kinds of the binders
-> ([TyVarBinder],TcType) -- ForAll tvs1 body1
-> ([TyVarBinder],TcType) -- ForAll tvs2 body2
-> TcS Coercion
deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
= do { let tvs1' = zipWithEqual "deferTcSForAllEq"
mkCastTy (mkTyVarTys tvs1) kind_cos
body2' = substTyWithUnchecked tvs2 tvs1' body2
; (subst, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
; let phi1 = Type.substTyUnchecked subst body1
phi2 = Type.substTyUnchecked subst body2'
skol_info = UnifyForAllSkol phi1
; (ctev, hole_co) <- newWantedEq loc role phi1 phi2
; env <- getLclEnv
; ev_binds <- newTcEvBinds
-- We have nowhere to put these bindings
-- but TcSimplify.setImplicationStatus
-- checks that we don't actually use them
; let new_tclvl = pushTcLevel (tcl_tclvl env)
wc = WC { wc_simple = singleCt (mkNonCanonical ctev)
, wc_impl = emptyBag
, wc_insol = emptyCts }
imp = Implic { ic_tclvl = new_tclvl
, ic_skols = skol_tvs
, ic_no_eqs = True
, ic_given = []
, ic_wanted = wc
, ic_status = IC_Unsolved
, ic_binds = ev_binds
, ic_env = env
, ic_needed = emptyVarSet
, ic_info = skol_info }
; updWorkListTcS (extendWorkListImplic imp)
; let cobndrs = zip skol_tvs kind_cos
; return $ mkForAllCos cobndrs hole_co }
where
tvs1 = binderVars bndrs1
tvs2 = binderVars bndrs2
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data HR (a :: j) (b :: k) where
HRefl :: HR a a
data instance Sing (z :: HR a b) where
SHRefl :: Sing HRefl
foo :: forall (j :: Type) (k :: Type) (a :: j)
(b :: k) (r :: HR a b)
(p :: forall (z :: Type) (y :: z). HR a y -> Type).
Sing r
-> App p HRefl
-> HRApp p r
foo SHRefl pHRefl = pHRefl
type App f x = f x
type HRApp (f :: forall (z :: Type) (y :: z). HR a y -> Type)
(x :: HR a b) = f x
......@@ -565,3 +565,4 @@ test('T13785', normal, compile, [''])
test('T13804', normal, compile, [''])
test('T13822', normal, compile, [''])
test('T13871', normal, compile, [''])
test('T13879', normal, compile, [''])
......@@ -10,7 +10,7 @@ tcfail174.hs:16:14: error:
• Couldn't match type ‘a’ with ‘a1’
because type variable ‘a1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type a1 -> a1
the type a -> a
at tcfail174.hs:16:1-14
Expected type: Capture (forall x. x -> a)
Actual type: Capture (forall a. a -> a)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment