Commit 53fb26e1 authored by dimitris's avatar dimitris
Browse files

Now the constraint simplifier solves kind constraints as well.

parent 477946c7
......@@ -8,9 +8,6 @@
module TcCanonical(
canonicalize,
canOccursCheck, canEq, canEvVar,
rewriteWithFunDeps,
emitFDWorkAsWanted, emitFDWorkAsDerived,
StopOrContinue (..)
) where
......@@ -19,8 +16,6 @@ module TcCanonical(
import BasicTypes ( IPName )
import TcErrors
import TcRnTypes
import FunDeps
import qualified TcMType as TcM
import TcType
import Type
import Kind
......@@ -32,7 +27,7 @@ import Name ( Name )
import Var
import VarEnv
import Outputable
import Control.Monad ( when, unless, zipWithM, foldM )
import Control.Monad ( when, unless, zipWithM )
import MonadUtils
import Control.Applicative ( (<|>) )
......@@ -42,7 +37,6 @@ import TcSMonad
import FastString
import Data.Maybe ( isNothing )
import Pair ( pSnd )
\end{code}
......@@ -204,11 +198,13 @@ canonicalize (CIrredEvCan { cc_id = ev, cc_flavor = fl
canEvVar :: EvVar -> PredTree
-> SubGoalDepth -> CtFlavor -> TcS StopOrContinue
-- Called only for non-canonical EvVars
canEvVar ev pred_classifier d fl
= case pred_classifier of
ClassPred cls tys -> canClass d fl ev cls tys
`andWhenContinue` emit_superclasses
EqPred ty1 ty2 -> canEq d fl ev ty1 ty2
EqPred ty1 ty2 -> canEq d fl ev ty1 ty2
`andWhenContinue` emit_kind_constraint
IPPred nm ty -> canIP d fl ev nm ty
IrredPred ev_ty -> canIrred d fl ev ev_ty
TuplePred tys -> canTuple d fl ev tys
......@@ -219,9 +215,58 @@ canEvVar ev pred_classifier d fl
= do { sctxt <- getTcSContext
; unless (simplEqsOnly sctxt) $
newSCWorkFromFlavored d v_new fl cls xis_new
-- Arguably we should "seq" the coercions if they are derived,
-- as we do below for emit_kind_constraint, to allow errors in
-- superclasses to be executed if deferred to runtime!
; continueWith ct }
emit_superclasses _ = panic "emit_superclasses of non-class!"
emit_kind_constraint ct@(CTyEqCan { cc_id = ev, cc_depth = d
, cc_flavor = fl, cc_tyvar = tv
, cc_rhs = ty })
= do_emit_kind_constraint ct ev d fl (mkTyVarTy tv) ty
emit_kind_constraint ct@(CFunEqCan { cc_id = ev, cc_depth = d
, cc_flavor = fl
, cc_fun = fn, cc_tyargs = xis1
, cc_rhs = xi2 })
= do_emit_kind_constraint ct ev d fl (mkTyConApp fn xis1) xi2
emit_kind_constraint ct = continueWith ct
do_emit_kind_constraint ct eqv d fl ty1 ty2
| compatKind k1 k2 = continueWith ct
| otherwise
= do { keqv <- forceNewEvVar kind_co_fl (mkEqPred (k1,k2))
; eqv' <- forceNewEvVar fl (mkEqPred (ty1,ty2))
; _fl <- case fl of
Wanted {}-> setEvBind eqv
(mkEvKindCast eqv' (mkTcCoVarCo keqv)) fl
Given {} -> setEvBind eqv'
(mkEvKindCast eqv (mkTcCoVarCo keqv)) fl
Derived {} -> return fl
; canEq_ d kind_co_fl keqv k1 k2 -- Emit kind equality
; continueWith (ct { cc_id = eqv' }) }
where k1 = typeKind ty1
k2 = typeKind ty2
ctxt = mkKindErrorCtxtTcS ty1 k1 ty2 k2
-- Always create a Wanted kind equality even if
-- you are decomposing a given constraint.
-- NB: DV finds this reasonable for now. Maybe we
-- have to revisit.
kind_co_fl
| Given (CtLoc _sk_info src_span err_ctxt) _ <- fl
= let orig = TypeEqOrigin (UnifyOrigin ty1 ty2)
ctloc = pushErrCtxtSameOrigin ctxt $
CtLoc orig src_span err_ctxt
in Wanted ctloc
| Wanted ctloc <- fl
= Wanted (pushErrCtxtSameOrigin ctxt ctloc)
| Derived ctloc <- fl
= Derived (pushErrCtxtSameOrigin ctxt ctloc)
| otherwise
= panic "do_emit_kind_constraint: non-CtLoc inside!"
-- Tuple canonicalisation
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -555,26 +600,28 @@ flatten :: SubGoalDepth -- Depth
flatten d ctxt ty
| Just ty' <- tcView ty
= do { (xi, co) <- flatten d ctxt ty'
; return (xi,co) }
-- DV: The following is tedious to do but maybe we should return to this
-- Preserve type synonyms if possible
-- ; if no_flattening
-- then return (xi, mkTcReflCo xi,no_flattening) -- Importantly, not xi!
-- else return (xi,co,no_flattening)
-- }
flatten d ctxt v@(TyVarTy _)
; return (xi,co) }
flatten d ctxt (TyVarTy tv)
= do { ieqs <- getInertEqs
; let co = liftInertEqsTy ieqs ctxt v -- co : v ~ ty
ty = pSnd (tcCoercionKind co)
; if v `eqType` ty then
return (ty,mkTcReflCo ty)
else -- NB recursive call. Why? See Note [Non-idempotent inert substitution]
-- Actually I believe that applying the substition only *twice* will suffice
do { (ty_final,co') <- flatten d ctxt ty -- co' : ty_final ~ ty
; return (ty_final,co' `mkTcTransCo` mkTcSymCo co) } }
; let mco = tv_eq_subst (fst ieqs) tv -- co : v ~ ty
; case mco of -- Done, but make sure the kind is zonked
Nothing ->
do { let knd = tyVarKind tv
; (new_knd,_kind_co) <- flatten d ctxt knd
; let ty = mkTyVarTy (setVarType tv new_knd)
; return (ty, mkTcReflCo ty) }
-- NB recursive call.
-- Why? See Note [Non-idempotent inert substitution]
-- Actually, I think applying the substition just twice will suffice
Just (co,ty) ->
do { (ty_final,co') <- flatten d ctxt ty
; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } }
where tv_eq_subst subst tv
| Just (ct,co) <- lookupVarEnv subst tv
, cc_flavor ct `canRewrite` ctxt
= Just (co,cc_rhs ct)
| otherwise = Nothing
\end{code}
......@@ -1106,28 +1153,17 @@ canEqLeafOriented :: SubGoalDepth -- Depth
-> TcType -> TcType -> TcS StopOrContinue
-- By now s1 will either be a variable or a type family application
canEqLeafOriented d fl eqv s1 s2
| let k1 = typeKind s1
, let k2 = typeKind s2
-- Establish kind invariants for CFunEqCan and CTyEqCan
= do { are_compat <- compatKindTcS k1 k2
; can_unify <- if not are_compat
then unifyKindTcS s1 s2 k1 k2
else return False
-- If the kinds cannot be unified or are not compatible, don't fail
-- right away; instead, emit a frozen error
; if (not are_compat && not can_unify) then
canEqFailure d fl eqv
else can_eq_kinds_ok d fl eqv s1 s2 }
where can_eq_kinds_ok d fl eqv s1 s2
= can_eq_split_lhs d fl eqv s1 s2
where can_eq_split_lhs d fl eqv s1 s2
| Just (fn,tys1) <- splitTyConApp_maybe s1
= canEqLeafFunEqLeftRec d fl eqv (fn,tys1) s2
| Just tv <- getTyVar_maybe s1
= canEqLeafTyVarLeftRec d fl eqv tv s2
| otherwise
= pprPanic "canEqLeafOriented" $
text "Non-variable or non-family equality LHS" <+> ppr eqv <+>
dcolon <+> ppr (evVarPred eqv)
text "Non-variable or non-family equality LHS" <+>
ppr eqv <+> dcolon <+> ppr (evVarPred eqv)
canEqLeafFunEqLeftRec :: SubGoalDepth
-> CtFlavor
-> EqVar
......@@ -1471,117 +1507,3 @@ we first try expanding each of the ti to types which no longer contain
a. If this turns out to be impossible, we next try expanding F
itself, and so on.
%************************************************************************
%* *
%* Functional dependencies, instantiation of equations
%* *
%************************************************************************
When we spot an equality arising from a functional dependency,
we now use that equality (a "wanted") to rewrite the work-item
constraint right away. This avoids two dangers
Danger 1: If we send the original constraint on down the pipeline
it may react with an instance declaration, and in delicate
situations (when a Given overlaps with an instance) that
may produce new insoluble goals: see Trac #4952
Danger 2: If we don't rewrite the constraint, it may re-react
with the same thing later, and produce the same equality
again --> termination worries.
To achieve this required some refactoring of FunDeps.lhs (nicer
now!).
\begin{code}
rewriteWithFunDeps :: [Equation]
-> [Xi]
-> WantedLoc
-> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)]))
-- Not quite a WantedEvVar unfortunately
-- Because our intention could be to make
-- it derived at the end of the day
-- NB: The flavor of the returned EvVars will be decided by the caller
-- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
rewriteWithFunDeps eqn_pred_locs xis wloc
= do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
; let fd_ev_pos :: [(Int,(EqVar,WantedLoc))]
fd_ev_pos = concat fd_ev_poss
(rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
; if null fd_ev_pos then return Nothing
else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
-- Post: Returns the position index as well as the corresponding FunDep equality
instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
, fd_pred1 = d1, fd_pred2 = d2 })
= do { let tvs = varSetElems qtvs
; tvs' <- mapM instFlexiTcS tvs -- IA0_TODO: we might need to do kind substitution
; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
; foldM (do_one subst) [] eqs }
where
do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
= let sty1 = Type.substTy subst ty1
sty2 = Type.substTy subst ty2
in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
else do { eqv <- newEqVar (Derived wl) sty1 sty2 -- Create derived or cached by deriveds
; let wl' = push_ctx wl
; if isNewEvVar eqv then
return $ (i,(evc_the_evvar eqv,wl')):ievs
else -- We are eventually going to emit FD work back in the work list so
-- it is important that we only return the /freshly created/ and not
-- some existing equality!
return ievs }
push_ctx :: WantedLoc -> WantedLoc
push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
mkEqnMsg :: (TcPredType, SDoc)
-> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
= do { zpred1 <- TcM.zonkTcPredType pred1
; zpred2 <- TcM.zonkTcPredType pred2
; let { tpred1 = tidyType tidy_env zpred1
; tpred2 = tidyType tidy_env zpred2 }
; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
; return (tidy_env, msg) }
rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
-> [Type] -- A sequence of types: tys
-> [(Type, TcCoercion)] -- Returns: [(ty', co : ty' ~ ty)]
rewriteDictParams param_eqs tys
= zipWith do_one tys [0..]
where
do_one :: Type -> Int -> (Type, TcCoercion)
do_one ty n = case lookup n param_eqs of
Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev))
Nothing -> (ty, mkTcReflCo ty) -- Identity
get_fst_ty (wev,_wloc)
| Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev )
= ty1
| otherwise
= panic "rewriteDictParams: non equality fundep!?"
emitFDWork :: Bool
-> [(EvVar,WantedLoc)]
-> SubGoalDepth -> TcS ()
emitFDWork as_wanted evlocs d
= updWorkListTcS $ appendWorkListEqs fd_cts
where fd_cts = map mk_fd_ct evlocs
mk_fl wl = if as_wanted then (Wanted wl) else (Derived wl)
mk_fd_ct (v,wl) = CNonCanonical { cc_id = v
, cc_flavor = mk_fl wl
, cc_depth = d }
emitFDWorkAsDerived, emitFDWorkAsWanted :: [(EvVar,WantedLoc)]
-> SubGoalDepth
-> TcS ()
emitFDWorkAsDerived = emitFDWork False
emitFDWorkAsWanted = emitFDWork True
\end{code}
\ No newline at end of file
......@@ -23,6 +23,7 @@ import TcSMonad
import TcType
import TypeRep
import Type
import Kind ( isKind )
import Class
import Unify ( tcMatchTys )
import Inst
......@@ -465,8 +466,12 @@ addExtraInfo ctxt ty1 ty2
extra2 = typeExtraInfoMsg (cec_encl ctxt) ty2
misMatchMsg :: TcType -> TcType -> SDoc -- Types are already tidy
misMatchMsg ty1 ty2 = sep [ ptext (sLit "Couldn't match type") <+> quotes (ppr ty1)
, nest 15 $ ptext (sLit "with") <+> quotes (ppr ty2)]
misMatchMsg ty1 ty2
= sep [ ptext cm_ty_or_knd <+> quotes (ppr ty1)
, nest 15 $ ptext (sLit "with") <+> quotes (ppr ty2)]
where cm_ty_or_knd
| isKind ty1 = sLit "Couldn't match kind"
| otherwise = sLit "Couldn't match type"
kindErrorMsg :: TcType -> TcType -> SDoc -- Types are already tidy
kindErrorMsg ty1 ty2
......
......@@ -37,6 +37,8 @@ import FunDeps
import TcEvidence
import Outputable
import TcMType ( zonkTcPredType )
import TcRnTypes
import TcErrors
import TcSMonad
......@@ -431,7 +433,16 @@ kick_out_rewritable ct (IS { inert_eqs = eqmap
(fro_out, fro_in) = partitionBag rewritable frozen
rewritable ct = (fl `canRewrite` cc_flavor ct) &&
(tv `elemVarSet` tyVarsOfCt ct)
(tv `elemVarSet` tyVarsOfCt ct)
-- NB: tyVarsOfCt will return the type
-- variables /and the kind variables/ that are
-- directly visible in the type. Hence we will
-- have exposed all the rewriting we care about
-- to make the most precise kinds visible for
-- matching classes etc. No need to kick out
-- constraints that mention type variables whose
-- kinds could contain this variable!
\end{code}
Note [Delicate equality kick-out]
......@@ -500,15 +511,9 @@ trySpontaneousSolve _ = return SPCantSolve
trySpontaneousEqOneWay :: SubGoalDepth
-> EqVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
-- tv is a MetaTyVar, not untouchable
trySpontaneousEqOneWay d eqv gw tv xi
| not (isSigTyVar tv) || isTyVarTy xi
= do { let kxi = typeKind xi -- NB: 'xi' is fully rewritten according to the inerts
-- so we have its more specific kind in our hands
; is_sub_kind <- kxi `isSubKindTcS` tyVarKind tv
; if is_sub_kind then
solveWithIdentity d eqv gw tv xi
else return SPCantSolve
}
trySpontaneousEqOneWay d eqv gw tv xi
| not (isSigTyVar tv) || isTyVarTy xi
= solveWithIdentity d eqv gw tv xi
| otherwise -- Still can't solve, sig tyvar and non-variable rhs
= return SPCantSolve
......@@ -518,13 +523,10 @@ trySpontaneousEqTwoWay :: SubGoalDepth
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
trySpontaneousEqTwoWay d eqv gw tv1 tv2
= do { k1_sub_k2 <- k1 `isSubKindTcS` k2
= do { let k1_sub_k2 = k1 `isSubKind` k2
; if k1_sub_k2 && nicer_to_update_tv2
then solveWithIdentity d eqv gw tv2 (mkTyVarTy tv1)
else do
{ k2_sub_k1 <- k2 `isSubKindTcS` k1
; MASSERT( k2_sub_k1 ) -- they were unified in TcCanonical
; solveWithIdentity d eqv gw tv1 (mkTyVarTy tv2) } }
else solveWithIdentity d eqv gw tv1 (mkTyVarTy tv2) }
where
k1 = tyVarKind tv1
k2 = tyVarKind tv2
......@@ -771,7 +773,6 @@ doInteractWithInert
, text "Inert item=" <+> ppr inertItem
]
-- Two pieces of irreducible evidence: if their types are *exactly identical* we can
-- rewrite them. We can never improve using this: if we want ty1 :: Constraint and have
-- ty2 :: Constraint it clearly does not mean that (ty1 ~ ty2)
......@@ -1262,6 +1263,116 @@ When we react a family instance with a type family equation in the work list
we keep the synonym-using RHS without expansion.
%************************************************************************
%* *
%* Functional dependencies, instantiation of equations
%* *
%************************************************************************
When we spot an equality arising from a functional dependency,
we now use that equality (a "wanted") to rewrite the work-item
constraint right away. This avoids two dangers
Danger 1: If we send the original constraint on down the pipeline
it may react with an instance declaration, and in delicate
situations (when a Given overlaps with an instance) that
may produce new insoluble goals: see Trac #4952
Danger 2: If we don't rewrite the constraint, it may re-react
with the same thing later, and produce the same equality
again --> termination worries.
To achieve this required some refactoring of FunDeps.lhs (nicer
now!).
\begin{code}
rewriteWithFunDeps :: [Equation]
-> [Xi]
-> WantedLoc
-> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)]))
-- Not quite a WantedEvVar unfortunately
-- Because our intention could be to make
-- it derived at the end of the day
-- NB: The flavor of the returned EvVars will be decided by the caller
-- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
rewriteWithFunDeps eqn_pred_locs xis wloc
= do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
; let fd_ev_pos :: [(Int,(EqVar,WantedLoc))]
fd_ev_pos = concat fd_ev_poss
(rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
; if null fd_ev_pos then return Nothing
else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
-- Post: Returns the position index as well as the corresponding FunDep equality
instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
, fd_pred1 = d1, fd_pred2 = d2 })
= do { let tvs = varSetElems qtvs
; tvs' <- mapM instFlexiTcS tvs -- IA0_TODO: we might need to do kind substitution
; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
; foldM (do_one subst) [] eqs }
where
do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
= let sty1 = Type.substTy subst ty1
sty2 = Type.substTy subst ty2
in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
else do { eqv <- newEqVar (Derived wl) sty1 sty2 -- Create derived or cached by deriveds
; let wl' = push_ctx wl
; if isNewEvVar eqv then
return $ (i,(evc_the_evvar eqv,wl')):ievs
else -- We are eventually going to emit FD work back in the work list so
-- it is important that we only return the /freshly created/ and not
-- some existing equality!
return ievs }
push_ctx :: WantedLoc -> WantedLoc
push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
mkEqnMsg :: (TcPredType, SDoc)
-> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
= do { zpred1 <- zonkTcPredType pred1
; zpred2 <- zonkTcPredType pred2
; let { tpred1 = tidyType tidy_env zpred1
; tpred2 = tidyType tidy_env zpred2 }
; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
; return (tidy_env, msg) }
rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
-> [Type] -- A sequence of types: tys
-> [(Type, TcCoercion)] -- Returns: [(ty', co : ty' ~ ty)]
rewriteDictParams param_eqs tys
= zipWith do_one tys [0..]
where
do_one :: Type -> Int -> (Type, TcCoercion)
do_one ty n = case lookup n param_eqs of
Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev))
Nothing -> (ty, mkTcReflCo ty) -- Identity
get_fst_ty (wev,_wloc)
| Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev )
= ty1
| otherwise
= panic "rewriteDictParams: non equality fundep!?"
emitFDWorkAsDerived :: [(EvVar,WantedLoc)]
-> SubGoalDepth -> TcS ()
emitFDWorkAsDerived evlocs d
= updWorkListTcS $ appendWorkListEqs fd_cts
where fd_cts = map mk_fd_ct evlocs
mk_fd_ct (v,wl) = CNonCanonical { cc_id = v
, cc_flavor = Derived wl
, cc_depth = d }
\end{code}
*********************************************************************************
* *
The top-reaction Stage
......@@ -1500,6 +1611,7 @@ Then it is solvable, but its very hard to detect this on the spot.
It's exactly the same with implicit parameters, except that the
"aggressive" approach would be much easier to implement.
Note [When improvement happens]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We fire an improvement rule when
......
......@@ -60,7 +60,7 @@ module TcSMonad (
-- Inerts
InertSet(..),
getInertEqs, liftInertEqsTy, getCtCoercion,
getInertEqs, getCtCoercion,
emptyInert, getTcSInerts, updInertSet, extractUnsolved,
extractUnsolvedTcS, modifyInertTcS,
updInertSetTcS, partitionCCanMap, partitionEqMap,
......@@ -72,7 +72,7 @@ module TcSMonad (
instDFunConstraints,
newFlexiTcSTy, instFlexiTcS,
compatKind, compatKindTcS, isSubKindTcS, unifyKindTcS,
compatKind, mkKindErrorCtxtTcS,
TcsUntouchables,
isTouchableMetaTyVar,
......@@ -104,7 +104,7 @@ import qualified TcRnMonad as TcM
import qualified TcMType as TcM
import qualified TcEnv as TcM
( checkWellStaged, topIdLvl, tcGetDefaultTys )
import {-# SOURCE #-} qualified TcUnify as TcM ( unifyKindEq, mkKindErrorCtxt )
import {-# SOURCE #-} qualified TcUnify as TcM ( mkKindErrorCtxt )
import Kind
import TcType
import DynFlags
......@@ -113,7 +113,6 @@ import Type
import TcEvidence
import Class
import TyCon
import TypeRep
import Name
import Var
......@@ -145,23 +144,12 @@ import TrieMap
compatKind :: Kind -> Kind -> Bool
compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
compatKindTcS :: Kind -> Kind -> TcS Bool
-- Because kind unification happens during constraint solving, we have
-- to make sure that two kinds are zonked before we compare them.
compatKindTcS k1 k2 = wrapTcS (TcM.compatKindTcM k1 k2)
isSubKindTcS :: Kind -> Kind -> TcS Bool
isSubKindTcS k1 k2 = wrapTcS (TcM.isSubKindTcM k1 k2)
unifyKindTcS :: Type -> Type -- Context
-> Kind -> Kind -- Corresponding kinds
-> TcS Bool
unifyKindTcS ty1 ty2 ki1 ki2
= wrapTcS $ TcM.addErrCtxtM ctxt $ do
(_errs, mb_r) <- TcM.tryTc (TcM.unifyKindEq ki1 ki2)
return (maybe False (const True) mb_r)
where
ctxt = TcM.mkKindErrorCtxt ty1 ki1 ty2 ki2
mkKindErrorCtxtTcS :: Type -> Kind
-> Type -> Kind
-> ErrCtxt
mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
= (False,TcM.mkKindErrorCtxt ty1 ty2 ki1 ki2)
\end{code}
%************************************************************************
......@@ -1506,67 +1494,5 @@ getCtCoercion ct
-- Instead we use the most accurate type, given by ctPred c
where maybe_given = isGiven_maybe (cc_flavor ct)
-- See Note [LiftInertEqs]
liftInertEqsTy :: (TyVarEnv (Ct, TcCoercion),InScopeSet)
-> CtFlavor
-> PredType -> TcCoercion
liftInertEqsTy (subst,inscope) fl pty
= ty_cts_subst subst inscope fl pty
ty_cts_subst :: TyVarEnv (Ct, TcCoercion)
-> InScopeSet -> CtFlavor -> Type -> TcCoercion
ty_cts_subst subst inscope fl ty
= go ty
where
go ty = go' ty
go' (TyVarTy tv) = tyvar_cts_subst tv `orElse` mkTcReflCo (TyVarTy tv)
go' (AppTy ty1 ty2) = mkTcAppCo (go ty1) (go ty2)
go' (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)
go' (ForAllTy v ty) = mkTcForAllCo v' $! co
where
(subst',inscope',v') = upd_tyvar_bndr subst inscope v
co = ty_cts_subst subst' inscope' fl ty
go' (FunTy ty1 ty2) = mkTcFunCo (go ty1) (go ty2)
tyvar_cts_subst tv
| Just (ct,co) <- lookupVarEnv subst tv, cc_flavor ct `canRewrite` fl
= Just co -- Warn: use cached, not cc_id directly, because of alpha-renamings!
| otherwise = Nothing
upd_tyvar_bndr subst inscope v
= (new_subst, (inscope `extendInScopeSet` new_v), new_v)
where new_subst
| no_change = delVarEnv subst v
-- Otherwise we have to extend the environment with /something/.
-- But we do not want to monadically create a new EvVar. So, we
-- create an 'unused_ct' but we cache reflexivity as the
-- associated coercion.
| otherwise = extendVarEnv subst v (unused_ct, mkTcReflCo (TyVarTy new_v))
no_change = new_v == v
new_v = uniqAway inscope v
unused_ct = CTyEqCan { cc_id = unused_evvar
, cc_flavor = fl -- canRewrite is reflexive.
, cc_tyvar = v
, cc_rhs = mkTyVarTy new_v
, cc_depth = unused_depth }
unused_depth = panic "ty_cts_subst: This depth should not be accessed!"
unused_evvar = panic "ty_cts_subst: This var is just an alpha-renaming!"
\end{code}