mkSymCoercion, mkTransCoercion,
mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
- mkNewTypeCoercion, mkAppsCoercion,
+ mkNewTypeCoercion, mkDataInstCoercion, mkAppsCoercion,
splitNewTypeRepCo_maybe, decomposeCo,
kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys,
coreEqType, splitAppTys, isTyVarTy, splitTyConApp_maybe
)
-import TyCon ( TyCon, tyConArity, mkCoercionTyCon, isNewTyCon,
- newTyConRhs, newTyConCo,
+import TyCon ( TyCon, tyConArity, mkCoercionTyCon, isClosedNewTyCon,
+ newTyConRhs, newTyConCo_maybe,
isCoercionTyCon, isCoercionTyCon_maybe )
import Var ( Var, TyVar, isTyVar, tyVarKind )
import Name ( BuiltInSyntax(..), Name, mkWiredInName, tcName )
splitRightCoercion_maybe other = Nothing
-- Unsafe coercion is not safe, it is used when we know we are dealing with
--- bottom, which is the one case in which it is safe. It is also used to
+-- bottom, which is one case in which it is safe. It is also used to
-- implement the unsafeCoerce# primitive.
mkUnsafeCoercion :: Type -> Type -> Coercion
mkUnsafeCoercion ty1 ty2
-- See note [Newtype coercions] in TyCon
-mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
-mkNewTypeCoercion name tycon tvs rhs_ty
- = ASSERT (length tvs == tyConArity tycon)
- mkCoercionTyCon name (tyConArity tycon) rule
+mkNewTypeCoercion :: Name -> TyCon -> ([TyVar], Type) -> TyCon
+mkNewTypeCoercion name tycon (tvs, rhs_ty)
+ = mkCoercionTyCon name co_con_arity (mkKindingFun rule)
where
- rule args = mkCoKind (TyConApp tycon args) (substTyWith tvs args rhs_ty)
+ co_con_arity = length tvs
+
+ rule args = (TyConApp tycon tys, substTyWith tvs tys rhs_ty, rest)
+ where
+ tys = take co_con_arity args
+ rest = drop co_con_arity args
+
+-- Coercion identifying a data/newtype representation type and its family
+-- instance. It has the form `Co tvs :: F ts :=: R tvs', where `Co' is the
+-- coercion tycon built here, `F' the family tycon and `R' the (derived)
+-- representation tycon.
+--
+mkDataInstCoercion :: 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')
+ -> TyCon -- => coercion tycon (`Co')
+mkDataInstCoercion name tvs family instTys rep_tycon
+ = mkCoercionTyCon name coArity (mkKindingFun rule)
+ where
+ coArity = length tvs
+
+ rule args = (substTyWith tvs tys $ -- with sigma = [tys/tvs],
+ TyConApp family instTys, -- sigma (F ts)
+ TyConApp rep_tycon tys, -- :=: R tys
+ rest) -- surplus arguments
+ where
+ tys = take coArity args
+ rest = drop coArity args
--------------------------------------
-- Coercion Type Constructors...
-- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
--
-- (mkKindingFun f) is given the args [c, sym d, sym e]
-mkKindingFun :: ([Type] -> (Type, Type, [Type])) -> [Type] -> Kind
+mkKindingFun :: ([Type] -> (Type, Type, [Type]))
+ -> [Type] -> Kind
mkKindingFun f args =
let (ty1, ty2, rest) = f args in
let (argtys1, argtys2) = unzip (map coercionKind rest) in
splitNewTypeRepCo_maybe ty
| Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
splitNewTypeRepCo_maybe (TyConApp tc tys)
- | isNewTyCon tc
+ | isClosedNewTyCon tc
= ASSERT( tys `lengthIs` tyConArity tc ) -- splitNewTypeRepCo_maybe only be applied
-- to *types* (of kind *)
case newTyConRhs tc of
ASSERT( length tvs == length tys )
Just (substTyWith tvs tys rep_ty, mkTyConApp co_con tys)
where
- co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo tc)
+ co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo_maybe tc)
splitNewTypeRepCo_maybe other = Nothing
\end{code}