+ n_tys = length tys
+ arity = coAxiomArity ax
+ rtys = map Refl tys
+
+-- | Apply a 'Coercion' to another 'Coercion'.
+mkAppCo :: Coercion -> Coercion -> Coercion
+mkAppCo (Refl ty1) (Refl ty2) = Refl (mkAppTy ty1 ty2)
+mkAppCo (Refl (TyConApp tc tys)) co = TyConAppCo tc (map Refl tys ++ [co])
+mkAppCo (TyConAppCo tc cos) co = TyConAppCo tc (cos ++ [co])
+mkAppCo co1 co2 = AppCo co1 co2
+-- Note, mkAppCo is careful to maintain invariants regarding
+-- where Refl constructors appear; see the comments in the definition
+-- of Coercion and the Note [Refl invariant] in types/TypeRep.lhs.
+
+-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
+-- See also 'mkAppCo'
+mkAppCos :: Coercion -> [Coercion] -> Coercion
+mkAppCos co1 tys = foldl mkAppCo co1 tys
+
+-- | Apply a type constructor to a list of coercions.
+mkTyConAppCo :: TyCon -> [Coercion] -> Coercion
+mkTyConAppCo tc cos
+ -- Expand type synonyms
+ | Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos
+ = mkAppCos (liftCoSubst (mkTopCvSubst tv_co_prs) rhs_ty) leftover_cos
+
+ | Just tys <- traverse isReflCo_maybe cos
+ = Refl (mkTyConApp tc tys) -- See Note [Refl invariant]
+
+ | otherwise = TyConAppCo tc cos
+
+-- | Make a function 'Coercion' between two other 'Coercion's
+mkFunCo :: Coercion -> Coercion -> Coercion
+mkFunCo co1 co2 = mkTyConAppCo funTyCon [co1, co2]
+
+-- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
+mkForAllCo :: Var -> Coercion -> Coercion
+-- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
+mkForAllCo tv (Refl ty) = ASSERT( isTyVar tv ) Refl (mkForAllTy tv ty)
+mkForAllCo tv co = ASSERT ( isTyVar tv ) ForAllCo tv co
+
+mkPredCo :: Pred Coercion -> Coercion
+-- See Note [Predicate coercions]
+mkPredCo (EqPred co1 co2) = mkTyConAppCo eqPredPrimTyCon [co1,co2]
+mkPredCo (ClassP cls cos) = mkTyConAppCo (classTyCon cls) cos
+mkPredCo (IParam _ co) = co
+
+-------------------------------
+
+-- | Create a symmetric version of the given 'Coercion' that asserts
+-- equality between the same types but in the other "direction", so
+-- a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
+mkSymCo :: Coercion -> Coercion
+
+-- Do a few simple optimizations, but don't bother pushing occurrences
+-- of symmetry to the leaves; the optimizer will take care of that.
+mkSymCo co@(Refl {}) = co
+mkSymCo (UnsafeCo ty1 ty2) = UnsafeCo ty2 ty1
+mkSymCo (SymCo co) = co
+mkSymCo co = SymCo co
+
+-- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
+mkTransCo :: Coercion -> Coercion -> Coercion
+mkTransCo (Refl _) co = co
+mkTransCo co (Refl _) = co
+mkTransCo co1 co2 = TransCo co1 co2
+
+mkNthCo :: Int -> Coercion -> Coercion
+mkNthCo n (Refl ty) = Refl (getNth n ty)
+mkNthCo n co = NthCo n co
+
+-- | Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
+-- the resulting beta-reduction, otherwise it creates a suspended instantiation.
+mkInstCo :: Coercion -> Type -> Coercion
+mkInstCo (ForAllCo tv co) ty = substCoWithTy tv ty co
+mkInstCo co ty = InstCo co ty
+
+-- | Manufacture a coercion from thin air. Needless to say, this is
+-- not usually safe, but it is used when we know we are dealing with
+-- bottom, which is one case in which it is safe. This is also used
+-- to implement the @unsafeCoerce#@ primitive. Optimise by pushing
+-- down through type constructors.
+mkUnsafeCo :: Type -> Type -> Coercion
+mkUnsafeCo ty1 ty2 | ty1 `eqType` ty2 = Refl ty1
+mkUnsafeCo (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+ | tc1 == tc2
+ = mkTyConAppCo tc1 (zipWith mkUnsafeCo tys1 tys2)
+
+mkUnsafeCo (FunTy a1 r1) (FunTy a2 r2)
+ = mkFunCo (mkUnsafeCo a1 a2) (mkUnsafeCo r1 r2)
+
+mkUnsafeCo ty1 ty2 = UnsafeCo ty1 ty2
+
+-- See note [Newtype coercions] in TyCon
+
+-- | Create a coercion constructor (axiom) suitable for the given
+-- newtype 'TyCon'. The 'Name' should be that of a new coercion
+-- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
+-- the type the appropriate right hand side of the @newtype@, with
+-- the free variables a subset of those 'TyVar's.
+mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom
+mkNewTypeCo name tycon tvs rhs_ty
+ = CoAxiom { co_ax_unique = nameUnique name
+ , co_ax_name = name
+ , co_ax_tvs = tvs
+ , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs)
+ , co_ax_rhs = rhs_ty }
+
+-- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
+-- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
+-- the coercion constructor built here, @F@ the family tycon and @R@ the (derived)
+-- representation tycon.
+mkFamInstCo :: Name -- ^ Unique name for the coercion tycon
+ -> [TyVar] -- ^ Type parameters of the coercion (@tvs@)
+ -> TyCon -- ^ Family tycon (@F@)
+ -> [Type] -- ^ Type instance (@ts@)
+ -> TyCon -- ^ Representation tycon (@R@)
+ -> CoAxiom -- ^ Coercion constructor (@Co@)
+mkFamInstCo name tvs family inst_tys rep_tycon
+ = CoAxiom { co_ax_unique = nameUnique name
+ , co_ax_name = name
+ , co_ax_tvs = tvs
+ , co_ax_lhs = mkTyConApp family inst_tys
+ , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
+
+mkPiCos :: [Var] -> Coercion -> Coercion
+mkPiCos vs co = foldr mkPiCo co vs
+
+mkPiCo :: Var -> Coercion -> Coercion
+mkPiCo v co | isTyVar v = mkForAllCo v co
+ | otherwise = mkFunCo (mkReflCo (varType v)) co
+\end{code}
+
+%************************************************************************
+%* *
+ Newtypes
+%* *
+%************************************************************************
+
+\begin{code}
+instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
+-- ^ If @co :: T ts ~ rep_ty@ then:
+--
+-- > instNewTyCon_maybe T ts = Just (rep_ty, co)
+instNewTyCon_maybe tc tys
+ | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc
+ = ASSERT( tys `lengthIs` tyConArity tc )
+ Just (substTyWith tvs tys ty, mkAxInstCo co_tc tys)
+ | otherwise
+ = Nothing
+
+-- this is here to avoid module loops
+splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
+-- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
+-- This function only strips *one layer* of @newtype@ off, so the caller will usually call
+-- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
+-- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
+--
+-- > splitNewTypeRepCo_maybe ty = Just (ty', co)
+--
+-- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
+splitNewTypeRepCo_maybe ty
+ | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
+splitNewTypeRepCo_maybe (TyConApp tc tys)
+ | Just (ty', co) <- instNewTyCon_maybe tc tys
+ = case co of
+ Refl _ -> panic "splitNewTypeRepCo_maybe"
+ -- This case handled by coreView
+ _ -> 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