diff options
Diffstat (limited to 'compiler/typecheck/TcEvidence.hs')
| -rw-r--r-- | compiler/typecheck/TcEvidence.hs | 663 |
1 files changed, 142 insertions, 521 deletions
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index 18f162256d..032cc54730 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -13,50 +13,50 @@ module TcEvidence ( -- Evidence bindings TcEvBinds(..), EvBindsVar(..), EvBindMap(..), emptyEvBindMap, extendEvBinds, - lookupEvBind, evBindMapBinds, foldEvBindMap, + lookupEvBind, evBindMapBinds, foldEvBindMap, EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind, + sccEvBinds, evBindVar, EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors, EvLit(..), evTermCoercion, EvCallStack(..), EvTypeable(..), -- TcCoercion - TcCoercion(..), TcCoercionR, TcCoercionN, - LeftOrRight(..), pickLR, + TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole, + Role(..), LeftOrRight(..), pickLR, mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo, - mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo, + mkTcTyConAppCo, mkTcAppCo, mkTcFunCo, mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos, mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo, - tcDowngradeRole, mkTcTransAppCo, - mkTcAxiomRuleCo, mkTcPhantomCo, - tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, - isTcReflCo, getTcCoVar_maybe, - tcCoercionRole, eqVarRole, + tcDowngradeRole, + mkTcAxiomRuleCo, mkTcCoherenceLeftCo, mkTcCoherenceRightCo, mkTcPhantomCo, + mkTcKindCo, + tcCoercionKind, coVarsOfTcCo, + mkTcCoVarCo, + isTcReflCo, + tcCoercionRole, unwrapIP, wrapIP ) where #include "HsVersions.h" import Var +import CoAxiom import Coercion import PprCore () -- Instance OutputableBndr TyVar -import TypeRep -- Knows type representation import TcType import Type import TyCon import Class( Class ) -import CoAxiom import PrelNames +import DynFlags ( gopt, GeneralFlag(Opt_PrintExplicitCoercions) ) import VarEnv import VarSet import Name +import Pair import Util import Bag -import Pair -#if __GLASGOW_HASKELL__ < 709 -import Control.Applicative -import Data.Traversable (traverse, sequenceA) -#endif +import Digraph import qualified Data.Data as Data import Outputable import FastString @@ -71,483 +71,82 @@ Coercions have free variables of type (a ~# b): we call these CoVars. However, the type checker passes around equality evidence (boxed up) at type (a ~ b). -An TcCoercion is simply a Coercion whose free variables have the -boxed type (a ~ b). After we are done with typechecking the -desugarer finds the free variables, unboxes them, and creates a -resulting real Coercion with kosher free variables. - -We can use most of the Coercion "smart constructors" to build TcCoercions. -However, mkCoVarCo will not work! The equivalent is mkTcCoVarCo. - -The data type is similar to Coercion.Coercion, with the following -differences - * Most important, TcLetCo adds let-bindings for coercions. - This is what lets us unify two for-all types and generate - equality constraints underneath - - * The kind of a TcCoercion is t1 ~ t2 (resp. Coercible t1 t2) - of a Coercion is t1 ~# t2 (resp. t1 ~#R t2) - - * UnsafeCo aren't required, but we do have TcPhantomCo - - * Representation invariants are weaker: - - we are allowed to have type synonyms in TcTyConAppCo - - the first arg of a TcAppCo can be a TcTyConAppCo - - TcSubCo is not applied as deep as done with mkSubCo - Reason: they'll get established when we desugar to Coercion - - * TcAxiomInstCo has a [TcCoercion] parameter, and not a [Type] parameter. - This differs from the formalism, but corresponds to AxiomInstCo (see - [Coercion axioms applied to coercions]). - -Note [mkTcTransAppCo] -~~~~~~~~~~~~~~~~~~~~~ -Suppose we have - - co1 :: a ~R Maybe - co2 :: b ~R Int - -and we want - - co3 :: a b ~R Maybe Int - -This seems sensible enough. But, we can't let (co3 = co1 co2), because -that's ill-roled! Note that mkTcAppCo requires a *nominal* second coercion. - -The way around this is to use transitivity: - - co3 = (co1 <b>_N) ; (Maybe co2) :: a b ~R Maybe Int - -Or, it's possible everything is the other way around: - - co1' :: Maybe ~R a - co2' :: Int ~R b - -and we want +An TcCoercion is simply a Coercion whose free variables have may be either +boxed or unboxed. After we are done with typechecking the desugarer finds the +boxed free variables, unboxes them, and creates a resulting real Coercion with +kosher free variables. - co3' :: Maybe Int ~R a b - -then - - co3' = (Maybe co2') ; (co1' <b>_N) - -This is exactly what `mkTcTransAppCo` builds for us. Information for all -the arguments tends to be to hand at call sites, so it's quicker than -using, say, tcCoercionKind. -} -type TcCoercionN = TcCoercion -- A Nominal corecion ~N -type TcCoercionR = TcCoercion -- A Representational corecion ~R - -data TcCoercion - = TcRefl Role TcType - | TcTyConAppCo Role TyCon [TcCoercion] - | TcAppCo TcCoercion TcCoercion - | TcForAllCo TyVar TcCoercion - | TcCoVarCo EqVar - | TcAxiomInstCo (CoAxiom Branched) Int -- Int specifies branch number - [TcCoercion] -- See [CoAxiom Index] in Coercion.hs - -- This is number of types and coercions are expected to match to CoAxiomRule - -- (i.e., the CoAxiomRules are always fully saturated) - | TcAxiomRuleCo CoAxiomRule [TcType] [TcCoercion] - | TcPhantomCo TcType TcType - | TcSymCo TcCoercion - | TcTransCo TcCoercion TcCoercion - | TcNthCo Int TcCoercion - | TcLRCo LeftOrRight TcCoercion - | TcSubCo TcCoercion -- Argument is never TcRefl - | TcCastCo TcCoercion TcCoercion -- co1 |> co2 - | TcLetCo TcEvBinds TcCoercion - | TcCoercion Coercion -- embed a Core Coercion - deriving (Data.Data, Data.Typeable) +type TcCoercion = Coercion +type TcCoercionN = CoercionN -- A Nominal corecion ~N +type TcCoercionR = CoercionR -- A Representational corecion ~R +type TcCoercionP = CoercionP -- a phantom coercion + +mkTcReflCo :: Role -> TcType -> TcCoercion +mkTcSymCo :: TcCoercion -> TcCoercion +mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion +mkTcNomReflCo :: TcType -> TcCoercionN +mkTcRepReflCo :: TcType -> TcCoercionR +mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion +mkTcAppCo :: TcCoercion -> TcCoercionN -> TcCoercion +mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion +mkTcAxInstCo :: Role -> CoAxiom br -> BranchIndex + -> [TcType] -> [TcCoercion] -> TcCoercion +mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] + -> [TcCoercion] -> TcCoercionR +mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion +mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion +mkTcNthCo :: Int -> TcCoercion -> TcCoercion +mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion +mkTcSubCo :: TcCoercionN -> TcCoercionR +maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion +tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion +mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR +mkTcCoherenceLeftCo :: TcCoercion -> TcCoercionN -> TcCoercion +mkTcCoherenceRightCo :: TcCoercion -> TcCoercionN -> TcCoercion +mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP +mkTcKindCo :: TcCoercion -> TcCoercionN +mkTcCoVarCo :: CoVar -> TcCoercion + +tcCoercionKind :: TcCoercion -> Pair TcType +tcCoercionRole :: TcCoercion -> Role +coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet +isTcReflCo :: TcCoercion -> Bool + +mkTcReflCo = mkReflCo +mkTcSymCo = mkSymCo +mkTcTransCo = mkTransCo +mkTcNomReflCo = mkNomReflCo +mkTcRepReflCo = mkRepReflCo +mkTcTyConAppCo = mkTyConAppCo +mkTcAppCo = mkAppCo +mkTcFunCo = mkFunCo +mkTcAxInstCo = mkAxInstCo +mkTcUnbranchedAxInstCo = mkUnbranchedAxInstCo Representational +mkTcForAllCo = mkForAllCo +mkTcForAllCos = mkForAllCos +mkTcNthCo = mkNthCo +mkTcLRCo = mkLRCo +mkTcSubCo = mkSubCo +maybeTcSubCo = maybeSubCo +tcDowngradeRole = downgradeRole +mkTcAxiomRuleCo = mkAxiomRuleCo +mkTcCoherenceLeftCo = mkCoherenceLeftCo +mkTcCoherenceRightCo = mkCoherenceRightCo +mkTcPhantomCo = mkPhantomCo +mkTcKindCo = mkKindCo +mkTcCoVarCo = mkCoVarCo + +tcCoercionKind = coercionKind +tcCoercionRole = coercionRole +coVarsOfTcCo = coVarsOfCo +isTcReflCo = isReflCo -isEqVar :: Var -> Bool --- Is lifted coercion variable (only!) -isEqVar v = case tyConAppTyCon_maybe (varType v) of - Just tc -> tc `hasKey` eqTyConKey - Nothing -> False - -isTcReflCo_maybe :: TcCoercion -> Maybe TcType -isTcReflCo_maybe (TcRefl _ ty) = Just ty -isTcReflCo_maybe (TcCoercion co) = isReflCo_maybe co -isTcReflCo_maybe _ = Nothing - -isTcReflCo :: TcCoercion -> Bool -isTcReflCo (TcRefl {}) = True -isTcReflCo (TcCoercion co) = isReflCo co -isTcReflCo _ = False - -getTcCoVar_maybe :: TcCoercion -> Maybe CoVar -getTcCoVar_maybe (TcCoVarCo v) = Just v -getTcCoVar_maybe _ = Nothing - -mkTcReflCo :: Role -> TcType -> TcCoercion -mkTcReflCo = TcRefl - -mkTcNomReflCo :: TcType -> TcCoercion -mkTcNomReflCo = TcRefl Nominal - -mkTcRepReflCo :: TcType -> TcCoercion -mkTcRepReflCo = TcRefl Representational - -mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion -mkTcFunCo role co1 co2 = mkTcTyConAppCo role funTyCon [co1, co2] - -mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion -mkTcTyConAppCo role tc cos -- No need to expand type synonyms - -- See Note [TcCoercions] - | Just tys <- traverse isTcReflCo_maybe cos - = TcRefl role (mkTyConApp tc tys) -- See Note [Refl invariant] - - | otherwise = TcTyConAppCo role tc cos - --- Input coercion is Nominal --- mkSubCo will do some normalisation. We do not do it for TcCoercions, but --- defer that to desugaring; just to reduce the code duplication a little bit -mkTcSubCo :: TcCoercionN -> TcCoercionR -mkTcSubCo (TcRefl _ ty) - = TcRefl Representational ty -mkTcSubCo co - = ASSERT2( tcCoercionRole co == Nominal, ppr co) - TcSubCo co - --- See Note [Role twiddling functions] in Coercion --- | Change the role of a 'TcCoercion'. Returns 'Nothing' if this isn't --- a downgrade. -tcDowngradeRole_maybe :: Role -- desired role - -> Role -- current role - -> TcCoercion -> Maybe TcCoercion -tcDowngradeRole_maybe Representational Nominal = Just . mkTcSubCo -tcDowngradeRole_maybe Nominal Representational = const Nothing -tcDowngradeRole_maybe Phantom _ - = panic "tcDowngradeRole_maybe Phantom" - -- not supported (not needed at the moment) -tcDowngradeRole_maybe _ Phantom = const Nothing -tcDowngradeRole_maybe _ _ = Just - --- See Note [Role twiddling functions] in Coercion --- | Change the role of a 'TcCoercion'. Panics if this isn't a downgrade. -tcDowngradeRole :: Role -- ^ desired role - -> Role -- ^ current role - -> TcCoercion -> TcCoercion -tcDowngradeRole r1 r2 co - = case tcDowngradeRole_maybe r1 r2 co of - Just co' -> co' - Nothing -> pprPanic "tcDowngradeRole" (ppr r1 <+> ppr r2 <+> ppr co) - --- | If the EqRel is ReprEq, makes a TcSubCo; otherwise, does nothing. --- Note that the input coercion should always be nominal. -maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion -maybeTcSubCo NomEq = id -maybeTcSubCo ReprEq = mkTcSubCo - -mkTcAxInstCo :: Role -> CoAxiom br -> Int -> [TcType] -> TcCoercion -mkTcAxInstCo role ax index tys - | ASSERT2( not (role == Nominal && ax_role == Representational) , ppr (ax, tys) ) - arity == n_tys = tcDowngradeRole role ax_role $ - TcAxiomInstCo ax_br index rtys - | otherwise = ASSERT( arity < n_tys ) - tcDowngradeRole role ax_role $ - foldl TcAppCo (TcAxiomInstCo ax_br index (take arity rtys)) - (drop arity rtys) - where - n_tys = length tys - ax_br = toBranchedAxiom ax - branch = coAxiomNthBranch ax_br index - arity = length $ coAxBranchTyVars branch - ax_role = coAxiomRole ax - arg_roles = coAxBranchRoles branch - rtys = zipWith mkTcReflCo (arg_roles ++ repeat Nominal) tys - -mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercionR -mkTcAxiomRuleCo = TcAxiomRuleCo - -mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] -> TcCoercionR -mkTcUnbranchedAxInstCo ax tys = mkTcAxInstCo Representational ax 0 tys - -mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion --- No need to deal with TyConApp on the left; see Note [TcCoercions] --- Second coercion *must* be nominal -mkTcAppCo (TcRefl r ty1) (TcRefl _ ty2) = TcRefl r (mkAppTy ty1 ty2) -mkTcAppCo co1 co2 = TcAppCo co1 co2 - --- | Like `mkTcAppCo`, but allows the second coercion to be other than --- nominal. See Note [mkTcTransAppCo]. Role r3 cannot be more stringent --- than either r1 or r2. -mkTcTransAppCo :: Role -- ^ r1 - -> TcCoercion -- ^ co1 :: ty1a ~r1 ty1b - -> TcType -- ^ ty1a - -> TcType -- ^ ty1b - -> Role -- ^ r2 - -> TcCoercion -- ^ co2 :: ty2a ~r2 ty2b - -> TcType -- ^ ty2a - -> TcType -- ^ ty2b - -> Role -- ^ r3 - -> TcCoercion -- ^ :: ty1a ty2a ~r3 ty1b ty2b -mkTcTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3 --- How incredibly fiddly! Is there a better way?? - = case (r1, r2, r3) of - (_, _, Phantom) - -> mkTcPhantomCo (mkAppTy ty1a ty2a) (mkAppTy ty1b ty2b) - (_, _, Nominal) - -> ASSERT( r1 == Nominal && r2 == Nominal ) - mkTcAppCo co1 co2 - (Nominal, Nominal, Representational) - -> mkTcSubCo (mkTcAppCo co1 co2) - (_, Nominal, Representational) - -> ASSERT( r1 == Representational ) - mkTcAppCo co1 co2 - (Nominal, Representational, Representational) - -> go (mkTcSubCo co1) - (_ , _, Representational) - -> ASSERT( r1 == Representational && r2 == Representational ) - go co1 - where - go co1_repr - | Just (tc1b, tys1b) <- tcSplitTyConApp_maybe ty1b - , nextRole ty1b == r2 - = (co1_repr `mkTcAppCo` mkTcNomReflCo ty2a) `mkTcTransCo` - (mkTcTyConAppCo Representational tc1b - (zipWith mkTcReflCo (tyConRolesX Representational tc1b) tys1b - ++ [co2])) - - | Just (tc1a, tys1a) <- tcSplitTyConApp_maybe ty1a - , nextRole ty1a == r2 - = (mkTcTyConAppCo Representational tc1a - (zipWith mkTcReflCo (tyConRolesX Representational tc1a) tys1a - ++ [co2])) - `mkTcTransCo` - (co1_repr `mkTcAppCo` mkTcNomReflCo ty2b) - - | otherwise - = pprPanic "mkTcTransAppCo" (vcat [ ppr r1, ppr co1, ppr ty1a, ppr ty1b - , ppr r2, ppr co2, ppr ty2a, ppr ty2b - , ppr r3 ]) - -mkTcSymCo :: TcCoercion -> TcCoercion -mkTcSymCo co@(TcRefl {}) = co -mkTcSymCo (TcSymCo co) = co -mkTcSymCo co = TcSymCo co - -mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion -mkTcTransCo (TcRefl {}) co = co -mkTcTransCo co (TcRefl {}) = co -mkTcTransCo co1 co2 = TcTransCo co1 co2 - -mkTcNthCo :: Int -> TcCoercion -> TcCoercion -mkTcNthCo n (TcRefl r ty) = TcRefl r (tyConAppArgN n ty) -mkTcNthCo n co = TcNthCo n co - -mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion -mkTcLRCo lr (TcRefl r ty) = TcRefl r (pickLR lr (tcSplitAppTy ty)) -mkTcLRCo lr co = TcLRCo lr co - -mkTcPhantomCo :: TcType -> TcType -> TcCoercion -mkTcPhantomCo = TcPhantomCo - -mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion -mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys - -mkTcForAllCo :: Var -> TcCoercion -> TcCoercion --- note that a TyVar should be used here, not a CoVar (nor a TcTyVar) -mkTcForAllCo tv (TcRefl r ty) = ASSERT( isTyVar tv ) TcRefl r (mkForAllTy tv ty) -mkTcForAllCo tv co = ASSERT( isTyVar tv ) TcForAllCo tv co - -mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion -mkTcForAllCos tvs (TcRefl r ty) = ASSERT( all isTyVar tvs ) TcRefl r (mkForAllTys tvs ty) -mkTcForAllCos tvs co = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs - -mkTcCoVarCo :: EqVar -> TcCoercion --- ipv :: s ~ t (the boxed equality type) or Coercible s t (the boxed representational equality type) -mkTcCoVarCo ipv = TcCoVarCo ipv - -- Previously I checked for (ty ~ ty) and generated Refl, - -- but in fact ipv may not even (visibly) have a (t1 ~ t2) type, because - -- the constraint solver does not substitute in the types of - -- evidence variables as it goes. In any case, the optimisation - -- will be done in the later zonking phase - -tcCoercionKind :: TcCoercion -> Pair Type -tcCoercionKind co = go co - where - go (TcRefl _ ty) = Pair ty ty - go (TcLetCo _ co) = go co - go (TcCastCo _ co) = case getEqPredTys (pSnd (go co)) of - (ty1,ty2) -> Pair ty1 ty2 - go (TcTyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos) - go (TcAppCo co1 co2) = mkAppTy <$> go co1 <*> go co2 - go (TcForAllCo tv co) = mkForAllTy tv <$> go co - go (TcCoVarCo cv) = eqVarKind cv - go (TcAxiomInstCo ax ind cos) - = let branch = coAxiomNthBranch ax ind - tvs = coAxBranchTyVars branch - Pair tys1 tys2 = sequenceA (map go cos) - in ASSERT( cos `equalLength` tvs ) - Pair (substTyWith tvs tys1 (coAxNthLHS ax ind)) - (substTyWith tvs tys2 (coAxBranchRHS branch)) - go (TcPhantomCo ty1 ty2) = Pair ty1 ty2 - go (TcSymCo co) = swap (go co) - go (TcTransCo co1 co2) = Pair (pFst (go co1)) (pSnd (go co2)) - go (TcNthCo d co) = tyConAppArgN d <$> go co - go (TcLRCo lr co) = (pickLR lr . tcSplitAppTy) <$> go co - go (TcSubCo co) = go co - go (TcAxiomRuleCo ax ts cs) = - case coaxrProves ax ts (map tcCoercionKind cs) of - Just res -> res - Nothing -> panic "tcCoercionKind: malformed TcAxiomRuleCo" - go (TcCoercion co) = coercionKind co - -eqVarRole :: EqVar -> Role -eqVarRole cv = getEqPredRole (varType cv) - -eqVarKind :: EqVar -> Pair Type -eqVarKind cv - | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv) - = ASSERT(tc `hasKey` eqTyConKey) - Pair ty1 ty2 - | otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv)) - -tcCoercionRole :: TcCoercion -> Role -tcCoercionRole = go - where - go (TcRefl r _) = r - go (TcTyConAppCo r _ _) = r - go (TcAppCo co _) = go co - go (TcForAllCo _ co) = go co - go (TcCoVarCo cv) = eqVarRole cv - go (TcAxiomInstCo ax _ _) = coAxiomRole ax - go (TcPhantomCo _ _) = Phantom - go (TcSymCo co) = go co - go (TcTransCo co1 _) = go co1 -- same as go co2 - go (TcNthCo n co) = let Pair ty1 _ = tcCoercionKind co - (tc, _) = tcSplitTyConApp ty1 - in nthRole (go co) tc n - go (TcLRCo _ _) = Nominal - go (TcSubCo _) = Representational - go (TcAxiomRuleCo c _ _) = coaxrRole c - go (TcCastCo c _) = go c - go (TcLetCo _ c) = go c - go (TcCoercion co) = coercionRole co - - -coVarsOfTcCo :: TcCoercion -> VarSet --- Only works on *zonked* coercions, because of TcLetCo -coVarsOfTcCo tc_co - = go tc_co - where - go (TcRefl _ _) = emptyVarSet - go (TcTyConAppCo _ _ cos) = mapUnionVarSet go cos - go (TcAppCo co1 co2) = go co1 `unionVarSet` go co2 - go (TcCastCo co1 co2) = go co1 `unionVarSet` go co2 - go (TcForAllCo _ co) = go co - go (TcCoVarCo v) = unitVarSet v - go (TcAxiomInstCo _ _ cos) = mapUnionVarSet go cos - go (TcPhantomCo _ _) = emptyVarSet - go (TcSymCo co) = go co - go (TcTransCo co1 co2) = go co1 `unionVarSet` go co2 - go (TcNthCo _ co) = go co - go (TcLRCo _ co) = go co - go (TcSubCo co) = go co - go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs - `minusVarSet` get_bndrs bs - go (TcLetCo {}) = emptyVarSet -- Harumph. This does legitimately happen in the call - -- to evVarsOfTerm in the DEBUG check of setEvBind - go (TcAxiomRuleCo _ _ cos) = mapUnionVarSet go cos - go (TcCoercion co) = -- the use of coVarsOfTcCo in dsTcCoercion will - -- fail if there are any proper, unlifted covars - ASSERT( isEmptyVarSet (coVarsOfCo co) ) - emptyVarSet - - -- We expect only coercion bindings, so use evTermCoercion - go_bind :: EvBind -> VarSet - go_bind (EvBind { eb_rhs =tm }) = go (evTermCoercion tm) - - get_bndrs :: Bag EvBind -> VarSet - get_bndrs = foldrBag (\ (EvBind { eb_lhs = b }) bs -> extendVarSet bs b) emptyVarSet - --- Pretty printing - -instance Outputable TcCoercion where - ppr = pprTcCo - -pprTcCo, pprParendTcCo :: TcCoercion -> SDoc -pprTcCo co = ppr_co TopPrec co -pprParendTcCo co = ppr_co TyConPrec co - -ppr_co :: TyPrec -> TcCoercion -> SDoc -ppr_co _ (TcRefl r ty) = angleBrackets (ppr ty) <> ppr_role r - -ppr_co p co@(TcTyConAppCo _ tc [_,_]) - | tc `hasKey` funTyConKey = ppr_fun_co p co - -ppr_co p (TcTyConAppCo r tc cos) = pprTcApp p ppr_co tc cos <> ppr_role r -ppr_co p (TcLetCo bs co) = maybeParen p TopPrec $ - sep [ptext (sLit "let") <+> braces (ppr bs), ppr co] -ppr_co p (TcAppCo co1 co2) = maybeParen p TyConPrec $ - pprTcCo co1 <+> ppr_co TyConPrec co2 -ppr_co p (TcCastCo co1 co2) = maybeParen p FunPrec $ - ppr_co FunPrec co1 <+> ptext (sLit "|>") <+> ppr_co FunPrec co2 -ppr_co p co@(TcForAllCo {}) = ppr_forall_co p co - -ppr_co _ (TcCoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv) - -ppr_co p (TcAxiomInstCo con ind cos) - = pprPrefixApp p (ppr (getName con) <> brackets (ppr ind)) (map pprParendTcCo cos) - -ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $ - ppr_co FunPrec co1 - <+> ptext (sLit ";") - <+> ppr_co FunPrec co2 -ppr_co p (TcPhantomCo t1 t2) = pprPrefixApp p (ptext (sLit "PhantomCo")) [pprParendType t1, pprParendType t2] -ppr_co p (TcSymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co] -ppr_co p (TcNthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co] -ppr_co p (TcLRCo lr co) = pprPrefixApp p (ppr lr) [pprParendTcCo co] -ppr_co p (TcSubCo co) = pprPrefixApp p (ptext (sLit "Sub")) [pprParendTcCo co] -ppr_co p (TcAxiomRuleCo co ts ps) = maybeParen p TopPrec - $ ppr_tc_axiom_rule_co co ts ps -ppr_co p (TcCoercion co) = pprPrefixApp p (text "Core co:") [ppr co] - -ppr_tc_axiom_rule_co :: CoAxiomRule -> [TcType] -> [TcCoercion] -> SDoc -ppr_tc_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps) - where - ppTs [] = Outputable.empty - ppTs [t] = ptext (sLit "@") <> ppr_type TopPrec t - ppTs ts = ptext (sLit "@") <> - parens (hsep $ punctuate comma $ map pprType ts) - - ppPs [] = Outputable.empty - ppPs [p] = pprParendTcCo p - ppPs (p : ps) = ptext (sLit "(") <+> pprTcCo p $$ - vcat [ ptext (sLit ",") <+> pprTcCo q | q <- ps ] $$ - ptext (sLit ")") - -ppr_role :: Role -> SDoc -ppr_role r = underscore <> pp_role - where pp_role = case r of - Nominal -> char 'N' - Representational -> char 'R' - Phantom -> char 'P' - -ppr_fun_co :: TyPrec -> TcCoercion -> SDoc -ppr_fun_co p co = pprArrowChain p (split co) - where - split :: TcCoercion -> [SDoc] - split (TcTyConAppCo _ f [arg,res]) - | f `hasKey` funTyConKey - = ppr_co FunPrec arg : split res - split co = [ppr_co TopPrec co] - -ppr_forall_co :: TyPrec -> TcCoercion -> SDoc -ppr_forall_co p ty - = maybeParen p FunPrec $ - sep [pprForAll tvs, ppr_co TopPrec rho] - where - (tvs, rho) = split1 [] ty - split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty - split1 tvs ty = (reverse tvs, ty) {- -************************************************************************ -* * +%************************************************************************ +%* * HsWrapper * * ************************************************************************ @@ -567,7 +166,7 @@ data HsWrapper -- So note that if wrap1 :: exp_arg <= act_arg -- wrap2 :: act_res <= exp_res -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res) - -- This isn't the same as for mkTcFunCo, but it has to be this way + -- This isn't the same as for mkFunCo, but it has to be this way -- because we can't use 'sym' to flip around these HsWrappers | WpCast TcCoercionR -- A cast: [] `cast` co @@ -576,9 +175,8 @@ data HsWrapper -- Evidence abstraction and application -- (both dictionaries and coercions) - | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable - | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint - + | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable + | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint -- Kind and Type abstraction and application | WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var) | WpTyApp KindOrType -- [] t the 't' is a type (not coercion) @@ -596,9 +194,9 @@ c1 <.> c2 = c1 `WpCompose` c2 mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> HsWrapper mkWpFun WpHole WpHole _ _ = WpHole -mkWpFun WpHole (WpCast co2) t1 _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2) -mkWpFun (WpCast co1) WpHole _ t2 = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2)) -mkWpFun (WpCast co1) (WpCast co2) _ _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2) +mkWpFun WpHole (WpCast co2) t1 _ = WpCast (mkFunCo Representational (mkRepReflCo t1) co2) +mkWpFun (WpCast co1) WpHole _ t2 = WpCast (mkFunCo Representational (mkSymCo co1) (mkRepReflCo t2)) +mkWpFun (WpCast co1) (WpCast co2) _ _ = WpCast (mkFunCo Representational (mkSymCo co1) co2) mkWpFun co1 co2 t1 t2 = WpFun co1 co2 t1 t2 mkWpCastR :: TcCoercionR -> HsWrapper @@ -621,7 +219,7 @@ mkWpEvApps :: [EvTerm] -> HsWrapper mkWpEvApps args = mk_co_app_fn WpEvApp args mkWpEvVarApps :: [EvVar] -> HsWrapper -mkWpEvVarApps vs = mkWpEvApps (map EvId vs) +mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map EvId vs) mkWpTyLams :: [TyVar] -> HsWrapper mkWpTyLams ids = mk_co_lam_fn WpTyLam ids @@ -668,7 +266,7 @@ data TcEvBinds deriving( Data.Typeable ) data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique - -- The Unique is only for debug printing + -- The Unique is for debug printing only instance Data.Data TcEvBinds where -- Placeholder; we can't travers into TcEvBinds @@ -727,22 +325,26 @@ data EvBind -- See Note [Tracking redundant constraints] in TcSimplify } +evBindVar :: EvBind -> EvVar +evBindVar = eb_lhs + mkWantedEvBind :: EvVar -> EvTerm -> EvBind mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm } + mkGivenEvBind :: EvVar -> EvTerm -> EvBind mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm } data EvTerm = EvId EvId -- Any sort of evidence Id, including coercions - | EvCoercion TcCoercion -- (Boxed) coercion bindings + | EvCoercion TcCoercion -- coercion bindings -- See Note [Coercion evidence terms] - | EvCast EvTerm TcCoercion -- d |> co, the coercion being at role representational + | EvCast EvTerm TcCoercionR -- d |> co | EvDFunApp DFunId -- Dictionary instance application - [Type] [EvId] + [Type] [EvTerm] | EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors -- See Note [Deferring coercion errors to runtime] @@ -765,7 +367,8 @@ data EvTerm -- | Instructions on how to make a 'Typeable' dictionary. -- See Note [Typeable evidence terms] data EvTypeable - = EvTypeableTyCon -- ^ Dictionary for @Typeable (T k1..kn)@ + = EvTypeableTyCon [EvTerm] -- ^ Dictionary for @Typeable (T k1..kn)@. + -- The EvTerms are for the arguments | EvTypeableTyApp EvTerm EvTerm -- ^ Dictionary for @Typeable (s t)@, @@ -806,7 +409,7 @@ inside can be EvIds. Eg Here for the (Typeable [a]) dictionary passed to typeRep we make evidence dl :: Typeable [a] = EvTypeable [a] - (EvTypeableTyApp EvTypeableTyCon (EvId d)) + (EvTypeableTyApp (EvTypeableTyCon []) (EvId d)) where d :: Typable a is the lambda-bound dictionary passed into f. @@ -814,14 +417,14 @@ is the lambda-bound dictionary passed into f. Note [Coercion evidence terms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ A "coercion evidence term" takes one of these forms - co_tm ::= EvId v where v :: t1 ~ t2 + co_tm ::= EvId v where v :: t1 ~# t2 | EvCoercion co | EvCast co_tm co We do quite often need to get a TcCoercion from an EvTerm; see 'evTermCoercion'. -INVARIANT: The evidence for any constraint with type (t1~t2) is +INVARIANT: The evidence for any constraint with type (t1 ~# t2) is a coercion evidence term. Consider for example [G] d :: F Int a If we have @@ -1037,17 +640,17 @@ isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds" evTermCoercion :: EvTerm -> TcCoercion -- Applied only to EvTerms of type (s~t) -- See Note [Coercion evidence terms] -evTermCoercion (EvId v) = mkTcCoVarCo v +evTermCoercion (EvId v) = mkCoVarCo v evTermCoercion (EvCoercion co) = co -evTermCoercion (EvCast tm co) = TcCastCo (evTermCoercion tm) co +evTermCoercion (EvCast tm co) = mkCoCast (evTermCoercion tm) co evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm) evVarsOfTerm :: EvTerm -> VarSet evVarsOfTerm (EvId v) = unitVarSet v -evVarsOfTerm (EvCoercion co) = coVarsOfTcCo co -evVarsOfTerm (EvDFunApp _ _ evs) = mkVarSet evs +evVarsOfTerm (EvCoercion co) = coVarsOfCo co +evVarsOfTerm (EvDFunApp _ _ evs) = mapUnionVarSet evVarsOfTerm evs evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v -evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co +evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfCo co evVarsOfTerm (EvDelayedError _ _) = emptyVarSet evVarsOfTerm (EvLit _) = emptyVarSet evVarsOfTerm (EvCallStack cs) = evVarsOfCallStack cs @@ -1056,6 +659,18 @@ evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev evVarsOfTerms :: [EvTerm] -> VarSet evVarsOfTerms = mapUnionVarSet evVarsOfTerm +-- | Do SCC analysis on a bag of 'EvBind's. +sccEvBinds :: Bag EvBind -> [SCC EvBind] +sccEvBinds bs = stronglyConnCompFromEdgedVertices edges + where + edges :: [(EvBind, EvVar, [EvVar])] + edges = foldrBag ((:) . mk_node) [] bs + + mk_node :: EvBind -> (EvBind, EvVar, [EvVar]) + mk_node b@(EvBind { eb_lhs = var, eb_rhs = term }) + = (b, var, varSetElems (evVarsOfTerm term `unionVarSet` + coVarsOfType (varType var))) + evVarsOfCallStack :: EvCallStack -> VarSet evVarsOfCallStack cs = case cs of EvCsEmpty -> emptyVarSet @@ -1065,7 +680,7 @@ evVarsOfCallStack cs = case cs of evVarsOfTypeable :: EvTypeable -> VarSet evVarsOfTypeable ev = case ev of - EvTypeableTyCon -> emptyVarSet + EvTypeableTyCon es -> evVarsOfTerms es EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2] EvTypeableTyLit e -> evVarsOfTerm e @@ -1084,7 +699,10 @@ pprHsWrapper :: SDoc -> HsWrapper -> SDoc -- In debug mode, print the wrapper -- otherwise just print what's inside pprHsWrapper doc wrap - = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc) + = sdocWithDynFlags $ \ dflags -> + getPprStyle (\ s -> if debugStyle s || gopt Opt_PrintExplicitCoercions dflags + then (help (add_parens doc) wrap False) + else doc ) where help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc -- True <=> appears in function application position @@ -1094,7 +712,7 @@ pprHsWrapper doc wrap help it (WpFun f1 f2 t1 _) = add_parens $ ptext (sLit "\\(x") <> dcolon <> ppr t1 <> ptext (sLit ").") <+> help (\_ -> it True <+> help (\_ -> ptext (sLit "x")) f1 True) f2 False help it (WpCast co) = add_parens $ sep [it False, nest 2 (ptext (sLit "|>") - <+> pprParendTcCo co)] + <+> pprParendCo co)] help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)] help it (WpTyApp ty) = no_parens $ sep [it True, ptext (sLit "@") <+> pprParendType ty] help it (WpEvLam id) = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False] @@ -1115,6 +733,9 @@ instance Outputable TcEvBinds where instance Outputable EvBindsVar where ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u) +instance Uniquable EvBindsVar where + getUnique (EvBindsVar _ u) = u + instance Outputable EvBind where ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given }) = sep [ pp_gw <+> ppr v @@ -1124,14 +745,14 @@ instance Outputable EvBind where -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing instance Outputable EvTerm where - ppr (EvId v) = ppr v - ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co - ppr (EvCoercion co) = ptext (sLit "CO") <+> ppr co - ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n)) - ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ] - ppr (EvLit l) = ppr l - ppr (EvCallStack cs) = ppr cs - ppr (EvDelayedError ty msg) = ptext (sLit "error") + ppr (EvId v) = ppr v + ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendCo co + ppr (EvCoercion co) = ptext (sLit "CO") <+> ppr co + ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n)) + ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ] + ppr (EvLit l) = ppr l + ppr (EvCallStack cs) = ppr cs + ppr (EvDelayedError ty msg) = ptext (sLit "error") <+> sep [ char '@' <> ppr ty, ppr msg ] ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> ptext (sLit "Typeable") <+> ppr ty @@ -1148,7 +769,7 @@ instance Outputable EvCallStack where = angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm instance Outputable EvTypeable where - ppr EvTypeableTyCon = ptext (sLit "TC") + ppr (EvTypeableTyCon ts) = ptext (sLit "TC") <+> ppr ts ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2) ppr (EvTypeableTyLit t1) = ptext (sLit "TyLit") <> ppr t1 @@ -1166,7 +787,7 @@ instance Outputable EvTypeable where unwrapIP :: Type -> CoercionR unwrapIP ty = case unwrapNewTyCon_maybe tc of - Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys + Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys [] Nothing -> pprPanic "unwrapIP" $ text "The dictionary for" <+> quotes (ppr tc) <+> text "is not a newtype!" |