summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorDimitrios.Vytiniotis <dimitris@microsoft.com>2012-03-28 08:41:09 +0100
committerDimitrios.Vytiniotis <dimitris@microsoft.com>2012-03-28 08:41:09 +0100
commitcc2d2e1d44405630fb34311dc3f5e42eadc5c6b1 (patch)
tree954e83abe1ef320d10b0fe2deb37c5221d6e8383 /compiler
parent4bbe9f719f4c26e7f2d8e5a3a8096ac956e1be6c (diff)
downloadhaskell-cc2d2e1d44405630fb34311dc3f5e42eadc5c6b1.tar.gz
Midstream check-in on
(i) Replaced a lot of clunky and fragile EvVar handling code with a more uniform ``flavor transformer'' API in the canonicalizer and the interaction solver. Now EvVars are just fields inside the CtFlavors. (ii) Significantly simplified our caching story This patch does not validate yet and more refactoring is on the way.
Diffstat (limited to 'compiler')
-rw-r--r--compiler/coreSyn/TrieMap.lhs40
-rw-r--r--compiler/typecheck/Inst.lhs52
-rw-r--r--compiler/typecheck/TcCanonical.lhs632
-rw-r--r--compiler/typecheck/TcErrors.lhs60
-rw-r--r--compiler/typecheck/TcInteract.lhs533
-rw-r--r--compiler/typecheck/TcMType.lhs23
-rw-r--r--compiler/typecheck/TcRnTypes.lhs170
-rw-r--r--compiler/typecheck/TcSMonad.lhs994
-rw-r--r--compiler/typecheck/TcSimplify.lhs82
-rw-r--r--compiler/typecheck/TcUnify.lhs2
10 files changed, 1769 insertions, 819 deletions
diff --git a/compiler/coreSyn/TrieMap.lhs b/compiler/coreSyn/TrieMap.lhs
index d8a134ed87..fefea6dfdb 100644
--- a/compiler/coreSyn/TrieMap.lhs
+++ b/compiler/coreSyn/TrieMap.lhs
@@ -14,7 +14,7 @@
{-# LANGUAGE TypeFamilies #-}
module TrieMap(
CoreMap, emptyCoreMap, extendCoreMap, lookupCoreMap, foldCoreMap,
- TypeMap, foldTypeMap,
+ TypeMap, foldTypeMap, lookupTypeMap_mod,
CoercionMap,
MaybeMap,
ListMap,
@@ -521,6 +521,44 @@ lkT env ty m
go (TyConApp tc tys) = tm_tc_app >.> lkNamed tc >=> lkList (lkT env) tys
go (ForAllTy tv ty) = tm_forall >.> lkT (extendCME env tv) ty >=> lkBndr env tv
+
+lkT_mod :: CmEnv
+ -> TyVarEnv a -- A substitution
+ -> (a -> Type)
+ -> Type
+ -> TypeMap b -> Maybe b
+lkT_mod env s f ty m
+ | EmptyTM <- m = Nothing
+ | Just ty' <- coreView ty
+ = lkT_mod env s f ty' m
+ | isEmptyVarEnv candidates
+ = go env s ty m
+ | otherwise
+ = Just $ head (varEnvElts candidates) -- Yikes!
+ where
+ candidates = filterVarEnv_Directly find_matching (vm_fvar $ tm_var m)
+ find_matching tv _b = case lookupVarEnv_Directly s tv of
+ Nothing -> False
+ Just a -> f a `eqType` ty
+ go env _s (TyVarTy v) = tm_var >.> lkVar env v
+ go env s (AppTy t1 t2) = tm_app >.> lkT_mod env s f t1 >=> lkT_mod env s f t2
+ go env s (FunTy t1 t2) = tm_fun >.> lkT_mod env s f t1 >=> lkT_mod env s f t2
+ go env s (TyConApp tc tys) = tm_tc_app >.> lkNamed tc >=> lkList (lkT_mod env s f) tys
+ go _env _s (ForAllTy _tv _ty) = const Nothing
+ {- TODO: bleah the following is wrong!
+ = let (s',inscope') = substTyVarBndr tv (s,inscope)
+ in
+ let s' = delVarEnv s tv -- I think it's enough to just restrict substution
+ -- without renaming anything
+ in tm_forall >.> lkT_mod (extendCME env tv) s' f ty >=> lkBndr env tv
+ -}
+
+lookupTypeMap_mod :: TyVarEnv a -- A substitution to be applied to the /keys/ of type map
+ -> (a -> Type)
+ -> Type
+ -> TypeMap b -> Maybe b
+lookupTypeMap_mod = lkT_mod emptyCME
+
-----------------
xtT :: CmEnv -> Type -> XT a -> TypeMap a -> TypeMap a
xtT env ty f m
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index 0833a7c7cf..ffaeac8af8 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -85,7 +85,7 @@ emitWanteds origin theta = mapM (emitWanted origin) theta
emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
emitWanted origin pred = do { loc <- getCtLoc origin
; ev <- newWantedEvVar pred
- ; emitFlat (mkNonCanonical ev (Wanted loc))
+ ; emitFlat (mkNonCanonical (Wanted loc ev))
; return ev }
newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
@@ -527,7 +527,7 @@ tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
tyVarsOfCt (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCt (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
tyVarsOfCt (CIrredEvCan { cc_ty = ty }) = tyVarsOfType ty
-tyVarsOfCt (CNonCanonical { cc_id = ev }) = tyVarsOfEvVar ev
+tyVarsOfCt (CNonCanonical { cc_flavor = fl }) = tyVarsOfType (ctFlavPred fl)
tyVarsOfCDict :: Ct -> TcTyVarSet
tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
@@ -563,19 +563,29 @@ tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
tidyCt :: TidyEnv -> Ct -> Ct
-- Also converts it to non-canonical
tidyCt env ct
- = CNonCanonical { cc_id = tidyEvVar env (cc_id ct)
- , cc_flavor = tidyFlavor env (cc_flavor ct)
+ = CNonCanonical { cc_flavor = tidy_flavor env (cc_flavor ct)
, cc_depth = cc_depth ct }
+ where tidy_flavor :: TidyEnv -> CtFlavor -> CtFlavor
+ tidy_flavor env (Given { flav_gloc = gloc, flav_evar = evar })
+ = Given { flav_gloc = tidyGivenLoc env gloc
+ , flav_evar = tidyEvVar env evar }
+ tidy_flavor env (Solved { flav_gloc = gloc
+ , flav_evar = evar })
+ = Solved { flav_gloc = tidyGivenLoc env gloc
+ , flav_evar = tidyEvVar env evar }
+ tidy_flavor env (Wanted { flav_wloc = wloc
+ , flav_evar = evar })
+ = Wanted { flav_wloc = wloc -- Interesting: no tidying needed?
+ , flav_evar = tidyEvVar env evar }
+ tidy_flavor env (Derived { flav_wloc = wloc, flav_der_pty = pty })
+ = Derived { flav_wloc = wloc, flav_der_pty = tidyType env pty }
tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar env var = setVarType var (tidyType env (varType var))
-tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
-tidyFlavor env (Given loc gk) = Given (tidyGivenLoc env loc) gk
-tidyFlavor _ fl = fl
-
tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
-tidyGivenLoc env (CtLoc skol span ctxt) = CtLoc (tidySkolemInfo env skol) span ctxt
+tidyGivenLoc env (CtLoc skol span ctxt)
+ = CtLoc (tidySkolemInfo env skol) span ctxt
tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
@@ -595,13 +605,12 @@ substCt :: TvSubst -> Ct -> Ct
-- Conservatively converts it to non-canonical:
-- Postcondition: if the constraint does not get rewritten
substCt subst ct
- | ev <- cc_id ct, pty <- evVarPred (cc_id ct)
+ | pty <- ctPred ct
, sty <- substTy subst pty
= if sty `eqType` pty then
ct { cc_flavor = substFlavor subst (cc_flavor ct) }
else
- CNonCanonical { cc_id = setVarType ev sty
- , cc_flavor = substFlavor subst (cc_flavor ct)
+ CNonCanonical { cc_flavor = substFlavor subst (cc_flavor ct)
, cc_depth = cc_depth ct }
substWC :: TvSubst -> WantedConstraints -> WantedConstraints
@@ -626,11 +635,24 @@ substEvVar :: TvSubst -> EvVar -> EvVar
substEvVar subst var = setVarType var (substTy subst (varType var))
substFlavor :: TvSubst -> CtFlavor -> CtFlavor
-substFlavor subst (Given loc gk) = Given (substGivenLoc subst loc) gk
-substFlavor _ fl = fl
+substFlavor subst (Given { flav_gloc = gloc, flav_evar = evar })
+ = Given { flav_gloc = substGivenLoc subst gloc
+ , flav_evar = substEvVar subst evar }
+substFlavor subst (Solved { flav_gloc = gloc, flav_evar = evar })
+ = Solved { flav_gloc = substGivenLoc subst gloc
+ , flav_evar = substEvVar subst evar }
+
+substFlavor subst (Wanted { flav_wloc = wloc, flav_evar = evar })
+ = Wanted { flav_wloc = wloc
+ , flav_evar = substEvVar subst evar }
+
+substFlavor subst (Derived { flav_wloc = wloc, flav_der_pty = pty })
+ = Derived { flav_wloc = wloc
+ , flav_der_pty = substTy subst pty }
substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
-substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
+substGivenLoc subst (CtLoc skol span ctxt)
+ = CtLoc (substSkolemInfo subst skol) span ctxt
substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index d0323a58b0..76b6626223 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -7,7 +7,7 @@
-- for details
module TcCanonical(
- canonicalize,
+ canonicalize, flatten, flattenMany,
StopOrContinue (..)
) where
@@ -26,9 +26,9 @@ import TypeRep
import Name ( Name )
import Var
import VarEnv
-import Util( equalLength )
+-- import Util( equalLength )
import Outputable
-import Control.Monad ( when, unless, zipWithM )
+import Control.Monad ( when, unless )
import MonadUtils
import Control.Applicative ( (<|>) )
@@ -37,8 +37,10 @@ import VarSet
import TcSMonad
import FastString
-import Data.Maybe ( isNothing )
-import Data.List ( zip4 )
+import TysWiredIn ( eqTyCon )
+
+import Data.Maybe ( isJust, fromMaybe )
+-- import Data.List ( zip4 )
\end{code}
@@ -169,53 +171,55 @@ EvBinds, so we are again good.
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
canonicalize :: Ct -> TcS StopOrContinue
-canonicalize ct@(CNonCanonical { cc_id = ev, cc_flavor = fl, cc_depth = d })
+canonicalize ct@(CNonCanonical { cc_flavor = fl, cc_depth = d })
= do { traceTcS "canonicalize (non-canonical)" (ppr ct)
; {-# SCC "canEvVar" #-}
- canEvVar ev (classifyPredType (evVarPred ev)) d fl }
+ canEvVar d fl (classifyPredType (ctPred ct)) }
-canonicalize (CDictCan { cc_id = ev, cc_depth = d
+canonicalize (CDictCan { cc_depth = d
, cc_flavor = fl
, cc_class = cls
, cc_tyargs = xis })
= {-# SCC "canClass" #-}
- canClass d fl ev cls xis -- Do not add any superclasses
-canonicalize (CTyEqCan { cc_id = ev, cc_depth = d
+ canClass d fl cls xis -- Do not add any superclasses
+canonicalize (CTyEqCan { cc_depth = d
, cc_flavor = fl
, cc_tyvar = tv
, cc_rhs = xi })
= {-# SCC "canEqLeafTyVarLeftRec" #-}
- canEqLeafTyVarLeftRec d fl ev tv xi
+ canEqLeafTyVarLeftRec d fl tv xi
-canonicalize (CFunEqCan { cc_id = ev, cc_depth = d
+canonicalize (CFunEqCan { cc_depth = d
, cc_flavor = fl
, cc_fun = fn
, cc_tyargs = xis1
, cc_rhs = xi2 })
= {-# SCC "canEqLeafFunEqLeftRec" #-}
- canEqLeafFunEqLeftRec d fl ev (fn,xis1) xi2
+ canEqLeafFunEqLeftRec d fl (fn,xis1) xi2
-canonicalize (CIPCan { cc_id = ev, cc_depth = d
+canonicalize (CIPCan { cc_depth = d
, cc_flavor = fl
, cc_ip_nm = nm
, cc_ip_ty = xi })
- = canIP d fl ev nm xi
-canonicalize (CIrredEvCan { cc_id = ev, cc_flavor = fl
+ = canIP d fl nm xi
+canonicalize (CIrredEvCan { cc_flavor = fl
, cc_depth = d
, cc_ty = xi })
- = canIrred d fl ev xi
+ = canIrred d fl xi
-canEvVar :: EvVar -> PredTree
- -> SubGoalDepth -> CtFlavor -> TcS StopOrContinue
+canEvVar :: SubGoalDepth
+ -> CtFlavor
+ -> PredTree
+ -> TcS StopOrContinue
-- Called only for non-canonical EvVars
-canEvVar ev pred_classifier d fl
+canEvVar d fl pred_classifier
= case pred_classifier of
- ClassPred cls tys -> canClassNC d fl ev cls tys
- EqPred ty1 ty2 -> canEqNC d fl ev ty1 ty2
- 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
+ ClassPred cls tys -> canClassNC d fl cls tys
+ EqPred ty1 ty2 -> canEqNC d fl ty1 ty2
+ IPPred nm ty -> canIP d fl nm ty
+ IrredPred ev_ty -> canIrred d fl ev_ty
+ TuplePred tys -> canTuple d fl tys
\end{code}
@@ -227,9 +231,20 @@ canEvVar ev pred_classifier d fl
\begin{code}
canTuple :: SubGoalDepth -- Depth
- -> CtFlavor -> EvVar -> [PredType] -> TcS StopOrContinue
-canTuple d fl ev tys
- = do { traceTcS "can_pred" (text "TuplePred!")
+ -> CtFlavor -> [PredType] -> TcS StopOrContinue
+canTuple d fl tys
+ = do { traceTcS "can_pred" (text "TuplePred!")
+ ; let xcomp = EvTupleMk
+ xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]
+ ; xCtFlavor fl tys (XEvTerm xcomp xdecomp) what_next }
+ where what_next fls = mapM_ add_to_work fls >> return Stop
+ add_to_work fl = addToWork $ canEvVar d fl (classifyPredType (ctFlavPred fl))
+
+{- DELETEME
+ ; return Stop }
+ do { mapM (\fl -> addToWork (canEvVar d fl (classifyPredType (ctFlavPred fl))))
+ ; return Stop }
+
; evs <- zipWithM can_pred_tup_one tys [0..]
; if (isWanted fl) then
do {_unused_fl <- setEvBind ev (EvTupleMk evs) fl
@@ -245,6 +260,7 @@ canTuple d fl ev tys
; when (isNewEvVar evc) $
addToWork (canEvVar ev' (classifyPredType (evVarPred ev')) d fl')
; return ev' }
+-}
\end{code}
@@ -256,14 +272,23 @@ canTuple d fl ev tys
\begin{code}
canIP :: SubGoalDepth -- Depth
- -> CtFlavor -> EvVar
+ -> CtFlavor
-> IPName Name -> Type -> TcS StopOrContinue
-- Precondition: EvVar is implicit parameter evidence
-canIP d fl v nm ty
+canIP d fl nm ty
= -- Note [Canonical implicit parameter constraints] explains why it's
-- possible in principle to not flatten, but since flattening applies
-- the inert substitution we choose to flatten anyway.
do { (xi,co) <- flatten d fl (mkIPPred nm ty)
+ ; mb <- rewriteCtFlavor fl xi co
+ ; case mb of
+ Just new_fl -> let IPPred _ xi_in = classifyPredType xi
+ in continueWith $ CIPCan { cc_flavor = new_fl
+ , cc_ip_nm = nm, cc_ip_ty = xi_in
+ , cc_depth = d }
+ Nothing -> return Stop }
+
+{- DELETEME
; let no_flattening = isTcReflCo co
; if no_flattening then
let IPPred _ xi_in = classifyPredType xi
@@ -283,6 +308,8 @@ canIP d fl v nm ty
, cc_ip_ty = ip_xi
, cc_depth = d }
else return Stop } }
+-}
+
\end{code}
Note [Canonical implicit parameter constraints]
@@ -305,7 +332,7 @@ flattened in the first place to facilitate comparing them.)
\begin{code}
canClass, canClassNC
:: SubGoalDepth -- Depth
- -> CtFlavor -> EvVar
+ -> CtFlavor
-> Class -> [Type] -> TcS StopOrContinue
-- Precondition: EvVar is class evidence
@@ -314,16 +341,24 @@ canClass, canClassNC
-- for already-canonical class constraints (but which might have
-- been subsituted or somthing), and hence do not need superclasses
-canClassNC d fl ev cls tys
- = canClass d fl ev cls tys
+canClassNC d fl cls tys
+ = canClass d fl cls tys
`andWhenContinue` emitSuperclasses
-canClass d fl v cls tys
+canClass d fl cls tys
= do { -- sctx <- getTcSContext
; (xis, cos) <- flattenMany d fl tys
; let co = mkTcTyConAppCo (classTyCon cls) cos
xi = mkClassPred cls xis
-
+
+ ; mb <- rewriteCtFlavor fl xi co
+ ; case mb of
+ Just new_fl -> continueWith $
+ CDictCan { cc_flavor = new_fl
+ , cc_tyargs = xis, cc_class = cls, cc_depth = d }
+ Nothing -> return Stop }
+
+{- DELETEME
; let no_flattening = all isTcReflCo cos
-- No flattening, continue with canonical
; if no_flattening then
@@ -343,15 +378,16 @@ canClass d fl v cls tys
, cc_tyargs = xis, cc_class = cls
, cc_depth = d }
else return Stop } }
+-}
emitSuperclasses :: Ct -> TcS StopOrContinue
-emitSuperclasses ct@(CDictCan { cc_id = v_new, cc_depth = d, cc_flavor = fl
+emitSuperclasses ct@(CDictCan { cc_depth = d, cc_flavor = fl
, cc_tyargs = xis_new, cc_class = cls })
-- Add superclasses of this one here, See Note [Adding superclasses].
-- But only if we are not simplifying the LHS of a rule.
= do { sctxt <- getTcSContext
; unless (simplEqsOnly sctxt) $
- newSCWorkFromFlavored d v_new fl cls xis_new
+ newSCWorkFromFlavored d 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!
@@ -425,52 +461,38 @@ happen.
\begin{code}
newSCWorkFromFlavored :: SubGoalDepth -- Depth
- -> EvVar -> CtFlavor -> Class -> [Xi] -> TcS ()
+ -> CtFlavor -> Class -> [Xi] -> TcS ()
-- Returns superclasses, see Note [Adding superclasses]
-newSCWorkFromFlavored d ev flavor cls xis
+newSCWorkFromFlavored d flavor cls xis
| isDerived flavor
= return () -- Deriveds don't yield more superclasses because we will
-- add them transitively in the case of wanteds.
-
- | Just gk <- isGiven_maybe flavor
- = case gk of
- GivenOrig -> do { let sc_theta = immSuperClasses cls xis
- ; sc_vars <- mapM (newEvVar flavor) sc_theta
- ; sc_cts <- zipWithM (\scv ev_trm ->
- do { let sc_evvar = evc_the_evvar scv
- ; _unused_fl <- setEvBind sc_evvar ev_trm flavor
- -- unused because it's the same
- ; return $
- CNonCanonical { cc_id = sc_evvar
- , cc_flavor = flavor
- , cc_depth = d }})
- sc_vars [EvSuperClass ev n | n <- [0..]]
- -- Emit now, canonicalize later in a lazier fashion
- ; traceTcS "newSCWorkFromFlavored" $
- text "Emitting superclass work:" <+> ppr sc_cts
- ; updWorkListTcS $ appendWorkListCt sc_cts }
- GivenSolved {} -> return ()
- -- Seems very dangerous to add the superclasses for dictionaries that may be
- -- partially solved because we may end up with evidence loops.
+ | isSolved flavor
+ = return ()
+
+ | isGiven flavor
+ = do { let sc_theta = immSuperClasses cls xis
+ xev = XEvTerm { ev_comp = panic "Can't compose for given!"
+ , ev_decomp = \x->zipWith (\_ i->EvSuperClass x i) sc_theta [0..] }
+ ; xCtFlavor flavor sc_theta xev (emit_sc_flavs d) }
| isEmptyVarSet (tyVarsOfTypes xis)
- = return () -- Wanteds with no variables yield no deriveds.
+ = return () -- Wanteds/Derived with no variables yield no deriveds.
-- See Note [Improvement from Ground Wanteds]
- | otherwise -- Wanted case, just add those SC that can lead to improvement.
+ | otherwise -- Wanted/Derived case, just add those SC that can lead to improvement.
= do { let sc_rec_theta = transSuperClasses cls xis
- impr_theta = filter is_improvement_pty sc_rec_theta
- Wanted wloc = flavor
- ; sc_cts <- mapM (\pty -> do { scv <- newEvVar (Derived wloc) pty
- ; if isNewEvVar scv then
- return [ CNonCanonical { cc_id = evc_the_evvar scv
- , cc_flavor = Derived wloc
- , cc_depth = d } ]
- else return [] }
- ) impr_theta
- ; let sc_cts_flat = concat sc_cts
- ; traceTcS "newSCWorkFromFlavored" (text "Emitting superclass work:" <+> ppr sc_cts_flat)
- ; updWorkListTcS $ appendWorkListCt sc_cts_flat }
+ impr_theta = filter is_improvement_pty sc_rec_theta
+ xev = panic "Derived's are not supposed to transform evidence!"
+ ; xCtFlavor (Derived (flav_wloc flavor) (ctFlavPred flavor)) impr_theta xev $
+ emit_sc_flavs d }
+
+emit_sc_flavs :: SubGoalDepth -> [CtFlavor] -> TcS ()
+emit_sc_flavs d fls
+ = do { traceTcS "newSCWorkFromFlavored" $
+ text "Emitting superclass work:" <+> ppr sc_cts
+ ; updWorkListTcS $ appendWorkListCt sc_cts }
+ where sc_cts = map (\fl -> CNonCanonical { cc_flavor = fl, cc_depth = d }) fls
is_improvement_pty :: PredType -> Bool
-- Either it's an equality, or has some functional dependency
@@ -494,15 +516,26 @@ is_improvement_pty ty = go (classifyPredType ty)
\begin{code}
canIrred :: SubGoalDepth -- Depth
- -> CtFlavor -> EvVar -> TcType -> TcS StopOrContinue
+ -> CtFlavor -> TcType -> TcS StopOrContinue
-- Precondition: ty not a tuple and no other evidence form
-canIrred d fl v ty
+canIrred d fl ty
= do { traceTcS "can_pred" (text "IrredPred = " <+> ppr ty)
; (xi,co) <- flatten d fl ty -- co :: xi ~ ty
; let no_flattening = xi `eqType` ty
-- In this particular case it is not safe to
-- say 'isTcReflCo' because the new constraint may
-- be reducible!
+ ; mb <- rewriteCtFlavor fl xi co
+ ; case mb of
+ Just new_fl
+ | no_flattening
+ -> continueWith $
+ CIrredEvCan { cc_flavor = new_fl, cc_ty = xi, cc_depth = d }
+ | otherwise
+ -> canEvVar d new_fl (classifyPredType (ctFlavPred new_fl))
+ Nothing -> return Stop }
+
+{- DELETEME
; if no_flattening then
continueWith $ CIrredEvCan { cc_id = v, cc_flavor = fl
, cc_ty = xi, cc_depth = d }
@@ -522,6 +555,7 @@ canIrred d fl v ty
else
return Stop }
}
+-}
\end{code}
@@ -577,6 +611,7 @@ flattenMany :: SubGoalDepth -- Depth
-> CtFlavor -> [Type] -> TcS ([Xi], [TcCoercion])
-- Coercions :: Xi ~ Type
-- Returns True iff (no flattening happened)
+-- NB: The EvVar inside the flavor is unused, we merely want Given/Solved/Derived/Wanted info
flattenMany d ctxt tys
= -- pprTrace "flattenMany" empty $
go tys
@@ -627,53 +662,66 @@ flatten d fl (TyConApp tc tys)
-- in which case the remaining arguments should
-- be dealt with by AppTys
fam_ty = mkTyConApp tc xi_args
+
; (ret_co, rhs_xi, ct) <-
- do { is_cached <- getCachedFlatEq tc xi_args fl Any
- ; case is_cached of
- Just (rhs_xi,ret_eq) ->
- do { traceTcS "is_cached!" $ ppr ret_eq
- ; return (ret_eq, rhs_xi, []) }
- Nothing
- | isGivenOrSolved fl ->
- do { rhs_xi_var <- newFlattenSkolemTy fam_ty
- ; (fl',eqv)
- <- newGivenEqVar fl fam_ty rhs_xi_var (mkTcReflCo fam_ty)
- ; let ct = CFunEqCan { cc_id = eqv
- , cc_flavor = fl' -- Given
- , cc_fun = tc
- , cc_tyargs = xi_args
- , cc_rhs = rhs_xi_var
- , cc_depth = d }
- -- Update the flat cache: just an optimisation!
- ; updateFlatCache eqv fl' tc xi_args rhs_xi_var WhileFlattening
- ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
- | otherwise ->
- -- Derived or Wanted: make a new /unification/ flatten variable
- do { rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
- ; let wanted_flavor = mkWantedFlavor fl
- ; evc <- newEqVar wanted_flavor fam_ty rhs_xi_var
- ; let eqv = evc_the_evvar evc -- Not going to be cached
- ct = CFunEqCan { cc_id = eqv
- , cc_flavor = wanted_flavor
- -- Always Wanted, not Derived
- , cc_fun = tc
- , cc_tyargs = xi_args
- , cc_rhs = rhs_xi_var
- , cc_depth = d }
+ do { flat_cache <- getFlatCache
+ ; case lookupTM fam_ty flat_cache of
+ Just ct
+ | cc_flavor ct `canRewrite` fl
+ -> -- You may think that we can just return (cc_rhs ct) but not so.
+ -- return (mkTcCoVarCo (ctId ct), cc_rhs ct, [])
+ -- The cached constraint resides in the cache so we have to flatten
+ -- the rhs to make sure we have applied any inert substitution to it.
+ -- Alternatively we could be applying the inert substitution to the
+ -- cache as well when we interact an equality with the inert.
+ -- The design choice is: do we keep the flat cache rewritten or not?
+ -- For now I say we don't keep it fully rewritten.
+ do { let rhs_xi = cc_rhs ct
+ ; (flat_rhs_xi,co) <- flatten (cc_depth ct) (cc_flavor ct) rhs_xi
+ ; let final_co = mkTcCoVarCo (ctId "flatten" ct) `mkTcTransCo` (mkTcSymCo co)
+ ; return (final_co, flat_rhs_xi,[]) }
+
+ _ | isGivenOrSolved fl -- Given or Solved: make new flatten skolem
+ -> do { rhs_xi_var <- newFlattenSkolemTy fam_ty
+ ; mg <- newGivenEvVar (mkTcEqPred fam_ty rhs_xi_var)
+ (EvCoercion (mkTcReflCo fam_ty))
+ ; case mg of
+ Fresh eqv ->
+ do { let new_fl = Given (flav_gloc fl) eqv
+ ct = CFunEqCan { cc_flavor = new_fl
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_xi_var
+ , cc_depth = d }
+ -- Update the flat cache
+ ; updFlatCache ct
+ ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
+ Cached {} -> panic "flatten TyConApp, var must be fresh!" }
+ | otherwise -- Wanted or Derived: make new unification variable
+ -> do { rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
+ ; mw <- newWantedEvVar (mkTcEqPred fam_ty rhs_xi_var)
+ ; case mw of
+ Fresh eqv ->
+ do { let new_fl = Wanted (flav_wloc fl) eqv
+ ct = CFunEqCan { cc_flavor = new_fl
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_xi_var
+ , cc_depth = d }
-- Update the flat cache: just an optimisation!
- ; updateFlatCache eqv fl tc xi_args rhs_xi_var WhileFlattening
- ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) } }
-
- -- Emit the flat constraints
+ ; updFlatCache ct
+ ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
+ Cached {} -> panic "flatten TyConApp, var must be fresh!" }
+ }
+ -- Emit the flat constraints
; updWorkListTcS $ appendWorkListEqs ct
-
; let (cos_args, cos_rest) = splitAt (tyConArity tc) cos
- ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
- -- cf Trac #5655
- , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo tc cos_args)
- cos_rest
- ) }
-
+ ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
+ -- cf Trac #5655
+ , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo tc cos_args) $
+ cos_rest
+ )
+ }
flatten d ctxt ty@(ForAllTy {})
-- We allow for-alls when, but only when, no type function
@@ -715,9 +763,11 @@ flattenTyVar d ctxt tv
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
+ | Just ct <- lookupVarEnv subst tv
, cc_flavor ct `canRewrite` ctxt
- = Just (co,cc_rhs ct)
+ = Just (mkTcCoVarCo (ctId "tv_eq_subst" ct),cc_rhs ct)
+ -- NB: even if ct is Derived we are not going to
+ -- touch the actual coercion so we are fine.
| otherwise = Nothing
\end{code}
@@ -728,7 +778,7 @@ The inert substitution is not idempotent in the broad sense. It is only idempote
that it cannot rewrite the RHS of other inert equalities any further. An example of such
an inert substitution is:
- [Ś] g1 : ta8 ~ ta4
+ [G] g1 : ta8 ~ ta4
[W] g2 : ta4 ~ a5Fj
Observe that the wanted cannot rewrite the solved goal, despite the fact that ta4 appears on
@@ -750,6 +800,8 @@ so that we can make sure that the inert substitution /is/ fully applied.
This insufficient rewriting was the reason for #5668.
\begin{code}
+
+{- DELETEME
getCachedFlatEq :: TyCon -> [Xi] -> CtFlavor
-> FlatEqOrigin
-> TcS (Maybe (Xi, TcCoercion))
@@ -777,6 +829,7 @@ getCachedFlatEq tc xi_args fl feq_origin
; return $ Just (xi'', co' `mkTcTransCo` (mkTcSymCo co)) }
_ -> do { traceTcS "getCachedFlatEq" $ text "failure!" <+> pprEvVarCache flat_cache
; return Nothing }
+-}
-----------------
addToWork :: TcS StopOrContinue -> TcS ()
@@ -794,6 +847,19 @@ addToWork tcs_action = tcs_action >>= stop_or_emit
%************************************************************************
\begin{code}
+canEqEvVarsCreated :: SubGoalDepth
+ -> [CtFlavor] -> TcS StopOrContinue
+canEqEvVarsCreated _d [] = return Stop
+canEqEvVarsCreated d (quad:quads)
+ = mapM_ (addToWork . do_quad) quads >> do_quad quad
+ -- Add all but one to the work list
+ -- and return the first (if any) for futher processing
+ where do_quad fl = let EqPred ty1 ty2 = classifyPredType $ ctFlavPred fl
+ in canEqNC d fl ty1 ty2
+ -- Note the "NC": these are fresh equalities so we must be
+ -- careful to add their kind constraints
+
+{- DELETEME
canEqEvVarsCreated :: SubGoalDepth
-> [CtFlavor] -> [EvVarCreated] -> [Type] -> [Type]
-> TcS StopOrContinue
@@ -810,53 +876,61 @@ canEqEvVarsCreated d fls evcs tys1 tys2
do_quad (fl, evc, ty1, ty2) = canEqNC d fl (evc_the_evvar evc) ty1 ty2
-- Note the "NC": these are fresh equalities so we must be
-- careful to add their kind constraints
+-}
-------------------------
canEqNC, canEq
:: SubGoalDepth
- -> CtFlavor -> EqVar
+ -> CtFlavor
-> Type -> Type -> TcS StopOrContinue
-canEqNC d fl ev ty1 ty2
- = canEq d fl ev ty1 ty2
+canEqNC d fl ty1 ty2
+ = canEq d fl ty1 ty2
`andWhenContinue` emitKindConstraint
-canEq _d fl eqv ty1 ty2
+canEq _d fl ty1 ty2
| eqType ty1 ty2 -- Dealing with equality here avoids
-- later spurious occurs checks for a~a
- = do { when (isWanted fl) $
- do { _ <- setEqBind eqv (mkTcReflCo ty1) fl; return () }
- ; return Stop }
+ = if isWanted fl then
+ setEvBind (flav_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop
+ else
+ return Stop
-- If one side is a variable, orient and flatten,
-- WITHOUT expanding type synonyms, so that we tend to
-- substitute a ~ Age rather than a ~ Int when @type Age = Int@
-canEq d fl eqv ty1@(TyVarTy {}) ty2
- = canEqLeaf d fl eqv ty1 ty2
-canEq d fl eqv ty1 ty2@(TyVarTy {})
- = canEqLeaf d fl eqv ty1 ty2
+canEq d fl ty1@(TyVarTy {}) ty2
+ = canEqLeaf d fl ty1 ty2
+canEq d fl ty1 ty2@(TyVarTy {})
+ = canEqLeaf d fl ty1 ty2
-- See Note [Naked given applications]
-canEq d fl eqv ty1 ty2
- | Just ty1' <- tcView ty1 = canEq d fl eqv ty1' ty2
- | Just ty2' <- tcView ty2 = canEq d fl eqv ty1 ty2'
+canEq d fl ty1 ty2
+ | Just ty1' <- tcView ty1 = canEq d fl ty1' ty2
+ | Just ty2' <- tcView ty2 = canEq d fl ty1 ty2'
-canEq d fl eqv ty1@(TyConApp fn tys) ty2
+canEq d fl ty1@(TyConApp fn tys) ty2
| isSynFamilyTyCon fn, length tys == tyConArity fn
- = canEqLeaf d fl eqv ty1 ty2
-canEq d fl eqv ty1 ty2@(TyConApp fn tys)
+ = canEqLeaf d fl ty1 ty2
+canEq d fl ty1 ty2@(TyConApp fn tys)
| isSynFamilyTyCon fn, length tys == tyConArity fn
- = canEqLeaf d fl eqv ty1 ty2
+ = canEqLeaf d fl ty1 ty2
-canEq d fl eqv ty1 ty2
+canEq d fl ty1 ty2
| Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
, Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
, isDecomposableTyCon tc1 && isDecomposableTyCon tc2
= -- Generate equalities for each of the corresponding arguments
if (tc1 /= tc2 || length tys1 /= length tys2)
-- Fail straight away for better error messages
- then canEqFailure d fl eqv
- else do
+ then canEqFailure d fl
+ else
+ let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map mkTcCoVarCo xs))
+ xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (mkTcCoVarCo x)) tys1 [0..]
+ xev = XEvTerm xcomp xdecomp
+ in xCtFlavor fl (zipWith mkTcEqPred tys1 tys2) xev (canEqEvVarsCreated d)
+
+{- DELETEME
{ argeqvs <- zipWithM (newEqVar fl) tys1 tys2
; fls <- case fl of
@@ -871,31 +945,33 @@ canEq d fl eqv ty1 ty2
Derived {} -> return (map (\_ -> fl) argeqvs)
; canEqEvVarsCreated d fls argeqvs tys1 tys2 }
+-}
-- See Note [Equality between type applications]
-- Note [Care with type applications] in TcUnify
-canEq d fl eqv ty1 ty2 -- e.g. F a b ~ Maybe c
+canEq d fl ty1 ty2 -- e.g. F a b ~ Maybe c
-- where F has arity 1
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
, Just (s2,t2) <- tcSplitAppTy_maybe ty2
- = canEqAppTy d fl eqv s1 t1 s2 t2
+ = canEqAppTy d fl s1 t1 s2 t2
-canEq d fl eqv s1@(ForAllTy {}) s2@(ForAllTy {})
+canEq d fl s1@(ForAllTy {}) s2@(ForAllTy {})
| tcIsForAllTy s1, tcIsForAllTy s2,
Wanted {} <- fl
- = canEqFailure d fl eqv
+ = canEqFailure d fl
| otherwise
= do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
; return Stop }
-canEq d fl eqv _ _ = canEqFailure d fl eqv
+canEq d fl _ _ = canEqFailure d fl
------------------------
-- Type application
canEqAppTy :: SubGoalDepth
- -> CtFlavor -> EqVar -> Type -> Type -> Type -> Type
+ -> CtFlavor
+ -> Type -> Type -> Type -> Type
-> TcS StopOrContinue
-canEqAppTy d fl eqv s1 t1 s2 t2
+canEqAppTy d fl s1 t1 s2 t2
= ASSERT( not (isKind t1) && not (isKind t2) )
if isGivenOrSolved fl then
do { traceTcS "canEq (app case)" $
@@ -904,19 +980,28 @@ canEqAppTy d fl eqv s1 t1 s2 t2
-- We cannot decompose given applications
-- because we no longer have 'left' and 'right'
; return Stop }
- else
+ else
+ let xevcomp [x,y] = EvCoercion (mkTcAppCo (mkTcCoVarCo x) (mkTcCoVarCo y))
+ xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
+ xev = XEvTerm { ev_comp = xevcomp
+ , ev_decomp = error "canEqAppTy: can't happen" }
+ in xCtFlavor fl [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev $
+ canEqEvVarsCreated d
+
+{- DELETEME
do { evc1 <- newEqVar fl s1 s2
; evc2 <- newEqVar fl t1 t2
; let eqv1 = evc_the_evvar evc1
eqv2 = evc_the_evvar evc2
-
; when (isWanted fl) $
do { _ <- setEqBind eqv (mkTcAppCo (mkTcCoVarCo eqv1) (mkTcCoVarCo eqv2)) fl
- ; return () }
-
+ ; return () }
; canEqEvVarsCreated d [fl,fl] [evc1,evc2] [s1,t1] [s2,t2] }
+-}
+
------------------------
+{- OLD CODE WAS:
canEqFailure :: SubGoalDepth
-> CtFlavor -> EvVar -> TcS StopOrContinue
canEqFailure d fl eqv
@@ -925,30 +1010,52 @@ canEqFailure d fl eqv
; emitFrozenError fl eqv d
; return Stop }
+In particular, is that: delCachedEvVar so important?
+
+-}
+
+canEqFailure :: SubGoalDepth -> CtFlavor -> TcS StopOrContinue
+canEqFailure d fl = emitFrozenError fl d >> return Stop
+
------------------------
emitKindConstraint :: Ct -> TcS StopOrContinue
emitKindConstraint ct
= case ct of
- CTyEqCan { cc_id = ev, cc_depth = d
+ CTyEqCan { cc_depth = d
, cc_flavor = fl, cc_tyvar = tv
, cc_rhs = ty }
- -> emit_kind_constraint ev d fl (mkTyVarTy tv) ty
+ -> emit_kind_constraint d fl (mkTyVarTy tv) ty
- CFunEqCan { cc_id = ev, cc_depth = d
+ CFunEqCan { cc_depth = d
, cc_flavor = fl
, cc_fun = fn, cc_tyargs = xis1
, cc_rhs = xi2 }
- -> emit_kind_constraint ev d fl (mkTyConApp fn xis1) xi2
+ -> emit_kind_constraint d fl (mkTyConApp fn xis1) xi2
- _ -> continueWith ct
+ _ -> continueWith ct
where
- emit_kind_constraint eqv d fl ty1 ty2
+ emit_kind_constraint d fl ty1 ty2
| compatKind k1 k2 -- True when ty1,ty2 are themselves kinds,
= continueWith ct -- because then k1, k2 are BOX
| otherwise
= ASSERT( isKind k1 && isKind k2 )
- do { keqv <- forceNewEvVar kind_co_fl (mkNakedEqPred superKind k1 k2)
+ do { kev <-
+ do { mw <- newWantedEvVar (mkNakedEqPred superKind k1 k2)
+ ; case mw of
+ Cached x -> return x
+ Fresh x -> addToWork (canEq d (kind_co_fl x) k1 k2) >> return x }
+ ; let xcomp [x] = mkEvKindCast x (mkTcCoVarCo kev)
+ xcomp _ = panic "emit_kind_constraint:can't happen"
+ xdecomp x = [mkEvKindCast x (mkTcCoVarCo kev)]
+ xev = XEvTerm xcomp xdecomp
+ in xCtFlavor fl [mkTcEqPred ty1 ty2] xev what_next }
+ where
+ what_next [new_fl] = continueWith (ct { cc_flavor = new_fl })
+ what_next _ = return Stop
+
+{- DELETEME
+ do { keqv <- forceNewEvVar kind_co_fl (mkNakedEqPred superKind k1 k2)
; eqv' <- forceNewEvVar fl (mkTcEqPred ty1 ty2)
; _fl <- case fl of
Wanted {}-> setEvBind eqv
@@ -962,26 +1069,32 @@ emitKindConstraint ct
, ppr eqv, ppr eqv' ]
; addToWork (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)
+ -- NB: DV finds this reasonable for now. Maybe we have to revisit.
+ kind_co_fl x
+ | isGivenOrSolved fl
+ = let (CtLoc _sk_info src_span err_ctxt) = flav_gloc fl
+ 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)
+ in Wanted ctloc x
+ | otherwise
+ = Wanted (pushErrCtxtSameOrigin ctxt (flav_wloc fl)) x
+
+{- DV: used to be .. DELETEME
+ | Wanted ctloc _ <- fl
+ = Wanted (pushErrCtxtSameOrigin ctxt ctloc) x
+ | Derived ctloc pty <- fl
+ = Derived (pushErrCtxtSameOrigin ctxt ctloc) pty
| otherwise
= panic "do_emit_kind_constraint: non-CtLoc inside!"
+-}
+
\end{code}
Note [Combining insoluble constraints]
@@ -1193,7 +1306,7 @@ reOrient _fl (FskCls {}) (OtherCls {}) = False
------------------
canEqLeaf :: SubGoalDepth -- Depth
- -> CtFlavor -> EqVar
+ -> CtFlavor
-> Type -> Type
-> TcS StopOrContinue
-- Canonicalizing "leaf" equality constraints which cannot be
@@ -1203,9 +1316,25 @@ canEqLeaf :: SubGoalDepth -- Depth
-- Preconditions:
-- * one of the two arguments is variable or family applications
-- * the two types are not equal (looking through synonyms)
-canEqLeaf d fl eqv s1 s2
+canEqLeaf d fl s1 s2
| cls1 `re_orient` cls2
- = do { traceTcS "canEqLeaf (reorienting)" $ ppr eqv <+> dcolon <+> pprEq s1 s2
+ = do { traceTcS "canEqLeaf (reorienting)" $ ppr fl <+> dcolon <+> pprEq s1 s2
+ ; let xcomp [x] = EvCoercion (mkTcSymCo (mkTcCoVarCo x))
+ xcomp _ = panic "canEqLeaf: can't happen"
+ xdecomp x = [EvCoercion (mkTcSymCo (mkTcCoVarCo x))]
+ xev = XEvTerm xcomp xdecomp
+ what_next [fl] = canEqLeafOriented d fl s2 s1
+ what_next _ = return Stop
+ ; xCtFlavor fl [mkTcEqPred s2 s1] xev what_next }
+ | otherwise
+ = do { traceTcS "canEqLeaf" $ ppr (mkTcEqPred s1 s2)
+ ; canEqLeafOriented d fl s1 s2 }
+ where
+ re_orient = reOrient fl
+ cls1 = classify s1
+ cls2 = classify s2
+
+{- DELETEME
; delCachedEvVar eqv fl
; evc <- newEqVar fl s2 s1
; let eqv' = evc_the_evvar evc
@@ -1217,52 +1346,53 @@ canEqLeaf d fl eqv s1 s2
do { canEqLeafOriented d fl' eqv' s2 s1 }
else return Stop
}
- | otherwise
- = do { traceTcS "canEqLeaf" $ ppr (mkEqPred s1 s2)
- ; canEqLeafOriented d fl eqv s1 s2 }
- where
- re_orient = reOrient fl
- cls1 = classify s1
- cls2 = classify s2
+-}
canEqLeafOriented :: SubGoalDepth -- Depth
- -> CtFlavor -> EqVar
+ -> CtFlavor
-> TcType -> TcType -> TcS StopOrContinue
-- By now s1 will either be a variable or a type family application
-canEqLeafOriented d fl eqv s1 s2
- = can_eq_split_lhs d fl eqv s1 s2
- where can_eq_split_lhs d fl eqv s1 s2
+canEqLeafOriented d fl s1 s2
+ = can_eq_split_lhs d fl s1 s2
+ where can_eq_split_lhs d fl s1 s2
| Just (fn,tys1) <- splitTyConApp_maybe s1
- = canEqLeafFunEqLeftRec d fl eqv (fn,tys1) s2
+ = canEqLeafFunEqLeftRec d fl (fn,tys1) s2
| Just tv <- getTyVar_maybe s1
- = canEqLeafTyVarLeftRec d fl eqv tv s2
+ = canEqLeafTyVarLeftRec d fl 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 (ctFlavPred fl)
canEqLeafFunEqLeftRec :: SubGoalDepth
- -> CtFlavor
- -> EqVar
+ -> CtFlavor
-> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
-canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2
+canEqLeafFunEqLeftRec d fl (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2
= do { traceTcS "canEqLeafFunEqLeftRec" $ pprEq (mkTyConApp fn tys1) ty2
; (xis1,cos1) <-
{-# SCC "flattenMany" #-}
flattenMany d fl tys1 -- Flatten type function arguments
-- cos1 :: xis1 ~ tys1
+
+ ; let fam_head = mkTyConApp fn xis1
+ -- Fancy higher-dimensional coercion between equalities!
+ ; let co = mkTcTyConAppCo eqTyCon $
+ [mkTcReflCo (typeKind ty2), mkTcTyConAppCo fn cos1, mkTcReflCo ty2]
+ -- co :: (F xis1 ~ ty2) ~ (F tys1 ~ ty2)
+
+ ; mb <- rewriteCtFlavor fl (mkTcEqPred fam_head ty2) co
+ ; case mb of
+ Nothing -> return Stop
+ Just new_fl -> canEqLeafFunEqLeft d new_fl (fn,xis1) ty2 }
+
--- ; inerts <- getTcSInerts
--- ; let fam_eqs = inert_funeqs inerts
+{- THERE WAS A LOT OF STUFF BELOW which allowed interactions with solved to happen
+ I am not convinced about how much benefit we got from those so I am provisionally deleting
+ the stuff below ...
- ; let flat_ty = mkTyConApp fn xis1
+ DELETEME
; is_cached <- getCachedFlatEq fn xis1 fl WhenSolved
-- Lookup if we have solved this goal already
-{-
- ; let is_cached = {-# SCC "lookupFunEq" #-}
- lookupFunEq flat_ty fl fam_eqs
--}
; let no_flattening = all isTcReflCo cos1
; if no_flattening && isNothing is_cached then
@@ -1294,7 +1424,6 @@ canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2
else return Stop
}
}
-
lookupFunEq :: PredType -> CtFlavor -> TypeMap Ct -> Maybe (TcType, TcCoercion)
lookupFunEq pty fl fam_eqs = lookup_funeq pty fam_eqs
where lookup_funeq pty fam_eqs
@@ -1303,17 +1432,33 @@ lookupFunEq pty fl fam_eqs = lookup_funeq pty fam_eqs
= Just (cc_rhs ct, mkTcCoVarCo (cc_id ct))
| otherwise
= Nothing
+-}
canEqLeafFunEqLeft :: SubGoalDepth -- Depth
- -> CtFlavor -> EqVar -> (TyCon,[Xi])
+ -> CtFlavor
+ -> (TyCon,[Xi])
-> TcType -> TcS StopOrContinue
-- Precondition: No more flattening is needed for the LHS
-canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
+canEqLeafFunEqLeft d fl (fn,xis1) s2
= {-# SCC "canEqLeafFunEqLeft" #-}
do { traceTcS "canEqLeafFunEqLeft" $ pprEq (mkTyConApp fn xis1) s2
; (xi2,co2) <-
{-# SCC "flatten" #-}
flatten d fl s2 -- co2 :: xi2 ~ s2
+
+ ; let fam_head = mkTyConApp fn xis1
+ -- Fancy coercion between equalities! But it should just work!
+ ; let co = mkTcTyConAppCo eqTyCon $ [mkTcReflCo (typeKind s2), mkTcReflCo fam_head, co2]
+ -- co :: (F xis1 ~ xi2) ~ (F xis1 ~ s2)
+ -- new pred old pred
+ ; mb <- rewriteCtFlavor fl (mkTcEqPred fam_head xi2) co
+ ; case mb of
+ Nothing -> return Stop
+ Just new_fl -> continueWith $
+ CFunEqCan { cc_flavor = new_fl, cc_depth = d
+ , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } }
+
+{- DELETEME
; let no_flattening_happened = isTcReflCo co2
; if no_flattening_happened then
continueWith $ CFunEqCan { cc_id = eqv
@@ -1322,6 +1467,7 @@ canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
, cc_tyargs = xis1
, cc_rhs = xi2
, cc_depth = d }
+ **** DV: Here
else do { delCachedEvVar eqv fl
; evc <-
{-# SCC "newEqVar" #-}
@@ -1342,14 +1488,33 @@ canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
, cc_rhs = xi2
, cc_depth = d } }
else return Stop } }
+-}
canEqLeafTyVarLeftRec :: SubGoalDepth
- -> CtFlavor -> EqVar
+ -> CtFlavor
-> TcTyVar -> TcType -> TcS StopOrContinue
-canEqLeafTyVarLeftRec d fl eqv tv s2 -- eqv :: tv ~ s2
+canEqLeafTyVarLeftRec d fl tv s2 -- fl :: tv ~ s2
= do { traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2
- ; (xi1,co1) <- flattenTyVar d fl tv -- co1 :: xi1 ~ tv
+ ; (xi1,co1) <- flattenTyVar d fl tv -- co1 :: xi1 ~ tv
+
+ ; traceTcS "canEqLeafTyVarLeftRec2" $ empty
+
+ ; let co = mkTcTyConAppCo eqTyCon $
+ [mkTcReflCo (typeKind s2), co1, mkTcReflCo s2]
+ -- co :: (xi1 ~ s2) ~ (tv ~ s2)
+ ; mb <- rewriteCtFlavor fl (mkTcEqPred xi1 s2) co
+
+ ; traceTcS "canEqLeafTyVarLeftRec3" $ empty
+
+ ; case mb of
+ Nothing -> return Stop
+ Just new_fl ->
+ case getTyVar_maybe xi1 of
+ Just tv' -> canEqLeafTyVarLeft d new_fl tv' s2
+ Nothing -> canEq d new_fl xi1 s2 }
+
+ {- DELETEME
; case isTcReflCo co1 of
True -> case getTyVar_maybe xi1 of
Just tv' -> canEqLeafTyVarLeft d fl eqv tv' s2
@@ -1371,21 +1536,60 @@ canEqLeafTyVarLeftRec d fl eqv tv s2 -- eqv :: tv ~ s2
else return Stop
}
}
+-}
+
canEqLeafTyVarLeft :: SubGoalDepth -- Depth
- -> CtFlavor -> EqVar
+ -> CtFlavor
-> TcTyVar -> TcType -> TcS StopOrContinue
-- Precondition LHS is fully rewritten from inerts (but not RHS)
-canEqLeafTyVarLeft d fl eqv tv s2 -- eqv : tv ~ s2
- = do { traceTcS "canEqLeafTyVarLeft" (pprEq (mkTyVarTy tv) s2)
- ; (xi2, co) <- flatten d fl s2 -- Flatten RHS co : xi2 ~ s2
-
- ; let no_flattening_happened = isTcReflCo co
-
+canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
+ = do { let tv_ty = mkTyVarTy tv
+ ; traceTcS "canEqLeafTyVarLeft" (pprEq tv_ty s2)
+ ; (xi2, co2) <- flatten d fl s2 -- Flatten RHS co : xi2 ~ s2
+
; traceTcS "canEqLeafTyVarLeft" (nest 2 (vcat [ text "tv =" <+> ppr tv
, text "s2 =" <+> ppr s2
, text "xi2 =" <+> ppr xi2]))
+ -- Reflexivity exposed through flattening
+ ; if tv_ty `eqType` xi2 then
+ when (isWanted fl) (setEvBind (flav_evar fl) (EvCoercion co2)) >>
+ return Stop
+ else do
+ -- Not reflexivity but maybe an occurs error
+ { occ_check_result <- canOccursCheck fl tv xi2
+ ; let xi2' = fromMaybe xi2 occ_check_result
+
+ not_occ_err = isJust occ_check_result
+ -- Delicate: don't want to cache as solved a constraint with occurs error!
+ co = mkTcTyConAppCo eqTyCon $
+ [mkTcReflCo (typeKind s2), mkTcReflCo tv_ty, co2]
+ ; mb <- rewriteCtFlavor_cache not_occ_err fl (mkTcEqPred tv_ty xi2') co
+ ; case mb of
+ Just new_fl -> if not_occ_err then
+ continueWith $
+ CTyEqCan { cc_flavor = new_fl, cc_depth = d
+ , cc_tyvar = tv, cc_rhs = xi2' }
+ else
+ canEqFailure d new_fl
+ Nothing -> return Stop
+ } }
+
+
+{- DELETEME
+
+ when (isWanted fl) $ setEvBind (ctFlavId fl) co2
+ else
+
+ -- eq_co :: (tv ~ xi2) ~ (tv ~ s2)
+ ; mb <- rewriteCtFlavor (CNonCanonical d fl) (mkTcEqPred (mkTyVarTy tv) xi2) eq_co
+ ********** HERE
+
+ ; let no_flattening_happened = isTcReflCo co
+
+
+
-- Flattening the RHS may reveal an identity coercion, which should
-- not be reported as occurs check error!
; let is_same_tv
@@ -1441,7 +1645,7 @@ canEqLeafTyVarLeft d fl eqv tv s2 -- eqv : tv ~ s2
, cc_depth = d }
else
return Stop } } }
-
+-}
-- See Note [Type synonyms and canonicalization].
-- Check whether the given variable occurs in the given type. We may
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index d2ea57ac24..e8dc9bcdff 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -159,10 +159,11 @@ reportTidyWanteds ctxt insols flats implics
deferToRuntime :: EvBindsVar -> ReportErrCtxt -> (ReportErrCtxt -> Ct -> TcM ErrMsg)
-> Ct -> TcM ()
deferToRuntime ev_binds_var ctxt mk_err_msg ct
- | Wanted loc <- cc_flavor ct
+ | fl <- cc_flavor ct
+ , Wanted loc _ <- fl
= do { err <- setCtLoc loc $
mk_err_msg ctxt ct
- ; let ev_id = cc_id ct
+ ; let ev_id = ctId "deferToRuntime" ct -- Prec satisfied: Wanted
err_msg = pprLocErrMsg err
err_fs = mkFastString $ showSDoc $
err_msg $$ text "(deferred type error)"
@@ -323,8 +324,8 @@ groupErrs mk_err (ct1 : rest)
same_group :: CtFlavor -> CtFlavor -> Bool
same_group (Given l1 _) (Given l2 _) = same_loc l1 l2
- same_group (Derived l1) (Derived l2) = same_loc l1 l2
- same_group (Wanted l1) (Wanted l2) = same_loc l1 l2
+ same_group (Derived l1 _) (Derived l2 _) = same_loc l1 l2
+ same_group (Wanted l1 _) (Wanted l2 _) = same_loc l1 l2
same_group _ _ = False
same_loc :: CtLoc o -> CtLoc o -> Bool
@@ -345,7 +346,7 @@ pprWithArising []
pprWithArising (ct:cts)
| null cts
= (loc, addArising (ctLocOrigin (ctWantedLoc ct))
- (pprEvVarTheta [cc_id ct]))
+ (pprTheta [ctPred ct]))
| otherwise
= (loc, vcat (map ppr_one (ct:cts)))
where
@@ -425,22 +426,23 @@ mkEqErr _ [] = panic "mkEqErr"
mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
-- Wanted constraints only!
mkEqErr1 ctxt ct
- = case cc_flavor ct of
- Given gl gk -> mkEqErr_help ctxt2 ct False ty1 ty2
- where
- ctxt2 = ctxt { cec_extra = cec_extra ctxt $$
- inaccessible_msg gl gk }
-
- flav -> do { let orig = ctLocOrigin (getWantedLoc flav)
- ; (ctxt1, orig') <- zonkTidyOrigin ctxt orig
- ; mk_err ctxt1 orig' }
+ = if isGivenOrSolved flav then
+ let ctx2 = ctxt { cec_extra = cec_extra ctxt $$ inaccessible_msg flav }
+ in mkEqErr_help ctx2 ct False ty1 ty2
+ else
+ do { let orig = ctLocOrigin (getWantedLoc flav)
+ ; (ctxt1, orig') <- zonkTidyOrigin ctxt orig
+ ; mk_err ctxt1 orig' }
where
- -- If a GivenSolved then we should not report inaccessible code
- inaccessible_msg loc GivenOrig = hang (ptext (sLit "Inaccessible code in"))
+
+ flav = cc_flavor ct
+
+ inaccessible_msg (Given loc _) = hang (ptext (sLit "Inaccessible code in"))
2 (ppr (ctLocOrigin loc))
- inaccessible_msg _ _ = empty
+ -- If a Solved then we should not report inaccessible code
+ inaccessible_msg _ = empty
- (ty1, ty2) = getEqPredTys (evVarPred (cc_id ct))
+ (ty1, ty2) = getEqPredTys (ctPred ct)
-- If the types in the error message are the same as the types
-- we are unifying, don't add the extra expected/actual message
@@ -1071,6 +1073,19 @@ solverDepthErrorTcS depth stack
= failWith msg
| otherwise
= setCtFlavorLoc (cc_flavor top_item) $
+ do { zstack <- mapM zonkCt stack
+ ; env0 <- tcInitTidyEnv
+ ; let zstack_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet zstack
+ tidy_env = tidyFreeTyVars env0 zstack_tvs
+ tidy_cts = map (tidyCt tidy_env) zstack
+ ; failWithTcM (tidy_env, hang msg 2 (vcat (map (ppr . ctPred) tidy_cts))) }
+ where
+ top_item = head stack
+ msg = vcat [ ptext (sLit "Context reduction stack overflow; size =") <+> int depth
+ , ptext (sLit "Use -fcontext-stack=N to increase stack size to N") ]
+
+{- DV: Changing this because Derived's no longer have ids ... Kind of a corner case ...
+ = setCtFlavorLoc (cc_flavor top_item) $
do { ev_vars <- mapM (zonkEvVar . cc_id) stack
; env0 <- tcInitTidyEnv
; let tidy_env = tidyFreeTyVars env0 (tyVarsOfEvVars ev_vars)
@@ -1080,6 +1095,8 @@ solverDepthErrorTcS depth stack
top_item = head stack
msg = vcat [ ptext (sLit "Context reduction stack overflow; size =") <+> int depth
, ptext (sLit "Use -fcontext-stack=N to increase stack size to N") ]
+-}
+
flattenForAllErrorTcS :: CtFlavor -> TcType -> TcM a
flattenForAllErrorTcS fl ty
@@ -1099,9 +1116,10 @@ flattenForAllErrorTcS fl ty
\begin{code}
setCtFlavorLoc :: CtFlavor -> TcM a -> TcM a
-setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing
-setCtFlavorLoc (Derived loc) thing = setCtLoc loc thing
-setCtFlavorLoc (Given loc _gk) thing = setCtLoc loc thing
+setCtFlavorLoc (Wanted loc _) thing = setCtLoc loc thing
+setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing
+setCtFlavorLoc (Given loc _) thing = setCtLoc loc thing
+setCtFlavorLoc (Solved loc _) thing = setCtLoc loc thing
\end{code}
%************************************************************************
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 5932934bb3..1c6760d18f 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -32,6 +32,7 @@ import TyCon
import Name
import IParam
+import TysWiredIn ( eqTyCon )
import FunDeps
import TcEvidence
@@ -90,6 +91,10 @@ depth and will simply fail.
solveInteractCts :: [Ct] -> TcS ()
solveInteractCts cts
+ = do { traceTcS "solveInteractCtS" (vcat [ text "cts =" <+> ppr cts ])
+ ; updWorkListTcS (appendWorkListCt cts) >> solveInteract }
+
+{- DELETEME
= do { evvar_cache <- getTcSEvVarCacheMap
; (cts_thinner, new_evvar_cache) <- add_cts_in_cache evvar_cache cts
; traceTcS "solveInteractCts" (vcat [ text "cts_original =" <+> ppr cts,
@@ -136,12 +141,12 @@ solveInteractCts cts
-- If we are simplifying equalities only,
-- do not cache non-equalities
-- See Note [Simplifying RULE lhs constraints] in TcSimplify
+-}
solveInteractGiven :: GivenLoc -> [EvVar] -> TcS ()
solveInteractGiven gloc evs
= solveInteractCts (map mk_noncan evs)
- where mk_noncan ev = CNonCanonical { cc_id = ev
- , cc_flavor = Given gloc GivenOrig
+ where mk_noncan ev = CNonCanonical { cc_flavor = Given gloc ev
, cc_depth = 0 }
-- The main solver loop implements Note [Basic Simplifier Plan]
@@ -259,6 +264,7 @@ thePipeline = [ ("canonicalization", canonicalizationStage)
\begin{code}
+
-- The canonicalization stage, see TcCanonical for details
----------------------------------------------------------
canonicalizationStage :: SimplifierStage
@@ -326,61 +332,95 @@ kickOutRewritableInerts :: Ct -> TcS ()
-- The rewritable end up in the worklist
kickOutRewritableInerts ct
= {-# SCC "kickOutRewritableInerts" #-}
- do { (wl,ieqs) <- {-# SCC "kick_out_rewritable" #-}
+ do { traceTcS "kickOutRewritableInerts" $ text "workitem = " <+> ppr ct
+ ; (wl,ieqs) <- {-# SCC "kick_out_rewritable" #-}
modifyInertTcS (kick_out_rewritable ct)
+ ; traceTcS "Kicked out the following constraints" $ ppr wl
+ ; is <- getTcSInerts
+ ; traceTcS "Remaining inerts are" $ ppr is
- -- Step 1: Rewrite as many of the inert_eqs on the spot!
- -- NB: if it is a solved constraint just use the cached evidence
-
- ; let ct_coercion = getCtCoercion ct
+ -- Step 1: Rewrite as many of the inert_eqs on the spot!
+ -- NB: if it is a given constraint just use the cached evidence
+ -- to optimize e.g. mkRefl coercions from spontaneously solved cts.
+ ; bnds <- getTcEvBindsMap
+ ; let ct_coercion = getCtCoercion bnds ct
; new_ieqs <- {-# SCC "rewriteInertEqsFromInertEq" #-}
- rewriteInertEqsFromInertEq (cc_tyvar ct,ct_coercion, cc_flavor ct) ieqs
- ; modifyInertTcS (\is -> ((), is { inert_eqs = new_ieqs }))
-
- -- Step 2: Add the new guy in
+ rewriteInertEqsFromInertEq (cc_tyvar ct,
+ ct_coercion,cc_flavor ct) ieqs
+ ; let upd_eqs is = is { inert_cans = new_ics }
+ where ics = inert_cans is
+ new_ics = ics { inert_eqs = new_ieqs }
+ ; modifyInertTcS (\is -> ((), upd_eqs is))
+
+ ; is <- getTcSInerts
+ ; traceTcS "Final inerts are" $ ppr is
+
+ -- Step 2: Add the new guy in
; updInertSetTcS ct
; traceTcS "Kick out" (ppr ct $$ ppr wl)
; updWorkListTcS (unionWorkList wl) }
rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtFlavor) -- A new substitution
- -> TyVarEnv (Ct, TcCoercion) -- All inert equalities
- -> TcS (TyVarEnv (Ct,TcCoercion)) -- The new inert equalities
+ -> TyVarEnv Ct -- All the inert equalities
+ -> TcS (TyVarEnv Ct) -- The new inert equalities
rewriteInertEqsFromInertEq (subst_tv, subst_co, subst_fl) ieqs
-- The goal: traverse the inert equalities and rewrite some of them, dropping some others
-- back to the worklist. This is delicate, see Note [Delicate equality kick-out]
= do { mieqs <- Traversable.mapM do_one ieqs
; traceTcS "Original inert equalities:" (ppr ieqs)
; let flatten_justs elem venv
- | Just (act,aco) <- elem = extendVarEnv venv (cc_tyvar act) (act,aco)
+ | Just act <- elem = extendVarEnv venv (cc_tyvar act) act
| otherwise = venv
final_ieqs = foldVarEnv flatten_justs emptyVarEnv mieqs
; traceTcS "Remaining inert equalities:" (ppr final_ieqs)
; return final_ieqs }
- where do_one (ct,inert_co)
+ where do_one ct
| subst_fl `canRewrite` fl && (subst_tv `elemVarSet` tyVarsOfCt ct)
- -- Annoyingly inefficient, but we can't simply check
- -- that isReflCo co because of cached solved ReflCo evidence.
- = if fl `canRewrite` subst_fl then
+ -- Annoyingly inefficient, but we can't simply check
+ -- that isReflCo co because of cached solved ReflCo evidence.
+ = if fl `canRewrite` subst_fl then
-- If also the inert can rewrite the subst it's totally safe
-- to rewrite on the spot
- do { (ct',inert_co') <- rewrite_on_the_spot (ct,inert_co)
- ; return $ Just (ct',inert_co') }
+ do { ct' <- rewrite_on_the_spot ct
+ ; return $ Just ct' }
else -- We have to throw inert back to worklist for occurs checks
do { updWorkListTcS (extendWorkListEq ct)
; return Nothing }
| otherwise -- Just keep it there
- = return $ Just (ct,inert_co)
+ = return $ Just ct
where
- -- We have new guy co : tv ~ something
- -- and old inert {wanted} cv : tv' ~ rhs[tv]
- -- We want to rewrite to
- -- {wanted} cv' : tv' ~ rhs[something]
- -- cv = cv' ; rhs[Sym co]
- --
- rewrite_on_the_spot (ct,_inert_co)
+ -- We have that: subst_co :: subst_tv ~ tau
+ -- An an old inert: tv ~ rhs
+ -- That we want to rewrite on-the-spot to tv ~ rhs[tau/subst_tv]
+ fl = cc_flavor ct
+ tv = cc_tyvar ct
+ rhs = cc_rhs ct
+
+ rewrite_on_the_spot ct
+ = do { let rhs_co = liftTcCoSubstWith [subst_tv] [subst_co] rhs
+ eq_co = mkTcTyConAppCo eqTyCon $
+ [ mkTcReflCo (typeKind rhs)
+ , mkTcReflCo (mkTyVarTy tv)
+ , mkTcSymCo rhs_co ]
+ new_rhs = pSnd (tcCoercionKind rhs_co)
+ new_eq_pred = mkTcEqPred (mkTyVarTy tv) new_rhs
+ -- eq_co :: (tv ~ rhs[s/x]) ~ (tv ~ rhs[x])
+
+ ; mb_fl <- rewriteCtFlavor fl new_eq_pred eq_co
+ ; case mb_fl of
+ Just new_fl -> return $
+ ct {cc_flavor=new_fl,cc_rhs=new_rhs}
+ Nothing -> -- Weird, rewritten constraint was solved
+ -- before -- I am uncertain about what to do
+ pprPanic "Interesting: \
+ rewrote inert equality to existing!" $
+ vcat [ text "original ="<+>ppr ct
+ , text "new eqpred ="<+>ppr new_eq_pred ]
+ }
+{- DELETEME
= do { let rhs' = pSnd (tcCoercionKind co)
; delCachedEvVar ev fl
; evc <- newEqVar fl (mkTyVarTy tv) rhs'
@@ -401,43 +441,46 @@ rewriteInertEqsFromInertEq (subst_tv, subst_co, subst_fl) ieqs
; let ct' = ct { cc_id = ev', cc_flavor = fl', cc_rhs = rhs' }
; return (ct',evco') }
ev = cc_id ct
- fl = cc_flavor ct
- tv = cc_tyvar ct
- rhs = cc_rhs ct
- co = liftTcCoSubstWith [subst_tv] [subst_co] rhs
-
-kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,TcCoercion)), InertSet)
--- Returns ALL equalities, to be dealt with later
-kick_out_rewritable ct (IS { inert_eqs = eqmap
- , inert_eq_tvs = inscope
- , inert_dicts = dictmap
- , inert_ips = ipmap
- , inert_funeqs = funeqmap
- , inert_irreds = irreds
- , inert_frozen = frozen
- } )
- = ((kicked_out, eqmap), remaining)
+-}
+
+kick_out_rewritable :: Ct
+ -> InertSet
+ -> ((WorkList, TyVarEnv Ct),InertSet)
+-- Post: returns ALL inert equalities, to be dealt with later
+--
+kick_out_rewritable ct is@(IS { inert_cans =
+ IC { inert_eqs = eqmap
+ , inert_eq_tvs = inscope
+ , inert_dicts = dictmap
+ , inert_ips = ipmap
+ , inert_funeqs = funeqmap
+ , inert_irreds = irreds }
+ , inert_frozen = frozen })
+ = ((kicked_out,eqmap), remaining)
where
kicked_out = WorkList { wl_eqs = []
, wl_funeqs = bagToList feqs_out
, wl_rest = bagToList (fro_out `andCts` dicts_out
`andCts` ips_out `andCts` irs_out) }
- remaining = IS { inert_eqs = emptyVarEnv
- , inert_eq_tvs = inscope -- keep the same, safe and cheap
- , inert_dicts = dicts_in
- , inert_ips = ips_in
- , inert_funeqs = feqs_in
- , inert_irreds = irs_in
- , inert_frozen = fro_in
- }
-
+ remaining = is { inert_cans = IC { inert_eqs = emptyVarEnv
+ , inert_eq_tvs = inscope
+ -- keep the same, safe and cheap
+ , inert_dicts = dicts_in
+ , inert_ips = ips_in
+ , inert_funeqs = feqs_in
+ , inert_irreds = irs_in }
+ , inert_frozen = fro_in }
+ -- NB: Notice that don't rewrite
+ -- inert_solved, inert_flat_cache and inert_solved_funeqs
+ -- optimistically. But when we lookup we have to take the
+ -- subsitution into account
fl = cc_flavor ct
tv = cc_tyvar ct
(ips_out, ips_in) = partitionCCanMap rewritable ipmap
- (feqs_out, feqs_in) = partitionCtTypeMap rewritable funeqmap
+ (feqs_out, feqs_in) = partCtFamHeadMap rewritable funeqmap
(dicts_out, dicts_in) = partitionCCanMap rewritable dictmap
(irs_out, irs_in) = partitionBag rewritable irreds
@@ -493,7 +536,7 @@ data SPSolveResult = SPCantSolve
-- touchable unification variable.
-- See Note [Touchables and givens]
trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
-trySpontaneousSolve workItem@(CTyEqCan { cc_id = eqv, cc_flavor = gw
+trySpontaneousSolve workItem@(CTyEqCan { cc_flavor = gw
, cc_tyvar = tv1, cc_rhs = xi, cc_depth = d })
| isGivenOrSolved gw
= return SPCantSolve
@@ -501,13 +544,13 @@ trySpontaneousSolve workItem@(CTyEqCan { cc_id = eqv, cc_flavor = gw
= do { tch1 <- isTouchableMetaTyVar tv1
; tch2 <- isTouchableMetaTyVar tv2
; case (tch1, tch2) of
- (True, True) -> trySpontaneousEqTwoWay d eqv gw tv1 tv2
- (True, False) -> trySpontaneousEqOneWay d eqv gw tv1 xi
- (False, True) -> trySpontaneousEqOneWay d eqv gw tv2 (mkTyVarTy tv1)
+ (True, True) -> trySpontaneousEqTwoWay d gw tv1 tv2
+ (True, False) -> trySpontaneousEqOneWay d gw tv1 xi
+ (False, True) -> trySpontaneousEqOneWay d gw tv2 (mkTyVarTy tv1)
_ -> return SPCantSolve }
| otherwise
= do { tch1 <- isTouchableMetaTyVar tv1
- ; if tch1 then trySpontaneousEqOneWay d eqv gw tv1 xi
+ ; if tch1 then trySpontaneousEqOneWay d gw tv1 xi
else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" $
ppr workItem
; return SPCantSolve }
@@ -520,24 +563,24 @@ trySpontaneousSolve _ = return SPCantSolve
----------------
trySpontaneousEqOneWay :: SubGoalDepth
- -> EqVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
+ -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
-- tv is a MetaTyVar, not untouchable
-trySpontaneousEqOneWay d eqv gw tv xi
+trySpontaneousEqOneWay d gw tv xi
| not (isSigTyVar tv) || isTyVarTy xi
- = solveWithIdentity d eqv gw tv xi
+ = solveWithIdentity d gw tv xi
| otherwise -- Still can't solve, sig tyvar and non-variable rhs
= return SPCantSolve
----------------
trySpontaneousEqTwoWay :: SubGoalDepth
- -> EqVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
+ -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
-trySpontaneousEqTwoWay d eqv gw tv1 tv2
+trySpontaneousEqTwoWay d gw tv1 tv2
= do { let k1_sub_k2 = k1 `tcIsSubKind` k2
; if k1_sub_k2 && nicer_to_update_tv2
- then solveWithIdentity d eqv gw tv2 (mkTyVarTy tv1)
- else solveWithIdentity d eqv gw tv1 (mkTyVarTy tv2) }
+ then solveWithIdentity d gw tv2 (mkTyVarTy tv1)
+ else solveWithIdentity d gw tv1 (mkTyVarTy tv2) }
where
k1 = tyVarKind tv1
k2 = tyVarKind tv2
@@ -617,7 +660,7 @@ unification variables as RHS of type family equations: F xis ~ alpha.
----------------
solveWithIdentity :: SubGoalDepth
- -> EqVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
+ -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
-- Solve with the identity coercion
-- Precondition: kind(xi) is a sub-kind of kind(tv)
-- Precondition: CtFlavor is Wanted or Derived
@@ -625,13 +668,13 @@ solveWithIdentity :: SubGoalDepth
-- must work for Derived as well as Wanted
-- Returns: workItem where
-- workItem = the new Given constraint
-solveWithIdentity d eqv wd tv xi
- = do { traceTcS "Sneaky unification:" $
- vcat [text "Coercion variable: " <+> ppr eqv <+> ppr wd,
- text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
- text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
- text "Right Kind is : " <+> ppr (typeKind xi)
- ]
+solveWithIdentity d wd tv xi
+ = do { let tv_ty = mkTyVarTy tv
+ ; traceTcS "Sneaky unification:" $
+ vcat [text "Constraint:" <+> ppr wd,
+ text "Coercion:" <+> pprEq tv_ty xi,
+ text "Left Kind is:" <+> ppr (typeKind tv_ty),
+ text "Right Kind is:" <+> ppr (typeKind xi) ]
; let xi' = defaultKind xi
-- We only instantiate kind unification variables
@@ -641,14 +684,16 @@ solveWithIdentity d eqv wd tv xi
; setWantedTyBind tv xi'
; let refl_xi = mkTcReflCo xi'
- ; let solved_fl = mkSolvedFlavor wd UnkSkol (EvCoercion refl_xi)
- ; (_,eqv_given) <- newGivenEqVar solved_fl (mkTyVarTy tv) xi' refl_xi
+ ; when (isWanted wd) $
+ setEvBind (flav_evar wd) (EvCoercion refl_xi)
- ; when (isWanted wd) $ do { _ <- setEqBind eqv refl_xi wd; return () }
- -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
- ; return $ SPSolved (CTyEqCan { cc_id = eqv_given
- , cc_flavor = solved_fl
- , cc_tyvar = tv, cc_rhs = xi', cc_depth = d }) }
+ ; ev_given <- newGivenEvVar (mkTcEqPred tv_ty xi')
+ (EvCoercion refl_xi) >>= (return . mn_thing)
+ ; let given_fl = Given (mkGivenLoc (flav_wloc wd) UnkSkol) ev_given
+
+ ; return $
+ SPSolved (CTyEqCan { cc_flavor = given_fl
+ , cc_tyvar = tv, cc_rhs = xi', cc_depth = d }) }
\end{code}
@@ -711,8 +756,10 @@ interactWithInertsStage wi
; if simplEqsOnly ctxt then
return (ContinueWith wi)
else
- extractRelevantInerts wi >>=
- foldlBagM interact_next (ContinueWith wi) }
+ do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
+ ; rels <- extractRelevantInerts wi
+ ; traceTcS "relevant inerts are:" $ ppr rels
+ ; foldlBagM interact_next (ContinueWith wi) rels } }
where interact_next Stop atomic_inert
= updInertSetTcS atomic_inert >> return Stop
@@ -740,13 +787,12 @@ interactWithInertsStage wi
}
--------------------------------------------
-data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
doInteractWithInert :: Ct -> Ct -> TcS InteractResult
-- Identical class constraints.
doInteractWithInert
- inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
- workItem@(CDictCan { cc_id = _d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
+ inertItem@(CDictCan { cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
+ workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
| cls1 == cls2
= do { let pty1 = mkClassPred cls1 tys1
@@ -771,7 +817,7 @@ doInteractWithInert
; case any_fundeps of
-- No Functional Dependencies
Nothing
- | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
+ | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" fl1 workItem
| otherwise -> irKeepGoing "NOP"
-- Actual Functional Dependencies
@@ -781,27 +827,27 @@ doInteractWithInert
-> do { emitFDWorkAsDerived fd_work (cc_depth workItem)
; irKeepGoing "Cls/Cls (new fundeps)" } -- Just keep going without droping the inert
}
- where get_workitem_wloc (Wanted wl) = return wl
- get_workitem_wloc (Derived wl) = return wl
- get_workitem_wloc (Given {}) = pprPanic "Unexpected given workitem!" $
- vcat [ text "Work item =" <+> ppr workItem
- , 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)
-doInteractWithInert (CIrredEvCan { cc_id = id1, cc_flavor = ifl, cc_ty = ty1 })
+ where get_workitem_wloc (Wanted wl _) = return wl
+ get_workitem_wloc (Derived wl _) = return wl
+ get_workitem_wloc _ = pprPanic "Unexpected given workitem!" $
+ vcat [ text "Work item =" <+> ppr workItem
+ , 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)
+doInteractWithInert (CIrredEvCan { cc_flavor = ifl, cc_ty = ty1 })
workItem@(CIrredEvCan { cc_ty = ty2 })
| ty1 `eqType` ty2
- = solveOneFromTheOther "Irred/Irred" (EvId id1,ifl) workItem
+ = solveOneFromTheOther "Irred/Irred" ifl workItem
-- Two implicit parameter constraints. If the names are the same,
-- but their types are not, we generate a wanted type equality
-- that equates the type (this is "improvement").
-- However, we don't actually need the coercion evidence,
-- so we just generate a fresh coercion variable that isn't used anywhere.
-doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
+doInteractWithInert (CIPCan { cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
| nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
= -- See Note [Overriding implicit parameters]
@@ -812,11 +858,56 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i
irInertConsumed "IP/IP (override inert)"
| nm1 == nm2 && ty1 `eqType` ty2
- = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem
+ = solveOneFromTheOther "IP/IP" ifl workItem
| nm1 == nm2
= -- See Note [When improvement happens]
- do { let flav = Wanted (combineCtLoc ifl wfl)
+ do { mb_eqv <- newWantedEvVar (mkEqPred ty2 ty1)
+ -- co :: ty2 ~ ty1, see Note [Efficient orientation]
+ ; cv <- case mb_eqv of
+ Fresh eqv ->
+ do { updWorkListTcS $ extendWorkListEq $
+ CNonCanonical { cc_flavor = Wanted new_wloc eqv
+ , cc_depth = cc_depth workItem }
+ ; return eqv }
+ Cached eqv -> return eqv
+ ; case wfl of
+ Wanted {} ->
+ let ip_co = mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo cv]
+ in do { setEvBind (ctId "doInteractWithInert" workItem) $
+ mkEvCast (flav_evar ifl) (mkTcSymCo ip_co)
+ ; irWorkItemConsumed "IP/IP (solved by rewriting)" }
+ _ -> pprPanic "Unexpected IP constraint" (ppr workItem) }
+ where new_wloc
+ | Wanted wl _ <- wfl = wl
+ | Derived wl _ <- wfl = wl
+ | Wanted wl _ <- ifl = wl
+ | Derived wl _ <- ifl = wl
+ | otherwise = panic "Solve IP: no WantedLoc!"
+
+ {-- DELETEME
+ ; when (isWanted wfl) $
+ do { setEvBind (flav_evar wfl) (mkEvCast (flav_evar ifl)
+
+
+ ; mb_new_fl <- rewriteCtFlavor wfl
+ (mkTyConApp (ipTyCon nm1) [ty1]) -- IP x ty1
+ (mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo cv])
+ -- IP x ty1 ~ IP x ty2
+ ; case mb_new_fl of
+ Nothing -> pprPanic "Unexpected cached IP constraint!" empty
+ Just new_fl -> irWorkItemConsumed "IP/IP (solved by rewriting)" }
+ where new_wloc
+ | Wanted wl _ <- wfl = wl
+ | Derived wl _ <- wfl = wl
+ | Wanted wl _ <- ifl = wl
+ | Derived wl _ <- ifl = wl
+ | otherwise = panic "Solve IP: no WantedLoc!"
+
+ eqv <- newWantedEvVar (mkEqPred ty2 ty1)
+ -- See Note [Efficient Orientation]
+ ;
+ let flav = Wanted (combineCtLoc ifl wfl)
; eqv <- newEqVar flav ty2 ty1 -- See Note [Efficient Orientation]
; when (isNewEvVar eqv) $
(let ct = CNonCanonical { cc_id = evc_the_evvar eqv
@@ -831,35 +922,50 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i
do { _ <- setEvBind (cc_id workItem)
(mkEvCast id1 (mkTcSymCo (mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo (evc_the_evvar eqv)]))) wfl
; irWorkItemConsumed "IP/IP (solved by rewriting)" } }
+-}
+
-doInteractWithInert (CFunEqCan { cc_id = eqv1, cc_flavor = fl1, cc_fun = tc1
- , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 })
- (CFunEqCan { cc_id = eqv2, cc_flavor = fl2, cc_fun = tc2
- , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
+doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1
+ , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 })
+ wi@(CFunEqCan { cc_flavor = fl2, cc_fun = tc2
+ , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
| lhss_match
- , Just (GivenSolved {}) <- isGiven_maybe fl1 -- Inert is solved and we can simply ignore it
- -- when workitem is given/solved
+ , isSolved fl1 -- Inert is solved and we can simply ignore it
+ -- when workitem is given/solved
, isGivenOrSolved fl2
= irInertConsumed "FunEq/FunEq"
- | lhss_match
- , Just (GivenSolved {}) <- isGiven_maybe fl2 -- Workitem is solved and we can ignore it when
- -- the inert is given/solved
+ | lhss_match
+ , isSolved fl2 -- Workitem is solved and we can ignore it when
+ -- the inert is given/solved
, isGivenOrSolved fl1
= irWorkItemConsumed "FunEq/FunEq"
| fl1 `canSolve` fl2 && lhss_match
- = do { rewriteEqLHS LeftComesFromInert (eqv1,xi1) (eqv2,d2,fl2,xi2)
+ = do { traceTcS "interact with inerts: FunEq/FunEq" $
+ vcat [ text "workitem =" <+> ppr wi
+ , text "inertitem=" <+> ppr ii ]
+
+ ; xCtFlavor fl2 [mkTcEqPred xi2 xi1] (xev co1) $ what_next d2
; irWorkItemConsumed "FunEq/FunEq" }
-
| fl2 `canSolve` fl1 && lhss_match
- = do { rewriteEqLHS RightComesFromInert (eqv2,xi2) (eqv1,d1,fl1,xi1)
+ = do { xCtFlavor fl1 [mkTcEqPred xi1 xi2] (xev co2) $ what_next d1
; irInertConsumed "FunEq/FunEq"}
where
lhss_match = tc1 == tc2 && eqTypes args1 args2
-
-
+ what_next d [new_fl]
+ = updWorkListTcS $
+ extendWorkListEq (CNonCanonical {cc_flavor=new_fl,cc_depth = d})
+ what_next _ _ = return ()
+ co1 = mkTcCoVarCo $ flav_evar fl1
+ co2 = mkTcCoVarCo $ flav_evar fl2
+ mk_sym_co x = mkTcSymCo (mkTcCoVarCo x)
+ xev co = XEvTerm xcomp xdecomp
+ where xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co)]
+ xcomp [x] = EvCoercion (co `mkTcTransCo` mk_sym_co x)
+ xcomp _ = panic "No more goals!"
+
doInteractWithInert _ _ = irKeepGoing "NOP"
-
+{- DELETE
rewriteEqLHS :: WhichComesFromInert -> (EqVar,Xi) -> (EqVar,SubGoalDepth,CtFlavor,Xi) -> TcS ()
-- Used to ineract two equalities of the following form:
-- First Equality: co1: (XXX ~ xi1)
@@ -904,14 +1010,17 @@ rewriteEqLHS RightComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2)
, cc_flavor = gw'
, cc_depth = d } ) ) }
-solveOneFromTheOther :: String -- Info
- -> (EvTerm, CtFlavor) -- Inert
+-}
+
+
+solveOneFromTheOther :: String -- Info
+ -> CtFlavor -- Inert
-> Ct -- WorkItem
-> TcS InteractResult
-- Preconditions:
-- 1) inert and work item represent evidence for the /same/ predicate
-- 2) ip/class/irred evidence (no coercions) only
-solveOneFromTheOther info (ev_term,ifl) workItem
+solveOneFromTheOther info ifl workItem
| isDerived wfl
= irWorkItemConsumed ("Solved[DW] " ++ info)
@@ -920,20 +1029,21 @@ solveOneFromTheOther info (ev_term,ifl) workItem
-- so it's safe to continue on from this point
= irInertConsumed ("Solved[DI] " ++ info)
- | Just (GivenSolved {}) <- isGiven_maybe ifl, isGivenOrSolved wfl
+ | isSolved ifl, isGivenOrSolved wfl
-- Same if the inert is a GivenSolved -- just get rid of it
= irInertConsumed ("Solved[SI] " ++ info)
| otherwise
= ASSERT( ifl `canSolve` wfl )
-- Because of Note [The Solver Invariant], plus Derived dealt with
- do { when (isWanted wfl) $ do { _ <- setEvBind wid ev_term wfl; return () }
+ do { when (isWanted wfl) $ setEvBind wid (EvId iid)
-- Overwrite the binding, if one exists
-- If both are Given, we already have evidence; no need to duplicate
; irWorkItemConsumed ("Solved " ++ info) }
where
wfl = cc_flavor workItem
- wid = cc_id workItem
+ wid = ctId "solveOneFromtheOther" workItem
+ iid = flav_evar ifl
\end{code}
@@ -1331,7 +1441,18 @@ instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
= 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
+ else do { mb_eqv <- newWantedEvVar (mkTcEqPred sty1 sty2)
+ ; case mb_eqv of
+ Fresh eqv -> return $ (i,(eqv, push_ctx wl)):ievs
+ Cached {} -> return ievs }
+ -- 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!
+ push_ctx :: WantedLoc -> WantedLoc
+ push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
+
+{- DELETEME
+ 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
@@ -1339,9 +1460,8 @@ instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
-- 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)
@@ -1378,9 +1498,9 @@ emitFDWorkAsDerived :: [(EvVar,WantedLoc)]
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 }
+ mk_fd_ct (v,wl)
+ = CNonCanonical { cc_flavor = Derived wl (evVarPred v)
+ , cc_depth = d }
\end{code}
@@ -1407,7 +1527,7 @@ tryTopReact wi
; ctxt <- getTcSContext
; if simplEqsOnly ctxt then return (ContinueWith wi) -- or Stop?
else
- do { tir <- doTopReact inerts wi
+ do { tir <- doTopReact inerts wi
; case tir of
NoTopInt
-> return (ContinueWith wi)
@@ -1438,7 +1558,7 @@ doTopReact _inerts (CDictCan { cc_flavor = Given {} })
= return NoTopInt -- NB: Superclasses already added since it's canonical
-- Derived dictionary: just look for functional dependencies
-doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc
+doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc _pty
, cc_class = cls, cc_tyargs = xis })
= do { instEnvs <- getInstEnvs
; let fd_eqns = improveFromInstEnv instEnvs
@@ -1448,7 +1568,7 @@ doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc
Nothing -> return NoTopInt
Just (xis',_,fd_work) ->
let workItem' = workItem { cc_tyargs = xis' }
- -- Deriveds are not supposed to have identity (cc_id is unused!)
+ -- Deriveds are not supposed to have identity
in do { emitFDWorkAsDerived fd_work (cc_depth workItem)
; return $
SomeTopInt { tir_rule = "Derived Cls fundeps"
@@ -1456,8 +1576,7 @@ doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc
}
-- Wanted dictionary
-doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
- , cc_id = dict_id
+doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc dict_id)
, cc_class = cls, cc_tyargs = xis
, cc_depth = depth })
-- See Note [MATCHING-SYNONYMS]
@@ -1473,7 +1592,9 @@ doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
do { lkup_inst_res <- matchClassInst inerts cls xis loc
; case lkup_inst_res of
GenInst wtvs ev_term
- -> doSolveFromInstance wtvs ev_term
+ -> let sfl = Solved (mkSolvedLoc loc UnkSkol) dict_id
+ in addToSolved (workItem { cc_flavor = sfl }) >>
+ doSolveFromInstance wtvs ev_term
NoInstance
-> return NoTopInt
}
@@ -1484,47 +1605,131 @@ doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
, tir_new_item = ContinueWith workItem } } }
where doSolveFromInstance :: [EvVar] -> EvTerm -> TcS TopInteractResult
- -- Precondition: evidence term matches the predicate of cc_id of workItem
+ -- Precondition: evidence term matches the predicate workItem
doSolveFromInstance evs ev_term
| null evs
- = do { traceTcS "doTopReact/found nullary instance for" (ppr dict_id)
- ; _ <- setEvBind dict_id ev_term fl
+ = do { traceTcS "doTopReact/found nullary instance for" $
+ ppr dict_id
+ ; setEvBind dict_id ev_term
; return $
SomeTopInt { tir_rule = "Dict/Top (solved, no new work)"
- , tir_new_item = Stop } } -- Don't put him in the inerts
+ , tir_new_item = Stop } }
| otherwise
- = do { traceTcS "doTopReact/found non-nullary instance for" (ppr dict_id)
- ; _ <- setEvBind dict_id ev_term fl
- -- Solved and new wanted work produced, you may cache the
- -- (tentatively solved) dictionary as Solved given.
--- ; let _solved = workItem { cc_flavor = solved_fl }
--- solved_fl = mkSolvedFlavor fl UnkSkol
+ = do { traceTcS "doTopReact/found non-nullary instance for" $
+ ppr dict_id
+ ; setEvBind dict_id ev_term
; let mk_new_wanted ev
- = CNonCanonical { cc_id = ev, cc_flavor = fl
+ = CNonCanonical { cc_flavor = fl { flav_evar = ev }
, cc_depth = depth + 1 }
; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs))
; return $
SomeTopInt { tir_rule = "Dict/Top (solved, more work)"
, tir_new_item = Stop }
}
--- , tir_new_item = ContinueWith solved } } -- Cache in inerts the Solved item
-- Type functions
doTopReact _inerts (CFunEqCan { cc_flavor = fl })
- | Just (GivenSolved {}) <- isGiven_maybe fl
+ | isSolved fl
= return NoTopInt -- If Solved, no more interactions should happen
-- Otherwise, it's a Given, Derived, or Wanted
-doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl
+doTopReact _inerts workItem@(CFunEqCan { cc_flavor = fl, cc_depth = d
, cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
- = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
+ = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
; case match_res of
Nothing -> return NoTopInt
Just (famInst, rep_tys)
- -> do { let coe_ax = famInstAxiom famInst
- rhs_ty = mkAxInstRHS coe_ax rep_tys
- coe = mkTcAxInstCo coe_ax rep_tys
+ -> do { mb_already_solved <- lkpFunEqCache (mkTyConApp tc args)
+ ; let (coe,rhs_ty)
+ | Just cached_ct <- mb_already_solved
+ = (mkTcCoVarCo (ctId "doTopReact" cached_ct),
+ cc_rhs cached_ct)
+ | otherwise
+ = let coe_ax = famInstAxiom famInst
+ in (mkTcAxInstCo coe_ax rep_tys,
+ mkAxInstRHS coe_ax rep_tys)
+
+ xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` mkTcCoVarCo x)]
+ xcomp [x] = EvCoercion (coe `mkTcTransCo` mkTcCoVarCo x)
+ xcomp _ = panic "No more goals!"
+
+ xev = XEvTerm xcomp xdecomp
+ ; xCtFlavor fl [mkTcEqPred rhs_ty xi] xev what_next } }
+ where what_next [ct_flav]
+ = do { updWorkListTcS $
+ extendWorkListEq (CNonCanonical { cc_flavor = ct_flav
+ , cc_depth = d+1 })
+ ; cache_in_solved fl
+ ; return $ SomeTopInt { tir_rule = "Fun/Top"
+ , tir_new_item = Stop } }
+ what_next _ -- No subgoal (because it's cached)
+ = do { cache_in_solved fl
+ ; return $ SomeTopInt { tir_rule = "Fun/Top"
+ , tir_new_item = Stop } }
+
+ cache_in_solved (Derived {}) = return ()
+ cache_in_solved (Wanted wl ev) =
+ let sfl = Solved (mkSolvedLoc wl UnkSkol) ev
+ solved = workItem { cc_flavor = sfl }
+ in updFunEqCache solved >> addToSolved solved
+ cache_in_solved fl =
+ let sfl = Solved (flav_gloc fl) (flav_evar fl)
+ solved = workItem { cc_flavor = sfl }
+ in updFunEqCache solved >> addToSolved solved
+
+-- Any other work item does not react with any top-level equations
+doTopReact _inerts _workItem = return NoTopInt
+
+
+lkpFunEqCache :: TcType -> TcS (Maybe Ct)
+lkpFunEqCache fam_head
+ = do { (subst,_inscope) <- getInertEqs
+ ; fun_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
+ ; rewrite_cached $
+ lookupTypeMap_mod subst cc_rhs fam_head (unCtFamHeadMap fun_cache) }
+ where rewrite_cached Nothing = return Nothing
+ rewrite_cached (Just (CFunEqCan { cc_flavor = fl, cc_depth = d
+ , cc_fun = tc, cc_tyargs = xis
+ , cc_rhs = xi}))
+ = ASSERT (isSolved fl)
+ do { (xis_subst,cos) <- flattenMany d fl xis
+ -- cos :: xis_subst ~ xis
+ ; (xi_subst,co) <- flatten d fl xi
+ -- co :: xi_subst ~ xi
+ ; let new_pty = mkTcEqPred (mkTyConApp tc xis_subst) xi_subst
+ new_co = mkTcTyConAppCo tc cos `mkTcTransCo`
+ mkTcCoVarCo (flav_evar fl) `mkTcTransCo`
+ mkTcSymCo co
+ ; new_fl <- rewriteCtFlavor fl new_pty new_co
+ ; case new_fl of
+ Nothing
+ -> return Nothing -- Strange: cached?
+ Just fl'
+ -> return $
+ Just (CFunEqCan { cc_flavor = fl'
+ , cc_depth = d
+ , cc_fun = tc
+ , cc_tyargs = xis_subst
+ , cc_rhs = xi_subst }) }
+ rewrite_cached (Just other_ct)
+ = pprPanic "lkpFunEqCache:not family equation!" $ ppr other_ct
+
+updFunEqCache :: Ct -> TcS ()
+updFunEqCache fun_eq@(CFunEqCan { cc_fun = tc, cc_tyargs = xis })
+ = modifyInertTcS $ \inert -> ((), upd_inert inert)
+ where upd_inert inert
+ = let slvd = unCtFamHeadMap (inert_solved_funeqs inert)
+ in inert { inert_solved_funeqs =
+ CtFamHeadMap (alterTM key upd_funeqs slvd) }
+ upd_funeqs Nothing = Just fun_eq
+ upd_funeqs (Just _ct) = Just fun_eq
+ -- Or _ct? depends on which caches more steps of computation
+ key = mkTyConApp tc xis
+updFunEqCache other = pprPanic "updFunEqCache:Non family equation" $ ppr other
+
+
+{- DELETEME
; case fl of
Wanted {} -> do { evc <- newEqVar fl rhs_ty xi -- Wanted version
; let eqv' = evc_the_evvar evc
@@ -1569,9 +1774,9 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl
}
}
+-}
+
--- Any other work item does not react with any top-level equations
-doTopReact _inerts _workItem = return NoTopInt
\end{code}
@@ -1807,23 +2012,25 @@ matchClassInst inerts clas tys loc
; if null theta then
return (GenInst [] (EvDFunApp dfun_id tys []))
else do
- { evc_vars <- instDFunConstraints theta (Wanted loc)
- ; let ev_vars = map evc_the_evvar evc_vars
- new_ev_vars = [evc_the_evvar evc | evc <- evc_vars, isNewEvVar evc]
+ { evc_vars <- instDFunConstraints theta
+ ; let ev_vars = map mn_thing evc_vars
+ new_ev_vars = [mn_thing evc | evc <- evc_vars
+ , isFresh evc ]
-- new_ev_vars are only the real new variables that can be emitted
- ; return $ GenInst new_ev_vars (EvDFunApp dfun_id tys ev_vars) }
- }
+ ; return $ GenInst new_ev_vars (EvDFunApp dfun_id tys ev_vars) } }
}
where
givens_for_this_clas :: Cts
givens_for_this_clas
- = lookupUFM (cts_given (inert_dicts inerts)) clas `orElse` emptyCts
+ = lookupUFM (cts_given (inert_dicts $ inert_cans inerts)) clas
+ `orElse` emptyCts
given_overlap :: TcsUntouchables -> Bool
given_overlap untch = anyBag (matchable untch) givens_for_this_clas
- matchable untch (CDictCan { cc_class = clas_g, cc_tyargs = sys, cc_flavor = fl })
- | Just GivenOrig <- isGiven_maybe fl
+ matchable untch (CDictCan { cc_class = clas_g, cc_tyargs = sys
+ , cc_flavor = fl })
+ | isGiven fl
= ASSERT( clas_g == clas )
case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv &&
tv `elemVarSet` tyVarsOfTypes tys
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index f045287692..831e130143 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -686,18 +686,29 @@ zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
zonkCt :: Ct -> TcM Ct
-- Zonking a Ct conservatively gives back a CNonCanonical
zonkCt ct
- = do { v' <- zonkEvVar (cc_id ct)
- ; fl' <- zonkFlavor (cc_flavor ct)
+ = do { fl' <- zonkFlavor (cc_flavor ct)
; return $
- CNonCanonical { cc_id = v'
- , cc_flavor = fl'
+ CNonCanonical { cc_flavor = fl'
, cc_depth = cc_depth ct } }
zonkCts :: Cts -> TcM Cts
zonkCts = mapBagM zonkCt
zonkFlavor :: CtFlavor -> TcM CtFlavor
-zonkFlavor (Given loc gk) = do { loc' <- zonkGivenLoc loc; return (Given loc' gk) }
-zonkFlavor fl = return fl
+zonkFlavor (Given loc evar)
+ = do { loc' <- zonkGivenLoc loc
+ ; evar' <- zonkEvVar evar
+ ; return (Given loc' evar') }
+zonkFlavor (Solved loc evar)
+ = do { loc' <- zonkGivenLoc loc
+ ; evar' <- zonkEvVar evar
+ ; return (Solved loc' evar') }
+zonkFlavor (Wanted loc evar)
+ = do { evar' <- zonkEvVar evar
+ ; return (Wanted loc evar') }
+zonkFlavor (Derived loc pty)
+ = do { pty' <- zonkTcType pty
+ ; return (Derived loc pty') }
+
zonkGivenLoc :: GivenLoc -> TcM GivenLoc
-- GivenLocs may have unification variables inside them!
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index e19ca3574d..a28b094072 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -55,9 +55,9 @@ module TcRnTypes(
singleCt, extendCts, isEmptyCts, isCTyEqCan,
isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
- isGivenCt_maybe, isGivenOrSolvedCt,
+ isGivenCt, isGivenOrSolvedCt,
ctWantedLoc,
- SubGoalDepth, mkNonCanonical, ctPred,
+ SubGoalDepth, mkNonCanonical, ctPred, ctFlavPred, ctId, ctFlavId,
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, addFlats, addImplics, mkFlatWC,
@@ -65,16 +65,15 @@ module TcRnTypes(
Implication(..),
CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin,
CtOrigin(..), EqOrigin(..),
- WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt,
+ WantedLoc, GivenLoc, pushErrCtxt,
pushErrCtxtSameOrigin,
SkolemInfo(..),
- CtFlavor(..), pprFlavorArising,
- mkSolvedFlavor, mkGivenFlavor, mkWantedFlavor,
- isWanted, isGivenOrSolved, isGiven_maybe, isSolved,
- isDerived, getWantedLoc, canSolve, canRewrite,
- combineCtLoc,
+ CtFlavor(..), pprFlavorArising,
+ mkSolvedLoc, mkGivenLoc,
+ isWanted, isGivenOrSolved, isGiven, isSolved,
+ isDerived, getWantedLoc, getGivenLoc, canSolve, canRewrite,
-- Pretty printing
pprEvVarTheta, pprWantedsWithLocs,
@@ -90,7 +89,7 @@ module TcRnTypes(
import HsSyn
import HscTypes
-import TcEvidence( EvBind, EvBindsVar, EvTerm )
+import TcEvidence( EvBind, EvBindsVar )
import Type
import Class ( Class )
import TyCon ( TyCon )
@@ -846,7 +845,6 @@ type SubGoalDepth = Int -- An ever increasing number used to restrict
data Ct
-- Atomic canonical constraints
= CDictCan { -- e.g. Num xi
- cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_class :: Class,
cc_tyargs :: [Xi],
@@ -857,7 +855,6 @@ data Ct
| CIPCan { -- ?x::tau
-- See note [Canonical implicit parameter constraints].
- cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_ip_nm :: IPName Name,
cc_ip_ty :: TcTauType, -- Not a Xi! See same not as above
@@ -865,7 +862,6 @@ data Ct
}
| CIrredEvCan { -- These stand for yet-unknown predicates
- cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_ty :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
-- Since, if it were a type constructor application, that'd make the
@@ -880,7 +876,6 @@ data Ct
-- * typeKind xi `compatKind` typeKind tv
-- See Note [Spontaneous solving and kind compatibility]
-- * We prefer unification variables on the left *JUST* for efficiency
- cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_tyvar :: TcTyVar,
cc_rhs :: Xi,
@@ -891,7 +886,6 @@ data Ct
| CFunEqCan { -- F xis ~ xi
-- Invariant: * isSynFamilyTyCon cc_fun
-- * typeKind (F xis) `compatKind` typeKind xi
- cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_fun :: TyCon, -- A type function
cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
@@ -903,7 +897,6 @@ data Ct
}
| CNonCanonical { -- See Note [NonCanonical Semantics]
- cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_depth :: SubGoalDepth
}
@@ -911,11 +904,11 @@ data Ct
\end{code}
\begin{code}
-mkNonCanonical :: EvVar -> CtFlavor -> Ct
-mkNonCanonical ev flav = CNonCanonical { cc_id = ev, cc_flavor = flav, cc_depth = 0}
+mkNonCanonical :: CtFlavor -> Ct
+mkNonCanonical flav = CNonCanonical { cc_flavor = flav, cc_depth = 0}
ctPred :: Ct -> PredType
-ctPred (CNonCanonical { cc_id = v }) = evVarPred v
+ctPred (CNonCanonical { cc_flavor = fl }) = ctFlavPred fl
ctPred (CDictCan { cc_class = cls, cc_tyargs = xis })
= mkClassPred cls xis
ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
@@ -925,6 +918,12 @@ ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 })
ctPred (CIPCan { cc_ip_nm = nm, cc_ip_ty = xi })
= mkIPPred nm xi
ctPred (CIrredEvCan { cc_ty = xi }) = xi
+
+
+ctId :: String -> Ct -> EvVar
+-- Precondition: not a derived!
+ctId origin ct = ctFlavId origin (cc_flavor ct)
+
\end{code}
@@ -942,16 +941,16 @@ ctWantedLoc ct = ASSERT2( not (isGivenOrSolved (cc_flavor ct)), ppr ct )
getWantedLoc (cc_flavor ct)
isWantedCt :: Ct -> Bool
-isWantedCt ct = isWanted (cc_flavor ct)
+isWantedCt = isWanted . cc_flavor
-isDerivedCt :: Ct -> Bool
-isDerivedCt ct = isDerived (cc_flavor ct)
+isGivenCt :: Ct -> Bool
+isGivenCt = isGiven . cc_flavor
-isGivenCt_maybe :: Ct -> Maybe GivenKind
-isGivenCt_maybe ct = isGiven_maybe (cc_flavor ct)
+isDerivedCt :: Ct -> Bool
+isDerivedCt = isDerived . cc_flavor
isGivenOrSolvedCt :: Ct -> Bool
-isGivenOrSolvedCt ct = isGivenOrSolved (cc_flavor ct)
+isGivenOrSolvedCt = isGivenOrSolved . cc_flavor
isCTyEqCan :: Ct -> Bool
isCTyEqCan (CTyEqCan {}) = True
@@ -981,11 +980,9 @@ isCNonCanonical _ = False
\begin{code}
instance Outputable Ct where
- ppr ct = ppr (cc_flavor ct) <> braces (ppr (cc_depth ct))
- <+> ppr ev_var <+> dcolon <+> ppr (ctPred ct)
- <+> parens (text ct_sort)
- where ev_var = cc_id ct
- ct_sort = case ct of
+ ppr ct = ppr (cc_flavor ct) <+>
+ braces (ppr (cc_depth ct)) <+> parens (text ct_sort)
+ where ct_sort = case ct of
CTyEqCan {} -> "CTyEqCan"
CFunEqCan {} -> "CFunEqCan"
CNonCanonical {} -> "CNonCanonical"
@@ -1225,55 +1222,85 @@ pprWantedsWithLocs wcs
\begin{code}
data CtFlavor
- = Given GivenLoc GivenKind -- We have evidence for this constraint in TcEvBinds
- | Derived WantedLoc -- Derived's are just hints for unifications
- | Wanted WantedLoc -- We have no evidence bindings for this constraint.
-
-data GivenKind
- = GivenOrig -- Originates in some given, such as signature or pattern match
- | GivenSolved (Maybe EvTerm)
- -- Is given as result of being solved, maybe provisionally on
- -- some other wanted constraints. We cache the evidence term
- -- sometimes here as well /as well as/ in the EvBinds,
- -- see Note [Optimizing Spontaneously Solved Coercions]
+ = Given { flav_gloc :: GivenLoc, flav_evar :: EvVar }
+ -- Trully given, not depending on subgoals
+ -- NB: Spontaneous unifications belong here
+ -- DV TODOs: (i) Consider caching actual evidence _term_
+ -- (ii) Revisit Note [Optimizing Spontaneously Solved Coercions]
+
+ | Solved { flav_gloc :: GivenLoc, flav_evar :: EvVar }
+ -- Originally wanted, but now we've produced and
+ -- bound some partial evidence for this constraint.
+ -- NB: Evidence may rely on yet-wanted constraints or other solved or given
+
+ | Wanted { flav_wloc :: WantedLoc, flav_evar :: EvVar }
+ -- Wanted goal
+
+ | Derived { flav_wloc :: WantedLoc, flav_der_pty :: TcPredType }
+ -- A goal that we don't really have to solve and can't immediately
+ -- rewrite anything other than a derived (there's no evidence variable!)
+ -- but if we do manage to solve it may help in solving other goals.
+
+ctFlavPred :: CtFlavor -> TcPredType
+-- The predicate of a flavor
+ctFlavPred (Given _ evar) = evVarPred evar
+ctFlavPred (Solved _ evar) = evVarPred evar
+ctFlavPred (Wanted _ evar) = evVarPred evar
+ctFlavPred (Derived { flav_der_pty = pty }) = pty
+
+ctFlavId :: String -> CtFlavor -> EvVar
+-- Precondition: can't be derived
+ctFlavId origin (Derived _ pty)
+ = pprPanic "ctFlavId: derived constraint cannot have id" $
+ vcat [ text "origin=" <+> text origin
+ , text "pty =" <+> ppr pty ]
+ctFlavId _ fl = flav_evar fl
instance Outputable CtFlavor where
- ppr (Given _ GivenOrig) = ptext (sLit "[G]")
- ppr (Given _ (GivenSolved {})) = ptext (sLit "[S]") -- Print [S] for Given/Solved's
- ppr (Wanted {}) = ptext (sLit "[W]")
- ppr (Derived {}) = ptext (sLit "[D]")
+ ppr fl = case fl of
+ (Given _ evar) -> ptext (sLit "[G]") <+> ppr evar <+> ppr_pty
+ (Solved _ evar) -> ptext (sLit "[S]") <+> ppr evar <+> ppr_pty
+ (Wanted _ evar) -> ptext (sLit "[W]") <+> ppr evar <+> ppr_pty
+ (Derived {}) -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty
+ where ppr_pty = dcolon <+> ppr (ctFlavPred fl)
getWantedLoc :: CtFlavor -> WantedLoc
-getWantedLoc (Wanted wl) = wl
-getWantedLoc (Derived wl) = wl
-getWantedLoc flav@(Given {}) = pprPanic "getWantedLoc" (ppr flav)
+-- Precondition: Wanted or Derived
+getWantedLoc fl = flav_wloc fl
+
+getGivenLoc :: CtFlavor -> GivenLoc
+-- Precondition: Given or Solved
+getGivenLoc fl = flav_gloc fl
pprFlavorArising :: CtFlavor -> SDoc
-pprFlavorArising (Derived wl) = pprArisingAt wl
-pprFlavorArising (Wanted wl) = pprArisingAt wl
pprFlavorArising (Given gl _) = pprArisingAt gl
+pprFlavorArising (Solved gl _) = pprArisingAt gl
+pprFlavorArising (Wanted wl _) = pprArisingAt wl
+pprFlavorArising (Derived wl _) = pprArisingAt wl
+
isWanted :: CtFlavor -> Bool
isWanted (Wanted {}) = True
-isWanted _ = False
+isWanted _ = False
isGivenOrSolved :: CtFlavor -> Bool
-isGivenOrSolved (Given {}) = True
+isGivenOrSolved (Given {}) = True
+isGivenOrSolved (Solved {}) = True
isGivenOrSolved _ = False
isSolved :: CtFlavor -> Bool
-isSolved (Given _ (GivenSolved {})) = True
+isSolved (Solved {}) = True
isSolved _ = False
-isGiven_maybe :: CtFlavor -> Maybe GivenKind
-isGiven_maybe (Given _ gk) = Just gk
-isGiven_maybe _ = Nothing
+isGiven :: CtFlavor -> Bool
+isGiven (Given {}) = True
+isGiven _ = False
-isDerived :: CtFlavor -> Bool
+isDerived :: CtFlavor -> Bool
isDerived (Derived {}) = True
-isDerived _ = False
+isDerived _ = False
-canSolve :: CtFlavor -> CtFlavor -> Bool
+canSolve :: CtFlavor -> CtFlavor -> Bool
-- canSolve ctid1 ctid2
-- The constraint ctid1 can be used to solve ctid2
-- "to solve" means a reaction where the active parts of the two constraints match.
@@ -1287,14 +1314,15 @@ canSolve :: CtFlavor -> CtFlavor -> Bool
canSolve (Given {}) _ = True
canSolve (Wanted {}) (Derived {}) = True
canSolve (Wanted {}) (Wanted {}) = True
-canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given
-canSolve _ _ = False -- (There is no *evidence* for a derived.)
+canSolve (Derived {}) (Derived {}) = True -- Derived can't solve wanted/given
+canSolve _ _ = False -- No evidence for a derived, anyway
canRewrite :: CtFlavor -> CtFlavor -> Bool
--- canRewrite ctid1 ctid2
--- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
+-- canRewrite ct1 ct2
+-- The equality constraint ct1 can be used to rewrite inside ct2
canRewrite = canSolve
+{- DELETEME
combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
-- Precondition: At least one of them should be wanted
combineCtLoc (Wanted loc) _ = loc
@@ -1303,12 +1331,28 @@ combineCtLoc (Derived loc ) _ = loc
combineCtLoc _ (Derived loc ) = loc
combineCtLoc _ _ = panic "combineCtLoc: both given"
+
mkSolvedFlavor :: CtFlavor -> SkolemInfo -> EvTerm -> CtFlavor
-- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
mkSolvedFlavor (Wanted loc) sk evterm = Given (setCtLocOrigin loc sk) (GivenSolved (Just evterm))
mkSolvedFlavor (Derived loc) sk evterm = Given (setCtLocOrigin loc sk) (GivenSolved (Just evterm))
mkSolvedFlavor fl@(Given {}) _sk _evterm = pprPanic "Solving a given constraint!" $ ppr fl
+-}
+
+-- combineWantedLoc :: Maybe WantedLoc -> Maybe WantedLoc -> WantedLoc
+-- -- Precondition: at least one is Just
+-- combineWantedLoc (Just wl) _ = wl
+-- combineWantedLoc _ (Just wl) = wl
+-- combineWantedLoc _ _ = panic "combineCtLoc: both given!"
+
+
+mkGivenLoc :: WantedLoc -> SkolemInfo -> GivenLoc
+mkGivenLoc wl sk = setCtLocOrigin wl sk
+mkSolvedLoc :: WantedLoc -> SkolemInfo -> GivenLoc
+mkSolvedLoc wl sk = setCtLocOrigin wl sk
+
+{- DELETEME
mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
@@ -1318,6 +1362,8 @@ mkWantedFlavor :: CtFlavor -> CtFlavor
mkWantedFlavor (Wanted loc) = Wanted loc
mkWantedFlavor (Derived loc) = Wanted loc
mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavor" (ppr fl)
+-}
+
\end{code}
%************************************************************************
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 5f87205dfb..0c3461891d 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -22,14 +22,13 @@ module TcSMonad (
emitFrozenError,
isWanted, isGivenOrSolved, isDerived,
- isGivenOrSolvedCt, isGivenCt_maybe,
+ isGivenOrSolvedCt, isGivenCt,
isWantedCt, isDerivedCt, pprFlavorArising,
isFlexiTcsTv,
canRewrite, canSolve,
- combineCtLoc, mkSolvedFlavor, mkGivenFlavor,
- mkWantedFlavor,
+ mkSolvedLoc, mkGivenLoc,
ctWantedLoc,
TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
@@ -39,8 +38,21 @@ module TcSMonad (
SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
+ -- Getting and setting the flattening cache
+ getFlatCache, updFlatCache, addToSolved,
+
+
+ setEvBind,
+ XEvTerm(..),
+ MaybeNew (..), isFresh,
+ xCtFlavor, -- Transform a CtFlavor during a step
+ rewriteCtFlavor, -- Specialized version of xCtFlavor for coercions
+ newWantedEvVar, newGivenEvVar, instDFunConstraints, newKindConstraint,
+ newDerived,
+ xCtFlavor_cache, rewriteCtFlavor_cache,
+
-- Creation of evidence variables
- newEvVar, forceNewEvVar, delCachedEvVar, updateFlatCache, flushFlatCache,
+{- DELETEME newEvVar, forceNewEvVar, delCachedEvVar, updateFlatCache, flushFlatCache,
newGivenEqVar,
newEqVar, newKindConstraint,
EvVarCreated (..), isNewEvVar, FlatEqOrigin ( .. ), origin_matches,
@@ -48,28 +60,31 @@ module TcSMonad (
-- Setting evidence variables
setEqBind,
setEvBind,
-
+-}
setWantedTyBind,
getInstEnvs, getFamInstEnvs, -- Getting the environments
getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
getTcEvBindsMap, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
- getTcSEvVarCacheMap, getTcSEvVarFlatCache, setTcSEvVarCacheMap, pprEvVarCache,
+{- DELETEME
+ getTcSEvVarCacheMap, getTcSEvVarFlatCache, setTcSEvVarCacheMap, pprEvVarCache,
+-}
newFlattenSkolemTy, -- Flatten skolems
-- Inerts
- InertSet(..),
+ InertSet(..), InertCans(..),
getInertEqs, getCtCoercion,
emptyInert, getTcSInerts, updInertSet, extractUnsolved,
extractUnsolvedTcS, modifyInertTcS,
updInertSetTcS, partitionCCanMap, partitionEqMap,
getRelevantCts, extractRelevantInerts,
- CCanMap (..), CtTypeMap, pprCtTypeMap, mkPredKeyForTypeMap, partitionCtTypeMap,
+ CCanMap (..), CtTypeMap, CtFamHeadMap(..), CtPredMap(..),
+ pprCtTypeMap, partCtFamHeadMap,
instDFunTypes, -- Instantiation
- instDFunConstraints,
+ -- instDFunConstraints,
newFlexiTcSTy, instFlexiTcS,
compatKind, mkKindErrorCtxtTcS,
@@ -134,7 +149,8 @@ import Maybes ( orElse )
import Control.Monad( when )
import StaticFlags( opt_PprStyle_Debug )
import Data.IORef
-
+import Data.List ( find )
+import Control.Monad ( zipWithM )
import TrieMap
\end{code}
@@ -215,7 +231,7 @@ extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt ct wl
- | isEqVar (cc_id ct) = extendWorkListEq ct wl
+ | isEqPred (ctPred ct) = extendWorkListEq ct wl
| otherwise = extendWorkListNonEq ct wl
appendWorkListCt :: [Ct] -> WorkList -> WorkList
@@ -241,8 +257,8 @@ workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
workListFromCt :: Ct -> WorkList
-- Agnostic
-workListFromCt ct | isEqVar (cc_id ct) = workListFromEq ct
- | otherwise = workListFromNonEq ct
+workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct
+ | otherwise = workListFromNonEq ct
selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
@@ -266,62 +282,7 @@ keepWanted = filterBag isWantedCt
-- ``Important: use fold*r*Bag to preserve the order of the evidence variables''
-- DV: Is this still relevant?
-\end{code}
-
-%************************************************************************
-%* *
-%* Inert sets *
-%* *
-%* *
-%************************************************************************
-
-
-Note [InertSet invariants]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-An InertSet is a bag of canonical constraints, with the following invariants:
-
- 1 No two constraints react with each other.
-
- A tricky case is when there exists a given (solved) dictionary
- constraint and a wanted identical constraint in the inert set, but do
- not react because reaction would create loopy dictionary evidence for
- the wanted. See note [Recursive dictionaries]
-
- 2 Given equalities form an idempotent substitution [none of the
- given LHS's occur in any of the given RHS's or reactant parts]
-
- 3 Wanted equalities also form an idempotent substitution
-
- 4 The entire set of equalities is acyclic.
-
- 5 Wanted dictionaries are inert with the top-level axiom set
-
- 6 Equalities of the form tv1 ~ tv2 always have a touchable variable
- on the left (if possible).
-
- 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
- will be marked as solved right before being pushed into the inert set.
- See note [Touchables and givens].
-
- 8 No Given constraint mentions a touchable unification variable, but
- Given/Solved may do so.
-
- 9 Given constraints will also have their superclasses in the inert set,
- but Given/Solved will not.
-
-Note that 6 and 7 are /not/ enforced by canonicalization but rather by
-insertion in the inert list, ie by TcInteract.
-
-During the process of solving, the inert set will contain some
-previously given constraints, some wanted constraints, and some given
-constraints which have arisen from solving wanted constraints. For
-now we do not distinguish between given and solved constraints.
-
-Note that we must switch wanted inert items to given when going under an
-implication constraint (when in top-level inference mode).
-
-\begin{code}
-
+-- Canonical constraint maps
data CCanMap a = CCanMap { cts_given :: UniqFM Cts
-- Invariant: all Given
, cts_derived :: UniqFM Cts
@@ -343,6 +304,7 @@ updCCanMap (a,ct) cmap
Wanted {} -> cmap { cts_wanted = insert_into (cts_wanted cmap) }
Given {} -> cmap { cts_given = insert_into (cts_given cmap) }
Derived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
+ Solved {} -> panic "updCCanMap update with solved!"
where
insert_into m = addToUFM_C unionBags m a (singleCt ct)
@@ -359,10 +321,12 @@ getRelevantCts a cmap
where
lookup map = lookupUFM map a `orElse` emptyCts
-
-getCtTypeMapRelevants :: PredType -> TypeMap Ct -> (Cts, TypeMap Ct)
-getCtTypeMapRelevants key_pty tmap
- = partitionCtTypeMap (\ct -> mkPredKeyForTypeMap ct `eqType` key_pty) tmap
+lookupCCanMap :: Uniquable a => a -> (Ct -> Bool) -> CCanMap a -> Maybe Ct
+lookupCCanMap a p map
+ = let possible_cts = lookupUFM (cts_given map) a `orElse`
+ lookupUFM (cts_wanted map) a `orElse`
+ lookupUFM (cts_derived map) a `orElse` emptyCts
+ in find p (bagToList possible_cts)
partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a)
@@ -396,29 +360,13 @@ extractUnsolvedCMap cmap =
in (wntd `unionBags` derd,
cmap { cts_wanted = emptyUFM, cts_derived = emptyUFM })
--- See Note [InertSet invariants]
-data InertSet
- = IS { inert_eqs :: TyVarEnv (Ct,TcCoercion)
- -- Must all be CTyEqCans! If an entry exists of the form:
- -- a |-> ct,co
- -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi }
- -- And co : a ~ xi
- , inert_eq_tvs :: InScopeSet -- Invariant: superset of inert_eqs tvs
-
- , inert_dicts :: CCanMap Class -- Dictionaries only, index is the class
- , inert_ips :: CCanMap (IPName Name) -- Implicit parameters
- -- NB: We do not want to use TypeMaps here because functional dependencies
- -- will only match on the class but not the type. Similarly IPs match on the
- -- name but not on the whole datatype
-
- , inert_funeqs :: CtTypeMap -- Map from family heads to CFunEqCan constraints
-
- , inert_irreds :: Cts -- Irreducible predicates
- , inert_frozen :: Cts -- All non-canonicals are kept here (as frozen errors)
- }
-
+-- Maps from PredTypes to Constraints
type CtTypeMap = TypeMap Ct
+newtype CtPredMap =
+ CtPredMap { unCtPredMap :: CtTypeMap } -- Indexed by TcPredType
+newtype CtFamHeadMap =
+ CtFamHeadMap { unCtFamHeadMap :: CtTypeMap } -- Indexed by family head
pprCtTypeMap :: TypeMap Ct -> SDoc
pprCtTypeMap ctmap = ppr (foldTM (:) ctmap [])
@@ -426,87 +374,198 @@ pprCtTypeMap ctmap = ppr (foldTM (:) ctmap [])
ctTypeMapCts :: TypeMap Ct -> Cts
ctTypeMapCts ctmap = foldTM (\ct cts -> extendCts cts ct) ctmap emptyCts
-mkPredKeyForTypeMap :: Ct -> PredType
--- Create a key from a constraint to use in the inert CtTypeMap.
--- The only interesting case is for family applications, where the
--- key is not the whole PredType of cc_id, but rather the family
--- equality left hand side (head)
-mkPredKeyForTypeMap (CFunEqCan { cc_fun = fn, cc_tyargs = xis })
- = mkTyConApp fn xis
-mkPredKeyForTypeMap ct
- = evVarPred (cc_id ct)
-
-partitionCtTypeMap :: (Ct -> Bool)
- -> TypeMap Ct -> (Cts, TypeMap Ct)
--- Kick out the ones that match the predicate and keep the rest in the typemap
-partitionCtTypeMap f ctmap
- = foldTM upd_acc ctmap (emptyBag,ctmap)
- where upd_acc ct (cts,acc_map)
+
+partCtFamHeadMap :: (Ct -> Bool)
+ -> CtFamHeadMap
+ -> (Cts, CtFamHeadMap)
+partCtFamHeadMap f ctmap
+ = let (cts,tymap_final) = foldTM upd_acc tymap_inside (emptyBag, tymap_inside)
+ in (cts, CtFamHeadMap tymap_final)
+ where
+ tymap_inside = unCtFamHeadMap ctmap
+ upd_acc ct (cts,acc_map)
| f ct = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map)
| otherwise = (cts,acc_map)
- where ct_key = mkPredKeyForTypeMap ct
+ where ct_key | EqPred ty1 _ <- classifyPredType (ctPred ct)
+ = ty1
+ | otherwise
+ = panic "partCtFamHeadMap, encountered non equality!"
+
+
+\end{code}
+
+%************************************************************************
+%* *
+%* Inert Sets *
+%* *
+%* *
+%************************************************************************
+
+\begin{code}
+
+
+-- All Given (fully known) or Wanted or Derived, never Solved
+-- See Note [Detailed InertCans Invariants] for more
+data InertCans
+ = IC { inert_eqs :: TyVarEnv Ct
+ -- Must all be CTyEqCans! If an entry exists of the form:
+ -- a |-> ct,co
+ -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi }
+ -- And co : a ~ xi
+ , inert_eq_tvs :: InScopeSet
+ -- Superset of the type variables of inert_eqs
+ , inert_dicts :: CCanMap Class
+ -- Dictionaries only, index is the class
+ -- NB: index is /not/ the whole type because FD reactions
+ -- need to match the class but not necessarily the whole type.
+ , inert_ips :: CCanMap (IPName Name)
+ -- Implicit parameters, index is the name
+ -- NB: index is /not/ the whole type because IP reactions need
+ -- to match the ip name but not necessarily the whole type.
+ , inert_funeqs :: CtFamHeadMap
+ -- Family equations, index is the whole family head type.
+ , inert_irreds :: Cts
+ -- Irreducible predicates
+ }
+
+
+\end{code}
+
+Note [Detailed InertCans Invariants]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The InertCans represents a collection of constraints with the following properties:
+ 1 All canonical
+ 2 All Given or Wanted or Derived. No (partially) Solved
+ 3 No two dictionaries with the same head
+ 4 No two family equations with the same head
+ 5 Family equations inert with top-level
+ 6 Dictionaries have no matching instance at top level
+ 7 Constraints are fully rewritten with respect to the equality constraints (CTyEqCan)
+ 8 Equalities form an idempotent substitution (taking flavors into consideration)
+ 9 Given family or dictionary constraints don't mention touchable unification variables
+\begin{code}
+
+{- DV Notes: 23/03/2012
+ 1) stage: if exact predicate exists then discard immediately else go on
+ 2) stage: canonicalization (with the newEvVarCache) and the flatCache stuff
+ 3) stage: whatever we do no but at the interact-top we share previously solved
+ family head equations
+-}
+
+-- The Inert Set
+data InertSet
+ = IS { inert_cans :: InertCans
+ -- Canonical Given,Wanted,Solved
+ , inert_frozen :: Cts
+ -- Frozen errors (as non-canonicals)
+
+ , inert_solved :: CtPredMap
+ -- Solved constraints (for caching):
+ -- (i) key is by predicate type
+ -- (ii) all of 'Solved' flavor, may or may not be canonicals
+ -- (iii) we use this field for avoiding creating newEvVars
+ , inert_flat_cache :: CtFamHeadMap
+ -- All ``flattening equations'' are kept here.
+ -- Always canonical CTyFunEqs (Given or Wanted only!)
+ -- Key is by family head. We used this field during flattening only
+ , inert_solved_funeqs :: CtFamHeadMap
+ -- Memoized *Solved* family equations co :: F xis ~ xi
+ -- Stored not necessarily as fully rewritten; we'll do that lazily
+ -- when we lookup
+ }
-instance Outputable InertSet where
- ppr is = vcat [ vcat (map ppr (varEnvElts (inert_eqs is)))
- , vcat (map ppr (Bag.bagToList $ inert_irreds is))
- , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
- , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
- , vcat (map ppr (Bag.bagToList $ ctTypeMapCts (inert_funeqs is)))
+instance Outputable InertCans where
+ ppr ics = vcat [ vcat (map ppr (varEnvElts (inert_eqs ics)))
+ , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics)))
+ , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips ics)))
+ , vcat (map ppr (Bag.bagToList $
+ ctTypeMapCts (unCtFamHeadMap $ inert_funeqs ics)))
+ , vcat (map ppr (Bag.bagToList $ inert_irreds ics))
+ ]
+
+instance Outputable InertSet where
+ ppr is = vcat [ ppr $ inert_cans is
, text "Frozen errors =" <+> -- Clearly print frozen errors
braces (vcat (map ppr (Bag.bagToList $ inert_frozen is)))
- , text "Warning: Not displaying cached (solved) constraints"
- ]
-
-emptyInert :: InertSet
-emptyInert = IS { inert_eqs = emptyVarEnv
- , inert_eq_tvs = emptyInScopeSet
- , inert_frozen = emptyCts
- , inert_irreds = emptyCts
- , inert_dicts = emptyCCanMap
- , inert_ips = emptyCCanMap
- , inert_funeqs = emptyTM
- }
+ , text "Solved and cached" <+>
+ int (foldTypeMap (\_ x -> x+1) 0
+ (unCtPredMap $ inert_solved is)) <+>
+ text "more constraints" ]
+emptyInert :: InertSet
+emptyInert
+ = IS { inert_cans = IC { inert_eqs = emptyVarEnv
+ , inert_eq_tvs = emptyInScopeSet
+ , inert_dicts = emptyCCanMap
+ , inert_ips = emptyCCanMap
+ , inert_funeqs = CtFamHeadMap emptyTM
+ , inert_irreds = emptyCts }
+ , inert_frozen = emptyCts
+ , inert_flat_cache = CtFamHeadMap emptyTM
+ , inert_solved = CtPredMap emptyTM
+ , inert_solved_funeqs = CtFamHeadMap emptyTM }
type AtomicInert = Ct
updInertSet :: InertSet -> AtomicInert -> InertSet
-- Add a new inert element to the inert set.
updInertSet is item
- | isCTyEqCan item
- = let upd_err a b = pprPanic "updInertSet" $
- vcat [ text "Multiple inert equalities:"
- , text "Old (already inert):" <+> ppr a
- , text "Trying to insert :" <+> ppr b
- ]
-
- -- If evidence is cached, pick it up from the flavor!
- coercion = getCtCoercion item
-
- eqs' = extendVarEnv_C upd_err (inert_eqs is)
- (cc_tyvar item)
- (item, coercion)
- inscope' = extendInScopeSetSet (inert_eq_tvs is) (tyVarsOfCt item)
- in is { inert_eqs = eqs', inert_eq_tvs = inscope' }
-
- | Just x <- isCIPCan_Maybe item -- IP
- = is { inert_ips = updCCanMap (x,item) (inert_ips is) }
- | isCIrredEvCan item -- Presently-irreducible evidence
- = is { inert_irreds = inert_irreds is `Bag.snocBag` item }
-
-
- | Just cls <- isCDictCan_Maybe item -- Dictionary
- = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
-
- | Just _tc <- isCFunEqCan_Maybe item -- Function equality
- = let pty = mkPredKeyForTypeMap item
- upd_funeqs Nothing = Just item
- upd_funeqs (Just _alredy_there) = panic "updInertSet: item already there!"
- in is { inert_funeqs = alterTM pty upd_funeqs (inert_funeqs is) }
-
- | otherwise
+ | isSolved (cc_flavor item)
+ -- Solved items go in their special place
+ = let pty = ctPred item
+ upd_solved Nothing = Just item
+ upd_solved (Just _existing_solved) = Just item
+ -- .. or Just existing_solved? Is this even possible to happen?
+ in is { inert_solved =
+ CtPredMap $
+ alterTM pty upd_solved (unCtPredMap $ inert_solved is) }
+
+ | isCNonCanonical item
+ -- NB: this may happen if we decide to kick some frozen error
+ -- out to rewrite him. Frozen errors are just NonCanonicals
= is { inert_frozen = inert_frozen is `Bag.snocBag` item }
+
+ | otherwise
+ -- A canonical Given, Wanted, or Derived
+ = is { inert_cans = upd_inert_cans (inert_cans is) item }
+
+ where upd_inert_cans :: InertCans -> AtomicInert -> InertCans
+ -- Precondition: item /is/ canonical
+ upd_inert_cans ics item
+ | isCTyEqCan item
+ = let upd_err a b = pprPanic "updInertSet" $
+ vcat [ text "Multiple inert equalities:"
+ , text "Old (already inert):" <+> ppr a
+ , text "Trying to insert :" <+> ppr b ]
+
+ eqs' = extendVarEnv_C upd_err (inert_eqs ics)
+ (cc_tyvar item) item
+ inscope' = extendInScopeSetSet (inert_eq_tvs ics)
+ (tyVarsOfCt item)
+
+ in ics { inert_eqs = eqs', inert_eq_tvs = inscope' }
+
+ | Just x <- isCIPCan_Maybe item -- IP
+ = ics { inert_ips = updCCanMap (x,item) (inert_ips ics) }
+
+ | isCIrredEvCan item -- Presently-irreducible evidence
+ = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
+
+ | Just cls <- isCDictCan_Maybe item -- Dictionary
+ = ics { inert_dicts = updCCanMap (cls,item) (inert_dicts ics) }
+
+ | Just _tc <- isCFunEqCan_Maybe item -- Function equality
+ = let fam_head = mkTyConApp (cc_fun item) (cc_tyargs item)
+ upd_funeqs Nothing = Just item
+ upd_funeqs (Just _already_there)
+ = panic "updInertSet: item already there!"
+ in ics { inert_funeqs = CtFamHeadMap
+ (alterTM fam_head upd_funeqs $
+ (unCtFamHeadMap $ inert_funeqs ics)) }
+ | otherwise
+ = pprPanic "upd_inert set: can't happen! Inserting " $
+ ppr item
updInertSetTcS :: AtomicInert -> TcS ()
-- Add a new item in the inerts of the monad
@@ -528,6 +587,12 @@ modifyInertTcS upd
; wrapTcS (TcM.writeTcRef is_var new_inert)
; return a }
+
+addToSolved :: Ct -> TcS ()
+addToSolved ct
+ = ASSERT ( isSolved (cc_flavor ct) )
+ updInertSetTcS ct
+
extractUnsolvedTcS :: TcS (Cts,Cts)
-- Extracts frozen errors and remaining unsolved and sets the
-- inert set to be the remaining!
@@ -549,33 +614,51 @@ extractUnsolved :: InertSet -> ((Cts,Cts), InertSet)
-- -----------|-----------------------------------------------------------------
-- is_solved | Whatever remains from the inert after removing the previous two.
-- -----------------------------------------------------------------------------
-extractUnsolved is@(IS {inert_eqs = eqs, inert_irreds = irreds})
- = let is_solved = is { inert_eqs = solved_eqs
- , inert_eq_tvs = inert_eq_tvs is
- , inert_dicts = solved_dicts
- , inert_ips = solved_ips
- , inert_irreds = solved_irreds
- , inert_frozen = emptyCts
- , inert_funeqs = solved_funeqs
+extractUnsolved (IS { inert_cans = IC { inert_eqs = eqs
+ , inert_eq_tvs = eq_tvs
+ , inert_irreds = irreds
+ , inert_ips = ips
+ , inert_funeqs = funeqs
+ , inert_dicts = dicts
+ }
+ , inert_frozen = frozen
+ , inert_solved = _solved
+ , inert_flat_cache = _flat_cache })
+
+ = let is_solved = IS { inert_cans = IC { inert_eqs = solved_eqs
+ , inert_eq_tvs = eq_tvs
+ , inert_dicts = solved_dicts
+ , inert_ips = solved_ips
+ , inert_irreds = solved_irreds
+ , inert_funeqs = solved_funeqs }
+ , inert_frozen = emptyCts -- All out
+
+ -- DV: For solved and the flat cache, I am flushing them here:
+ -- Solved cts may depend on wanteds which we kick out. But later
+ -- we may try to re-solve some kicked-out wanteds and I am worried
+ -- that there is a danger or evidence loops if we keep the solved
+ -- in for caching purposes. So I am flushing the solved and the
+ -- flattening cache, quite conservatively.
+ , inert_solved = CtPredMap emptyTM
+ , inert_flat_cache = CtFamHeadMap emptyTM
+ , inert_solved_funeqs = CtFamHeadMap emptyTM
}
- in ((inert_frozen is, unsolved), is_solved)
+ in ((frozen, unsolved), is_solved)
- where solved_eqs = filterVarEnv_Directly (\_ (ct,_) -> isGivenOrSolvedCt ct) eqs
- unsolved_eqs = foldVarEnv (\(ct,_co) cts -> cts `extendCts` ct) emptyCts $
+ where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenOrSolvedCt ct) eqs
+ unsolved_eqs = foldVarEnv (\ct cts -> cts `extendCts` ct) emptyCts $
eqs `minusVarEnv` solved_eqs
(unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenOrSolvedCt) irreds
- (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is)
- (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is)
+ (unsolved_ips, solved_ips) = extractUnsolvedCMap ips
+ (unsolved_dicts, solved_dicts) = extractUnsolvedCMap dicts
- (unsolved_funeqs, solved_funeqs) = extractUnsolvedCtTypeMap (inert_funeqs is)
+ (unsolved_funeqs, solved_funeqs) =
+ partCtFamHeadMap (not . isGivenOrSolved . cc_flavor) funeqs
unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
-extractUnsolvedCtTypeMap :: TypeMap Ct -> (Cts,TypeMap Ct)
-extractUnsolvedCtTypeMap
- = partitionCtTypeMap (not . isGivenOrSolved . cc_flavor)
extractRelevantInerts :: Ct -> TcS Cts
@@ -583,23 +666,70 @@ extractRelevantInerts :: Ct -> TcS Cts
-- this constraint. The monad is left with the 'thinner' inerts.
-- NB: This function contains logic specific to the constraint solver, maybe move there?
extractRelevantInerts wi
- = modifyInertTcS (extract_inert_relevants wi)
- where extract_inert_relevants (CDictCan {cc_class = cl}) is =
- let (cts,dict_map) = getRelevantCts cl (inert_dicts is)
- in (cts, is { inert_dicts = dict_map })
- extract_inert_relevants (CFunEqCan {cc_fun = tc, cc_tyargs = xis}) is =
- let (cts,feqs_map) = getCtTypeMapRelevants (mkTyConApp tc xis) (inert_funeqs is)
- in (cts, is { inert_funeqs = feqs_map })
- extract_inert_relevants (CIPCan { cc_ip_nm = nm } ) is =
- let (cts, ips_map) = getRelevantCts nm (inert_ips is)
- in (cts, is { inert_ips = ips_map })
- extract_inert_relevants (CIrredEvCan { }) is =
- let cts = inert_irreds is
- in (cts, is { inert_irreds = emptyCts })
- extract_inert_relevants _ is = (emptyCts,is)
+ = modifyInertTcS (extract_relevants wi)
+ where extract_relevants wi is
+ = let (cts,ics') = extract_ics_relevants wi (inert_cans is)
+ in (cts, is { inert_cans = ics' })
+
+ extract_ics_relevants (CDictCan {cc_class = cl}) ics =
+ let (cts,dict_map) = getRelevantCts cl (inert_dicts ics)
+ in (cts, ics { inert_dicts = dict_map })
+ extract_ics_relevants ct@(CFunEqCan {}) ics =
+ let (cts,feqs_map) =
+ let funeq_map = unCtFamHeadMap $ inert_funeqs ics
+ fam_head = mkTyConApp (cc_fun ct) (cc_tyargs ct)
+ lkp = lookupTM fam_head funeq_map
+ new_funeq_map = alterTM fam_head xtm funeq_map
+ xtm Nothing = Nothing
+ xtm (Just _ct) = Nothing
+ in case lkp of
+ Nothing -> (emptyCts, funeq_map)
+ Just ct -> (singleCt ct, new_funeq_map)
+ in (cts, ics { inert_funeqs = CtFamHeadMap feqs_map })
+ extract_ics_relevants (CIPCan { cc_ip_nm = nm } ) ics =
+ let (cts, ips_map) = getRelevantCts nm (inert_ips ics)
+ in (cts, ics { inert_ips = ips_map })
+ extract_ics_relevants (CIrredEvCan { }) ics =
+ let cts = inert_irreds ics
+ in (cts, ics { inert_irreds = emptyCts })
+ extract_ics_relevants _ ics = (emptyCts,ics)
+
+
+lookupInInerts :: InertSet -> TcPredType -> Maybe Ct
+-- Is this exact predicate type cached in the solved or canonicals of the InertSet
+lookupInInerts (IS { inert_solved = solved, inert_cans = ics }) pty
+ = case lookupInSolved solved pty of
+ Just ct -> return ct
+ Nothing -> lookupInInertCans ics pty
+
+lookupInSolved :: CtPredMap -> TcPredType -> Maybe Ct
+-- Returns just if exactly this predicate type exists in the solved.
+lookupInSolved tm pty = lookupTM pty $ unCtPredMap tm
+
+lookupInInertCans :: InertCans -> TcPredType -> Maybe Ct
+-- Returns Just if exactly this pred type exists in the inert canonicals
+lookupInInertCans ics pty
+ = lkp_ics (classifyPredType pty)
+ where lkp_ics (ClassPred cls _)
+ = lookupCCanMap cls (\ct -> ctPred ct `eqType` pty) (inert_dicts ics)
+ lkp_ics (EqPred ty1 _ty2)
+ | Just tv <- getTyVar_maybe ty1
+ , Just ct <- lookupVarEnv (inert_eqs ics) tv
+ , ctPred ct `eqType` pty
+ = Just ct
+ lkp_ics (EqPred ty1 _ty2) -- Family equation
+ | Just _ <- splitTyConApp_maybe ty1
+ , Just ct <- lookupTM ty1 (unCtFamHeadMap $ inert_funeqs ics)
+ , ctPred ct `eqType` pty
+ = Just ct
+ lkp_ics (IrredPred {})
+ = find (\ct -> ctPred ct `eqType` pty) (bagToList (inert_irreds ics))
+ lkp_ics _ = Nothing -- NB: No caching for IPs
\end{code}
+
+
%************************************************************************
%* *
%* The TcS solver monad *
@@ -623,10 +753,7 @@ added. This is initialised from the innermost implication constraint.
data TcSEnv
= TcSEnv {
tcs_ev_binds :: EvBindsVar,
- tcs_evvar_cache :: IORef EvVarCache,
- -- Evidence bindings and a cache from predicate types to the created evidence
- -- variables. The scope of the cache will be the same as the scope of tcs_ev_binds
-
+
tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
-- Global type bindings
@@ -640,11 +767,9 @@ data TcSEnv
tcs_inerts :: IORef InertSet, -- Current inert set
tcs_worklist :: IORef WorkList -- Current worklist
-
- -- TcSEnv invariant: the tcs_evvar_cache is a superset of tcs_inerts, tcs_worklist, tcs_ev_binds which must
- -- all be disjoint with each other.
}
+{- DELETEME
data EvVarCache
= EvVarCache { evc_cache :: TypeMap (EvVar,CtFlavor)
-- Map from PredTys to Evidence variables
@@ -666,7 +791,7 @@ origin_matches Any _ = True
origin_matches WhenSolved WhenSolved = True
origin_matches WhileFlattening WhileFlattening = True
origin_matches _ _ = False
-
+-}
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables,
@@ -764,8 +889,6 @@ runTcS :: SimplContext
-> TcM (a, Bag EvBind)
runTcS context untouch is wl tcs
= do { ty_binds_var <- TcM.newTcRef emptyVarEnv
- ; ev_cache_var <- TcM.newTcRef $
- EvVarCache { evc_cache = emptyTM, evc_flat_cache = emptyTM }
; ev_binds_var <- TcM.newTcEvBinds
; step_count <- TcM.newTcRef 0
@@ -773,7 +896,6 @@ runTcS context untouch is wl tcs
; wl_var <- TcM.newTcRef wl
; let env = TcSEnv { tcs_ev_binds = ev_binds_var
- , tcs_evvar_cache = ev_cache_var
, tcs_ty_binds = ty_binds_var
, tcs_context = context
, tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
@@ -804,16 +926,11 @@ runTcS context untouch is wl tcs
doWithInert :: InertSet -> TcS a -> TcS a
doWithInert inert (TcS action)
= TcS $ \env -> do { new_inert_var <- TcM.newTcRef inert
- ; orig_cache_var <- TcM.readTcRef (tcs_evvar_cache env)
- ; new_cache_var <- TcM.newTcRef orig_cache_var
- ; action (env { tcs_inerts = new_inert_var
- , tcs_evvar_cache = new_cache_var }) }
-
+ ; action (env { tcs_inerts = new_inert_var }) }
nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
= TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
- , tcs_evvar_cache = orig_evvar_cache_var
, tcs_untch = (_outer_range, outer_tcs)
, tcs_count = count
, tcs_ic_depth = idepth
@@ -829,13 +946,8 @@ nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
-- Inherit the inerts from the outer scope
; orig_inerts <- TcM.readTcRef inert_var
; new_inert_var <- TcM.newTcRef orig_inerts
-
- -- Inherit EvVar cache
- ; orig_evvar_cache <- TcM.readTcRef orig_evvar_cache_var
- ; evvar_cache <- TcM.newTcRef orig_evvar_cache
-
+
; let nest_env = TcSEnv { tcs_ev_binds = ref
- , tcs_evvar_cache = evvar_cache
, tcs_ty_binds = ty_binds
, tcs_untch = inner_untch
, tcs_count = count
@@ -871,12 +983,7 @@ tryTcS tcs
; ty_binds_var <- TcM.newTcRef emptyVarEnv
; ev_binds_var <- TcM.newTcEvBinds
- ; ev_binds_cache_var <- TcM.newTcRef (EvVarCache emptyTM emptyTM)
- -- Empty cache: Don't inherit cache from above, see
- -- Note [tryTcS for defaulting] in TcSimplify
-
; let env1 = env { tcs_ev_binds = ev_binds_var
- , tcs_evvar_cache = ev_binds_cache_var
, tcs_ty_binds = ty_binds_var
, tcs_inerts = is_var
, tcs_worklist = wl_var }
@@ -910,14 +1017,13 @@ updWorkListTcS_return f
; wrapTcS (TcM.writeTcRef wl_var new_work)
; return res }
-emitFrozenError :: CtFlavor -> EvVar -> SubGoalDepth -> TcS ()
+emitFrozenError :: CtFlavor -> SubGoalDepth -> TcS ()
-- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
-emitFrozenError fl ev depth
- = do { traceTcS "Emit frozen error" (ppr ev <+> dcolon <+> ppr (evVarPred ev))
+emitFrozenError fl depth
+ = do { traceTcS "Emit frozen error" (ppr (ctFlavPred fl))
; inert_ref <- getTcSInertsRef
; inerts <- wrapTcS (TcM.readTcRef inert_ref)
- ; let ct = CNonCanonical { cc_id = ev
- , cc_flavor = fl
+ ; let ct = CNonCanonical { cc_flavor = fl
, cc_depth = depth }
inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct }
; wrapTcS (TcM.writeTcRef inert_ref inerts_new) }
@@ -931,9 +1037,25 @@ getTcSContext = TcS (return . tcs_context)
getTcEvBinds :: TcS EvBindsVar
getTcEvBinds = TcS (return . tcs_ev_binds)
-getTcSEvVarCache :: TcS (IORef EvVarCache)
-getTcSEvVarCache = TcS (return . tcs_evvar_cache)
+getFlatCache :: TcS CtTypeMap
+getFlatCache = getTcSInerts >>= (return . unCtFamHeadMap . inert_flat_cache)
+
+updFlatCache :: Ct -> TcS ()
+-- Pre: constraint is a flat family equation (equal to a flatten skolem)
+updFlatCache flat_eq@(CFunEqCan { cc_flavor = fl, cc_fun = tc, cc_tyargs = xis })
+ = modifyInertTcS upd_inert_cache
+ where upd_inert_cache is = ((), is { inert_flat_cache = CtFamHeadMap new_fc })
+ where new_fc = alterTM pred_key upd_cache fc
+ fc = unCtFamHeadMap $ inert_flat_cache is
+ pred_key = mkTyConApp tc xis
+ upd_cache (Just ct) | cc_flavor ct `canSolve` fl = Just ct
+ upd_cache (Just _ct) = Just flat_eq
+ upd_cache Nothing = Just flat_eq
+updFlatCache other_ct = pprPanic "updFlatCache: non-family constraint" $
+ ppr other_ct
+
+{- DELETEME
flushFlatCache :: TcS ()
flushFlatCache
= do { cache_var <- getTcSEvVarCache
@@ -941,6 +1063,7 @@ flushFlatCache
; wrapTcS $ TcM.writeTcRef cache_var (the_cache { evc_flat_cache = emptyTM }) }
+
getTcSEvVarCacheMap :: TcS (TypeMap (EvVar,CtFlavor))
getTcSEvVarCacheMap = do { cache_var <- getTcSEvVarCache
; the_cache <- wrapTcS $ TcM.readTcRef cache_var
@@ -956,6 +1079,8 @@ setTcSEvVarCacheMap cache = do { cache_var <- getTcSEvVarCache
; orig_cache <- wrapTcS $ TcM.readTcRef cache_var
; let new_cache = orig_cache { evc_cache = cache }
; wrapTcS $ TcM.writeTcRef cache_var new_cache }
+-}
+
getUntouchables :: TcS TcsUntouchables
getUntouchables = TcS (return . tcs_untch)
@@ -966,16 +1091,11 @@ getTcSTyBinds = TcS (return . tcs_ty_binds)
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
-
getTcEvBindsMap :: TcS EvBindMap
getTcEvBindsMap
= do { EvBindsVar ev_ref _ <- getTcEvBinds
; wrapTcS $ TcM.readTcRef ev_ref }
-
-setEqBind :: EqVar -> TcCoercion -> CtFlavor -> TcS CtFlavor
-setEqBind eqv co fl = setEvBind eqv (EvCoercion co) fl
-
setWantedTyBind :: TcTyVar -> TcType -> TcS ()
-- Add a type binding
-- We never do this twice!
@@ -991,41 +1111,6 @@ setWantedTyBind tv ty
; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
-setEvBind :: EvVar -> EvTerm -> CtFlavor -> TcS CtFlavor
--- If the flavor is Solved, we cache the new evidence term inside the returned flavor
--- see Note [Optimizing Spontaneously Solved Coercions]
-setEvBind ev t fl
- = do { tc_evbinds <- getTcEvBinds
- ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t
-
-#ifdef DEBUG
- ; binds <- getTcEvBindsMap
- ; let cycle = any (reaches binds) (evVarsOfTerm t)
- ; when cycle (fail_if_co_loop binds)
-#endif
- ; return $
- case fl of
- Given gl (GivenSolved _)
- -> Given gl (GivenSolved (Just t))
- _ -> fl
- }
-
-#ifdef DEBUG
- where fail_if_co_loop binds
- = pprTrace "setEvBind" (vcat [ text "Cycle in evidence binds, evvar =" <+> ppr ev
- , ppr (evBindMapBinds binds) ]) $
- when (isEqVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!"))
-
- reaches :: EvBindMap -> Var -> Bool
- -- Does this evvar reach ev?
- reaches ebm ev0 = go ev0
- where go ev0
- | ev0 == ev = True
- | Just (EvBind _ evtrm) <- lookupEvBind ebm ev0
- = any go (evVarsOfTerm evtrm)
- | otherwise = False
-#endif
-
\end{code}
Note [Optimizing Spontaneously Solved Coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1153,11 +1238,12 @@ newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
newFlattenSkolemTyVar ty
- = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
- ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
- ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
- ; traceTcS "New Flatten Skolem Born" $
- (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
+ = do { tv <- wrapTcS $
+ do { uniq <- TcM.newUnique
+ ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
+ ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
+ ; traceTcS "New Flatten Skolem Born" $
+ ppr tv <+> text "[:= " <+> ppr ty <+> text "]"
; return tv }
-- Instantiations
@@ -1171,13 +1257,9 @@ instDFunTypes mb_inst_tys
inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
inst_tv (Right ty) = return ty
-instDFunConstraints :: TcThetaType -> CtFlavor -> TcS [EvVarCreated]
-instDFunConstraints preds fl
- = mapM (newEvVar fl) preds
-
instFlexiTcS :: TyVar -> TcS TcTyVar
--- Like TcM.instMetaTyVar but the variable that is created is always
--- touchable; we are supposed to guess its instantiation.
+-- Like TcM.instMetaTyVar but the variable that is created is
+-- always touchable; we are supposed to guess its instantiation.
-- See Note [Touchable meta type variables]
instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
@@ -1195,14 +1277,6 @@ isFlexiTcsTv tv
| MetaTv TcsTv _ <- tcTyVarDetails tv = True
| otherwise = False
-newKindConstraint :: TcTyVar -> Kind -> CtFlavor -> TcS EvVarCreated
--- Create new wanted CoVar that constrains the type to have the specified kind.
-newKindConstraint tv knd fl
- = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
- ; let ty_k = mkTyVarTy tv_k
- ; eqv <- newEqVar fl (mkTyVarTy tv) ty_k
- ; return eqv }
-
instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
instFlexiTcSHelper tvname tvkind
= wrapTcS $
@@ -1212,9 +1286,264 @@ instFlexiTcSHelper tvname tvkind
kind = tvkind
; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
--- Superclasses and recursive dictionaries
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- Creating and setting evidence variables and CtFlavors
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+data XEvTerm =
+ XEvTerm { ev_comp :: [EvVar] -> EvTerm
+ -- How to compose evidence
+ , ev_decomp :: EvVar -> [EvTerm]
+ -- How to decompose evidence
+ }
+
+data MaybeNew a = Fresh { mn_thing :: a }
+ | Cached { mn_thing :: a }
+
+isFresh :: MaybeNew a -> Bool
+isFresh (Fresh {}) = True
+isFresh _ = False
+
+setEvBind :: EvVar -> EvTerm -> TcS ()
+setEvBind ev t
+ = do { tc_evbinds <- getTcEvBinds
+ ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t
+
+#ifdef DEBUG
+ ; binds <- getTcEvBindsMap
+ ; let cycle = any (reaches binds) (evVarsOfTerm t)
+ ; when cycle (fail_if_co_loop binds)
+#endif
+ ; return () }
+
+#ifdef DEBUG
+ where fail_if_co_loop binds
+ = pprTrace "setEvBind" (vcat [ text "Cycle in evidence binds, evvar =" <+> ppr ev
+ , ppr (evBindMapBinds binds) ]) $
+ when (isEqVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!"))
+
+ reaches :: EvBindMap -> Var -> Bool
+ -- Does this evvar reach ev?
+ reaches ebm ev0 = go ev0
+ where go ev0
+ | ev0 == ev = True
+ | Just (EvBind _ evtrm) <- lookupEvBind ebm ev0
+ = any go (evVarsOfTerm evtrm)
+ | otherwise = False
+#endif
+
+newGivenEvVar :: TcPredType -> EvTerm -> TcS (MaybeNew EvVar)
+newGivenEvVar pty evterm
+ = do { is <- getTcSInerts
+ ; case lookupInInerts is pty of
+ Just ct | isGivenOrSolvedCt ct
+ -> return (Cached (ctId "newGivenEvVar" ct))
+ _ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
+ ; setEvBind new_ev evterm
+ ; return (Fresh new_ev) } }
+
+newWantedEvVar :: TcPredType -> TcS (MaybeNew EvVar)
+newWantedEvVar pty
+ = do { is <- getTcSInerts
+ ; case lookupInInerts is pty of
+ Just ct | not (isDerivedCt ct)
+ -> return (Cached (ctId "newWantedEvVar" ct))
+ _ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
+ ; return (Fresh new_ev) } }
+
+newDerived :: TcPredType -> TcS (MaybeNew TcPredType)
+newDerived pty
+ = do { is <- getTcSInerts
+ ; case lookupInInerts is pty of
+ Just {} -> return (Cached pty)
+ _ -> return (Fresh pty) }
+
+newKindConstraint :: TcTyVar -> Kind -> TcS (MaybeNew EvVar)
+-- Create new wanted CoVar that constrains the type to have the specified kind.
+newKindConstraint tv knd
+ = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
+ ; let ty_k = mkTyVarTy tv_k
+ ; newWantedEvVar (mkTcEqPred (mkTyVarTy tv) ty_k) }
+
+instDFunConstraints :: TcThetaType -> TcS [MaybeNew EvVar]
+instDFunConstraints = mapM newWantedEvVar
+
+
+xCtFlavor :: CtFlavor -- Original flavor
+ -> [TcPredType] -- New predicate types
+ -> XEvTerm -- Instructions about how to manipulate evidence
+ -> ([CtFlavor] -> TcS a) -- What to do with any remaining /fresh/ goals!
+ -> TcS a
+xCtFlavor = xCtFlavor_cache True
+
+
+xCtFlavor_cache :: Bool -- True = if wanted add to the solved bag!
+ -> CtFlavor -- Original flavor
+ -> [TcPredType] -- New predicate types
+ -> XEvTerm -- Instructions about how to manipulate evidence
+ -> ([CtFlavor] -> TcS a) -- What to do with any remaining /fresh/ goals!
+ -> TcS a
+xCtFlavor_cache _ (Given { flav_gloc = gl, flav_evar = evar }) ptys xev cont_with
+ = do { let ev_trms = ev_decomp xev evar
+ ; new_evars <- zipWithM newGivenEvVar ptys ev_trms
+ ; cont_with $
+ map (\x -> Given gl (mn_thing x)) (filter isFresh new_evars) }
+
+xCtFlavor_cache cache (Wanted { flav_wloc = wl, flav_evar = evar }) ptys xev cont_with
+ = do { new_evars <- mapM newWantedEvVar ptys
+ ; let evars = map mn_thing new_evars
+ evterm = ev_comp xev evars
+ ; setEvBind evar evterm
+ ; let solved_flav = Solved { flav_gloc = mkSolvedLoc wl UnkSkol
+ , flav_evar = evar }
+ ; when cache $ addToSolved (mkNonCanonical solved_flav)
+ ; cont_with $
+ map (\x -> Wanted wl (mn_thing x)) (filter isFresh new_evars) }
+
+xCtFlavor_cache _ (Derived { flav_wloc = wl }) ptys _xev cont_with
+ = do { ders <- mapM newDerived ptys
+ ; cont_with $
+ map (\x -> Derived wl (mn_thing x)) (filter isFresh ders) }
+
+ -- I am not sure I actually want to do this (e.g. from recanonicalizing a solved?)
+ -- but if we plan to use xCtFlavor for rewriting as well then I might as well add a case
+xCtFlavor_cache _ (Solved { flav_gloc = gl, flav_evar = evar }) ptys xev cont_with
+ = do { let ev_trms = ev_decomp xev evar
+ ; new_evars <- zipWithM newGivenEvVar ptys ev_trms
+ ; cont_with $
+ map (\x -> Solved gl (mn_thing x)) (filter isFresh new_evars) }
+
+rewriteCtFlavor :: CtFlavor
+ -> TcPredType -- new predicate
+ -> TcCoercion -- new ~ old
+ -> TcS (Maybe CtFlavor)
+rewriteCtFlavor = rewriteCtFlavor_cache True
+-- Returns Nothing only if rewriting has happened and the rewritten constraint is cached
+-- Returns Just if either (i) we rewrite by reflexivity or
+-- (ii) we rewrite and original not cached
+
+rewriteCtFlavor_cache :: Bool
+ -> CtFlavor
+ -> TcPredType -- new predicate
+ -> TcCoercion -- new ~ old
+ -> TcS (Maybe CtFlavor)
+-- If derived, don't even look at the coercion
+-- NB: this allows us to sneak away with ``error'' thunks for
+-- coercions that come from derived ids (which don't exist!)
+rewriteCtFlavor_cache _cache (Derived wl _pty_orig) pty_new _co
+ = newDerived pty_new >>= from_mn
+ where from_mn (Cached {}) = return Nothing
+ from_mn (Fresh {}) = return $ Just (Derived wl pty_new)
+
+rewriteCtFlavor_cache cache fl pty co
+ | isTcReflCo co
+ -- If just reflexivity then you may re-use the same variable as optimization
+ = return (Just $ case fl of
+ Derived wl _pty_orig -> Derived wl pty
+ Given gl ev -> Given gl (setVarType ev pty)
+ Wanted wl ev -> Wanted wl (setVarType ev pty)
+ Solved gl ev -> Solved gl (setVarType ev pty))
+ | otherwise
+ = xCtFlavor_cache cache fl [pty] (XEvTerm ev_comp ev_decomp) cont
+ where ev_comp [x] = EvCast x co
+ ev_comp _ = panic "Coercion can only have one subgoal"
+ ev_decomp x = [EvCast x (mkTcSymCo co)]
+ cont [] = return Nothing
+ cont [fl] = return $ Just fl
+ cont _ = panic "At most one constraint can be subgoal of coercion!"
+
+{- REFACTOR -- HERE HERE HERE
+rewriteCtFlavor :: Ct -- Original ct
+ -> PredType -- New predicate
+ -> TcCoercion -- ctPred ct ~ new_predicate
+ -> TcS (Maybe CtFlavor) -- Nothing if we already have a constraint
+ -- like this in the solved or in the inert set
+
+rewriteCtFlavor orig_ct pty co
+ | isReflCo co
+ -- If the coercion is just reflexivity then you may re-use the same variable
+ = return (Just $ case cc_flavor orig_ct of
+ Derived wl pty_orig -> Derived wl pty
+ Given gl ev -> Given gl (setVarType ev pty)
+ Wanted wl ev -> Wanted wl (setVarType ev pty)
+ Solved gl ev -> Solved gl (setVarType ev pty))
+ | otherwise
+ = new_ct_flav orig_ct (cc_flavor orig_ct) pty co
+ where
+ -- Given
+ new_ct_flav _orig_ct (Given { flav_gloc = gl, flav_evar = ev }) pty co
+ = do { new_ev <- wrapTcS $ TcM.newEvVar pty -- 1) Create new variable
+ ; setEvBind new_ev (mkEvCast ev co) -- 2) Set evidence
+ ; return $ Just (Given { flav_gloc = gl, flav_evar = new_ev }) }
+ -- 3) Return new given
+ -- Wanted
+ new_ct_flav orig_ct (Wanted { flav_wloc = wl, flav_evar = ev }) pty co
+ = do { is <- getTcSInerts
+ ; case lookupInInerts is pty of
+ Just ct | not (isDerived ct) -> -- Cached (and has a ctId)
+ do { setEvBind ev (mkCast (ctId ct) (mkSymCo co))
+ ; return Nothing }
+ _ -> -- Not Cached!
+ do { new_ev <- wrapTcS $ TcM.newEvVar pty -- 1) Create new variable
+ ; setEvBind ev (mkCast new_ev (mkSymCo co)) -- 2) Solve old from new
+ ; let gl = mkSolvedLoc wl UnkSkol
+ ; addToSolved (orig_ct { cc_flavor = Solved gl ev })
+ -- 3) Add old as solved
+ ; return (Just (Wanted { flav_wloc = wl -- 4) Return new wanted
+ , flav_evar = new_ev })) } }
+ -- Derived
+ new_ct_flav _orig_ct (Derived { flav_wloc = wl, flav_der_pty = _pty }) pty _co
+ = do { is <- getTcSInerts
+ ; case lookupInInerts is pty of
+ Just ct -> return Nothing -- Some other constraint already there
+ _ -> return $
+ Just (Derived {flav_wloc = wl, flav_der_pty = pty }) }
+
+ -- Solved
+ new_ct_flav _orig_ct (Solved { flav_gloc = gl, flav_evar = ev }) pty co
+ = do { new_ev <- wrapTcS $ TcM.newEvVar pty -- 1) Create new variable
+ ; setEvBind new_ev (mkEvCast ev co) -- 2) Set new evidence
+ ; let new_fl = Solved gl new_ev
+ ; return $ Just new_fl } -- 3) Return. NB: no need to addToSolved here
+
+
+
+
+newGivenFlavor :: GivenLoc -> TcPredType -> TcS CtFlavor
+newGivenFlavor gl pty
+ = do { new_ev <- wrapTcS $ TcM.newEvVar pty
+ ; return (Given gl pty) }
+
+newWantedFlavor :: WantedLoc
+ -> TcPredType
+ -> TcS (Either CtFlavor Ct)
+-- Returns either a new flavor or a cached constraint
+newWantedFlavor wl pty
+ = do { is <- getTcSInerts
+ ; case lookupInInerts is pty of
+ Just ct | not (isDerived ct) -> return (Right ct)
+ _ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
+ ; return $ Left (Wanted wl new_ev) } }
+
+newDerivedFlavor :: WantedLoc
+ -> TcPredType -> TcS CtFlavor
+newDerivedFlavor wl pty = return (Derived wl pty)
+
+
+newCtFlavor :: CtFlavor -> TcPredType -> TcS CtFlavor
+-- CtFlavor might not necessarily be fresh if constraint is cached
+newCtFlavor (Wanted { flav_wloc = wl }) pty
+ = do { lr <- newWantedFlavor wl pty
+ ; case lr of Left fl -> return fl
+ Right ct -> return (cc_flavor ct) }
+newCtFlavor (Given { flav_gloc = gl }) pty
+ = newGivenFlavor gl pty
+newCtFlavor (Derived { flav_wloc = wl }) pty
+ = newDerivedFlavor wl pty
+
+-}
+
+{- DELETEME
data EvVarCreated
= EvVarCreated { evc_is_new :: Bool -- True iff the variable was just created
, evc_the_evvar :: EvVar } -- The actual evidence variable could be cached or new
@@ -1223,6 +1552,57 @@ instance Outputable EvVarCreated where
ppr (EvVarCreated { evc_is_new = is_new, evc_the_evvar = ev })
= ppr ev <> parens (if is_new then ptext (sLit "new") else ptext (sLit "old"))
+
+
+
+newKindConstraint :: TcTyVar -> Kind -> CtFlavor -> TcS EvVarCreated
+-- Create new wanted CoVar that constrains the type to have the specified kind.
+newKindConstraint tv knd fl
+ = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
+ ; let ty_k = mkTyVarTy tv_k
+ ; eqv <- newEqVar fl (mkTyVarTy tv) ty_k
+ ; return eqv }
+
+
+setEqBind :: EqVar -> TcCoercion -> CtFlavor -> TcS CtFlavor
+setEqBind eqv co fl = setEvBind eqv (EvCoercion co) fl
+
+setEvBind :: EvVar -> EvTerm -> CtFlavor -> TcS CtFlavor
+-- If the flavor is Solved, we cache the new evidence term inside the returned flavor
+-- see Note [Optimizing Spontaneously Solved Coercions]
+setEvBind ev t fl
+ = do { tc_evbinds <- getTcEvBinds
+ ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t
+
+#ifdef DEBUG
+ ; binds <- getTcEvBindsMap
+ ; let cycle = any (reaches binds) (evVarsOfTerm t)
+ ; when cycle (fail_if_co_loop binds)
+#endif
+ ; return $
+ case fl of
+ Given gl (GivenSolved _)
+ -> Given gl (GivenSolved (Just t))
+ _ -> fl
+ }
+
+#ifdef DEBUG
+ where fail_if_co_loop binds
+ = pprTrace "setEvBind" (vcat [ text "Cycle in evidence binds, evvar =" <+> ppr ev
+ , ppr (evBindMapBinds binds) ]) $
+ when (isEqVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!"))
+
+ reaches :: EvBindMap -> Var -> Bool
+ -- Does this evvar reach ev?
+ reaches ebm ev0 = go ev0
+ where go ev0
+ | ev0 == ev = True
+ | Just (EvBind _ evtrm) <- lookupEvBind ebm ev0
+ = any go (evVarsOfTerm evtrm)
+ | otherwise = False
+#endif
+
+
isNewEvVar :: EvVarCreated -> Bool
isNewEvVar = evc_is_new
@@ -1355,10 +1735,9 @@ newEqVar fl ty1 ty2
; v <- newEvVar fl pred
; traceTcS "newEqVar" (ppr v <+> dcolon <+> ppr pred)
; return v }
-\end{code}
+-}
-\begin{code}
-- Matching and looking up classes and family instances
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1408,19 +1787,28 @@ matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{code}
-getInertEqs :: TcS (TyVarEnv (Ct,TcCoercion), InScopeSet)
+getInertEqs :: TcS (TyVarEnv Ct, InScopeSet)
getInertEqs = do { inert <- getTcSInerts
- ; return (inert_eqs inert, inert_eq_tvs inert) }
+ ; let ics = inert_cans inert
+ ; return (inert_eqs ics, inert_eq_tvs ics) }
+
+getCtCoercion :: EvBindMap -> Ct -> TcCoercion
+-- Precondition: A CTyEqCan which is either Wanted or Given, never Derived or Solved!
+getCtCoercion bs ct
+ = case lookupEvBind bs cc_id of
+ -- Given and bound to a coercion term
+ Just (EvBind _ (EvCoercion co)) -> co
+ -- NB: The constraint could have been rewritten due to spontaneous
+ -- unifications but because we are optimizing away mkRefls the evidence
+ -- variable may still have type (alpha ~ [beta]). The constraint may
+ -- however have a more accurate type (alpha ~ [Int]) (where beta ~ Int has
+ -- been previously solved by spontaneous unification). So if we are going
+ -- to use the evidence variable for rewriting other constraints, we'd better
+ -- make sure it's of the right type!
+ -- Always the ctPred type is more accurate, so we just pick that type
+
+ _ -> mkTcCoVarCo (setVarType cc_id (ctPred ct))
+
+ where cc_id = ctId "getCtCoercion" ct
-getCtCoercion :: Ct -> TcCoercion
--- Precondition: A CTyEqCan.
-getCtCoercion ct
- | Just (GivenSolved (Just (EvCoercion co))) <- maybe_given
- = co
- | otherwise
- = mkTcCoVarCo (setVarType (cc_id ct) (ctPred ct))
- -- NB: The variable could be rewritten by a spontaneously
- -- solved, so it is not safe to simply do a mkTcCoVarCo (cc_id ct)
- -- Instead we use the most accurate type, given by ctPred c
- where maybe_given = isGiven_maybe (cc_flavor ct)
\end{code}
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index eff1890d76..30376288b2 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -39,7 +39,7 @@ import BasicTypes ( RuleName )
import Control.Monad ( when )
import Outputable
import FastString
-import TrieMap
+import TrieMap () -- DV: for now
import DynFlags
\end{code}
@@ -603,7 +603,7 @@ simplifyRule name tv_bndrs lhs_wanted rhs_wanted
; traceTc "simplifyRule" $
vcat [ text "zonked_lhs" <+> ppr zonked_lhs
- , text "lhs_results" <+> ppr lhs_results
+ , text "lhs_results" <+> ppr lhs_results
, text "lhs_binds" <+> ppr lhs_binds
, text "rhs_wanted" <+> ppr rhs_wanted ]
@@ -611,8 +611,11 @@ simplifyRule name tv_bndrs lhs_wanted rhs_wanted
-- Don't quantify over equalities (judgement call here)
; let (eqs, dicts) = partitionBag (isEqPred . ctPred)
(wc_flat lhs_results)
- lhs_dicts = map cc_id (bagToList dicts)
+ lhs_dicts = map (ctId "tcSimplify") (bagToList dicts)
-- Dicts and implicit parameters
+ -- NB: dicts come from lhs_results which
+ -- are all Wanted, hence have ids, hence
+ -- it's fine to call ctId on them
-- Fail if we have not got down to unsolved flats
; ev_binds_var <- newTcEvBinds
@@ -808,17 +811,21 @@ simpl_loop n implics
; inerts <- getTcSInerts
; let ((_,unsolved_flats),_) = extractUnsolved inerts
+ {- DELETEME
; ecache_pre <- getTcSEvVarCacheMap
; let pr = ppr ((\k z m -> foldTM k m z) (:) [] ecache_pre)
; traceTcS "ecache_pre" $ pr
-
+ -}
+
; improve_eqs <- if not (isEmptyBag implic_eqs)
then return implic_eqs
else applyDefaultingRules unsolved_flats
+ {- DELETEME
; ecache_post <- getTcSEvVarCacheMap
; let po = ppr ((\k z m -> foldTM k m z) (:) [] ecache_post)
; traceTcS "ecache_po" $ po
+ -}
; traceTcS "solveWanteds: simpl_loop end" $
vcat [ text "improve_eqs =" <+> ppr improve_eqs
@@ -865,7 +872,10 @@ solveNestedImplications implics
where givens_from_wanteds = foldrBag get_wanted []
get_wanted cc rest_givens
| pushable_wanted cc
- = let this_given = cc { cc_flavor = mkGivenFlavor (cc_flavor cc) UnkSkol }
+ = let fl = cc_flavor cc
+ wloc = flav_wloc fl
+ gfl = Given (mkGivenLoc wloc UnkSkol) (flav_evar fl)
+ this_given = cc { cc_flavor = gfl }
in this_given : rest_givens
| otherwise = rest_givens
@@ -1096,23 +1106,22 @@ solveCTyFunEqs cts
; return (niFixTvSubst ni_subst, unsolved_can_cts) }
where
- solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
- ; _ <- setEqBind cv (mkTcReflCo ty) $
- (Wanted $ panic "Met an already solved function equality!")
- ; return () -- Don't care about flavors etc this is
- -- the last thing happening
- }
-
+ solve_one (Wanted _ cv,tv,ty)
+ = setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
+ solve_one (Derived {}, tv, ty)
+ = setWantedTyBind tv ty
+ solve_one arg
+ = pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
------------
-type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
+type FunEqBinds = (TvSubstEnv, [(CtFlavor, TcTyVar, TcType)])
-- The TvSubstEnv is not idempotent, but is loop-free
-- See Note [Non-idempotent substitution] in Unify
emptyFunEqBinds :: FunEqBinds
emptyFunEqBinds = (emptyVarEnv, [])
-extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
-extendFunEqBinds (tv_subst, cv_binds) cv tv ty
- = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
+extendFunEqBinds :: FunEqBinds -> CtFlavor -> TcTyVar -> TcType -> FunEqBinds
+extendFunEqBinds (tv_subst, cv_binds) fl tv ty
+ = (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds)
------------
getSolvableCTyFunEqs :: TcsUntouchables
@@ -1124,8 +1133,7 @@ getSolvableCTyFunEqs untch cts
dflt_funeq :: (Cts, FunEqBinds) -> Ct
-> (Cts, FunEqBinds)
dflt_funeq (cts_in, feb@(tv_subst, _))
- (CFunEqCan { cc_id = cv
- , cc_flavor = fl
+ (CFunEqCan { cc_flavor = fl
, cc_fun = tc
, cc_tyargs = xis
, cc_rhs = xi })
@@ -1145,7 +1153,7 @@ getSolvableCTyFunEqs untch cts
, not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
-- Occurs check: see Note [Solving Family Equations], Point 2
= ASSERT ( not (isGivenOrSolved fl) )
- (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
+ (cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis))
dflt_funeq (cts_in, fun_eq_binds) ct
= (cts_in `extendCts` ct, fun_eq_binds)
@@ -1283,12 +1291,19 @@ defaultTyVar untch the_tv
, not (k `eqKind` default_k)
= tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
do { let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
- fl = Wanted loc
- ; eqv <- TcSMonad.newKindConstraint the_tv default_k fl
- ; if isNewEvVar eqv then
+ ; eqv <- TcSMonad.newKindConstraint the_tv default_k
+ ; case eqv of
+ Fresh x ->
+ return $ unitBag $
+ CNonCanonical { cc_flavor = Wanted loc x, cc_depth = 0 }
+ Cached _ -> return emptyBag }
+{- DELETEME
+ if isNewEvVar eqv then
return $ unitBag (CNonCanonical { cc_id = evc_the_evvar eqv
, cc_flavor = fl, cc_depth = 0 })
else return emptyBag }
+-}
+
| otherwise
= return emptyBag -- The common case
where
@@ -1364,12 +1379,16 @@ disambigGroup [] _grp
disambigGroup (default_ty:default_tys) group
= do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
- do { let der_flav = mk_derived_flavor (cc_flavor the_ct)
- ; derived_eq <- tryTcS $
+ do { derived_eq <- tryTcS $
-- I need a new tryTcS because we will call solveInteractCts below!
- do { eqv <- TcSMonad.newEqVar der_flav (mkTyVarTy the_tv) default_ty
- ; return [ CNonCanonical { cc_id = evc_the_evvar eqv
- , cc_flavor = der_flav, cc_depth = 0 } ] }
+ do { md <- newDerived (mkTcEqPred (mkTyVarTy the_tv) default_ty)
+ ; case md of
+ Cached _ -> return []
+ Fresh pty ->
+ -- flav_wloc because constraint is not Given/Solved!
+ let dfl = Derived (flav_wloc the_fl) pty
+ in return [ CNonCanonical { cc_flavor = dfl, cc_depth = 0 } ] }
+
; traceTcS "disambigGroup (solving) {"
(text "trying to solve constraints along with default equations ...")
; solveInteractCts (derived_eq ++ wanteds)
@@ -1392,10 +1411,8 @@ disambigGroup (default_ty:default_tys) group
; disambigGroup default_tys group } }
where
((the_ct,the_tv):_) = group
+ the_fl = cc_flavor the_ct
wanteds = map fst group
- mk_derived_flavor :: CtFlavor -> CtFlavor
- mk_derived_flavor (Wanted loc) = Derived loc
- mk_derived_flavor _ = panic "Asked to disambiguate given or derived!"
\end{code}
Note [Avoiding spurious errors]
@@ -1425,9 +1442,8 @@ newFlatWanteds orig theta
= do { loc <- getCtLoc orig
; mapM (inst_to_wanted loc) theta }
where inst_to_wanted loc pty
- = do { v <- newWantedEvVar pty
+ = do { v <- TcMType.newWantedEvVar pty
; return $
- CNonCanonical { cc_id = v
- , cc_flavor = Wanted loc
+ CNonCanonical { cc_flavor = Wanted loc v
, cc_depth = 0 } }
\end{code} \ No newline at end of file
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index b1767b860d..c3b939de2a 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -535,7 +535,7 @@ uType_defer items ty1 ty2
= ASSERT( not (null items) )
do { eqv <- newEq ty1 ty2
; loc <- getCtLoc (TypeEqOrigin (last items))
- ; emitFlat (mkNonCanonical eqv (Wanted loc))
+ ; emitFlat $ mkNonCanonical (Wanted loc eqv)
-- Error trace only
-- NB. do *not* call mkErrInfo unless tracing is on, because
View Lorry Controller Status