-
-%************************************************************************
-%* *
- Coercion Type Constructors
-%* *
-%************************************************************************
-
-Example. The coercion ((sym c) (sym d) (sym e))
-will be represented by (TyConApp sym [c, sym d, sym e])
-If sym c :: p1=q1
- sym d :: p2=q2
- sym e :: p3=q3
-then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
-
-\begin{code}
--- | Coercion type constructors: avoid using these directly and instead use
--- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
---
--- Each coercion TyCon is built with the special CoercionTyCon record and
--- carries its own kinding rule. Such CoercionTyCons must be fully applied
--- by any TyConApp in which they are applied, however they may also be over
--- applied (see example above) and the kinding function must deal with this.
-symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon,
- rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
- csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
-
-symCoercionTyCon
- = mkCoercionTyCon symCoercionTyConName 1 kc_sym
- where
- kc_sym :: CoTyConKindChecker
- kc_sym _kc_ty kc_co _ (co:_)
- = do { (ty1,ty2) <- kc_co co
- ; return (ty2,ty1) }
- kc_sym _ _ _ _ = panic "kc_sym"
-
-transCoercionTyCon
- = mkCoercionTyCon transCoercionTyConName 2 kc_trans
- where
- kc_trans :: CoTyConKindChecker
- kc_trans _kc_ty kc_co checking (co1:co2:_)
- = do { (a1, r1) <- kc_co co1
- ; (a2, r2) <- kc_co co2
- ; unless (not checking || (r1 `coreEqType` a2))
- (fail "Trans coercion mis-match")
- ; return (a1, r2) }
- kc_trans _ _ _ _ = panic "kc_sym"
-
----------------------------------------------------
-leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 (kcLR_help fst)
-rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (kcLR_help snd)
-
-kcLR_help :: (forall a. (a,a)->a) -> CoTyConKindChecker
-kcLR_help select _kc_ty kc_co _checking (co : _)
- = do { (ty1, ty2) <- kc_co co
- ; case decompLR_maybe ty1 ty2 of
- Nothing -> fail "decompLR"
- Just res -> return (select res) }
-kcLR_help _ _ _ _ _ = panic "kcLR_help"
-
-decompLR_maybe :: Type -> Type -> Maybe ((Type,Type), (Type,Type))
--- Helper for left and right. Finds coercion kind of its input and
--- returns the left and right projections of the coercion...
---
--- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
-decompLR_maybe ty1 ty2
- | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
- , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
- = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
-decompLR_maybe _ _ = Nothing
-
----------------------------------------------------
-instCoercionTyCon
- = mkCoercionTyCon instCoercionTyConName 2 kcInst_help
- where
- kcInst_help :: CoTyConKindChecker
- kcInst_help kc_ty kc_co checking (co : ty : _)
- = do { (t1,t2) <- kc_co co
- ; k <- kc_ty ty
- ; case decompInst_maybe t1 t2 of
- Nothing -> fail "decompInst"
- Just ((tv1,tv2), (ty1,ty2)) -> do
- { unless (not checking || (k `isSubKind` tyVarKind tv1))
- (fail "Coercion instantation kind mis-match")
- ; return (substTyWith [tv1] [ty] ty1,
- substTyWith [tv2] [ty] ty2) } }
- kcInst_help _ _ _ _ = panic "kcInst_help"
-
-decompInst_maybe :: Type -> Type -> Maybe ((TyVar,TyVar), (Type,Type))
-decompInst_maybe ty1 ty2
- | Just (tv1,r1) <- splitForAllTy_maybe ty1
- , Just (tv2,r2) <- splitForAllTy_maybe ty2
- = Just ((tv1,tv2), (r1,r2))
-decompInst_maybe _ _ = Nothing
-
----------------------------------------------------
-unsafeCoercionTyCon
- = mkCoercionTyCon unsafeCoercionTyConName 2 kc_unsafe
- where
- kc_unsafe kc_ty _kc_co _checking (ty1:ty2:_)
- = do { _ <- kc_ty ty1
- ; _ <- kc_ty ty2
- ; return (ty1,ty2) }
- kc_unsafe _ _ _ _ = panic "kc_unsafe"
-
----------------------------------------------------
--- The csel* family
-
-csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 (kcCsel_help fstOf3)
-csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 (kcCsel_help sndOf3)
-cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (kcCsel_help thirdOf3)
-
-kcCsel_help :: (forall a. (a,a,a) -> a) -> CoTyConKindChecker
-kcCsel_help select _kc_ty kc_co _checking (co : _)
- = do { (ty1,ty2) <- kc_co co
- ; case decompCsel_maybe ty1 ty2 of
- Nothing -> fail "decompCsel"
- Just res -> return (select res) }
-kcCsel_help _ _ _ _ _ = panic "kcCsel_help"
-
-decompCsel_maybe :: Type -> Type -> Maybe ((Type,Type), (Type,Type), (Type,Type))
--- If co :: (s1~t1 => r1) ~ (s2~t2 => r2)
--- Then csel1 co :: s1 ~ s2
--- csel2 co :: t1 ~ t2
--- cselR co :: r1 ~ r2
-decompCsel_maybe ty1 ty2
- | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
- , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
- = Just ((s1,s2), (t1,t2), (r1,r2))
-decompCsel_maybe _ _ = Nothing
-
-fstOf3 :: (a,b,c) -> a
-sndOf3 :: (a,b,c) -> b
-thirdOf3 :: (a,b,c) -> c
-fstOf3 (a,_,_) = a
-sndOf3 (_,b,_) = b
-thirdOf3 (_,_,c) = c
-
---------------------------------------
--- Their Names
-
-transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
- rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
- csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
-
-transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
-symCoercionTyConName = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
-leftCoercionTyConName = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
-rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
-instCoercionTyConName = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
-csel1CoercionTyConName = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
-csel2CoercionTyConName = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
-cselRCoercionTyConName = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
-unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
-
-mkCoConName :: FastString -> Unique -> TyCon -> Name
-mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
- key (ATyCon coCon) BuiltInSyntax
-\end{code}
-
-