-- | Strictness of evidence arguments to the wrapper function
dataConExStricts :: DataCon -> [HsBang]
-- Usually empty, so we don't bother to cache this
-dataConExStricts dc = map mk_dict_strict_mark $ (dcOtherTheta dc)
+dataConExStricts dc = map mk_dict_strict_mark $ (dataConTheta dc)
-- | Source-level arity of the data constructor
dataConSourceArity :: DataCon -> Arity
= DCIds Nothing wrk_id
where
(univ_tvs, ex_tvs, eq_spec,
- theta, orig_arg_tys, res_ty) = dataConFullSig data_con
+ other_theta, orig_arg_tys, res_ty) = dataConFullSig data_con
tycon = dataConTyCon data_con -- The representation TyCon (not family)
----------- Worker (algebraic data types only) --------------
-- extra constraints where necessary.
wrap_tvs = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs
res_ty_args = substTyVars (mkTopTvSubst eq_spec) univ_tvs
- ev_tys = mkPredTys theta
+ ev_tys = mkPredTys other_theta
wrap_ty = mkForAllTys wrap_tvs $
mkFunTys ev_tys $
mkFunTys orig_arg_tys $ res_ty
`setStrictnessInfo` Just wrap_sig
all_strict_marks = dataConExStricts data_con ++ dataConStrictMarks data_con
- wrap_sig = mkStrictSig (mkTopDmdType arg_dmds cpr_info)
- arg_dmds = map mk_dmd all_strict_marks
+ wrap_sig = mkStrictSig (mkTopDmdType wrap_arg_dmds cpr_info)
+ wrap_stricts = dropList eq_spec all_strict_marks
+ wrap_arg_dmds = map mk_dmd wrap_stricts
mk_dmd str | isBanged str = evalDmd
| otherwise = lazyDmd
-- The Cpr info can be important inside INLINE rhss, where the
mkLams ev_args $
mkLams id_args $
foldr mk_case con_app
- (zip (ev_args ++ id_args) all_strict_marks)
+ (zip (ev_args ++ id_args) wrap_stricts)
i3 []
+ -- The ev_args is the evidence arguments *other than* the eq_spec
+ -- Because we are going to apply the eq_spec args manually in the
+ -- wrapper
con_app _ rep_ids = wrapFamInstBody tycon res_ty_args $
Var wrk_id `mkTyApps` res_ty_args
mkReboxingAlt
:: [Unique] -- Uniques for the new Ids
-> DataCon
- -> [Var] -- Source-level args, including existential dicts
+ -> [Var] -- Source-level args, *including* all evidence vars
-> CoreExpr -- RHS
-> CoreAlt
-- Term variable case
go (arg:args) (str:stricts) us
| isMarkedUnboxed str
- =
- let (binds, unpacked_args') = go args stricts us'
+ = let (binds, unpacked_args') = go args stricts us'
(us', bind_rhs, unpacked_args) = reboxProduct us (idType arg)
in
(NonRec arg bind_rhs : binds, unpacked_args ++ unpacked_args')
body2 = freeVars body
body_fvs = freeVarsOf body2
-
freeVars (Cast expr co)
- = (freeVarsOf expr2 `unionFVs` cfvs, AnnCast expr2 co)
+ = (freeVarsOf expr2 `unionFVs` cfvs, AnnCast expr2 (cfvs, co))
where
expr2 = freeVars expr
cfvs = tyCoVarsOfCo co
; (s,t) <- addInScopeVar v (lintCoercion co)
; return (ForAllTy v s, ForAllTy v t) }
-lintCoercion co@(PredCo (ClassP cls cos))
- = do { (ss,ts) <- mapAndUnzipM lintCoercion cos
- ; check_co_app co (tyConKind (classTyCon cls)) ss
- ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
-
-lintCoercion (PredCo (IParam ip co))
- = do { (s,t) <- lintCoercion co
- ; return (PredTy (IParam ip s), PredTy (IParam ip t)) }
-
-lintCoercion (PredCo (EqPred c1 c2))
- = do { (s1,t1) <- lintCoercion c1
- ; (s2,t2) <- lintCoercion c2
- ; return (PredTy (EqPred s1 s2), PredTy (EqPred t1 t2)) }
-
lintCoercion (CoVarCo cv)
= do { checkTyCoVarInScope cv
; return (coVarKind cv) }
| AnnApp (AnnExpr bndr annot) (AnnExpr bndr annot)
| AnnCase (AnnExpr bndr annot) bndr Type [AnnAlt bndr annot]
| AnnLet (AnnBind bndr annot) (AnnExpr bndr annot)
- | AnnCast (AnnExpr bndr annot) Coercion
+ | AnnCast (AnnExpr bndr annot) (annot, Coercion)
+ -- Put an annotation on the (root of) the coercion
| AnnNote Note (AnnExpr bndr annot)
| AnnType Type
| AnnCoercion Coercion
deAnnotate' (AnnLit lit) = Lit lit
deAnnotate' (AnnLam binder body) = Lam binder (deAnnotate body)
deAnnotate' (AnnApp fun arg) = App (deAnnotate fun) (deAnnotate arg)
-deAnnotate' (AnnCast e co) = Cast (deAnnotate e) co
+deAnnotate' (AnnCast e (_,co)) = Cast (deAnnotate e) co
deAnnotate' (AnnNote note body) = Note note (deAnnotate body)
deAnnotate' (AnnLet bind body)
import CoreSyn
import HscTypes
import TyCon
-import Class
-import TysPrim( eqPredPrimTyCon )
+-- import Class
+-- import TysPrim( eqPredPrimTyCon )
import TypeRep
import Type
import PprExternalCore () -- Instances
make_co (TyConAppCo tc cos) = make_conAppCo (qtc tc) cos
make_co (AppCo c1 c2) = C.Tapp (make_co c1) (make_co c2)
make_co (ForAllCo tv co) = C.Tforall (make_tbind tv) (make_co co)
-make_co (PredCo (ClassP cls cos)) = make_conAppCo (qtc (classTyCon cls)) cos
-make_co (PredCo (IParam _ co)) = make_co co
-make_co (PredCo (EqPred co1 co2)) = make_conAppCo (qtc eqPredPrimTyCon) [co1,co2]
make_co (CoVarCo cv) = C.Tvar (make_var_id (coVarName cv))
make_co (AxiomInstCo cc cos) = make_conAppCo (qcc cc) cos
make_co (UnsafeCo t1 t2) = C.UnsafeCoercion (make_ty t1) (make_ty t2)
return (LitAlt lit, [], body)
-mkCoAlgCaseMatchResult :: Id -- Scrutinee
- -> Type -- Type of exp
- -> [(DataCon, [CoreBndr], MatchResult)] -- Alternatives
- -> MatchResult
+mkCoAlgCaseMatchResult
+ :: Id -- Scrutinee
+ -> Type -- Type of exp
+ -> [(DataCon, [CoreBndr], MatchResult)] -- Alternatives (bndrs *include* tyvars, dicts)
+ -> MatchResult
mkCoAlgCaseMatchResult var ty match_alts
| isNewTyCon tycon -- Newtype case; use a let
= ASSERT( null (tail match_alts) && null (tail arg_ids1) )
(coToIfaceType co2)
coToIfaceType (ForAllCo v co) = IfaceForAllTy (toIfaceTvBndr v)
(coToIfaceType co)
-coToIfaceType (PredCo pco) = IfacePredTy (toIfacePred coToIfaceType pco)
coToIfaceType (CoVarCo cv) = IfaceTyVar (toIfaceTyCoVar cv)
coToIfaceType (AxiomInstCo con cos) = IfaceCoConApp (IfaceCoAx (coAxiomName con))
(map coToIfaceType cos)
tcIfaceCo (IfaceCoConApp tc ts) = tcIfaceCoApp tc ts
tcIfaceCo (IfaceForAllTy tv t) = bindIfaceTyVar tv $ \ tv' ->
mkForAllCo tv' <$> tcIfaceCo t
-tcIfaceCo (IfacePredTy co) = mkPredCo <$> tcIfacePred tcIfaceCo co
+-- tcIfaceCo (IfacePredTy co) = mkPredCo <$> tcIfacePred tcIfaceCo co
+tcIfaceCo (IfacePredTy _) = panic "tcIfaceCo"
tcIfaceCoApp :: IfaceCoCon -> [IfaceType] -> IfL Coercion
tcIfaceCoApp IfaceReflCo [t] = Refl <$> tcIfaceType t
import Id
import IdInfo
import TyCon
+import Coercion( pprCoAxiom )
import TcType
import Name
import Outputable
ppr_ty_thing pefas _ (AnId id) = pprId pefas id
ppr_ty_thing pefas _ (ADataCon dataCon) = pprDataConSig pefas dataCon
ppr_ty_thing pefas show_me (ATyCon tyCon) = pprTyCon pefas show_me tyCon
-ppr_ty_thing _ _ (ACoAxiom _ ) = error "ppr_ty_thing (ACoCon)" -- BAY
+ppr_ty_thing _ _ (ACoAxiom ax) = pprCoAxiom ax
ppr_ty_thing pefas show_me (AClass cls) = pprClass pefas show_me cls
-- | Pretty-prints a 'TyThing' in context: that is, if the entity
pprTyThingHdr pefas (AnId id) = pprId pefas id
pprTyThingHdr pefas (ADataCon dataCon) = pprDataConSig pefas dataCon
pprTyThingHdr pefas (ATyCon tyCon) = pprTyConHdr pefas tyCon
-pprTyThingHdr _ (ACoAxiom _) = error "pprTyThingHdr (ACoCon)" -- BAY
+pprTyThingHdr _ (ACoAxiom ax) = pprCoAxiom ax
pprTyThingHdr pefas (AClass cls) = pprClassHdr pefas cls
pprTyConHdr :: PrintExplicitForalls -> TyCon -> SDoc
-> CoreExprWithFVs -- Input expr
-> CoreExpr -- Result
-fiExpr to_drop (_, AnnVar v) = mkCoLets' to_drop (Var v)
-
-fiExpr to_drop (_, AnnType ty) = ASSERT( null to_drop )
- Type ty
-fiExpr to_drop (_, AnnCoercion co) = ASSERT( null to_drop )
- Coercion co
-fiExpr to_drop (_, AnnCast expr co)
- = Cast (fiExpr to_drop expr) co -- Just float in past coercion
-
-fiExpr _ (_, AnnLit lit) = Lit lit
+fiExpr to_drop (_, AnnLit lit) = ASSERT( null to_drop ) Lit lit
+fiExpr to_drop (_, AnnType ty) = ASSERT( null to_drop ) Type ty
+fiExpr to_drop (_, AnnVar v) = mkCoLets' to_drop (Var v)
+fiExpr to_drop (_, AnnCoercion co) = mkCoLets' to_drop (Coercion co)
+fiExpr to_drop (_, AnnCast expr (fvs_co, co))
+ = mkCoLets' (drop_here ++ co_drop) $
+ Cast (fiExpr e_drop expr) co
+ where
+ [drop_here, e_drop, co_drop] = sepBindsByDropPoint False [freeVarsOf expr, fvs_co] to_drop
\end{code}
Applications: we do float inside applications, mainly because we
expr' <- lvlExpr ctxt_lvl env expr
return (Note note expr')
-lvlExpr ctxt_lvl env (_, AnnCast expr co) = do
+lvlExpr ctxt_lvl env (_, AnnCast expr (_, co)) = do
expr' <- lvlExpr ctxt_lvl env expr
return (Cast expr' co)
= do { e' <- lvlMFE strict_ctxt ctxt_lvl env e
; return (Note n e') }
-lvlMFE strict_ctxt ctxt_lvl env (_, AnnCast e co)
+lvlMFE strict_ctxt ctxt_lvl env (_, AnnCast e (_, co))
= do { e' <- lvlMFE strict_ctxt ctxt_lvl env e
; return (Cast e' co) }
---------------------
extendIdSubst :: SimplEnv -> Id -> SimplSR -> SimplEnv
extendIdSubst env@(SimplEnv {seIdSubst = subst}) var res
- = env {seIdSubst = extendVarEnv subst var res}
+ = ASSERT2( isId var && not (isCoVar var), ppr var )
+ env {seIdSubst = extendVarEnv subst var res}
extendTvSubst :: SimplEnv -> TyVar -> Type -> SimplEnv
extendTvSubst env@(SimplEnv {seTvSubst = subst}) var res
simplBinder env bndr
| isTyVar bndr = do { let (env', tv) = substTyVarBndr env bndr
; seqTyVar tv `seq` return (env', tv) }
- | isCoVar bndr = do { let (env', tv) = substCoVarBndr env bndr
- ; seqId tv `seq` return (env', tv) }
| otherwise = do { let (env', id) = substIdBndr env bndr
; seqId id `seq` return (env', id) }
; seqIds ids1 `seq` return env1 }
---------------
-substIdBndr :: SimplEnv
- -> InBndr -- Env and binder to transform
- -> (SimplEnv, OutBndr)
+substIdBndr :: SimplEnv -> InBndr -> (SimplEnv, OutBndr)
+-- Might be a coercion variable
+substIdBndr env bndr
+ | isCoVar bndr = substCoVarBndr env bndr
+ | otherwise = substNonCoVarIdBndr env bndr
+
+---------------
+substNonCoVarIdBndr
+ :: SimplEnv
+ -> InBndr -- Env and binder to transform
+ -> (SimplEnv, OutBndr)
-- Clone Id if necessary, substitute its type
-- Return an Id with its
-- * Type substituted
-- Similar to CoreSubst.substIdBndr, except that
-- the type of id_subst differs
-- all fragile info is zapped
-
-substIdBndr env@(SimplEnv { seInScope = in_scope, seIdSubst = id_subst })
- old_id
- = (env { seInScope = in_scope `extendInScopeSet` new_id,
+substNonCoVarIdBndr env@(SimplEnv { seInScope = in_scope, seIdSubst = id_subst })
+ old_id
+ = ASSERT2( not (isCoVar old_id), ppr old_id )
+ (env { seInScope = in_scope `extendInScopeSet` new_id,
seIdSubst = new_subst }, new_id)
where
id1 = uniqAway in_scope old_id
| CoerceIt -- C `cast` co
OutCoercion -- The coercion simplified
+ -- Invariant: never an identity coercion
SimplCont
| ApplyTo -- C arg
once, because FloatOut has gone to some trouble to extract them out.
Inlining them won't make the program run faster!
+Note [Do not inline CoVars unconditionally]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Coercion variables appear inside coercions, and have a separate
+substitution, so don't inline them via the IdSubst!
+
\begin{code}
preInlineUnconditionally :: SimplEnv -> TopLevelFlag -> InId -> InExpr -> Bool
preInlineUnconditionally env top_lvl bndr rhs
| isStableUnfolding (idUnfolding bndr) = False -- Note [InlineRule and preInlineUnconditionally]
| isTopLevel top_lvl && isBottomingId bndr = False -- Note [Top-level bottoming Ids]
| opt_SimplNoPreInlining = False
+ | isCoVar bndr = False -- Note [Do not inline CoVars unconditionally]
| otherwise = case idOccInfo bndr of
IAmDead -> True -- Happens in ((\x.1) v)
OneOcc in_lam True int_cxt -> try_once in_lam int_cxt
postInlineUnconditionally
:: SimplEnv -> TopLevelFlag
-> OutId -- The binder (an InId would be fine too)
+ -- (*not* a CoVar)
-> OccInfo -- From the InId
-> OutExpr
-> Unfolding
-> SimplM SimplEnv
simplNonRecX env bndr new_rhs
- | isDeadBinder bndr -- Not uncommon; e.g. case (a,b) of b { (p,q) -> p }
- = return env -- Here b is dead, and we avoid creating
- | Coercion co <- new_rhs
+ | isDeadBinder bndr -- Not uncommon; e.g. case (a,b) of c { (p,q) -> p }
+ = return env -- Here c is dead, and we avoid creating
+ -- the binding c = (a,b)
+ | Coercion co <- new_rhs
= return (extendCvSubst env bndr co)
| otherwise -- the binding b = (a,b)
= do { (env', bndr') <- simplBinder env bndr
-- * or by adding to the floats in the envt
completeBind env top_lvl old_bndr new_bndr new_rhs
+ | isCoVar old_bndr
+ = case new_rhs of
+ Coercion co -> return (extendCvSubst env old_bndr co)
+ _ -> return (addNonRec env new_bndr new_rhs)
+
+ | otherwise
= ASSERT( isId new_bndr )
do { let old_info = idInfo old_bndr
old_unf = unfoldingInfo old_info
; if postInlineUnconditionally env top_lvl new_bndr occ_info final_rhs new_unfolding
-- Inline and discard the binding
then do { tick (PostInlineUnconditionally old_bndr)
- ; -- pprTrace "postInlineUnconditionally"
- -- (ppr old_bndr <+> equals <+> ppr final_rhs $$ ppr occ_info) $
- return (extendIdSubst env old_bndr (DoneEx final_rhs)) }
+ ; return (extendIdSubst env old_bndr (DoneEx final_rhs)) }
-- Use the substitution to make quite, quite sure that the
-- substitution will happen, since we are going to discard the binding
else
simplExprF env e cont
= -- pprTrace "simplExprF" (ppr e $$ ppr cont $$ ppr (seTvSubst env) $$ ppr (seIdSubst env) {- $$ ppr (seFloats env) -} ) $
- simplExprF' env e cont
+ simplExprF1 env e cont
-simplExprF' :: SimplEnv -> InExpr -> SimplCont
+simplExprF1 :: SimplEnv -> InExpr -> SimplCont
-> SimplM (SimplEnv, OutExpr)
-simplExprF' env (Var v) cont = simplIdF env v cont
-simplExprF' env (Lit lit) cont = rebuild env (Lit lit) cont
-simplExprF' env (Note n expr) cont = simplNote env n expr cont
-simplExprF' env (Cast body co) cont = simplCast env body co cont
-simplExprF' env (App fun arg) cont = simplExprF env fun $
+simplExprF1 env (Var v) cont = simplIdF env v cont
+simplExprF1 env (Lit lit) cont = rebuild env (Lit lit) cont
+simplExprF1 env (Note n expr) cont = simplNote env n expr cont
+simplExprF1 env (Cast body co) cont = simplCast env body co cont
+simplExprF1 env (Coercion co) cont = simplCoercionF env co cont
+simplExprF1 env (Type ty) cont = ASSERT( contIsRhsOrArg cont )
+ rebuild env (Type (substTy env ty)) cont
+simplExprF1 env (App fun arg) cont = simplExprF env fun $
ApplyTo NoDup arg env cont
-simplExprF' env expr@(Lam {}) cont
+simplExprF1 env expr@(Lam {}) cont
= simplLam env zapped_bndrs body cont
-- The main issue here is under-saturated lambdas
-- (\x1. \x2. e) arg1
zap b | isTyVar b = b
| otherwise = zapLamIdInfo b
-simplExprF' env (Type ty) cont
- = ASSERT( contIsRhsOrArg cont )
- rebuild env (Type (substTy env ty)) cont
-
-simplExprF' env (Coercion co) cont
- = ASSERT( contIsRhsOrArg cont )
- do { co' <- simplCoercion env co
- ; rebuild env (Coercion co') cont }
-
-simplExprF' env (Case scrut bndr _ alts) cont
+simplExprF1 env (Case scrut bndr _ alts) cont
| sm_case_case (getMode env)
= -- Simplify the scrutinee with a Select continuation
simplExprF env scrut (Select NoDup bndr alts env cont)
(Select NoDup bndr alts env mkBoringStop)
; rebuild env case_expr' cont }
-simplExprF' env (Let (Rec pairs) body) cont
+simplExprF1 env (Let (Rec pairs) body) cont
= do { env' <- simplRecBndrs env (map fst pairs)
-- NB: bndrs' don't have unfoldings or rules
-- We add them as we go down
; env'' <- simplRecBind env' NotTopLevel pairs
; simplExprF env'' body cont }
-simplExprF' env (Let (NonRec bndr rhs) body) cont
+simplExprF1 env (Let (NonRec bndr rhs) body) cont
= simplNonRecE env bndr (rhs, env) ([], body) cont
---------------------------------
new_ty = substTy env ty
---------------------------------
+simplCoercionF :: SimplEnv -> InCoercion -> SimplCont
+ -> SimplM (SimplEnv, OutExpr)
+-- We are simplifying a term of form (Coercion co)
+-- Simplify the InCoercion, and then try to combine with the
+-- context, to implememt the rule
+-- (Coercion co) |> g
+-- = Coercion (syn (nth 0 g) ; co ; nth 1 g)
+simplCoercionF env co cont
+ = do { co' <- simplCoercion env co
+ ; simpl_co co' cont }
+ where
+ simpl_co co (CoerceIt g cont)
+ = simpl_co new_co cont
+ where
+ new_co = mkSymCo g0 `mkTransCo` co `mkTransCo` g1
+ [g0, g1] = decomposeCo 2 g
+
+ simpl_co co cont
+ = seqCo co `seq` rebuild env (Coercion co) cont
+
simplCoercion :: SimplEnv -> InCoercion -> SimplM OutCoercion
simplCoercion env co
- = -- pprTrace "simplCoercion" (ppr co $$ ppr (getCvSubst env)) $
- seqCo new_co `seq` return new_co
- where
- new_co = optCoercion (getCvSubst env) co
+ = let opt_co = optCoercion (getCvSubst env) co
+ in opt_co `seq` return opt_co
\end{code}
rebuild env expr cont
= case cont of
Stop {} -> return (env, expr)
- CoerceIt co cont -> rebuild env (mkCoerce co expr) cont
+ CoerceIt co cont -> rebuild env (Cast expr co) cont
Select _ bndr alts se cont -> rebuildCase (se `setFloats` env) expr bndr alts cont
StrictArg info _ cont -> rebuildCall env (info `addArgTo` expr) cont
StrictBind b bs body se cont -> do { env' <- simplNonRecX (se `setFloats` env) b expr
-- and we'd like it to simplify to e[y/x] in one round
-- of simplification
, s1 `eqType` t1 = cont -- The coerces cancel out
- | otherwise = CoerceIt (mkTransCo co1 co2) cont
+ | otherwise = CoerceIt (mkTransCo co1 co2) cont
add_coerce co (Pair s1s2 _t1t2) (ApplyTo dup (Type arg_ty) arg_se cont)
-- (f |> g) ty ---> (f ty) |> (g @ ty)
do { ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
-simplNonRecE env bndr (Coercion co_arg, rhs_se) (bndrs, body) cont
- = ASSERT( isCoVar bndr )
- do { co_arg' <- simplCoercion (rhs_se `setInScope` env) co_arg
- ; simplLam (extendCvSubst env bndr co_arg') bndrs body cont }
-
simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
| preInlineUnconditionally env NotTopLevel bndr rhs
= do { tick (PreInlineUnconditionally bndr)
; -- pprTrace "preInlineUncond" (ppr bndr <+> ppr rhs) $
simplLam (extendIdSubst env bndr (mkContEx rhs_se rhs)) bndrs body cont }
- | isStrictId bndr
+ | isStrictId bndr -- Includes coercions
= do { simplExprF (rhs_se `setFloats` env) rhs
(StrictBind bndr bndrs body env cont) }
else simplType (se `setInScope` env) arg_ty
; rebuildCall env (info `addArgTo` Type arg_ty') cont }
-rebuildCall env info (ApplyTo dup_flag (Coercion arg_co) se cont)
- = do { arg_co' <- if isSimplified dup_flag then return arg_co
- else simplCoercion (se `setInScope` env) arg_co
- ; rebuildCall env (info `addArgTo` Coercion arg_co') cont }
-
rebuildCall env info@(ArgInfo { ai_encl = encl_rules
, ai_strs = str:strs, ai_discs = disc:discs })
(ApplyTo dup_flag arg arg_se cont)
decisions. Hence no black holes.
\begin{code}
-coreToStgExpr (Lit l) = return (StgLit l, emptyFVInfo, emptyVarSet)
-coreToStgExpr (Var v) = coreToStgApp Nothing v []
+coreToStgExpr (Lit l) = return (StgLit l, emptyFVInfo, emptyVarSet)
+coreToStgExpr (Var v) = coreToStgApp Nothing v []
+coreToStgExpr (Coercion _) = coreToStgApp Nothing coercionTokenId []
coreToStgExpr expr@(App _ _)
= coreToStgApp Nothing f args
-- witness dictionary is identical to the argument
-- dictionary. Hence no bindings, no pragmas.
- -- BAY* : should this be a CoAxiom?
Coercion -- The coercion maps from newtype to the representation type
-- (mentioning type variables bound by the forall'd iSpec variables)
-- E.g. newtype instance N [a] = N1 (Tree a)
import Bag
import FastString
import Outputable
-import Data.Traversable( traverse )
+-- import Data.Traversable( traverse )
\end{code}
\begin{code}
go (AxiomInstCo ax cos) = do { cos' <- mapM go cos; return (AxiomInstCo ax cos') }
go (AppCo co1 co2) = do { co1' <- go co1; co2' <- go co2
; return (mkAppCo co1' co2') }
- go (PredCo pco) = do { pco' <- go `traverse` pco; return (mkPredCo pco') }
go (UnsafeCo t1 t2) = do { t1' <- zonkTcTypeToType env t1
; t2' <- zonkTcTypeToType env t2
; return (mkUnsafeCo t1' t2') }
import DataCon
import Type
import Class
-import Pair
import TcType ( orphNamesOfDFunHead )
import Inst ( tcGetInstEnvs )
import Data.List ( sortBy )
= vcat [ text "TYPE CONSTRUCTORS"
, nest 2 (ppr_tydecls tycons)
, text "COERCION AXIOMS"
- , nest 2 (ppr_axioms (typeEnvCoAxioms type_env)) ]
+ , nest 2 (vcat (map pprCoAxiom (typeEnvCoAxioms type_env))) ]
where
fi_tycons = map famInstTyCon fam_insts
tycons = [tycon | tycon <- typeEnvTyCons type_env, want_tycon tycon]
ppr_tycon tycon = ppr (tyThingToIfaceDecl (ATyCon tycon))
where
-ppr_axioms :: [CoAxiom] -> SDoc
-ppr_axioms axs
- = vcat (map ppr_ax axs)
- where
- ppr_ax ax = sep [ ptext (sLit "coercion") <+> ppr ax <+> ppr (co_ax_tvs ax)
- , nest 2 (dcolon <+> pprEqPred
- (Pair (co_ax_lhs ax) (co_ax_rhs ax))) ]
-
ppr_rules :: [CoreRule] -> SDoc
ppr_rules [] = empty
ppr_rules rs = vcat [ptext (sLit "{-# RULES"),
import Outputable
import FastString
-import qualified Data.Foldable as Foldable
-import Data.Functor( (<$>) )
import Data.List( mapAccumL )
import Data.IORef
\end{code}
go (ForAllCo tv co) = ForAllCo tvp $! (tidyCo envp co)
where
(envp, tvp) = tidyTyVarBndr env tv
- go (PredCo pco) = PredCo $! (go <$> pco)
go (CoVarCo cv) = case lookupVarEnv subst cv of
Nothing -> CoVarCo cv
Just cv' -> CoVarCo cv'
orphNamesOfCo (TyConAppCo tc cos) = unitNameSet (getName tc) `unionNameSets` orphNamesOfCos cos
orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSets` orphNamesOfCo co2
orphNamesOfCo (ForAllCo _ co) = orphNamesOfCo co
-orphNamesOfCo (PredCo p) = Foldable.foldr (unionNameSets . orphNamesOfCo)
- emptyNameSet p
orphNamesOfCo (CoVarCo _) = emptyNameSet
orphNamesOfCo (AxiomInstCo con cos) = orphNamesOfCoCon con `unionNameSets` orphNamesOfCos cos
orphNamesOfCo (UnsafeCo ty1 ty2) = orphNamesOfType ty1 `unionNameSets` orphNamesOfType ty2
seqCo,
-- * Pretty-printing
- pprCo, pprParendCo,
+ pprCo, pprParendCo, pprCoAxiom,
-- * Other
applyCo, coVarPred
import qualified Type
import Type hiding( substTy, substTyVarBndr, extendTvSubst )
import Kind
+import Class ( classTyCon )
import TyCon
import Var
import VarEnv
import Outputable
import Unique
import Pair
-import PrelNames( funTyConKey )
+import TysPrim ( eqPredPrimTyCon )
+import PrelNames ( funTyConKey )
import Control.Applicative
import Data.Traversable (traverse, sequenceA)
import Control.Arrow (second)
\begin{code}
-- | A 'Coercion' is concrete evidence of the equality/convertibility
-- of two types.
+
data Coercion
-- These ones mirror the shape of types
= Refl Type -- See Note [Refl invariant]
-- See Note [Forall coercions]
| ForAllCo TyVar Coercion -- forall a. g
- | PredCo (Pred Coercion) -- (g1~g2) etc
-- These are special
| CoVarCo CoVar
where the type variables have identical kinds, because equality on
kinds is trivial.
- ForAllCoCo Coercion Coercion Coercion
-
-represents a coercion between types abstracted over equality proofs,
-which we might more suggestively write as
-
- ForAllCoCo (_:Coercion~Coercion) Coercion
+Note [Predicate coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+ g :: a~b
+How can we coerce between types
+ ([c]~a) => [a] -> c
+and
+ ([c]~b) => [b] -> c
+where the equality predicate *itself* differs?
-The rule is
+Answer: we simply treat (~) as an ordinary type constructor, so these
+types really look like
- g1 : t1 ~ t1' g2 : t2 ~ t2' g3 : t3 ~ t3'
- ------------------------------------------------------------------
- ForAllCoCo g1 g2 g3 : ( (t1 ~ t2) => t3 ) ~ ( (t1' ~ t2') => t3' )
+ ((~) [c] a) -> [a] -> c
+ ((~) [c] b) -> [b] -> c
-There are several things to note. First, we don't need to bind a
-variable, since coercion variables do not appear in types. Second,
-note that here we DO need to convert between "kinds" (the types of the
-required coercions).
+So the coercion between the two is obviously
-In the future, if we collapse the type and kind levels and add a bit
-more dependency, we will need something like
+ ((~) [c] g) -> [g] -> c
- | ForAllCo TyVar Coercion Coercion
- | ForAllCoCo CoVar Coercion Coercion Coercion
-
-The addition of the extra coercion in the first case handles
-converting between possibly different kinds; the addition of a CoVar
-in the second case is needed since now types may mention coercion
-variables (in casts).
+Another way to see this to say that we simply collapse predicates to
+their representation type (see Type.coreView and Type.predTypeRep).
+This collapse is done by mkPredCo; there is no PredCo constructor
+in Coercion. This is important because we need Nth to work on
+predicates too:
+ Nth 1 ((~) [c] g) = g
+See Simplify.simplCoercionF, which generates such selections.
%************************************************************************
%* *
tyCoVarsOfCo (TyConAppCo _ cos) = tyCoVarsOfCos cos
tyCoVarsOfCo (AppCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
tyCoVarsOfCo (ForAllCo tv co) = tyCoVarsOfCo co `delVarSet` tv
-tyCoVarsOfCo (PredCo pred) = varsOfPred tyCoVarsOfCo pred
tyCoVarsOfCo (CoVarCo v) = unitVarSet v
tyCoVarsOfCo (AxiomInstCo _ cos) = tyCoVarsOfCos cos
tyCoVarsOfCo (UnsafeCo ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
coVarsOfCo (TyConAppCo _ cos) = coVarsOfCos cos
coVarsOfCo (AppCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (ForAllCo _ co) = coVarsOfCo co
-coVarsOfCo (PredCo pred) = varsOfPred coVarsOfCo pred
coVarsOfCo (CoVarCo v) = unitVarSet v
coVarsOfCo (AxiomInstCo _ cos) = coVarsOfCos cos
coVarsOfCo (UnsafeCo _ _) = emptyVarSet
coercionSize (TyConAppCo _ cos) = 1 + sum (map coercionSize cos)
coercionSize (AppCo co1 co2) = coercionSize co1 + coercionSize co2
coercionSize (ForAllCo _ co) = 1 + coercionSize co
-coercionSize (PredCo pred) = predSize coercionSize pred
coercionSize (CoVarCo _) = 1
coercionSize (AxiomInstCo _ cos) = 1 + sum (map coercionSize cos)
coercionSize (UnsafeCo ty1 ty2) = typeSize ty1 + typeSize ty2
ppr_co p co@(TyConAppCo tc cos)
| tc `hasKey` funTyConKey = ppr_fun_co p co
- | otherwise = maybeParen p TyConPrec $
- pprTcApp p ppr_co tc cos
+ | otherwise = pprTcApp p ppr_co tc cos
ppr_co p (AppCo co1 co2) = maybeParen p TyConPrec $
pprCo co1 <+> ppr_co TyConPrec co2
ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
-ppr_co _ (PredCo pred) = pprPred ppr_co pred
ppr_co _ (CoVarCo cv)
| isSymOcc (getOccName cv) = parens (ppr cv)
ppr_forall_co :: Prec -> Coercion -> SDoc
ppr_forall_co p ty
= maybeParen p FunPrec $
- sep [pprForAll tvs, pprThetaArrow ppr_co ctxt, ppr_co TopPrec tau]
+ sep [pprForAll tvs, ppr_co TopPrec rho]
where
(tvs, rho) = split1 [] ty
- (ctxt, tau) = split2 [] rho
-
- -- We need to be extra careful here as equality constraints will occur as
- -- type variables with an equality kind. So, while collecting quantified
- -- variables, we separate the coercion variables out and turn them into
- -- equality predicates.
split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
split1 tvs ty = (reverse tvs, ty)
-
- split2 ps (TyConAppCo tc [PredCo p, co])
- | tc `hasKey` funTyConKey = split2 (p:ps) co
- split2 ps co = (reverse ps, co)
\end{code}
+\begin{code}
+pprCoAxiom :: CoAxiom -> SDoc
+pprCoAxiom ax
+ = sep [ ptext (sLit "axiom") <+> ppr ax <+> ppr (co_ax_tvs ax)
+ , nest 2 (dcolon <+> pprEqPred (Pair (co_ax_lhs ax) (co_ax_rhs ax))) ]
+\end{code}
%************************************************************************
%* *
-- ^ Attempt to take a coercion application apart.
splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
splitAppCo_maybe (TyConAppCo tc cos)
- | not (null cos) = Just (mkTyConAppCo tc (init cos), last cos)
+ | isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc
+ , Just (cos', co') <- snocView cos
+ = Just (mkTyConAppCo tc cos', co') -- Never create unsaturated type family apps!
-- Use mkTyConAppCo to preserve the invariant
-- that identity coercions are always represented by Refl
splitAppCo_maybe (Refl ty)
- | Just (ty1, ty2) <- splitAppTy_maybe ty = Just (Refl ty1, Refl ty2)
- | otherwise = Nothing
+ | Just (ty1, ty2) <- splitAppTy_maybe ty
+ = Just (Refl ty1, Refl ty2)
splitAppCo_maybe _ = Nothing
splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
mkForAllCo tv co = ASSERT ( isTyVar tv ) ForAllCo tv co
mkPredCo :: Pred Coercion -> Coercion
-mkPredCo pred_co
- = case traverse isReflCo_maybe pred_co of
- Just pred_ty -> Refl (PredTy pred_ty)
- Nothing -> PredCo pred_co
+-- See Note [Predicate coercions]
+mkPredCo (EqPred co1 co2) = mkTyConAppCo eqPredPrimTyCon [co1,co2]
+mkPredCo (ClassP cls cos) = mkTyConAppCo (classTyCon cls) cos
+mkPredCo (IParam _ co) = co
-------------------------------
go (Refl ty) = Refl $! go_ty ty
go (TyConAppCo tc cos) = let args = map go cos
in args `seqList` TyConAppCo tc args
-
go (AppCo co1 co2) = mkAppCo (go co1) $! go co2
go (ForAllCo tv co) = case substTyVarBndr subst tv of
(subst', tv') ->
ForAllCo tv' $! subst_co subst' co
-
- go (PredCo p) = mkPredCo (go <$> p)
go (CoVarCo cv) = substCoVar subst cv
go (AxiomInstCo con cos) = AxiomInstCo con $! map go cos
go (UnsafeCo ty1 ty2) = (UnsafeCo $! go_ty ty1) $! go_ty ty2
rn_env = me_env menv
tv1' = rnOccL rn_env tv1
-ty_co_match menv subst (AppTy ty1 ty2) (AppCo co1 co2) -- BAY: do we need to work harder to decompose the AppCo?
+ty_co_match menv subst (AppTy ty1 ty2) co
+ | Just (co1, co2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
= do { subst' <- ty_co_match menv subst ty1 co1
; ty_co_match menv subst' ty2 co2 }
seqCo (TyConAppCo tc cos) = tc `seq` seqCos cos
seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (ForAllCo tv co) = tv `seq` seqCo co
-seqCo (PredCo p) = seqPred seqCo p
seqCo (CoVarCo cv) = cv `seq` ()
seqCo (AxiomInstCo con cos) = con `seq` seqCos cos
seqCo (UnsafeCo ty1 ty2) = seqType ty1 `seq` seqType ty2
--
-- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
coercionKind :: Coercion -> Pair Type
-coercionKind (Refl ty) = Pair ty ty
-coercionKind (TyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map coercionKind cos)
-coercionKind (AppCo co1 co2) = mkAppTy <$> coercionKind co1 <*> coercionKind co2
-coercionKind (ForAllCo tv co) = mkForAllTy tv <$> coercionKind co
- -- BAY*: is the above still correct for equality
- -- abstractions? the System FC paper seems to imply we can
- -- only ever construct coercions between foralls whose
- -- variables have *equal* kinds. But there was this comment
- -- below suggesting otherwise:
-
--- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
--- ----------------------------------------------
--- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2
--- or
--- forall (_:c1~c2)
+coercionKind (Refl ty) = Pair ty ty
+coercionKind (TyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map coercionKind cos)
+coercionKind (AppCo co1 co2) = mkAppTy <$> coercionKind co1 <*> coercionKind co2
+coercionKind (ForAllCo tv co) = mkForAllTy tv <$> coercionKind co
coercionKind (CoVarCo cv) = ASSERT( isCoVar cv ) toPair $ coVarKind cv
coercionKind (AxiomInstCo ax cos) = let Pair tys1 tys2 = coercionKinds cos
in Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax))
coercionKind (SymCo co) = swap $ coercionKind co
coercionKind (TransCo co1 co2) = Pair (pFst $ coercionKind co1) (pSnd $ coercionKind co2)
coercionKind (NthCo d co) = getNth d <$> coercionKind co
-coercionKind (InstCo co ty) | Just ks <- splitForAllTy_maybe `traverse` coercionKind co
+coercionKind co@(InstCo aco ty) | Just ks <- splitForAllTy_maybe `traverse` coercionKind aco
= (\(tv, body) -> substTyWith [tv] [ty] body) <$> ks
- -- fall-through error case.
-coercionKind co = pprPanic "coercionKind" (ppr co)
+ | otherwise = pprPanic "coercionKind" (ppr co)
-- | Apply 'coercionKind' to multiple 'Coercion's
coercionKinds :: [Coercion] -> Pair [Type]
fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
-- Don't discard anything!
-- We could discard equal types but it's an overkill to call
- -- tcEqType again, since we know for sure that /at least one/
+ -- eqType again, since we know for sure that /at least one/
-- equation in there is useful)
qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
-%\r
-% (c) The University of Glasgow 2006\r
-%\r
-\r
-\begin{code}\r
-module OptCoercion ( optCoercion ) where \r
-\r
-#include "HsVersions.h"\r
-\r
-import Coercion\r
-import Type hiding( substTyVarBndr, substTy, extendTvSubst )\r
-import TyCon\r
-import Var\r
-import VarSet\r
-import VarEnv\r
-import StaticFlags ( opt_NoOptCoercion )\r
-import Outputable\r
-import Pair\r
-import Maybes( allMaybes )\r
-import FastString\r
-\end{code}\r
-\r
-%************************************************************************\r
-%* *\r
- Optimising coercions \r
-%* *\r
-%************************************************************************\r
-\r
-Note [Subtle shadowing in coercions]\r
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\r
-Supose we optimising a coercion\r
- optCoercion (forall (co_X5:t1~t2). ...co_B1...)\r
-The co_X5 is a wild-card; the bound variable of a coercion for-all\r
-should never appear in the body of the forall. Indeed we often\r
-write it like this\r
- optCoercion ( (t1~t2) => ...co_B1... )\r
-\r
-Just because it's a wild-card doesn't mean we are free to choose\r
-whatever variable we like. For example it'd be wrong for optCoercion\r
-to return\r
- forall (co_B1:t1~t2). ...co_B1...\r
-because now the co_B1 (which is really free) has been captured, and\r
-subsequent substitutions will go wrong. That's why we can't use\r
-mkCoPredTy in the ForAll case, where this note appears. \r
-\r
-\begin{code}\r
-optCoercion :: CvSubst -> Coercion -> NormalCo\r
--- ^ optCoercion applies a substitution to a coercion, \r
--- *and* optimises it to reduce its size\r
-optCoercion env co \r
- | opt_NoOptCoercion = substCo env co\r
- | otherwise = opt_co env False co\r
-\r
-type NormalCo = Coercion\r
- -- Invariants: \r
- -- * The substitution has been fully applied\r
- -- * For trans coercions (co1 `trans` co2)\r
- -- co1 is not a trans, and neither co1 nor co2 is identity\r
- -- * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)\r
-\r
-type NormalNonIdCo = NormalCo -- Extra invariant: not the identity\r
-\r
-opt_co, opt_co' :: CvSubst\r
- -> Bool -- True <=> return (sym co)\r
- -> Coercion\r
- -> NormalCo \r
-opt_co = opt_co'\r
-{-\r
-opt_co env sym co\r
- = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $\r
- co1 `seq`\r
- pprTrace "opt_co done }" (ppr co1) $\r
- (WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (Pair s1 t1)\r
- $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )\r
- WARN( not (coreEqCoercion co1 simple_result),\r
- (text "env=" <+> ppr env) $$\r
- (text "input=" <+> ppr co) $$\r
- (text "simple=" <+> ppr simple_result) $$\r
- (text "opt=" <+> ppr co1) )\r
- co1)\r
- where\r
- co1 = opt_co' env sym co\r
- same_co_kind = s1 `eqType` s2 && t1 `eqType` t2\r
- Pair s t = coercionKind (substCo env co)\r
- (s1,t1) | sym = (t,s)\r
- | otherwise = (s,t)\r
- Pair s2 t2 = coercionKind co1\r
-\r
- simple_result | sym = mkSymCo (substCo env co)\r
- | otherwise = substCo env co\r
--}\r
-\r
-opt_co' env _ (Refl ty) = Refl (substTy env ty)\r
-opt_co' env sym (SymCo co) = opt_co env (not sym) co\r
-opt_co' env sym (TyConAppCo tc cos) = mkTyConAppCo tc (map (opt_co env sym) cos)\r
-opt_co' env sym (PredCo cos) = mkPredCo (fmap (opt_co env sym) cos)\r
-opt_co' env sym (AppCo co1 co2) = mkAppCo (opt_co env sym co1) (opt_co env sym co2)\r
-opt_co' env sym (ForAllCo tv co) = case substTyVarBndr env tv of\r
- (env', tv') -> mkForAllCo tv' (opt_co env' sym co)\r
- -- Use the "mk" functions to check for nested Refls\r
-\r
-opt_co' env sym (CoVarCo cv)\r
- | Just co <- lookupCoVar env cv\r
- = opt_co (zapCvSubstEnv env) sym co\r
-\r
- | Just cv1 <- lookupInScope (getCvInScope env) cv\r
- = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)\r
- -- cv1 might have a substituted kind!\r
-\r
- | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)\r
- ASSERT( isCoVar cv )\r
- wrapSym sym (CoVarCo cv)\r
-\r
-opt_co' env sym (AxiomInstCo con cos)\r
- -- Do *not* push sym inside top-level axioms\r
- -- e.g. if g is a top-level axiom\r
- -- g a : f a ~ a\r
- -- then (sym (g ty)) /= g (sym ty) !!\r
- = wrapSym sym $ AxiomInstCo con (map (opt_co env False) cos)\r
- -- Note that the_co does *not* have sym pushed into it\r
-\r
-opt_co' env sym (UnsafeCo ty1 ty2)\r
- | ty1' `eqType` ty2' = Refl ty1'\r
- | sym = mkUnsafeCo ty2' ty1'\r
- | otherwise = mkUnsafeCo ty1' ty2'\r
- where\r
- ty1' = substTy env ty1\r
- ty2' = substTy env ty2\r
-\r
-opt_co' env sym (TransCo co1 co2)\r
- | sym = opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g\r
- | otherwise = opt_trans opt_co1 opt_co2\r
- where\r
- opt_co1 = opt_co env sym co1\r
- opt_co2 = opt_co env sym co2\r
-\r
-opt_co' env sym (NthCo n co)\r
- | TyConAppCo tc cos <- co'\r
- , isDecomposableTyCon tc -- Not synonym families\r
- = ASSERT( n < length cos )\r
- cos !! n\r
- | otherwise\r
- = NthCo n co'\r
- where\r
- co' = opt_co env sym co\r
-\r
-opt_co' env sym (InstCo co ty)\r
- -- See if the first arg is already a forall\r
- -- ...then we can just extend the current substitution\r
- | Just (tv, co_body) <- splitForAllCo_maybe co\r
- = opt_co (extendTvSubst env tv ty') sym co_body\r
-\r
- -- See if it is a forall after optimization\r
- | Just (tv, co'_body) <- splitForAllCo_maybe co'\r
- = substCoWithTy tv ty' co'_body -- An inefficient one-variable substitution\r
-\r
- | otherwise = InstCo co' ty'\r
-\r
- where\r
- co' = opt_co env sym co\r
- ty' = substTy env ty\r
-\r
--------------\r
-opt_transList :: [NormalCo] -> [NormalCo] -> [NormalCo]\r
-opt_transList = zipWith opt_trans\r
-\r
-opt_trans :: NormalCo -> NormalCo -> NormalCo\r
-opt_trans co1 co2\r
- | isReflCo co1 = co2\r
- | otherwise = opt_trans1 co1 co2\r
-\r
-opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo\r
--- First arg is not the identity\r
-opt_trans1 co1 co2\r
- | isReflCo co2 = co1\r
- | otherwise = opt_trans2 co1 co2\r
-\r
-opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo\r
--- Neither arg is the identity\r
-opt_trans2 (TransCo co1a co1b) co2\r
- -- Don't know whether the sub-coercions are the identity\r
- = opt_trans co1a (opt_trans co1b co2) \r
-\r
-opt_trans2 co1 co2 \r
- | Just co <- opt_trans_rule co1 co2\r
- = co\r
-\r
-opt_trans2 co1 (TransCo co2a co2b)\r
- | Just co1_2a <- opt_trans_rule co1 co2a\r
- = if isReflCo co1_2a\r
- then co2b\r
- else opt_trans1 co1_2a co2b\r
-\r
-opt_trans2 co1 co2\r
- = mkTransCo co1 co2\r
-\r
-------\r
--- Optimize coercions with a top-level use of transitivity.\r
-opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo\r
-\r
--- push transitivity down through matching top-level constructors.\r
-opt_trans_rule in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)\r
- | tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $\r
- TyConAppCo tc1 (opt_transList cos1 cos2)\r
-\r
--- push transitivity through matching destructors\r
-opt_trans_rule in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)\r
- | d1 == d2\r
- , co1 `compatible_co` co2\r
- = fireTransRule "PushNth" in_co1 in_co2 $\r
- mkNthCo d1 (opt_trans co1 co2)\r
-\r
--- Push transitivity inside instantiation\r
-opt_trans_rule in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)\r
- | ty1 `eqType` ty2\r
- , co1 `compatible_co` co2\r
- = fireTransRule "TrPushInst" in_co1 in_co2 $\r
- mkInstCo (opt_trans co1 co2) ty1\r
- \r
--- Push transitivity inside apply\r
-opt_trans_rule in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)\r
- = fireTransRule "TrPushApp" in_co1 in_co2 $\r
- mkAppCo (opt_trans co1a co2a) (opt_trans co1b co2b)\r
-\r
--- Push transitivity inside PredCos\r
-opt_trans_rule in_co1@(PredCo pco1) in_co2@(PredCo pco2)\r
- | Just pco' <- opt_trans_pred pco1 pco2\r
- = fireTransRule "TrPushPrd" in_co1 in_co2 $\r
- mkPredCo pco'\r
-\r
-opt_trans_rule co1@(TyConAppCo tc cos1) co2\r
- | Just cos2 <- etaTyConAppCo_maybe tc co2\r
- = ASSERT( length cos1 == length cos2 )\r
- fireTransRule "EtaCompL" co1 co2 $\r
- TyConAppCo tc (zipWith opt_trans cos1 cos2)\r
-\r
-opt_trans_rule co1 co2@(TyConAppCo tc cos2)\r
- | Just cos1 <- etaTyConAppCo_maybe tc co1\r
- = ASSERT( length cos1 == length cos2 )\r
- fireTransRule "EtaCompR" co1 co2 $\r
- TyConAppCo tc (zipWith opt_trans cos1 cos2)\r
-\r
-\r
-{- BAY: think harder about this. do we still need it?\r
--- Push transitivity inside (s~t)=>r\r
--- We re-use the CoVar rather than using mkCoPredTy\r
--- See Note [Subtle shadowing in coercions]\r
-opt_trans_rule co1 co2\r
- | Just (cv1,r1) <- splitForAllTy_maybe co1\r
- , isCoVar cv1\r
- , Just (s1,t1) <- coVarKind_maybe cv1\r
- , Just (s2,t2,r2) <- etaCoPred_maybe co2\r
- = Just (ForAllTy (mkCoVar (coVarName cv1) (mkCoType (opt_trans s1 s2) (opt_trans t1 t2)))\r
- (opt_trans r1 r2))\r
-\r
- | Just (cv2,r2) <- splitForAllTy_maybe co2\r
- , isCoVar cv2\r
- , Just (s2,t2) <- coVarKind_maybe cv2\r
- , Just (s1,t1,r1) <- etaCoPred_maybe co1\r
- = Just (ForAllTy (mkCoVar (coVarName cv2) (mkCoType (opt_trans s1 s2) (opt_trans t1 t2)))\r
- (opt_trans r1 r2))\r
--}\r
-\r
--- Push transitivity inside forall\r
-opt_trans_rule co1 co2\r
- | Just (tv1,r1) <- splitForAllCo_maybe co1\r
- , Just (tv2,r2) <- etaForAllCo_maybe co2\r
- , let r2' = substCoWithTy tv2 (mkTyVarTy tv1) r2\r
- = fireTransRule "EtaAllL" co1 co2 $\r
- mkForAllCo tv1 (opt_trans2 r1 r2')\r
-\r
- | Just (tv2,r2) <- splitForAllCo_maybe co2\r
- , Just (tv1,r1) <- etaForAllCo_maybe co1\r
- , let r1' = substCoWithTy tv1 (mkTyVarTy tv2) r1\r
- = fireTransRule "EtaAllR" co1 co2 $\r
- mkForAllCo tv1 (opt_trans2 r1' r2)\r
-\r
--- Push transitivity inside axioms\r
-opt_trans_rule co1 co2\r
-\r
- -- TrPushAxR/TrPushSymAxR\r
- | Just (sym, con, cos1) <- co1_is_axiom_maybe\r
- , Just cos2 <- matchAxiom sym con co2\r
- = fireTransRule "TrPushAxR" co1 co2 $\r
- if sym \r
- then SymCo $ AxiomInstCo con (opt_transList (map mkSymCo cos2) cos1)\r
- else AxiomInstCo con (opt_transList cos1 cos2)\r
-\r
- -- TrPushAxL/TrPushSymAxL\r
- | Just (sym, con, cos2) <- co2_is_axiom_maybe\r
- , Just cos1 <- matchAxiom (not sym) con co1\r
- = fireTransRule "TrPushAxL" co1 co2 $\r
- if sym \r
- then SymCo $ AxiomInstCo con (opt_transList cos2 (map mkSymCo cos1))\r
- else AxiomInstCo con (opt_transList cos1 cos2)\r
-\r
- -- TrPushAxSym/TrPushSymAx\r
- | Just (sym1, con1, cos1) <- co1_is_axiom_maybe\r
- , Just (sym2, con2, cos2) <- co2_is_axiom_maybe\r
- , con1 == con2\r
- , sym1 == not sym2\r
- , let qtvs = co_ax_tvs con1\r
- lhs = co_ax_lhs con1 \r
- rhs = co_ax_rhs con1 \r
- pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)\r
- , all (`elemVarSet` pivot_tvs) qtvs\r
- = fireTransRule "TrPushAxSym" co1 co2 $\r
- if sym2\r
- then liftCoSubstWith qtvs (opt_transList cos1 (map mkSymCo cos2)) lhs -- TrPushAxSym\r
- else liftCoSubstWith qtvs (opt_transList (map mkSymCo cos1) cos2) rhs -- TrPushSymAx\r
- where\r
- co1_is_axiom_maybe = isAxiom_maybe co1\r
- co2_is_axiom_maybe = isAxiom_maybe co2\r
-\r
-opt_trans_rule co1 co2 -- Identity rule\r
- | Pair ty1 _ <- coercionKind co1\r
- , Pair _ ty2 <- coercionKind co2\r
- , ty1 `eqType` ty2\r
- = fireTransRule "RedTypeDirRefl" co1 co2 $\r
- Refl ty2\r
-\r
-opt_trans_rule _ _ = Nothing\r
-\r
-opt_trans_pred :: Pred Coercion -> Pred Coercion -> Maybe (Pred Coercion)\r
-opt_trans_pred (EqPred co1a co1b) (EqPred co2a co2b)\r
- = Just (EqPred (opt_trans co1a co2a) (opt_trans co1b co2b))\r
-opt_trans_pred (ClassP cls1 cos1) (ClassP cls2 cos2)\r
- | cls1 == cls2\r
- = Just (ClassP cls1 (opt_transList cos1 cos2))\r
-opt_trans_pred (IParam n1 co1) (IParam n2 co2)\r
- | n1 == n2\r
- = Just (IParam n1 (opt_trans co1 co2))\r
-opt_trans_pred _ _ = Nothing\r
-\r
-fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion\r
-fireTransRule _rule _co1 _co2 res\r
- = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $\r
- Just res\r
-\r
------------\r
-wrapSym :: Bool -> Coercion -> Coercion\r
-wrapSym sym co | sym = SymCo co\r
- | otherwise = co\r
-\r
------------\r
-isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom, [Coercion])\r
-isAxiom_maybe (SymCo co) \r
- | Just (sym, con, cos) <- isAxiom_maybe co\r
- = Just (not sym, con, cos)\r
-isAxiom_maybe (AxiomInstCo con cos)\r
- = Just (False, con, cos)\r
-isAxiom_maybe _ = Nothing\r
-\r
-matchAxiom :: Bool -- True = match LHS, False = match RHS\r
- -> CoAxiom -> Coercion -> Maybe [Coercion]\r
--- If we succeed in matching, then *all the quantified type variables are bound*\r
--- E.g. if tvs = [a,b], lhs/rhs = [b], we'll fail\r
-matchAxiom sym (CoAxiom { co_ax_tvs = qtvs, co_ax_lhs = lhs, co_ax_rhs = rhs }) co\r
- = case liftCoMatch (mkVarSet qtvs) (if sym then lhs else rhs) co of\r
- Nothing -> Nothing\r
- Just subst -> allMaybes (map (liftCoSubstTyVar subst) qtvs)\r
-\r
--------------\r
-compatible_co :: Coercion -> Coercion -> Bool\r
--- Check whether (co1 . co2) will be well-kinded\r
-compatible_co co1 co2\r
- = x1 `eqType` x2 \r
- where\r
- Pair _ x1 = coercionKind co1\r
- Pair x2 _ = coercionKind co2\r
-\r
--------------\r
-etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)\r
--- Try to make the coercion be of form (forall tv. co)\r
-etaForAllCo_maybe co\r
- | Just (tv, r) <- splitForAllCo_maybe co\r
- = Just (tv, r)\r
-\r
- | Pair ty1 ty2 <- coercionKind co\r
- , Just (tv1, _) <- splitForAllTy_maybe ty1\r
- , Just (tv2, _) <- splitForAllTy_maybe ty2\r
- , tyVarKind tv1 `eqKind` tyVarKind tv2\r
- = Just (tv1, mkInstCo co (mkTyVarTy tv1))\r
-\r
- | otherwise\r
- = Nothing\r
-\r
-etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]\r
--- If possible, split a coercion \r
--- g :: T s1 .. sn ~ T t1 .. tn\r
--- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ] \r
-etaTyConAppCo_maybe tc (TyConAppCo tc2 cos2)\r
- = ASSERT( tc == tc2 ) Just cos2\r
-\r
-etaTyConAppCo_maybe tc co\r
- | isDecomposableTyCon tc\r
- , Pair ty1 ty2 <- coercionKind co\r
- , Just (tc1, tys1) <- splitTyConApp_maybe ty1\r
- , Just (tc2, tys2) <- splitTyConApp_maybe ty2\r
- , tc1 == tc2\r
- , let n = length tys1\r
- = ASSERT( tc == tc1 ) \r
- ASSERT( n == length tys2 )\r
- Just (decomposeCo n co) \r
- -- NB: n might be <> tyConArity tc\r
- -- e.g. data family T a :: * -> *\r
- -- g :: T a b ~ T c d\r
-\r
- | otherwise\r
- = Nothing\r
-\end{code} \r
+%
+% (c) The University of Glasgow 2006
+%
+
+\begin{code}
+module OptCoercion ( optCoercion ) where
+
+#include "HsVersions.h"
+
+import Coercion
+import Type hiding( substTyVarBndr, substTy, extendTvSubst )
+import TyCon
+import Var
+import VarSet
+import VarEnv
+import StaticFlags ( opt_NoOptCoercion )
+import Outputable
+import Pair
+import Maybes( allMaybes )
+import FastString
+\end{code}
+
+%************************************************************************
+%* *
+ Optimising coercions
+%* *
+%************************************************************************
+
+Note [Subtle shadowing in coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Supose we optimising a coercion
+ optCoercion (forall (co_X5:t1~t2). ...co_B1...)
+The co_X5 is a wild-card; the bound variable of a coercion for-all
+should never appear in the body of the forall. Indeed we often
+write it like this
+ optCoercion ( (t1~t2) => ...co_B1... )
+
+Just because it's a wild-card doesn't mean we are free to choose
+whatever variable we like. For example it'd be wrong for optCoercion
+to return
+ forall (co_B1:t1~t2). ...co_B1...
+because now the co_B1 (which is really free) has been captured, and
+subsequent substitutions will go wrong. That's why we can't use
+mkCoPredTy in the ForAll case, where this note appears.
+
+\begin{code}
+optCoercion :: CvSubst -> Coercion -> NormalCo
+-- ^ optCoercion applies a substitution to a coercion,
+-- *and* optimises it to reduce its size
+optCoercion env co
+ | opt_NoOptCoercion = substCo env co
+ | otherwise = opt_co env False co
+
+type NormalCo = Coercion
+ -- Invariants:
+ -- * The substitution has been fully applied
+ -- * For trans coercions (co1 `trans` co2)
+ -- co1 is not a trans, and neither co1 nor co2 is identity
+ -- * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
+
+type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
+
+opt_co, opt_co' :: CvSubst
+ -> Bool -- True <=> return (sym co)
+ -> Coercion
+ -> NormalCo
+opt_co = opt_co'
+{-
+opt_co env sym co
+ = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $
+ co1 `seq`
+ pprTrace "opt_co done }" (ppr co1) $
+ (WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (Pair s1 t1)
+ $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )
+ WARN( not (coreEqCoercion co1 simple_result),
+ (text "env=" <+> ppr env) $$
+ (text "input=" <+> ppr co) $$
+ (text "simple=" <+> ppr simple_result) $$
+ (text "opt=" <+> ppr co1) )
+ co1)
+ where
+ co1 = opt_co' env sym co
+ same_co_kind = s1 `eqType` s2 && t1 `eqType` t2
+ Pair s t = coercionKind (substCo env co)
+ (s1,t1) | sym = (t,s)
+ | otherwise = (s,t)
+ Pair s2 t2 = coercionKind co1
+
+ simple_result | sym = mkSymCo (substCo env co)
+ | otherwise = substCo env co
+-}
+
+opt_co' env _ (Refl ty) = Refl (substTy env ty)
+opt_co' env sym (SymCo co) = opt_co env (not sym) co
+opt_co' env sym (TyConAppCo tc cos) = mkTyConAppCo tc (map (opt_co env sym) cos)
+opt_co' env sym (AppCo co1 co2) = mkAppCo (opt_co env sym co1) (opt_co env sym co2)
+opt_co' env sym (ForAllCo tv co) = case substTyVarBndr env tv of
+ (env', tv') -> mkForAllCo tv' (opt_co env' sym co)
+ -- Use the "mk" functions to check for nested Refls
+
+opt_co' env sym (CoVarCo cv)
+ | Just co <- lookupCoVar env cv
+ = opt_co (zapCvSubstEnv env) sym co
+
+ | Just cv1 <- lookupInScope (getCvInScope env) cv
+ = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)
+ -- cv1 might have a substituted kind!
+
+ | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
+ ASSERT( isCoVar cv )
+ wrapSym sym (CoVarCo cv)
+
+opt_co' env sym (AxiomInstCo con cos)
+ -- Do *not* push sym inside top-level axioms
+ -- e.g. if g is a top-level axiom
+ -- g a : f a ~ a
+ -- then (sym (g ty)) /= g (sym ty) !!
+ = wrapSym sym $ AxiomInstCo con (map (opt_co env False) cos)
+ -- Note that the_co does *not* have sym pushed into it
+
+opt_co' env sym (UnsafeCo ty1 ty2)
+ | ty1' `eqType` ty2' = Refl ty1'
+ | sym = mkUnsafeCo ty2' ty1'
+ | otherwise = mkUnsafeCo ty1' ty2'
+ where
+ ty1' = substTy env ty1
+ ty2' = substTy env ty2
+
+opt_co' env sym (TransCo co1 co2)
+ | sym = opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g
+ | otherwise = opt_trans opt_co1 opt_co2
+ where
+ opt_co1 = opt_co env sym co1
+ opt_co2 = opt_co env sym co2
+
+opt_co' env sym (NthCo n co)
+ | TyConAppCo tc cos <- co'
+ , isDecomposableTyCon tc -- Not synonym families
+ = ASSERT( n < length cos )
+ cos !! n
+ | otherwise
+ = NthCo n co'
+ where
+ co' = opt_co env sym co
+
+opt_co' env sym (InstCo co ty)
+ -- See if the first arg is already a forall
+ -- ...then we can just extend the current substitution
+ | Just (tv, co_body) <- splitForAllCo_maybe co
+ = opt_co (extendTvSubst env tv ty') sym co_body
+
+ -- See if it is a forall after optimization
+ | Just (tv, co'_body) <- splitForAllCo_maybe co'
+ = substCoWithTy tv ty' co'_body -- An inefficient one-variable substitution
+
+ | otherwise = InstCo co' ty'
+
+ where
+ co' = opt_co env sym co
+ ty' = substTy env ty
+
+-------------
+opt_transList :: [NormalCo] -> [NormalCo] -> [NormalCo]
+opt_transList = zipWith opt_trans
+
+opt_trans :: NormalCo -> NormalCo -> NormalCo
+opt_trans co1 co2
+ | isReflCo co1 = co2
+ | otherwise = opt_trans1 co1 co2
+
+opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
+-- First arg is not the identity
+opt_trans1 co1 co2
+ | isReflCo co2 = co1
+ | otherwise = opt_trans2 co1 co2
+
+opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
+-- Neither arg is the identity
+opt_trans2 (TransCo co1a co1b) co2
+ -- Don't know whether the sub-coercions are the identity
+ = opt_trans co1a (opt_trans co1b co2)
+
+opt_trans2 co1 co2
+ | Just co <- opt_trans_rule co1 co2
+ = co
+
+opt_trans2 co1 (TransCo co2a co2b)
+ | Just co1_2a <- opt_trans_rule co1 co2a
+ = if isReflCo co1_2a
+ then co2b
+ else opt_trans1 co1_2a co2b
+
+opt_trans2 co1 co2
+ = mkTransCo co1 co2
+
+------
+-- Optimize coercions with a top-level use of transitivity.
+opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
+
+-- push transitivity down through matching top-level constructors.
+opt_trans_rule in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
+ | tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $
+ TyConAppCo tc1 (opt_transList cos1 cos2)
+
+-- push transitivity through matching destructors
+opt_trans_rule in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
+ | d1 == d2
+ , co1 `compatible_co` co2
+ = fireTransRule "PushNth" in_co1 in_co2 $
+ mkNthCo d1 (opt_trans co1 co2)
+
+-- Push transitivity inside instantiation
+opt_trans_rule in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
+ | ty1 `eqType` ty2
+ , co1 `compatible_co` co2
+ = fireTransRule "TrPushInst" in_co1 in_co2 $
+ mkInstCo (opt_trans co1 co2) ty1
+
+-- Push transitivity inside apply
+opt_trans_rule in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
+ = fireTransRule "TrPushApp" in_co1 in_co2 $
+ mkAppCo (opt_trans co1a co2a) (opt_trans co1b co2b)
+
+opt_trans_rule co1@(TyConAppCo tc cos1) co2
+ | Just cos2 <- etaTyConAppCo_maybe tc co2
+ = ASSERT( length cos1 == length cos2 )
+ fireTransRule "EtaCompL" co1 co2 $
+ TyConAppCo tc (zipWith opt_trans cos1 cos2)
+
+opt_trans_rule co1 co2@(TyConAppCo tc cos2)
+ | Just cos1 <- etaTyConAppCo_maybe tc co1
+ = ASSERT( length cos1 == length cos2 )
+ fireTransRule "EtaCompR" co1 co2 $
+ TyConAppCo tc (zipWith opt_trans cos1 cos2)
+
+-- Push transitivity inside forall
+opt_trans_rule co1 co2
+ | Just (tv1,r1) <- splitForAllCo_maybe co1
+ , Just (tv2,r2) <- etaForAllCo_maybe co2
+ , let r2' = substCoWithTy tv2 (mkTyVarTy tv1) r2
+ = fireTransRule "EtaAllL" co1 co2 $
+ mkForAllCo tv1 (opt_trans2 r1 r2')
+
+ | Just (tv2,r2) <- splitForAllCo_maybe co2
+ , Just (tv1,r1) <- etaForAllCo_maybe co1
+ , let r1' = substCoWithTy tv1 (mkTyVarTy tv2) r1
+ = fireTransRule "EtaAllR" co1 co2 $
+ mkForAllCo tv1 (opt_trans2 r1' r2)
+
+-- Push transitivity inside axioms
+opt_trans_rule co1 co2
+
+ -- TrPushAxR/TrPushSymAxR
+ | Just (sym, con, cos1) <- co1_is_axiom_maybe
+ , Just cos2 <- matchAxiom sym con co2
+ = fireTransRule "TrPushAxR" co1 co2 $
+ if sym
+ then SymCo $ AxiomInstCo con (opt_transList (map mkSymCo cos2) cos1)
+ else AxiomInstCo con (opt_transList cos1 cos2)
+
+ -- TrPushAxL/TrPushSymAxL
+ | Just (sym, con, cos2) <- co2_is_axiom_maybe
+ , Just cos1 <- matchAxiom (not sym) con co1
+ = fireTransRule "TrPushAxL" co1 co2 $
+ if sym
+ then SymCo $ AxiomInstCo con (opt_transList cos2 (map mkSymCo cos1))
+ else AxiomInstCo con (opt_transList cos1 cos2)
+
+ -- TrPushAxSym/TrPushSymAx
+ | Just (sym1, con1, cos1) <- co1_is_axiom_maybe
+ , Just (sym2, con2, cos2) <- co2_is_axiom_maybe
+ , con1 == con2
+ , sym1 == not sym2
+ , let qtvs = co_ax_tvs con1
+ lhs = co_ax_lhs con1
+ rhs = co_ax_rhs con1
+ pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
+ , all (`elemVarSet` pivot_tvs) qtvs
+ = fireTransRule "TrPushAxSym" co1 co2 $
+ if sym2
+ then liftCoSubstWith qtvs (opt_transList cos1 (map mkSymCo cos2)) lhs -- TrPushAxSym
+ else liftCoSubstWith qtvs (opt_transList (map mkSymCo cos1) cos2) rhs -- TrPushSymAx
+ where
+ co1_is_axiom_maybe = isAxiom_maybe co1
+ co2_is_axiom_maybe = isAxiom_maybe co2
+
+opt_trans_rule co1 co2 -- Identity rule
+ | Pair ty1 _ <- coercionKind co1
+ , Pair _ ty2 <- coercionKind co2
+ , ty1 `eqType` ty2
+ = fireTransRule "RedTypeDirRefl" co1 co2 $
+ Refl ty2
+
+opt_trans_rule _ _ = Nothing
+
+fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
+fireTransRule _rule _co1 _co2 res
+ = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
+ Just res
+
+-----------
+wrapSym :: Bool -> Coercion -> Coercion
+wrapSym sym co | sym = SymCo co
+ | otherwise = co
+
+-----------
+isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom, [Coercion])
+isAxiom_maybe (SymCo co)
+ | Just (sym, con, cos) <- isAxiom_maybe co
+ = Just (not sym, con, cos)
+isAxiom_maybe (AxiomInstCo con cos)
+ = Just (False, con, cos)
+isAxiom_maybe _ = Nothing
+
+matchAxiom :: Bool -- True = match LHS, False = match RHS
+ -> CoAxiom -> Coercion -> Maybe [Coercion]
+-- If we succeed in matching, then *all the quantified type variables are bound*
+-- E.g. if tvs = [a,b], lhs/rhs = [b], we'll fail
+matchAxiom sym (CoAxiom { co_ax_tvs = qtvs, co_ax_lhs = lhs, co_ax_rhs = rhs }) co
+ = case liftCoMatch (mkVarSet qtvs) (if sym then lhs else rhs) co of
+ Nothing -> Nothing
+ Just subst -> allMaybes (map (liftCoSubstTyVar subst) qtvs)
+
+-------------
+compatible_co :: Coercion -> Coercion -> Bool
+-- Check whether (co1 . co2) will be well-kinded
+compatible_co co1 co2
+ = x1 `eqType` x2
+ where
+ Pair _ x1 = coercionKind co1
+ Pair x2 _ = coercionKind co2
+
+-------------
+etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
+-- Try to make the coercion be of form (forall tv. co)
+etaForAllCo_maybe co
+ | Just (tv, r) <- splitForAllCo_maybe co
+ = Just (tv, r)
+
+ | Pair ty1 ty2 <- coercionKind co
+ , Just (tv1, _) <- splitForAllTy_maybe ty1
+ , Just (tv2, _) <- splitForAllTy_maybe ty2
+ , tyVarKind tv1 `eqKind` tyVarKind tv2
+ = Just (tv1, mkInstCo co (mkTyVarTy tv1))
+
+ | otherwise
+ = Nothing
+
+etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
+-- If possible, split a coercion
+-- g :: T s1 .. sn ~ T t1 .. tn
+-- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
+etaTyConAppCo_maybe tc (TyConAppCo tc2 cos2)
+ = ASSERT( tc == tc2 ) Just cos2
+
+etaTyConAppCo_maybe tc co
+ | isDecomposableTyCon tc
+ , Pair ty1 ty2 <- coercionKind co
+ , Just (tc1, tys1) <- splitTyConApp_maybe ty1
+ , Just (tc2, tys2) <- splitTyConApp_maybe ty2
+ , tc1 == tc2
+ , let n = length tys1
+ = ASSERT( tc == tc1 )
+ ASSERT( n == length tys2 )
+ Just (decomposeCo n co)
+ -- NB: n might be <> tyConArity tc
+ -- e.g. data family T a :: * -> *
+ -- g :: T a b ~ T c d
+
+ | otherwise
+ = Nothing
+\end{code}
-- its underlying representation type.
-- Returns Nothing if there is nothing to look through.
--
--- In the case of @newtype@s, it returns one of:
---
--- 1) A vanilla 'TyConApp' (recursive newtype, or non-saturated)
---
--- 2) The newtype representation (otherwise), meaning the
--- type written in the RHS of the newtype declaration,
--- which may itself be a newtype
---
--- For example, with:
---
--- > newtype R = MkR S
--- > newtype S = MkS T
--- > newtype T = MkT (T -> T)
---
--- 'expandNewTcApp' on:
---
--- * @R@ gives @Just S@
--- * @S@ gives @Just T@
--- * @T@ gives @Nothing@ (no expansion)
-
-- By being non-recursive and inlined, this case analysis gets efficiently
-- joined onto the case analysis that the caller is already doing
-coreView (PredTy p)
--- | isEqPred p = Nothing
- | otherwise = Just (predTypeRep p)
+coreView (PredTy p) = Just (predTypeRep p)
coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
= Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
-- Its important to use mkAppTys, rather than (foldl AppTy),
coreView _ = Nothing
-
-----------------------------------------------
{-# INLINE tcView #-}
tcView :: Type -> Maybe Type
repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
repSplitAppTy_maybe (TyConApp tc tys)
- | isDecomposableTyCon tc || length tys > tyConArity tc
- = case snocView tys of -- never create unsaturated type family apps
- Just (tys', ty') -> Just (TyConApp tc tys', ty')
- Nothing -> Nothing
+ | isDecomposableTyCon tc || tys `lengthExceeds` tyConArity tc
+ , Just (tys', ty') <- snocView tys
+ = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
repSplitAppTy_maybe _other = Nothing
-------------
splitAppTy :: Type -> (Type, Type)