+ _ -> Just (ty', co)
+splitNewTypeRepCo_maybe _
+ = Nothing
+
+-- | Determines syntactic equality of coercions
+coreEqCoercion :: Coercion -> Coercion -> Bool
+coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
+ where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
+
+coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
+coreEqCoercion2 env (Refl ty1) (Refl ty2) = eqTypeX env ty1 ty2
+coreEqCoercion2 env (TyConAppCo tc1 cos1) (TyConAppCo tc2 cos2)
+ = tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2
+
+coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22)
+ = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
+
+coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2)
+ = coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2
+
+coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2)
+ = rnOccL env cv1 == rnOccR env cv2
+
+coreEqCoercion2 env (AxiomInstCo con1 cos1) (AxiomInstCo con2 cos2)
+ = con1 == con2
+ && all2 (coreEqCoercion2 env) cos1 cos2
+
+coreEqCoercion2 env (UnsafeCo ty11 ty12) (UnsafeCo ty21 ty22)
+ = eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
+
+coreEqCoercion2 env (SymCo co1) (SymCo co2)
+ = coreEqCoercion2 env co1 co2
+
+coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
+ = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
+
+coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
+ = d1 == d2 && coreEqCoercion2 env co1 co2
+
+coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
+ = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
+
+coreEqCoercion2 _ _ _ = False
+\end{code}
+
+%************************************************************************
+%* *
+ Substitution of coercions
+%* *
+%************************************************************************
+
+\begin{code}
+-- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
+-- doing a \"lifting\" substitution)
+type CvSubstEnv = VarEnv Coercion
+
+emptyCvSubstEnv :: CvSubstEnv
+emptyCvSubstEnv = emptyVarEnv
+
+data CvSubst
+ = CvSubst InScopeSet -- The in-scope type variables
+ TvSubstEnv -- Substitution of types
+ CvSubstEnv -- Substitution of coercions
+
+instance Outputable CvSubst where
+ ppr (CvSubst ins tenv cenv)
+ = brackets $ sep[ ptext (sLit "CvSubst"),
+ nest 2 (ptext (sLit "In scope:") <+> ppr ins),
+ nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
+ nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
+
+emptyCvSubst :: CvSubst
+emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
+
+isEmptyCvSubst :: CvSubst -> Bool
+isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
+
+getCvInScope :: CvSubst -> InScopeSet
+getCvInScope (CvSubst in_scope _ _) = in_scope
+
+zapCvSubstEnv :: CvSubst -> CvSubst
+zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
+
+cvTvSubst :: CvSubst -> TvSubst
+cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
+
+tvCvSubst :: TvSubst -> CvSubst
+tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
+
+extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
+extendTvSubst (CvSubst in_scope tenv cenv) tv ty
+ = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
+
+substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
+substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
+ = ASSERT( isCoVar old_var )
+ (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
+ where
+ -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
+ -- In that case, mkCoVarCo will return a ReflCoercion, and
+ -- we want to substitute that (not new_var) for old_var
+ new_co = mkCoVarCo new_var
+ no_change = new_var == old_var && not (isReflCo new_co)
+
+ new_cenv | no_change = delVarEnv cenv old_var
+ | otherwise = extendVarEnv cenv old_var new_co
+
+ new_var = uniqAway in_scope subst_old_var
+ subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
+ -- It's important to do the substitution for coercions,
+ -- because only they can have free type variables
+
+substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
+substTyVarBndr (CvSubst in_scope tenv cenv) old_var
+ = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
+ (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
+
+zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
+zipOpenCvSubst vs cos
+ | debugIsOn && (length vs /= length cos)
+ = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
+ | otherwise
+ = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
+
+mkTopCvSubst :: [(Var,Coercion)] -> CvSubst
+mkTopCvSubst prs = CvSubst emptyInScopeSet emptyTvSubstEnv (mkVarEnv prs)
+
+substCoWithTy :: TyVar -> Type -> Coercion -> Coercion
+substCoWithTy tv ty = substCoWithTys [tv] [ty]
+
+substCoWithTys :: [TyVar] -> [Type] -> Coercion -> Coercion
+substCoWithTys tvs tys co
+ | debugIsOn && (length tvs /= length tys)
+ = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
+ | otherwise
+ = ASSERT( length tvs == length tys )
+ substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
+ where
+ in_scope = mkInScopeSet (tyVarsOfTypes tys)
+
+-- | Substitute within a 'Coercion'
+substCo :: CvSubst -> Coercion -> Coercion
+substCo subst co | isEmptyCvSubst subst = co
+ | otherwise = subst_co subst co
+
+-- | Substitute within several 'Coercion's
+substCos :: CvSubst -> [Coercion] -> [Coercion]
+substCos subst cos | isEmptyCvSubst subst = cos
+ | otherwise = map (substCo subst) cos
+
+substTy :: CvSubst -> Type -> Type
+substTy subst = Type.substTy (cvTvSubst subst)
+
+subst_co :: CvSubst -> Coercion -> Coercion
+subst_co subst co
+ = go co
+ where
+ go_ty :: Type -> Type
+ go_ty = Coercion.substTy subst
+
+ go :: Coercion -> Coercion
+ 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 (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
+ go (SymCo co) = mkSymCo (go co)
+ go (TransCo co1 co2) = mkTransCo (go co1) (go co2)
+ go (NthCo d co) = mkNthCo d (go co)
+ go (InstCo co ty) = mkInstCo (go co) $! go_ty ty
+
+substCoVar :: CvSubst -> CoVar -> Coercion
+substCoVar (CvSubst in_scope _ cenv) cv
+ | Just co <- lookupVarEnv cenv cv = co
+ | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
+ | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv )
+ ASSERT( isCoVar cv ) CoVarCo cv
+
+substCoVars :: CvSubst -> [CoVar] -> [Coercion]
+substCoVars subst cvs = map (substCoVar subst) cvs
+
+lookupTyVar :: CvSubst -> TyVar -> Maybe Type
+lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
+
+lookupCoVar :: CvSubst -> Var -> Maybe Coercion
+lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
+\end{code}
+
+%************************************************************************
+%* *
+ "Lifting" substitution
+ [(TyVar,Coercion)] -> Type -> Coercion
+%* *
+%************************************************************************
+
+\begin{code}
+liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
+liftCoSubstWith tvs cos = liftCoSubst (zipOpenCvSubst tvs cos)
+
+-- | The \"lifting\" operation which substitutes coercions for type
+-- variables in a type to produce a coercion.
+--
+-- For the inverse operation, see 'liftCoMatch'
+liftCoSubst :: CvSubst -> Type -> Coercion
+-- The CvSubst maps TyVar -> Type (mainly for cloning foralls)
+-- TyVar -> Coercion (this is the payload)
+-- The unusual thing is that the *coercion* substitution maps
+-- some *type* variables. That's the whole point of this function!
+liftCoSubst subst ty | isEmptyCvSubst subst = Refl ty
+ | otherwise = ty_co_subst subst ty
+
+ty_co_subst :: CvSubst -> Type -> Coercion
+ty_co_subst subst ty
+ = go ty
+ where
+ go (TyVarTy tv) = liftCoSubstTyVar subst tv `orElse` Refl (TyVarTy tv)
+ go (AppTy ty1 ty2) = mkAppCo (go ty1) (go ty2)
+ go (TyConApp tc tys) = mkTyConAppCo tc (map go tys)
+ go (FunTy ty1 ty2) = mkFunCo (go ty1) (go ty2)
+ go (ForAllTy v ty) = mkForAllCo v' $! (ty_co_subst subst' ty)
+ where
+ (subst', v') = liftCoSubstTyVarBndr subst v
+ go (PredTy p) = mkPredCo (go <$> p)
+
+liftCoSubstTyVar :: CvSubst -> TyVar -> Maybe Coercion
+liftCoSubstTyVar subst@(CvSubst _ tenv cenv) tv
+ = case (lookupVarEnv tenv tv, lookupVarEnv cenv tv) of
+ (Nothing, Nothing) -> Nothing
+ (Just ty, Nothing) -> Just (Refl ty)
+ (Nothing, Just co) -> Just co
+ (Just {}, Just {}) -> pprPanic "ty_co_subst" (ppr tv $$ ppr subst)
+
+liftCoSubstTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
+liftCoSubstTyVarBndr (CvSubst in_scope tenv cenv) old_var
+ = (CvSubst (in_scope `extendInScopeSet` new_var)
+ new_tenv
+ (delVarEnv cenv old_var) -- See Note [Lifting substitutions]
+ , new_var)
+ where
+ new_tenv | no_change = delVarEnv tenv old_var
+ | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
+
+ no_change = new_var == old_var
+ new_var = uniqAway in_scope old_var
+\end{code}
+
+Note [Lifting substitutions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider liftCoSubstWith [a] [co] (a, forall a. a)
+Then we want to substitute for the free 'a', but obviously not for
+the bound 'a'. hence the (delVarEnv cent old_var) in liftCoSubstTyVarBndr.
+
+This also why we need a full CvSubst when doing lifting substitutions.
+
+\begin{code}
+-- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
+-- @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
+-- That is, it matches a type against a coercion of the same
+-- "shape", and returns a lifting substitution which could have been
+-- used to produce the given coercion from the given type.
+liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe CvSubst
+liftCoMatch tmpls ty co
+ = case ty_co_match menv (emptyVarEnv, emptyVarEnv) ty co of
+ Just (tv_env, cv_env) -> Just (CvSubst in_scope tv_env cv_env)
+ Nothing -> Nothing
+ where
+ menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
+ in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
+ -- Like tcMatchTy, assume all the interesting variables
+ -- in ty are in tmpls
+
+type TyCoSubstEnv = (TvSubstEnv, CvSubstEnv)
+ -- Used locally inside ty_co_match only
+
+-- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
+ty_co_match :: MatchEnv -> TyCoSubstEnv -> Type -> Coercion -> Maybe TyCoSubstEnv
+ty_co_match menv subst ty co | Just ty' <- coreView ty = ty_co_match menv subst ty' co
+
+ -- Deal with the Refl case by delegating to type matching
+ty_co_match menv (tenv, cenv) ty co
+ | Just ty' <- isReflCo_maybe co
+ = case ruleMatchTyX ty_menv tenv ty ty' of
+ Just tenv' -> Just (tenv', cenv)
+ Nothing -> Nothing
+ where
+ ty_menv = menv { me_tmpls = me_tmpls menv `minusUFM` cenv }
+ -- Remove from the template set any variables already bound to non-refl coercions
+
+ -- Match a type variable against a non-refl coercion
+ty_co_match menv subst@(tenv, cenv) (TyVarTy tv1) co
+ | Just {} <- lookupVarEnv tenv tv1' -- tv1' is already bound to (Refl ty)
+ = Nothing -- The coercion 'co' is not Refl
+
+ | Just co1' <- lookupVarEnv cenv tv1' -- tv1' is already bound to co1
+ = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
+ then Just subst
+ else Nothing -- no match since tv1 matches two different coercions
+
+ | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
+ = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
+ then Nothing -- occurs check failed
+ else return (tenv, extendVarEnv cenv tv1' co)
+ -- BAY: I don't think we need to do any kind matching here yet
+ -- (compare 'match'), but we probably will when moving to SHE.
+
+ | otherwise -- tv1 is not a template ty var, so the only thing it
+ -- can match is a reflexivity coercion for itself.
+ -- But that case is dealt with already