- (s1,t1) `eq` (s2,t2) = s1 `coreEqType` s2 && t1 `coreEqType` t2
-
- (result,_,_) = go co
- -- optimized, changed?, identity?
- go :: Coercion -> ( Coercion, Bool, Bool )
- -- traverse coercion term bottom up and return
- --
- -- 1) equivalent coercion, in optimized form
- --
- -- 2) whether the output coercion differs from
- -- the input coercion
- --
- -- 3) whether the coercion is an identity coercion
- --
- -- Performs the following optimizations:
- --
- -- sym id >-> id
- -- trans id co >-> co
- -- trans co id >-> co
- -- sym (sym co) >-> co
- -- trans g (sym g) >-> id
- -- trans (sym g) g >-> id
- --
- go ty@(TyVarTy a) | isCoVar a = let (ty1,ty2) = coercionKind ty
- in (ty, False, ty1 `coreEqType` ty2)
- | otherwise = (ty, False, True)
- go ty@(AppTy ty1 ty2)
- = let (ty1', chan1, id1) = go ty1
- (ty2', chan2, id2) = go ty2
- in if chan1 || chan2
- then (AppTy ty1' ty2', True, id1 && id2)
- else (ty , False, id1 && id2)
- go ty@(TyConApp tc args)
- | tc == symCoercionTyCon, (ty1:tys) <- args
- = goSym ty ty1 tys
- | tc == transCoercionTyCon, [ty1,ty2] <- args
- = goTrans ty ty1 ty2
- | tc == leftCoercionTyCon, [ty1] <- args
- = goLeft ty ty1
- | tc == rightCoercionTyCon, [ty1] <- args
- = goRight ty ty1
- | tc == instCoercionTyCon, [ty1,ty2] <- args
- = goInst ty ty1 ty2
- | not (isCoercionTyCon tc)
- = let (args', chans, ids) = mapAndUnzip3 go args
- in if or chans
- then (TyConApp tc args', True , and ids)
- else (ty , False, and ids)
- | otherwise
- = (ty, False, False)
- go ty@(FunTy ty1 ty2)
- = let (ty1',chan1,id1) = go ty1
- (ty2',chan2,id2) = go ty2
- in if chan1 || chan2
- then (FunTy ty1' ty2', True , id1 && id2)
- else (ty , False, id1 && id2)
- go ty@(ForAllTy tv ty1)
- = let (ty1', chan1, id1) = go ty1
- in if chan1
- then (ForAllTy tv ty1', True , id1)
- else (ty , False, id1)
- go ty@(PredTy (EqPred ty1 ty2))
- = let (ty1', chan1, id1) = go ty1
- (ty2', chan2, id2) = go ty2
- in if chan1 || chan2
- then (PredTy (EqPred ty1' ty2'), True , id1 && id2)
- else (ty , False, id1 && id2)
- go ty@(PredTy (ClassP cl args))
- = let (args', chans, ids) = mapAndUnzip3 go args
- in if or chans
- then (PredTy (ClassP cl args'), True , and ids)
- else (ty , False, and ids)
- go ty@(PredTy (IParam name ty1))
- = let (ty1', chan1, id1) = go ty1
- in if chan1
- then (PredTy (IParam name ty1'), True , id1)
- else (ty , False, id1)
-
- goSym :: Coercion -> Coercion -> [Coercion] -> ( Coercion, Bool, Bool )
- --
- -- pushes the sym constructor inwards, if possible
- --
- -- takes original coercion term
- -- first argument
- -- rest of arguments
- goSym ty ty1 tys
- = case mkSymCoercion ty1 of
- (TyConApp tc _ ) | tc == symCoercionTyCon
- -> let (tys',chans',ids) = mapAndUnzip3 go (ty1:tys)
- in if or chans'
- then (TyConApp symCoercionTyCon tys', True , and ids)
- else (ty , False, and ids)
- ty1' -> let (ty',_ ,id') = go (mkAppsCoercion ty1' tys)
- in (ty',True,id')
-
-
- goRight :: Coercion -> Coercion -> ( Coercion, Bool, Bool )
- --
- -- reduces the right constructor, if possible
- --
- -- takes original coercion term
- -- argument
- --
- goRight ty ty1
- = case mkRightCoercion ty1 of
- (TyConApp tc _ ) | tc == rightCoercionTyCon
- -> let (ty1',chan1,id1) = go ty1
- in if chan1
- then (TyConApp rightCoercionTyCon [ty1'], True , id1)
- else (ty , False, id1)
- ty1' -> let (ty',_ ,id') = go ty1'
- in (ty',True,id')
-
- goLeft :: Coercion -> Coercion -> ( Coercion, Bool, Bool )
- --
- -- reduces the left constructor, if possible
- --
- -- takes original coercion term
- -- argument
- --
- goLeft ty ty1
- = case mkLeftCoercion ty1 of
- (TyConApp tc _ ) | tc == leftCoercionTyCon
- -> let (ty1',chan1,id1) = go ty1
- in if chan1
- then (TyConApp leftCoercionTyCon [ty1'], True , id1)
- else (ty , False, id1)
- ty1' -> let (ty',_ ,id') = go ty1'
- in (ty',True,id')
-
- goInst :: Coercion -> Coercion -> Coercion -> ( Coercion, Bool, Bool )
- --
- -- reduces the inst constructor, if possible
- --
- -- takes original coercion term
- -- coercion argument
- -- type argument
- --
- goInst ty ty1 ty2
- = case mkInstCoercion ty1 ty2 of
- (TyConApp tc _ ) | tc == instCoercionTyCon
- -> let (ty1',chan1,id1) = go ty1
- in if chan1
- then (TyConApp instCoercionTyCon [ty1',ty2], True , id1)
- else (ty , False, id1)
- ty1' -> let (ty',_ ,id') = go ty1'
- in (ty',True,id')
-
- goTrans :: Coercion -> Coercion -> Coercion -> ( Coercion, Bool, Bool )
- --
- -- trans id co >-> co
- -- trans co id >-> co
- -- trans g (sym g) >-> id
- -- trans (sym g) g >-> id
- --
- goTrans ty ty1 ty2
- | id1
- = (ty2', True, id2)
- | id2
- = (ty1', True, False)
- | chan1 || chan2
- = (TyConApp transCoercionTyCon [ty1',ty2'], True , False)
- | Just ty' <- mty'
- = (ty', True, True)
- | otherwise
- = (ty, False, False)
- where (ty1', chan1, id1) = go ty1
- (ty2', chan2, id2) = go ty2
- mty' = case mkTransCoercion ty1' ty2'
- of (TyConApp tc _) | tc == transCoercionTyCon
- -> Nothing
- ty' -> Just ty'
-\end{code}
+ coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
+
+------------------
+-- | Apply 'coercionKind' to multiple 'Coercion's
+coercionKinds :: [Coercion] -> ([Type], [Type])
+coercionKinds tys = unzip $ map coercionKind tys
+
+------------------
+-- | 'coTyConAppKind' is given a list of the type arguments to the 'CoTyCon',
+-- and constructs the types that the resulting coercion relates.
+-- Fails (in the monad) if ill-kinded.
+-- Typically the monad is
+-- either the Lint monad (with the consistency-check flag = True),
+-- or the ID monad with a panic on failure (and the consistency-check flag = False)
+coTyConAppKind
+ :: CoTyConDesc
+ -> [Type] -- Exactly right number of args
+ -> (Type, Type) -- Kind of this application
+coTyConAppKind CoUnsafe (ty1:ty2:_)
+ = (ty1,ty2)
+coTyConAppKind CoSym (co:_)
+ | (ty1,ty2) <- coercionKind co = (ty2,ty1)
+coTyConAppKind CoTrans (co1:co2:_)
+ = (fst (coercionKind co1), snd (coercionKind co2))
+coTyConAppKind CoLeft (co:_)
+ | Just (res,_) <- decompLR_maybe (coercionKind co) = res
+coTyConAppKind CoRight (co:_)
+ | Just (_,res) <- decompLR_maybe (coercionKind co) = res
+coTyConAppKind CoCsel1 (co:_)
+ | Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res
+coTyConAppKind CoCsel2 (co:_)
+ | Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res
+coTyConAppKind CoCselR (co:_)
+ | Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res
+coTyConAppKind CoInst (co:ty:_)
+ | Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co)
+ = (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2)
+coTyConAppKind (CoAxiom { co_ax_tvs = tvs
+ , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
+ = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
+ where
+ (tys1, tys2) = coercionKinds cos
+coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat
+ [ ppr co <+> dcolon <+> pprEqPred (coercionKind co)
+ | co <- cos ])) $
+ coercionKind (head cos)
+\end{code}