summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/typecheck/TcCanonical.lhs224
-rw-r--r--compiler/typecheck/TcHsSyn.lhs44
-rw-r--r--compiler/typecheck/TcInteract.lhs349
-rw-r--r--compiler/typecheck/TcRnTypes.lhs21
-rw-r--r--compiler/typecheck/TcSMonad.lhs72
-rw-r--r--compiler/typecheck/TcSimplify.lhs6
-rw-r--r--compiler/types/Coercion.lhs1
7 files changed, 415 insertions, 302 deletions
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 16dea420ac..c1f679ee70 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -32,7 +32,7 @@ import Name ( Name )
import Var
import VarEnv
import Outputable
-import Control.Monad ( when, unless, zipWithM, zipWithM_, foldM )
+import Control.Monad ( when, unless, zipWithM, foldM )
import MonadUtils
import Control.Applicative ( (<|>) )
@@ -166,25 +166,29 @@ are again good.
canonicalize :: Ct -> TcS StopOrContinue
canonicalize ct@(CNonCanonical { cc_id = ev, cc_flavor = fl, cc_depth = d })
= do { traceTcS "canonicalize (non-canonical)" (ppr ct)
- ; canEvVar ev (classifyPredType (evVarPred ev)) d fl }
+ ; {-# SCC "canEvVar" #-}
+ canEvVar ev (classifyPredType (evVarPred ev)) d fl }
canonicalize (CDictCan { cc_id = ev, cc_depth = d
, cc_flavor = fl
, cc_class = cls
, cc_tyargs = xis })
- = canClass d fl ev cls xis -- Do not add any superclasses
+ = {-# SCC "canClass" #-}
+ canClass d fl ev cls xis -- Do not add any superclasses
canonicalize (CTyEqCan { cc_id = ev, cc_depth = d
, cc_flavor = fl
, cc_tyvar = tv
, cc_rhs = xi })
- = canEqLeafTyVarLeftRec d fl ev tv xi
+ = {-# SCC "canEqLeafTyVarLeftRec" #-}
+ canEqLeafTyVarLeftRec d fl ev tv xi
canonicalize (CFunEqCan { cc_id = ev, cc_depth = d
, cc_flavor = fl
, cc_fun = fn
, cc_tyargs = xis1
, cc_rhs = xi2 })
- = canEqLeafFunEqLeftRec d fl ev (fn,xis1) xi2
+ = {-# SCC "canEqLeafFunEqLeftRec" #-}
+ canEqLeafFunEqLeftRec d fl ev (fn,xis1) xi2
canonicalize (CIPCan { cc_id = ev, cc_depth = d
, cc_flavor = fl
@@ -225,16 +229,19 @@ canTuple :: SubGoalDepth -- Depth
canTuple d fl ev tys
= do { traceTcS "can_pred" (text "TuplePred!")
; evs <- zipWithM can_pred_tup_one tys [0..]
- ; when (isWanted fl) $ setEvBind ev (EvTupleMk evs)
- ; return Stop }
+ ; if (isWanted fl) then
+ do {_unused_fl <- setEvBind ev (EvTupleMk evs) fl
+ ; return Stop }
+ else return Stop }
where
can_pred_tup_one ty n
= do { evc <- newEvVar fl ty
- ; let ev' = evc_the_evvar evc
- ; when (isGivenOrSolved fl) $
- setEvBind ev' (EvTupleSel ev n)
- ; when (isNewEvVar evc) $
- addToWork (canEvVar ev' (classifyPredType (evVarPred ev')) d fl)
+ ; let ev' = evc_the_evvar evc
+ ; fl' <- if isGivenOrSolved fl then
+ setEvBind ev' (EvTupleSel ev n) fl
+ else return fl
+ ; when (isNewEvVar evc) $
+ addToWork (canEvVar ev' (classifyPredType (evVarPred ev')) d fl')
; return ev' }
-- Implicit Parameter Canonicalization
@@ -255,13 +262,13 @@ canIP d fl v nm ty
else do { evc <- newEvVar fl xi
; let v_new = evc_the_evvar evc
IPPred _ ip_xi = classifyPredType xi
- ; case fl of
- Wanted {} -> setEvBind v (EvCast v_new co)
- Given {} -> setEvBind v_new (EvCast v (mkSymCo co))
- Derived {} -> return ()
+ ; fl_new <- case fl of
+ Wanted {} -> setEvBind v (EvCast v_new co) fl
+ Given {} -> setEvBind v_new (EvCast v (mkSymCo co)) fl
+ Derived {} -> return fl
; if isNewEvVar evc then
continueWith $ CIPCan { cc_id = v_new
- , cc_flavor = fl, cc_ip_nm = nm
+ , cc_flavor = fl_new, cc_ip_nm = nm
, cc_ip_ty = ip_xi
, cc_depth = d }
else return Stop } }
@@ -301,13 +308,13 @@ canClass d fl v cls tys
-- Flattening happened
else do { evc <- newEvVar fl xi
; let v_new = evc_the_evvar evc
- ; case fl of
- Wanted {} -> setEvBind v (EvCast v_new co)
- Given {} -> setEvBind v_new (EvCast v (mkSymCo co))
- Derived {} -> return ()
+ ; fl_new <- case fl of
+ Wanted {} -> setEvBind v (EvCast v_new co) fl
+ Given {} -> setEvBind v_new (EvCast v (mkSymCo co)) fl
+ Derived {} -> return fl
-- Continue only if flat constraint is new
; if isNewEvVar evc then
- continueWith $ CDictCan { cc_id = v_new, cc_flavor = fl
+ continueWith $ CDictCan { cc_id = v_new, cc_flavor = fl_new
, cc_tyargs = xis, cc_class = cls
, cc_depth = d }
else return Stop } }
@@ -392,7 +399,8 @@ newSCWorkFromFlavored d ev flavor cls xis
; sc_vars <- mapM (newEvVar flavor) sc_theta
; sc_cts <- zipWithM (\scv ev_trm ->
do { let sc_evvar = evc_the_evvar scv
- ; setEvBind sc_evvar ev_trm
+ ; _unused_fl <- setEvBind sc_evvar ev_trm flavor
+ -- unused because it's the same
; return $
CNonCanonical { cc_id = sc_evvar
, cc_flavor = flavor
@@ -402,7 +410,7 @@ newSCWorkFromFlavored d ev flavor cls xis
; traceTcS "newSCWorkFromFlavored" $
text "Emitting superclass work:" <+> ppr sc_cts
; updWorkListTcS $ appendWorkListCt sc_cts }
- GivenSolved -> return ()
+ GivenSolved {} -> return ()
-- Seems very dangerous to add the superclasses for dictionaries that may be
-- partially solved because we may end up with evidence loops.
@@ -458,13 +466,13 @@ canIrred d fl v ty
-- canonicalise the resulting evidence variable
evc <- newEvVar fl xi
; let v' = evc_the_evvar evc
- ; case fl of
- Wanted {} -> setEvBind v (EvCast v' co)
- Given {} -> setEvBind v' (EvCast v (mkSymCo co))
- Derived {} -> return ()
+ ; fl' <- case fl of
+ Wanted {} -> setEvBind v (EvCast v' co) fl
+ Given {} -> setEvBind v' (EvCast v (mkSymCo co)) fl
+ Derived {} -> return fl
; if isNewEvVar evc then
- canEvVar v' (classifyPredType (evVarPred v')) d fl
+ canEvVar v' (classifyPredType (evVarPred v')) d fl'
else
return Stop }
}
@@ -588,16 +596,16 @@ flatten d fl (TyConApp tc tys)
Nothing
| isGivenOrSolved fl ->
do { rhs_xi_var <- newFlattenSkolemTy fam_ty
- ; eqv <- newGivenEqVar fl fam_ty rhs_xi_var (mkReflCo fam_ty)
+ ; (fl',eqv)
+ <- newGivenEqVar fl fam_ty rhs_xi_var (mkReflCo fam_ty)
; let ct = CFunEqCan { cc_id = eqv
- , cc_flavor = fl -- Given
+ , 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 (mkEqVarLCo eqv, rhs_xi_var, [ct]) }
| otherwise ->
-- Derived or Wanted: make a new /unification/ flatten variable
@@ -688,11 +696,11 @@ addToWork tcs_action = tcs_action >>= stop_or_emit
stop_or_emit (ContinueWith ct) = updWorkListTcS $
extendWorkListCt ct
-canEqEvVarsCreated :: SubGoalDepth -> CtFlavor
- -> [EvVarCreated] -> [Type] -> [Type]
+canEqEvVarsCreated :: SubGoalDepth
+ -> [CtFlavor] -> [EvVarCreated] -> [Type] -> [Type]
-> TcS StopOrContinue
canEqEvVarsCreated _d _fl [] _ _ = return Stop
-canEqEvVarsCreated d fl (evc:evcs) (ty1:tys1) (ty2:tys2)
+canEqEvVarsCreated d (fl:fls) (evc:evcs) (ty1:tys1) (ty2:tys2)
| isNewEvVar evc
= let do_one evc0 sy1 sy2
| isNewEvVar evc0
@@ -701,7 +709,7 @@ canEqEvVarsCreated d fl (evc:evcs) (ty1:tys1) (ty2:tys2)
in do { _unused <- zipWith3M do_one evcs tys1 tys2
; canEq d fl (evc_the_evvar evc) ty1 ty2 }
| otherwise
- = canEqEvVarsCreated d fl evcs tys1 tys2
+ = canEqEvVarsCreated d fls evcs tys1 tys2
canEqEvVarsCreated _ _ _ _ _ = return Stop
@@ -714,7 +722,8 @@ canEq :: SubGoalDepth
canEq _d fl eqv ty1 ty2
| eqType ty1 ty2 -- Dealing with equality here avoids
-- later spurious occurs checks for a~a
- = do { when (isWanted fl) (setEqBind eqv (mkReflCo ty1))
+ = do { when (isWanted fl) $
+ do { _ <- setEqBind eqv (mkReflCo ty1) fl; return () }
; return Stop }
-- Split up an equality between function types into two equalities.
@@ -723,16 +732,19 @@ canEq d fl eqv (FunTy s1 t1) (FunTy s2 t2)
; reseqv <- newEqVar fl t1 t2
; let argeqv_v = evc_the_evvar argeqv
reseqv_v = evc_the_evvar reseqv
- ; case fl of
+ ; (fl1,fl2) <- case fl of
Wanted {} ->
- setEqBind eqv (mkFunCo (mkEqVarLCo argeqv_v) (mkEqVarLCo reseqv_v))
+ do { _ <- setEqBind eqv (mkFunCo (mkEqVarLCo argeqv_v) (mkEqVarLCo reseqv_v)) fl
+ ; return (fl,fl) }
Given {} ->
- do { setEqBind argeqv_v (mkNthCo 0 (mkEqVarLCo eqv))
- ; setEqBind reseqv_v (mkNthCo 1 (mkEqVarLCo eqv)) }
+ do { fl1 <- setEqBind argeqv_v (mkNthCo 0 (mkEqVarLCo eqv)) fl
+ ; fl2 <- setEqBind reseqv_v (mkNthCo 1 (mkEqVarLCo eqv)) fl
+ ; return (fl1,fl2)
+ }
Derived {} ->
- return ()
+ return (fl,fl)
- ; canEqEvVarsCreated d fl [reseqv,argeqv] [t1,s1] [t2,s2] }
+ ; canEqEvVarsCreated d [fl2,fl1] [reseqv,argeqv] [t1,s1] [t2,s2] }
-- If one side is a variable, orient and flatten,
-- WITHOUT expanding type synonyms, so that we tend to
@@ -759,17 +771,18 @@ canEq d fl eqv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
; let kicos = map mkReflCo kis1
; argeqvs <- zipWithM (newEqVar fl) tys1' tys2'
- ; case fl of
+ ; fls <- case fl of
Wanted {} ->
- setEqBind eqv $
- mkTyConAppCo tc1 (kicos ++ map (mkEqVarLCo . evc_the_evvar) argeqvs)
+ do { _ <- setEqBind eqv
+ (mkTyConAppCo tc1 (kicos ++ map (mkEqVarLCo . evc_the_evvar) argeqvs)) fl
+ ; return (map (\_ -> fl) argeqvs) }
Given {} ->
let do_one argeqv n = setEqBind (evc_the_evvar argeqv)
- (mkNthCo n (mkEqVarLCo eqv))
- in zipWithM_ do_one argeqvs [(length kicos)..]
- Derived {} -> return ()
+ (mkNthCo n (mkEqVarLCo eqv)) fl
+ in zipWithM do_one argeqvs [(length kicos)..]
+ Derived {} -> return (map (\_ -> fl) argeqvs)
- ; canEqEvVarsCreated d fl argeqvs tys1' tys2' }
+ ; canEqEvVarsCreated d fls argeqvs tys1' tys2' }
-- See Note [Equality between type applications]
-- Note [Care with type applications] in TcUnify
@@ -793,9 +806,10 @@ canEq d fl eqv ty1 ty2
eqv2 = evc_the_evvar evc2
; when (isWanted fl) $
- setEqBind eqv (mkAppCo (mkEqVarLCo eqv1) (mkEqVarLCo eqv2))
+ do { _ <- setEqBind eqv (mkAppCo (mkEqVarLCo eqv1) (mkEqVarLCo eqv2)) fl
+ ; return () }
- ; canEqEvVarsCreated d fl [evc1,evc2] [s1,t1] [s2,t2] }
+ ; canEqEvVarsCreated d [fl,fl] [evc1,evc2] [s1,t1] [s2,t2] }
canEq d fl eqv s1@(ForAllTy {}) s2@(ForAllTy {})
@@ -1023,15 +1037,15 @@ canEqLeaf :: SubGoalDepth -- Depth
canEqLeaf d fl eqv s1 s2
| cls1 `re_orient` cls2
= do { traceTcS "canEqLeaf (reorienting)" $ ppr (evVarPred eqv)
- ; delCachedEvVar eqv
+ ; delCachedEvVar eqv fl
; evc <- newEqVar fl s2 s1
; let eqv' = evc_the_evvar evc
- ; case fl of
- Wanted {} -> setEqBind eqv (mkSymCo (mkEqVarLCo eqv'))
- Given {} -> setEqBind eqv' (mkSymCo (mkEqVarLCo eqv))
- Derived {} -> return ()
+ ; fl' <- case fl of
+ Wanted {} -> setEqBind eqv (mkSymCo (mkEqVarLCo eqv')) fl
+ Given {} -> setEqBind eqv' (mkSymCo (mkEqVarLCo eqv)) fl
+ Derived {} -> return fl
; if isNewEvVar evc then
- do { canEqLeafOriented d fl eqv' s2 s1 }
+ do { canEqLeafOriented d fl' eqv' s2 s1 }
else return Stop
}
| otherwise
@@ -1075,15 +1089,24 @@ canEqLeafFunEqLeftRec :: SubGoalDepth
-> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2
= do { traceTcS "canEqLeafFunEqLeftRec" $ ppr (evVarPred eqv)
- ; (xis1,cos1) <- flattenMany d fl tys1 -- Flatten type function arguments
- -- cos1 :: xis1 ~ tys1
+ ; (xis1,cos1) <-
+ {-# SCC "flattenMany" #-}
+ flattenMany d fl tys1 -- Flatten type function arguments
+ -- cos1 :: xis1 ~ tys1
; let no_flattening = all isReflCo cos1
- ; inerts <- getTcSInerts
- ; let fam_eqs = inert_funeqs inerts
+-- ; inerts <- getTcSInerts
+-- ; let fam_eqs = inert_funeqs inerts
- ; let is_cached = lookupFunEq (mkTyConApp fn xis1) fl fam_eqs
+ ; let flat_ty = mkTyConApp fn xis1
+
+ ; 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
+-}
; if no_flattening && isNothing is_cached then
canEqLeafFunEqLeft d fl eqv (fn,xis1) ty2
@@ -1093,23 +1116,24 @@ canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2
, Just (rhs_ty, ret_eq) <- is_cached
= (mkSymCo ret_eq, rhs_ty)
| Nothing <- is_cached -- Just flattening
- = (mkTyConAppCo fn cos1, mkTyConApp fn xis1)
+ = (mkTyConAppCo fn cos1, flat_ty)
| Just (rhs_ty, ret_eq) <- is_cached -- Both
= (mkSymCo ret_eq `mkTransCo` mkTyConAppCo fn cos1, rhs_ty)
| otherwise = panic "No flattening and not cached!"
- ; delCachedEvVar eqv
+ ; delCachedEvVar eqv fl
; evc <- newEqVar fl final_ty ty2
; let new_eqv = evc_the_evvar evc
- ; case fl of
- Wanted {} -> setEqBind eqv $
- mkSymCo final_co `mkTransCo` (mkEqVarLCo new_eqv)
- Given {} -> setEqBind new_eqv $ final_co `mkTransCo` (mkEqVarLCo eqv)
- Derived {} -> return ()
+ ; fl' <- case fl of
+ Wanted {} -> setEqBind eqv
+ (mkSymCo final_co `mkTransCo` (mkEqVarLCo new_eqv)) fl
+ Given {} -> setEqBind new_eqv (final_co `mkTransCo` (mkEqVarLCo eqv)) fl
+ Derived {} -> return fl
; if isNewEvVar evc then
if isNothing is_cached then
- canEqLeafFunEqLeft d fl new_eqv (fn,xis1) ty2
+ {-# SCC "canEqLeafFunEqLeft" #-}
+ canEqLeafFunEqLeft d fl' new_eqv (fn,xis1) ty2
else
- canEq (d+1) fl new_eqv final_ty ty2
+ canEq (d+1) fl' new_eqv final_ty ty2
else return Stop
}
}
@@ -1148,8 +1172,11 @@ canEqLeafFunEqLeft :: SubGoalDepth -- Depth
-> TcType -> TcS StopOrContinue
-- Precondition: No more flattening is needed for the LHS
canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
- = do { traceTcS "canEqLeafFunEqLeft" $ ppr (evVarPred eqv)
- ; (xi2,co2) <- flatten d fl s2 -- co2 :: xi2 ~ s2
+ = {-# SCC "canEqLeafFunEqLeft" #-}
+ do { traceTcS "canEqLeafFunEqLeft" $ ppr (evVarPred eqv)
+ ; (xi2,co2) <-
+ {-# SCC "flatten" #-}
+ flatten d fl s2 -- co2 :: xi2 ~ s2
; let no_flattening_happened = isReflCo co2
; if no_flattening_happened then
continueWith $ CFunEqCan { cc_id = eqv
@@ -1158,19 +1185,21 @@ canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
, cc_tyargs = xis1
, cc_rhs = xi2
, cc_depth = d }
- else do { delCachedEvVar eqv
- ; evc <- newEqVar fl (mkTyConApp fn xis1) xi2
+ else do { delCachedEvVar eqv fl
+ ; evc <-
+ {-# SCC "newEqVar" #-}
+ newEqVar fl (mkTyConApp fn xis1) xi2
; let new_eqv = evc_the_evvar evc -- F xis1 ~ xi2
new_cv = mkEqVarLCo new_eqv
cv = mkEqVarLCo eqv -- F xis1 ~ s2
- ; case fl of
- Wanted {} -> setEqBind eqv $ new_cv `mkTransCo` co2
- Given {} -> setEqBind new_eqv $ cv `mkTransCo` mkSymCo co2
- Derived {} -> return ()
+ ; fl' <- case fl of
+ Wanted {} -> setEqBind eqv (new_cv `mkTransCo` co2) fl
+ Given {} -> setEqBind new_eqv (cv `mkTransCo` mkSymCo co2) fl
+ Derived {} -> return fl
; if isNewEvVar evc then
do { continueWith $
CFunEqCan { cc_id = new_eqv
- , cc_flavor = fl
+ , cc_flavor = fl'
, cc_fun = fn
, cc_tyargs = xis1
, cc_rhs = xi2
@@ -1186,17 +1215,17 @@ canEqLeafTyVarLeftRec d fl eqv tv s2 -- eqv :: tv ~ s2
; (xi1,co1) <- flatten d fl (mkTyVarTy tv) -- co1 :: xi1 ~ tv
; if isReflCo co1 then
canEqLeafTyVarLeft d fl eqv tv s2
- else do { delCachedEvVar eqv
+ else do { delCachedEvVar eqv fl
; evc <- newEqVar fl xi1 s2 -- new_ev :: xi1 ~ s2
; let new_ev = evc_the_evvar evc
- ; case fl of
- Wanted {} -> setEqBind eqv $
- mkSymCo co1 `mkTransCo` mkEqVarLCo new_ev
- Given {} -> setEqBind new_ev $
- co1 `mkTransCo` mkEqVarLCo eqv
- Derived {} -> return ()
+ ; fl' <- case fl of
+ Wanted {} -> setEqBind eqv
+ (mkSymCo co1 `mkTransCo` mkEqVarLCo new_ev) fl
+ Given {} -> setEqBind new_ev
+ (co1 `mkTransCo` mkEqVarLCo eqv) fl
+ Derived {} -> return fl
; if isNewEvVar evc then
- do { canEq d fl new_ev xi1 s2 }
+ do { canEq d fl' new_ev xi1 s2 }
else return Stop
}
}
@@ -1219,8 +1248,9 @@ canEqLeafTyVarLeft d fl eqv tv s2 -- eqv : tv ~ s2
= True
| otherwise = False
; if is_same_tv then
- do { delCachedEvVar eqv
- ; when (isWanted fl) $ setEqBind eqv co
+ do { delCachedEvVar eqv fl
+ ; when (isWanted fl) $
+ do { _ <- setEqBind eqv co fl; return () }
; return Stop }
else
do { -- Do an occurs check, and return a possibly
@@ -1246,21 +1276,21 @@ canEqLeafTyVarLeft d fl eqv tv s2 -- eqv : tv ~ s2
, cc_depth = d }
else -- Flattening happened, in any case we have to create new variable
-- even if we report an occurs check error
- do { delCachedEvVar eqv
+ do { delCachedEvVar eqv fl
; evc <- newEqVar fl (mkTyVarTy tv) xi2'
; let eqv' = evc_the_evvar evc -- eqv' : tv ~ xi2'
cv = mkEqVarLCo eqv -- cv : tv ~ s2
cv' = mkEqVarLCo eqv' -- cv': tv ~ xi2'
- ; case fl of
- Wanted {} -> setEqBind eqv (cv' `mkTransCo` co) -- tv ~ xi2' ~ s2
- Given {} -> setEqBind eqv' (cv `mkTransCo` mkSymCo co) -- tv ~ s2 ~ xi2'
- Derived {} -> return ()
+ ; fl' <- case fl of
+ Wanted {} -> setEqBind eqv (cv' `mkTransCo` co) fl -- tv ~ xi2' ~ s2
+ Given {} -> setEqBind eqv' (cv `mkTransCo` mkSymCo co) fl -- tv ~ s2 ~ xi2'
+ Derived {} -> return fl
; if isNewEvVar evc then
if isNothing occ_check_result then
canEqFailure d fl eqv'
else continueWith CTyEqCan { cc_id = eqv'
- , cc_flavor = fl
+ , cc_flavor = fl'
, cc_tyvar = tv
, cc_rhs = xi2'
, cc_depth = d }
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 4f8cdb2a77..12bb2821fd 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -280,7 +280,10 @@ zonkEvBndr :: ZonkEnv -> EvVar -> TcM EvVar
-- Works for dictionaries and coercions
-- Does not extend the ZonkEnv
zonkEvBndr env var
- = do { ty <- zonkTcTypeToType env (varType var)
+ = do { let var_ty = varType var
+ ; ty <-
+ {-# SCC "zonkEvBndr_zonkTcTypeToType" #-}
+ zonkTcTypeToType env var_ty
; return (setVarType var ty) }
zonkEvVarOcc :: ZonkEnv -> EvVar -> EvVar
@@ -1103,7 +1106,8 @@ zonkEvBindsVar env (EvBindsVar ref _) = do { bs <- readMutVar ref
zonkEvBinds :: ZonkEnv -> Bag EvBind -> TcM (ZonkEnv, Bag EvBind)
zonkEvBinds env binds
- = fixM (\ ~( _, new_binds) -> do
+ = {-# SCC "zonkEvBinds" #-}
+ fixM (\ ~( _, new_binds) -> do
{ let env1 = extendIdZonkEnv env (collect_ev_bndrs new_binds)
; binds' <- mapBagM (zonkEvBind env1) binds
; return (env1, binds') })
@@ -1113,10 +1117,31 @@ zonkEvBinds env binds
add (EvBind var _) vars = var : vars
zonkEvBind :: ZonkEnv -> EvBind -> TcM EvBind
+
+
zonkEvBind env (EvBind var term)
- = do { var' <- zonkEvBndr env var
- ; term' <- zonkEvTerm env term
- ; return (EvBind var' term') }
+ = case term of
+ -- Fast path for reflexivity coercions:
+ EvCoercionBox co
+ | Just ty <- isReflCo_maybe co
+ ->
+ do { zty <- zonkTcTypeToType env ty
+ ; let var' = setVarType var (mkEqPred (zty,zty))
+ ; return (EvBind var' (EvCoercionBox (mkReflCo zty))) }
+
+ -- Fast path for variable-variable bindings
+ -- NB: could be optimized further! (e.g. SymCo cv)
+ | Just {} <- getCoVar_maybe co
+ -> do { term'@(EvCoercionBox (CoVarCo cv')) <- zonkEvTerm env term
+ ; let var' = setVarType var (varType cv')
+ ; return (EvBind var' term') }
+
+ -- Ugly safe and slow path
+ _ -> do { var' <- {-# SCC "zonkEvBndr" #-} zonkEvBndr env var
+ ; term' <- zonkEvTerm env term
+ ; return (EvBind var' term')
+ }
+
\end{code}
%************************************************************************
@@ -1186,9 +1211,14 @@ mkZonkTcTyVar unbound_mvar_fn unbound_ivar_fn
FlatSkol ty -> zonkType zonk_tv ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
- Flexi -> do { kind <- zonkType zonk_tv (tyVarKind tv)
+ Flexi -> do { kind <- {-# SCC "zonkKind1" #-}
+ zonkType zonk_tv (tyVarKind tv)
; unbound_mvar_fn (setTyVarKind tv kind) }
- Indirect ty -> zonkType zonk_tv ty }
+ Indirect ty -> do { zty <- zonkType zonk_tv ty
+ -- Small optimisation: shortern-out indirect steps
+ -- so that the old type may be more easily collected.
+ ; writeMutVar ref (Indirect zty)
+ ; return zty } }
zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
zonkTcTypeToType (ZonkEnv zonk_unbound_tyvar tv_env _id_env)
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 7fc6a966a4..18f4e552a4 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -51,6 +51,7 @@ import VarEnv
import qualified Data.Traversable as Traversable
import Control.Monad( when )
+import Pair ( pSnd )
import UniqFM
import FastString ( sLit )
import DynFlags
@@ -107,7 +108,7 @@ solveInteractCts cts
| Just (ev',fl') <- lookupTM pty acc_cache
, fl' `canSolve` fl
, isWanted fl
- = do { setEvBind ev (EvId ev')
+ = do { _ <- setEvBind ev (EvId ev') fl
; return (acc_cts,acc_cache) }
| otherwise -- If it's a given keep it in the work list, even if it exists in the cache!
= return (ct:acc_cts, alterTM pty (\_ -> Just (ev,fl)) acc_cache)
@@ -136,10 +137,12 @@ solveInteractWanted wevs
solveInteract :: TcS ()
-- Returns the final InertSet in TcS, WorkList will be eventually empty.
solveInteract
- = do { dyn_flags <- getDynFlags
+ = {-# SCC "solveInteract" #-}
+ do { dyn_flags <- getDynFlags
; let max_depth = ctxtStkDepth dyn_flags
solve_loop
- = do { sel <- selectNextWorkItem max_depth
+ = {-# SCC "solve_loop" #-}
+ do { sel <- selectNextWorkItem max_depth
; case sel of
NoWorkRemaining -- Done, successfuly (modulo frozen)
-> return ()
@@ -236,12 +239,7 @@ React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canoni
\begin{code}
thePipeline :: [(String,SimplifierStage)]
thePipeline = [ ("canonicalization", canonicalizationStage)
- -- If ContinueWith, will be canonical and fully rewritten wrt inert eqs
- , ("interact the inert eqs", interactWithInertEqsStage)
- -- If ContinueWith, will be wanted/derived eq or non-eq
- -- but can't rewrite not can be rewritten by the inerts
, ("spontaneous solve", spontaneousSolveStage)
- -- If ContinueWith its not spontaneously solved equality
, ("interact with inerts", interactWithInertsStage)
, ("top-level reactions", topReactionsStage) ]
\end{code}
@@ -292,70 +290,124 @@ spontaneousSolveStage :: SimplifierStage
spontaneousSolveStage workItem
= do { mSolve <- trySpontaneousSolve workItem
; spont_solve mSolve }
- where spont_solve SPCantSolve = continueWith workItem
- spont_solve (SPSolved workItem')
+ where spont_solve SPCantSolve
+ | isCTyEqCan workItem -- Unsolved equality
+ = do { kickOutRewritableInerts workItem -- NB: will add workItem in inerts
+ ; return Stop }
+ | otherwise
+ = continueWith workItem
+ spont_solve (SPSolved workItem') -- Post: workItem' must be equality
= do { bumpStepCountTcS
; traceFireTcS (cc_depth workItem) $
ptext (sLit "Spontaneous")
<+> parens (ppr (cc_flavor workItem)) <+> ppr workItem
- -- If original was /not/ given we may have to kick out now-rewritable inerts
- ; when (not (isGivenOrSolvedCt workItem)) $
- kickOutRewritableInerts workItem'
- -- Add solved guy in inerts anyway
- ; updInertSetTcS workItem'
- -- .. and Stop
+
+ -- NB: will add the item in the inerts
+ ; kickOutRewritableInerts workItem'
+ -- .. and Stop
; return Stop }
kickOutRewritableInerts :: Ct -> TcS ()
-- Pre: ct is a CTyEqCan
--- Post: the TcS monad is left with the thinner non-rewritable inerts; the
--- rewritable end up in the worklist
+-- Post: The TcS monad is left with the thinner non-rewritable inerts; but which
+-- contains the new constraint.
+-- The rewritable end up in the worklist
kickOutRewritableInerts ct
- = do { (wl,ieqs,solved_out) <- modifyInertTcS (kick_out_rewritable ct)
-
- -- Rewrite the inert_eqs on the spot!
- ; let ct_subst = unitVarEnv (cc_tyvar ct) (ct, mkEqVarLCo (cc_id ct))
- inscope = mkInScopeSet $ tyVarsOfCt ct
-
- ; new_ieqs <- rewriteInertEqsFromInertEq (ct_subst,inscope) ieqs
+ = {-# SCC "kickOutRewritableInerts" #-}
+ do { (wl,ieqs) <- {-# SCC "kick_out_rewritable" #-}
+ modifyInertTcS (kick_out_rewritable ct)
+
+ -- 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
+ | Just (GivenSolved (Just (EvCoercionBox co))) <- isGiven_maybe (cc_flavor ct)
+ = co
+ | otherwise
+ = mkEqVarLCo (cc_id ct)
+
+ ; new_ieqs <- {-# SCC "rewriteInertEqsFromInertEq" #-}
+ rewriteInertEqsFromInertEq (cc_tyvar ct,ct_coercion, cc_flavor ct) ieqs
; modifyInertTcS (\is -> ((), is { inert_eqs = new_ieqs }))
-
- -- Rewrite the rewritable solved on the spot and stick them back in the inerts
- ; _unused <- mapBagM (rewrite_solved (ct_subst,inscope)) solved_out
+ -- Step 2: Add the new guy in
+ ; updInertSetTcS ct
; traceTcS "Kick out" (ppr ct $$ ppr wl)
; updWorkListTcS (unionWorkList wl) }
- where rewrite_solved inert_eqs solved_ct
- = do { (new_ev,_) <- rewriteFromInertEqs inert_eqs fl ev
- ; mk_canonical new_ev }
- where fl = cc_flavor solved_ct
- ev = cc_id solved_ct
- d = cc_depth solved_ct
- mk_canonical new_ev
- -- A bit of an overkill to call the canonicalizer, but ok ...
- = do { let new_pty = evVarPred new_ev
- ; r <- canEvVar new_ev (classifyPredType new_pty) d fl
- ; case r of
- Stop -> return ()
- ContinueWith ct -> updInertSetTcS ct }
-
-
-rewriteInertEqsFromInertEq :: (TyVarEnv (Ct,Coercion), InScopeSet) -- A new substitution
- -> TyVarEnv (Ct,Coercion) -- The inert equalities
- -> TcS (TyVarEnv (Ct,Coercion)) -- The new inert equalities
-rewriteInertEqsFromInertEq the_subst ieqs = Traversable.mapM do_one ieqs
- where do_one (ct,co)
- | ev <- cc_id ct, fl <- cc_flavor ct
- = do { (new_ev,not_rewritten) <- rewriteFromInertEqs the_subst fl ev
- ; let EqPred _ xi = classifyPredType (evVarPred new_ev)
- ; if not_rewritten then
- return (ct,co) -- return the same
+rewriteInertEqsFromInertEq :: (TcTyVar,Coercion, CtFlavor) -- A new substitution
+ -> TyVarEnv (Ct,Coercion) -- All inert equalities
+ -> TcS (TyVarEnv (Ct,Coercion)) -- The new inert equalities
+rewriteInertEqsFromInertEq (subst_tv,subst_co, subst_fl) ieqs
+-- The goal: traverse the inert equalities:
+-- 1) If current inert element cannot itself rewrite subst_fl then:
+-- a) if it is rewritable by subst fl throw him out
+-- b) if it is not rewritable by subst keep him in as is
+-- 2) otherwise
+-- a) if it is rewritable by subst fl rewrite him on the spot
+-- b) if it is not rewritable by subst fl then keep him as is
+
+ = do { mieqs <- Traversable.mapM do_one ieqs -- mieqs :: TyVarEnv (Maybe (Ct,Coercion))
+ ; case Traversable.sequence mieqs of
+ Nothing -> return emptyVarEnv
+ Just final_ieqs -> return final_ieqs }
+
+ where do_one (ct,inert_co)
+ | (not (subst_fl `canRewrite` fl)) || isReflCo co
+ -- If the inert is not rewritable we just keep it
+ = return (Just (ct,inert_co))
+ -- Inert is definitely rewritable
+ | not (fl `canRewrite` subst_fl) -- But the inert cannot itself rewrite the subst item
+ -- so there is need for recanonicalization.
+ = do { updWorkListTcS (extendWorkListEq ct)
+ ; return Nothing }
+ | otherwise -- Or the inert can rewrite subst as well, so it's safe to rewrite on-the-spot
+ = do { let rhs' = pSnd (liftedCoercionKind co)
+ ; delCachedEvVar ev fl
+ ; evc <- newEqVar fl (mkTyVarTy tv) rhs'
+ ; let ev' = evc_the_evvar evc
+ ; let evco' = mkEqVarLCo ev'
+ ; fl' <- if isNewEvVar evc then
+ do { case fl of
+ Wanted {} -> setEqBind ev
+ (evco' `mkTransCo` mkSymCo co) fl
+ Given {} -> setEqBind ev'
+ (mkEqVarLCo ev `mkTransCo` co) fl
+ Derived {} -> return fl }
else
- return (ct { cc_id = new_ev, cc_rhs = xi }, mkEqVarLCo new_ev) }
+ if (isWanted fl) then
+ setEqBind ev (evco' `mkTransCo` mkSymCo co) fl
+ else
+ return fl
+
+ ; let ct' = ct { cc_id = ev', cc_flavor = fl', cc_rhs = rhs' }
+ ; return (Just (ct',evco')) }
+ where ev = cc_id ct
+ fl = cc_flavor ct
+ tv = cc_tyvar ct
+ rhs = cc_rhs ct
+ co = liftCoSubstWith [subst_tv] [subst_co] rhs
+
+
+
+-- (eqs_out, eqs_in) = partitionEqMap
+-- (\inert_ct -> (not (cc_flavor inert_ct `canRewrite` fl)) &&
+-- rewritable inert_ct) eqmap
+-- -- Why not just (rewritable_inert ct)? Check out Note [Delicate equality kick-out]
+
-kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,Coercion),Cts), InertSet)
+
+-- {-
+-- traceTcS "rewriteInertEqsFromInertEq" $
+-- vcat [ text "rewriting equality: " <+> ppr ct
+-- , text "from: " <+> ppr subst_co <+> text "of flavor: " <+> ppr subst_fl
+-- , text "can rewrite? " <+> ppr (subst_fl `canRewrite` fl) ]
+-- -}
+
+
+
+kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,Coercion)), InertSet)
+-- Returns ALL equalities, to be dealt with later
kick_out_rewritable ct (IS { inert_eqs = eqmap
, inert_eq_tvs = inscope
, inert_dicts = dictmap
@@ -364,15 +416,14 @@ kick_out_rewritable ct (IS { inert_eqs = eqmap
, inert_irreds = irreds
, inert_frozen = frozen
} )
- = ((kicked_out, eqs_in, feqs_out_solved `andCts` dicts_out_solved), remaining)
+ = ((kicked_out, eqmap), remaining)
where
-
- kicked_out = WorkList { wl_eqs = eqs_out
+ 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 = eqs_in
+ remaining = IS { inert_eqs = emptyVarEnv
, inert_eq_tvs = inscope -- keep the same, safe and cheap
, inert_dicts = dicts_in
, inert_ips = ips_in
@@ -383,39 +434,46 @@ kick_out_rewritable ct (IS { inert_eqs = eqmap
fl = cc_flavor ct
tv = cc_tyvar ct
-
- (eqs_out, eqs_in) = partitionEqMap
- (\inert_ct -> rewritable inert_ct &&
- not (cc_flavor inert_ct `canRewrite` fl)) eqmap
- -- Delicate:
- -- We want to throw out only the rewritables which cannot
- -- themselves rewrite the workitem. Because, what will remain
- -- in eqs_in, even if rewritable, can be readily substituted
- -- in-place from the new item, without dangers for occurs
- -- loops or further need for canonicalization.
+
+ (ips_out, ips_in) = partitionCCanMap rewritable ipmap
- (ips_out, ips_in) = partitionCCanMap rewritable ipmap
-
- (feqs_out_all, feqs_in) = partitionCtTypeMap rewritable funeqmap
- (feqs_out_solved, feqs_out) = partitionBag is_solved feqs_out_all
-
- (dicts_out_all, dicts_in) = partitionCCanMap rewritable dictmap
- (dicts_out_solved, dicts_out) = partitionBag is_solved dicts_out_all
+ (feqs_out, feqs_in) = partitionCtTypeMap rewritable funeqmap
+ (dicts_out, dicts_in) = partitionCCanMap rewritable dictmap
(irs_out, irs_in) = partitionBag rewritable irreds
(fro_out, fro_in) = partitionBag rewritable frozen
rewritable ct = (fl `canRewrite` cc_flavor ct) &&
(tv `elemVarSet` tyVarsOfCt ct)
+\end{code}
+
+Note [Delicate equality kick-out]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- is_solved ct
- | Just GivenSolved <- isGiven_maybe (cc_flavor ct)
- = True
- | otherwise = False
+Delicate:
+When kicking out rewritable constraints, it would be safe to simply
+kick out all rewritable equalities, but instead we only kick out those
+that, when rewritten, may result in occur-check errors. We rewrite the
+rest on the spot. Example:
-
+ WorkItem = [S] a ~ b
+ Inerts = { [W] b ~ [a] }
+Now at this point the work item cannot be further rewritten by the
+inert (due to the weaker inert flavor), so we are examining if we can
+instead rewrite the inert from the workitem. But if we rewrite it on
+the spot we have to recanonicalize because of the danger of occurs
+errors. On the other hand if the inert flavor was just as powerful or
+more powerful than the workitem flavor, the work-item could not have
+reached this stage (because it would have already been rewritten by
+the inert).
-
+The coclusion is: we kick out the 'dangerous' equalities that may
+require recanonicalization (occurs checks) and the rest we rewrite
+unconditionally without further checks, on-the-spot with function
+rewriteInertEqsFromInertEq.
+
+
+\begin{code}
data SPSolveResult = SPCantSolve
| SPSolved WorkItem
@@ -484,21 +542,7 @@ trySpontaneousEqTwoWay d eqv gw tv1 tv2
k1 = tyVarKind tv1
k2 = tyVarKind tv2
nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
-{-
--- Previous code below (before kind polymorphism and unification):
- -- | k1 `isSubKind` k2
- -- , nicer_to_update_tv2 = solveWithIdentity eqv gw tv2 (mkTyVarTy tv1)
- -- | k2 `isSubKind` k1
- -- = solveWithIdentity eqv gw tv1 (mkTyVarTy tv2)
- -- | otherwise -- None is a subkind of the other, but they are both touchable!
- -- = return SPCantSolve
- -- -- do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
- -- -- ; return SPError }
- -- where
- -- k1 = tyVarKind tv1
- -- k2 = tyVarKind tv2
- -- nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
--}
+
\end{code}
Note [Kind errors]
@@ -584,7 +628,7 @@ solveWithIdentity :: SubGoalDepth
-- workItem = the new Given constraint
solveWithIdentity d eqv wd tv xi
= do { traceTcS "Sneaky unification:" $
- vcat [text "Coercion variable: " <+> ppr wd,
+ 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)
@@ -593,36 +637,16 @@ solveWithIdentity d eqv wd tv xi
; setWantedTyBind tv xi
; let refl_xi = mkReflCo xi
- ; let solved_fl = mkSolvedFlavor wd UnkSkol
- ; eqv_given <- newGivenEqVar solved_fl (mkTyVarTy tv) xi refl_xi
+ ; let solved_fl = mkSolvedFlavor wd UnkSkol (EvCoercionBox refl_xi)
+ ; (_,eqv_given) <- newGivenEqVar solved_fl (mkTyVarTy tv) xi refl_xi
- ; when (isWanted wd) (setEqBind eqv 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 }) }
\end{code}
-*********************************************************************************
-* *
-* Interact with inert equalities *
-* *
-*********************************************************************************
-
-\begin{code}
-
-interactWithInertEqsStage :: WorkItem -> TcS StopOrContinue
-interactWithInertEqsStage ct
- | isCTyEqCan ct
- = do { kickOutRewritableInerts ct
- ; if isGivenOrSolved (cc_flavor ct) then updInertSetTcS ct >> return Stop
- else continueWith ct } -- If wanted or derived we may spontaneously solve him
- | isCNonCanonical ct
- = pprPanic "Interact with inerts eqs stage met non-canonical constraint!" (ppr ct)
- | otherwise
- = continueWith ct
-\end{code}
-
*********************************************************************************
* *
@@ -798,9 +822,8 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i
Given {} -> pprPanic "Unexpected given IP" (ppr workItem)
Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
Wanted {} ->
- do { setEvBind (cc_id workItem) $
- mkEvCast id1 (mkSymCo (mkTyConAppCo (ipTyCon nm1) [mkEqVarLCo (evc_the_evvar eqv)]))
- -- DV: Changing: used to be (mkSymCo (mkEqVarLCo eqv))
+ do { _ <- setEvBind (cc_id workItem)
+ (mkEvCast id1 (mkSymCo (mkTyConAppCo (ipTyCon nm1) [mkEqVarLCo (evc_the_evvar eqv)]))) wfl
; irWorkItemConsumed "IP/IP (solved by rewriting)" } }
doInteractWithInert (CFunEqCan { cc_id = eqv1, cc_flavor = fl1, cc_fun = tc1
@@ -808,13 +831,13 @@ doInteractWithInert (CFunEqCan { cc_id = eqv1, cc_flavor = fl1, cc_fun = tc1
(CFunEqCan { cc_id = eqv2, 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
+ , Just (GivenSolved {}) <- isGiven_maybe 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
+ , Just (GivenSolved {}) <- isGiven_maybe 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
@@ -839,40 +862,40 @@ rewriteEqLHS :: WhichComesFromInert -> (EqVar,Xi) -> (EqVar,SubGoalDepth,CtFlavo
-- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
-- See Note [Efficient Orientation] for that
rewriteEqLHS LeftComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2)
- = do { delCachedEvVar eqv2 -- Similarly to canonicalization!
+ = do { delCachedEvVar eqv2 gw -- Similarly to canonicalization!
; evc <- newEqVar gw xi2 xi1
; let eqv2' = evc_the_evvar evc
- ; case gw of
+ ; gw' <- case gw of
Wanted {}
- -> setEqBind eqv2 $
- mkEqVarLCo eqv1 `mkTransCo` mkSymCo (mkEqVarLCo eqv2')
- Given {}
- -> setEqBind eqv2' $
- mkSymCo (mkEqVarLCo eqv2) `mkTransCo` mkEqVarLCo eqv1
+ -> setEqBind eqv2
+ (mkEqVarLCo eqv1 `mkTransCo` mkSymCo (mkEqVarLCo eqv2')) gw
+ Given {}
+ -> setEqBind eqv2'
+ (mkSymCo (mkEqVarLCo eqv2) `mkTransCo` mkEqVarLCo eqv1) gw
Derived {}
- -> return ()
+ -> return gw
; when (isNewEvVar evc) $
updWorkListTcS (extendWorkListEq (CNonCanonical { cc_id = eqv2'
- , cc_flavor = gw
+ , cc_flavor = gw'
, cc_depth = d } ) ) }
rewriteEqLHS RightComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2)
- = do { delCachedEvVar eqv2 -- Similarly to canonicalization!
+ = do { delCachedEvVar eqv2 gw -- Similarly to canonicalization!
; evc <- newEqVar gw xi1 xi2
; let eqv2' = evc_the_evvar evc
- ; case gw of
+ ; gw' <- case gw of
Wanted {}
- -> setEqBind eqv2 $
- mkEqVarLCo eqv1 `mkTransCo` mkEqVarLCo eqv2'
+ -> setEqBind eqv2
+ (mkEqVarLCo eqv1 `mkTransCo` mkEqVarLCo eqv2') gw
Given {}
- -> setEqBind eqv2' $
- mkSymCo (mkEqVarLCo eqv1) `mkTransCo` mkEqVarLCo eqv2
+ -> setEqBind eqv2'
+ (mkSymCo (mkEqVarLCo eqv1) `mkTransCo` mkEqVarLCo eqv2) gw
Derived {}
- -> return ()
+ -> return gw
; when (isNewEvVar evc) $
updWorkListTcS (extendWorkListEq (CNonCanonical { cc_id = eqv2'
- , cc_flavor = gw
+ , cc_flavor = gw'
, cc_depth = d } ) ) }
solveOneFromTheOther :: String -- Info
@@ -891,14 +914,14 @@ 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
+ | Just (GivenSolved {}) <- isGiven_maybe 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) $ setEvBind wid ev_term
+ do { when (isWanted wfl) $ do { _ <- setEvBind wid ev_term wfl; return () }
-- Overwrite the binding, if one exists
-- If both are Given, we already have evidence; no need to duplicate
; irWorkItemConsumed ("Solved " ++ info) }
@@ -1350,30 +1373,32 @@ doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
doSolveFromInstance wtvs ev_term workItem
| null wtvs
= do { traceTcS "doTopReact/found nullary instance for" (ppr (cc_id workItem))
- ; setEvBind (cc_id workItem) ev_term
+ ; _ <- setEvBind (cc_id workItem) ev_term fl
; return $
SomeTopInt { tir_rule = "Dict/Top (solved, no new work)"
, tir_new_item = Stop } } -- Don't put him in the inerts
| otherwise
= do { traceTcS "doTopReact/found non-nullary instance for" $
ppr (cc_id workItem)
- ; setEvBind (cc_id workItem) ev_term
+ ; _ <- setEvBind (cc_id workItem) 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
+-- ; let _solved = workItem { cc_flavor = solved_fl }
+-- solved_fl = mkSolvedFlavor fl UnkSkol
; let ct_from_wev (EvVarX v fl)
= CNonCanonical { cc_id = v, cc_flavor = Wanted fl
, cc_depth = cc_depth workItem + 1 }
wtvs_cts = map ct_from_wev wtvs
; updWorkListTcS (appendWorkListCt wtvs_cts)
- ; return $
+ ; return $
SomeTopInt { tir_rule = "Dict/Top (solved, more work)"
- , tir_new_item = ContinueWith solved } } -- Cache in inerts the Solved item
+ , 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
+ | Just (GivenSolved {}) <- isGiven_maybe fl
= return NoTopInt -- If Solved, no more interactions should happen
-- Otherwise, it's a Given, Derived, or Wanted
@@ -1394,25 +1419,29 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl
; case fl of
Wanted {} -> do { evc <- newEqVar fl rhs_ty xi -- Wanted version
; let eqv' = evc_the_evvar evc
- ; setEqBind eqv (coe `mkTransCo` mkEqVarLCo eqv')
+ ; let coercion = coe `mkTransCo` mkEqVarLCo eqv'
+ ; _ <- setEqBind eqv coercion fl
; when (isNewEvVar evc) $
(let ct = CNonCanonical { cc_id = eqv'
, cc_flavor = fl
, cc_depth = cc_depth workItem + 1}
in updWorkListTcS (extendWorkListEq ct))
- ; let solved = workItem { cc_flavor = solved_fl }
- solved_fl = mkSolvedFlavor fl UnkSkol
+ ; let _solved = workItem { cc_flavor = solved_fl }
+ solved_fl = mkSolvedFlavor fl UnkSkol (EvCoercionBox coercion)
+
+ ; updateFlatCache eqv solved_fl tc args xi WhenSolved
; return $
SomeTopInt { tir_rule = "Fun/Top (solved, more work)"
- , tir_new_item = ContinueWith solved } }
+ , tir_new_item = Stop } }
+ -- , tir_new_item = ContinueWith solved } }
-- Cache in inerts the Solved item
- Given {} -> do { eqv' <- newGivenEqVar fl xi rhs_ty $
- mkSymCo (mkEqVarLCo eqv) `mkTransCo` coe
+ Given {} -> do { (fl',eqv') <- newGivenEqVar fl xi rhs_ty $
+ mkSymCo (mkEqVarLCo eqv) `mkTransCo` coe
; let ct = CNonCanonical { cc_id = eqv'
- , cc_flavor = fl
+ , cc_flavor = fl'
, cc_depth = cc_depth workItem + 1}
; updWorkListTcS (extendWorkListEq ct)
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index da2c8981ed..a7074e6207 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -71,7 +71,7 @@ module TcRnTypes(
SkolemInfo(..),
CtFlavor(..), pprFlavorArising, isWanted,
- isGivenOrSolved, isGiven_maybe,
+ isGivenOrSolved, isGiven_maybe, isSolved,
isDerived,
-- Pretty printing
@@ -1210,14 +1210,17 @@ data CtFlavor
data GivenKind
= GivenOrig -- Originates in some given, such as signature or pattern match
- | GivenSolved -- Is given as result of being solved, maybe provisionally on
- -- some other wanted constraints.
+ | 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]
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 (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]")
pprFlavorArising :: CtFlavor -> SDoc
pprFlavorArising (Derived wl) = pprArisingAt wl
@@ -1232,6 +1235,10 @@ isGivenOrSolved :: CtFlavor -> Bool
isGivenOrSolved (Given {}) = True
isGivenOrSolved _ = False
+isSolved :: CtFlavor -> Bool
+isSolved (Given _ (GivenSolved {})) = True
+isSolved _ = False
+
isGiven_maybe :: CtFlavor -> Maybe GivenKind
isGiven_maybe (Given _ gk) = Just gk
isGiven_maybe _ = Nothing
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index a777706f86..e1e1d96b8e 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -47,8 +47,6 @@ module TcSMonad (
-- Setting evidence variables
setEqBind,
- setIPBind,
- setDictBind,
setEvBind,
setWantedTyBind,
@@ -62,7 +60,7 @@ module TcSMonad (
-- Inerts
InertSet(..),
- getInertEqs, rewriteFromInertEqs, liftInertEqsTy,
+ getInertEqs, liftInertEqsTy,
emptyInert, getTcSInerts, updInertSet, extractUnsolved,
extractUnsolvedTcS, modifyInertTcS,
updInertSetTcS, partitionCCanMap, partitionEqMap,
@@ -125,7 +123,7 @@ import Bag
import MonadUtils
import VarSet
-import Pair ( pSnd )
+-- import Pair ( pSnd )
import FastString
import Util
@@ -493,9 +491,17 @@ updInertSet is item
| isCTyEqCan item
= let upd_err a b = pprPanic "updInertSet" $
vcat [text "Multiple inert equalities:", ppr a, ppr b]
+
+ -- If evidence is cached, pick it up from the flavor!
+ coercion
+ | Just (GivenSolved (Just (EvCoercionBox co))) <- isGiven_maybe (cc_flavor item)
+ = co
+ | otherwise
+ = mkEqVarLCo (cc_id item)
+
eqs' = extendVarEnv_C upd_err (inert_eqs is)
(cc_tyvar item)
- (item, mkEqVarLCo (cc_id item))
+ (item, coercion)
inscope' = extendInScopeSetSet (inert_eq_tvs is) (tyVarsOfCt item)
in is { inert_eqs = eqs', inert_eq_tvs = inscope' }
@@ -668,11 +674,11 @@ combineCtLoc (Derived loc ) _ = loc
combineCtLoc _ (Derived loc ) = loc
combineCtLoc _ _ = panic "combineCtLoc: both given"
-mkSolvedFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
+mkSolvedFlavor :: CtFlavor -> SkolemInfo -> EvTerm -> CtFlavor
-- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
-mkSolvedFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
-mkSolvedFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
-mkSolvedFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
+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
mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
@@ -1058,8 +1064,8 @@ getTcEvBindsMap
; wrapTcS $ TcM.readTcRef ev_ref }
-setEqBind :: EqVar -> LCoercion -> TcS ()
-setEqBind eqv co = setEvBind eqv (EvCoercionBox co)
+setEqBind :: EqVar -> LCoercion -> CtFlavor -> TcS CtFlavor
+setEqBind eqv co fl = setEvBind eqv (EvCoercionBox co) fl
setWantedTyBind :: TcTyVar -> TcType -> TcS ()
-- Add a type binding
@@ -1075,15 +1081,10 @@ setWantedTyBind tv ty
, text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
-setIPBind :: EvVar -> EvTerm -> TcS ()
-setIPBind = setEvBind
-
-setDictBind :: EvVar -> EvTerm -> TcS ()
-setDictBind = setEvBind
-setEvBind :: EvVar -> EvTerm -> TcS ()
--- Internal
-setEvBind ev t
+setEvBind :: EvVar -> EvTerm -> CtFlavor -> TcS CtFlavor
+-- If the flavor is Solved, we cache the new evidence term inside the returned flavor
+setEvBind ev t fl
= do { tc_evbinds <- getTcEvBinds
; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t
@@ -1092,6 +1093,11 @@ setEvBind ev t
; let cycle = any (reaches binds) (evterm_evs t)
; when cycle (fail_if_co_loop binds)
#endif
+ ; return $
+ case fl of
+ Given gl (GivenSolved _)
+ -> Given gl (GivenSolved (Just t))
+ _ -> fl
}
#ifdef DEBUG
@@ -1275,7 +1281,9 @@ newEvVar :: CtFlavor -> TcPredType -> TcS EvVarCreated
-- the call sites for this invariant to be quickly restored.
newEvVar fl pty
| isGivenOrSolved fl -- Create new variable and update the cache
- = do { eref <- getTcSEvVarCache
+ = do {
+{- We lose a lot of time if we enable this check:
+ eref <- getTcSEvVarCache
; ecache <- wrapTcS (TcM.readTcRef eref)
; case lookupTM pty (evc_cache ecache) of
Just (_,cached_fl)
@@ -1283,11 +1291,13 @@ newEvVar fl pty
-> pprTrace "Interesting: given newEvVar, missed caching opportunity!" empty $
return ()
_ -> return ()
- ; new <- forceNewEvVar fl pty
+-}
+ new <- forceNewEvVar fl pty
; return (EvVarCreated True new) }
| otherwise -- Otherwise lookup first
- = do { eref <- getTcSEvVarCache
+ = {-# SCC "newEvVarWanted" #-}
+ do { eref <- getTcSEvVarCache
; ecache <- wrapTcS (TcM.readTcRef eref)
; case lookupTM pty (evc_cache ecache) of
Just (cached_evvar, cached_flavor)
@@ -1338,9 +1348,10 @@ updateCache ecache (ev,fl,pty)
ecache' = alterTM pty (\_ -> Just (ev,fl)) $
evc_cache ecache
-delCachedEvVar :: EvVar -> TcS ()
-delCachedEvVar ev
- = do { eref <- getTcSEvVarCache
+delCachedEvVar :: EvVar -> CtFlavor -> TcS ()
+delCachedEvVar ev _fl
+ = {-# SCC "delCachedEvVarOther" #-}
+ do { eref <- getTcSEvVarCache
; ecache <- wrapTcS (TcM.readTcRef eref)
; wrapTcS $ TcM.writeTcRef eref (delFromCache ecache ev) }
@@ -1377,13 +1388,13 @@ pprEvVarCache tm = ppr (foldTM mk_pair tm [])
where mk_pair (co,_) cos = (co, liftedCoercionKind co) : cos
-newGivenEqVar :: CtFlavor -> TcType -> TcType -> Coercion -> TcS EvVar
+newGivenEqVar :: CtFlavor -> TcType -> TcType -> Coercion -> TcS (CtFlavor,EvVar)
-- Pre: fl is Given
newGivenEqVar fl ty1 ty2 co
= do { ecv <- newEqVar fl ty1 ty2
; let v = evc_the_evvar ecv -- Will be a new EvVar by post of newEvVar
- ; setEvBind v (EvCoercionBox co)
- ; return v }
+ ; fl' <- setEvBind v (EvCoercionBox co) fl
+ ; return (fl',v) }
newEqVar :: CtFlavor -> TcType -> TcType -> TcS EvVarCreated
newEqVar fl ty1 ty2
@@ -1447,6 +1458,7 @@ getInertEqs :: TcS (TyVarEnv (Ct,Coercion), InScopeSet)
getInertEqs = do { inert <- getTcSInerts
; return (inert_eqs inert, inert_eq_tvs inert) }
+{-- UNSAFE in the prsence of Solved flavors! Don't use!
rewriteFromInertEqs :: (TyVarEnv (Ct,Coercion), InScopeSet)
-- Precondition: Ct are CTyEqCans only!
-> CtFlavor
@@ -1458,7 +1470,7 @@ rewriteFromInertEqs (subst,inscope) fl v
; if isReflCo co then return (v,True)
else do { traceTcS "rewriteFromInertEqs" $
text "Original item =" <+> ppr v <+> dcolon <+> ppr (evVarPred v)
- ; delCachedEvVar v
+ ; delCachedEvVar v fl
; evc <- newEvVar fl (pSnd (liftedCoercionKind co))
; let v' = evc_the_evvar evc
; if isNewEvVar evc then
@@ -1476,7 +1488,7 @@ rewriteFromInertEqs (subst,inscope) fl v
_ -> return ()
; return (v',True) } -- As if rewriting never happened?
} }
-
+--}
-- See Note [LiftInertEqs]
liftInertEqsTy :: (TyVarEnv (Ct,Coercion),InScopeSet)
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 68082d4156..76e02e6629 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1046,7 +1046,11 @@ solveCTyFunEqs cts
; return (niFixTvSubst ni_subst, unsolved_can_cts) }
where
solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
- ; setEqBind cv (mkReflCo ty) }
+ ; _ <- setEqBind cv (mkReflCo ty) $
+ (Wanted $ panic "Met an already solved function equality!")
+ ; return () -- Don't care about flavors etc this is
+ -- the last thing happening
+ }
------------
type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index aaed359a10..17179fd2f1 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -22,6 +22,7 @@ module Coercion (
-- ** Functions over coercions
coVarKind,
coercionType, coercionKind, coercionKinds, isReflCo, liftedCoercionKind,
+ isReflCo_maybe,
mkCoercionType,
-- ** Constructing coercions
View Lorry Controller Status