-isCoVar tv = isTyVar tv && isCoercionKind (tyVarKind tv)
-
-type Coercion = Type
-type CoercionKind = Kind -- A CoercionKind is always of form (ty1 :=: ty2)
-
-coercionKind :: Coercion -> (Type, Type)
--- c :: (t1 :=: t2)
--- Then (coercionKind c) = (t1,t2)
-coercionKind (TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
- | otherwise = let t = (TyVarTy a) in (t, t)
-coercionKind (AppTy ty1 ty2)
- = let (t1, t2) = coercionKind ty1
- (s1, s2) = coercionKind ty2 in
- (mkAppTy t1 s1, mkAppTy t2 s2)
-coercionKind (TyConApp tc args)
- | Just (ar, rule) <- isCoercionTyCon_maybe tc
- -- CoercionTyCons carry their kinding rule, so we use it here
- = if length args >= ar
- then splitCoercionKind (rule args)
- else pprPanic ("arity/arguments mismatch in coercionKind:")
- (ppr ar $$ ppr tc <+> ppr args)
- | otherwise
- = let (lArgs, rArgs) = coercionKinds args in
- (TyConApp tc lArgs, TyConApp tc rArgs)
-coercionKind (FunTy ty1 ty2)
- = let (t1, t2) = coercionKind ty1
- (s1, s2) = coercionKind ty2 in
- (mkFunTy t1 s1, mkFunTy t2 s2)
-coercionKind (ForAllTy tv ty)
- = let (ty1, ty2) = coercionKind ty in
- (ForAllTy tv ty1, ForAllTy tv ty2)
-coercionKind (NoteTy _ ty) = coercionKind ty
-coercionKind (PredTy (EqPred c1 c2))
- = let k1 = coercionKindPredTy c1
- k2 = coercionKindPredTy c2 in
- (k1,k2)
-coercionKind (PredTy (ClassP cl args))
- = let (lArgs, rArgs) = coercionKinds args in
- (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
-coercionKind (PredTy (IParam name ty))
- = let (ty1, ty2) = coercionKind ty in
- (PredTy (IParam name ty1), PredTy (IParam name ty2))
-
-coercionKindPredTy :: Coercion -> CoercionKind
-coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
-
-coercionKinds :: [Coercion] -> ([Type], [Type])
-coercionKinds tys = unzip $ map coercionKind tys
-
--------------------------------------
--- Coercion kind and type mk's
--- (make saturated TyConApp CoercionTyCon{...} args)
-
-mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
- TyConApp coCon args
-
-mkAppCoercion, mkFunCoercion, mkTransCoercion, mkInstCoercion :: Coercion -> Coercion -> Coercion
-mkSymCoercion, mkLeftCoercion, mkRightCoercion :: Coercion -> Coercion
-
-mkAppCoercion co1 co2 = mkAppTy co1 co2
-mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
--- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
-mkForAllCoercion tv co = ASSERT ( isTyVar tv ) mkForAllTy tv co
-mkFunCoercion co1 co2 = mkFunTy co1 co2
-
-
--- This smart constructor creates a sym'ed version its argument,
--- but tries to push the sym's down to the leaves. If we come to
--- sym tv or sym tycon then we can drop the sym because tv and tycon
--- are reflexive coercions
-mkSymCoercion co
- | Just co2 <- splitSymCoercion_maybe co = co2
- -- sym (sym co) --> co
- | Just (co1, arg_tys) <- splitTyConApp_maybe co
- , not (isCoercionTyCon co1) = mkTyConApp co1 (map mkSymCoercion arg_tys)
- -- we can drop the sym for a TyCon
- -- sym (ty [t1, ..., tn]) --> ty [sym t1, ..., sym tn]
- | (co1, arg_tys) <- splitAppTys co
- , isTyVarTy co1 = mkAppTys (maybe_drop co1) (map mkSymCoercion arg_tys)
- -- sym (tv [t1, ..., tn]) --> tv [sym t1, ..., sym tn]
- -- if tv type variable
- -- sym (cv [t1, ..., tn]) --> (sym cv) [sym t1, ..., sym tn]
- -- if cv is a coercion variable
- -- fall through if head is a CoercionTyCon
- | Just (co1, co2) <- splitTransCoercion_maybe co
- -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
- = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
- | Just (co, ty) <- splitInstCoercion_maybe co
- -- sym (co @ ty) --> (sym co) @ ty
- = mkInstCoercion (mkSymCoercion co) ty
- | Just co <- splitLeftCoercion_maybe co
- -- sym (left co) --> left (sym co)
- = mkLeftCoercion (mkSymCoercion co)
- | Just co <- splitRightCoercion_maybe co
- -- sym (right co) --> right (sym co)
- = mkRightCoercion (mkSymCoercion co)
- where
- maybe_drop (TyVarTy tv)
- | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
- | otherwise = TyVarTy tv
- maybe_drop other = other
-mkSymCoercion (ForAllTy tv ty) = ForAllTy tv (mkSymCoercion ty)
--- for atomic types and constructors, we can just ignore sym since these
--- are reflexive coercions
-mkSymCoercion (TyVarTy tv)
- | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
- | otherwise = TyVarTy tv
-mkSymCoercion co = mkCoercion symCoercionTyCon [co]
-
--- Smart constructors for left and right
-mkLeftCoercion co
- | Just (co', _) <- splitAppCoercion_maybe co = co'
- | otherwise = mkCoercion leftCoercionTyCon [co]
-
-mkRightCoercion co
- | Just (co1, co2) <- splitAppCoercion_maybe co = co2
- | otherwise = mkCoercion rightCoercionTyCon [co]
-
-mkTransCoercion co1 co2 = mkCoercion transCoercionTyCon [co1, co2]
-
-mkInstCoercion co ty = mkCoercion instCoercionTyCon [co, ty]
-
-mkInstsCoercion co tys = foldl mkInstCoercion co tys
-
-splitSymCoercion_maybe :: Coercion -> Maybe Coercion
-splitSymCoercion_maybe (TyConApp tc [co]) =
- if tc `hasKey` symCoercionTyConKey
- then Just co
- else Nothing
-splitSymCoercion_maybe co = Nothing
-
-splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
--- Splits a coercion application, being careful *not* to split (left c), etc
--- which are really sytactic constructs, not applications
-splitAppCoercion_maybe co | Just co' <- coreView co = splitAppCoercion_maybe co'
-splitAppCoercion_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
-splitAppCoercion_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
-splitAppCoercion_maybe (TyConApp tc tys)
- | not (isCoercionTyCon tc)
- = case snocView tys of
- Just (tys', ty') -> Just (TyConApp tc tys', ty')
- Nothing -> Nothing
-splitAppCoercion_maybe co = Nothing
-
-splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
-splitTransCoercion_maybe (TyConApp tc [ty1, ty2])
- = if tc `hasKey` transCoercionTyConKey then
- Just (ty1, ty2)
- else
- Nothing
-splitTransCoercion_maybe other = Nothing
-
-splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
-splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
- = if tc `hasKey` instCoercionTyConKey then
- Just (ty1, ty2)
- else
- Nothing
-splitInstCoercion_maybe other = Nothing
-
-splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
-splitLeftCoercion_maybe (TyConApp tc [co])
- = if tc `hasKey` leftCoercionTyConKey then
- Just co
- else
- Nothing
-splitLeftCoercion_maybe other = Nothing
-
-splitRightCoercion_maybe :: Coercion -> Maybe Coercion
-splitRightCoercion_maybe (TyConApp tc [co])
- = if tc `hasKey` rightCoercionTyConKey then
- Just co
- else
- Nothing
-splitRightCoercion_maybe other = Nothing
-
--- Unsafe coercion is not safe, it is used when we know we are dealing with
--- 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
- = mkCoercion unsafeCoercionTyCon [ty1, ty2]