- (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}
+ rn_env = me_env menv
+ tv1' = rnOccL rn_env tv1
+
+ty_co_match menv subst (AppTy ty1 ty2) (AppCo co1 co2) -- BAY: do we need to work harder to decompose the AppCo?
+ = do { subst' <- ty_co_match menv subst ty1 co1
+ ; ty_co_match menv subst' ty2 co2 }
+
+ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo tc2 cos)
+ | tc1 == tc2 = ty_co_matches menv subst tys cos
+
+ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos)
+ | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
+
+ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co)
+ = ty_co_match menv' subst ty co
+ where
+ menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
+
+ty_co_match _ _ _ _ = Nothing
+
+ty_co_matches :: MatchEnv -> TyCoSubstEnv -> [Type] -> [Coercion] -> Maybe TyCoSubstEnv
+ty_co_matches menv = matchList (ty_co_match menv)
+\end{code}
+
+%************************************************************************
+%* *
+ Sequencing on coercions
+%* *
+%************************************************************************
+
+\begin{code}
+seqCo :: Coercion -> ()
+seqCo (Refl ty) = seqType ty
+seqCo (TyConAppCo tc cos) = tc `seq` seqCos cos
+seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
+seqCo (ForAllCo tv co) = tv `seq` seqCo co
+seqCo (PredCo p) = seqPred seqCo p
+seqCo (CoVarCo cv) = cv `seq` ()
+seqCo (AxiomInstCo con cos) = con `seq` seqCos cos
+seqCo (UnsafeCo ty1 ty2) = seqType ty1 `seq` seqType ty2
+seqCo (SymCo co) = seqCo co
+seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
+seqCo (NthCo _ co) = seqCo co
+seqCo (InstCo co ty) = seqCo co `seq` seqType ty
+
+seqCos :: [Coercion] -> ()
+seqCos [] = ()
+seqCos (co:cos) = seqCo co `seq` seqCos cos
+\end{code}
+
+
+%************************************************************************
+%* *
+ The kind of a type, and of a coercion
+%* *
+%************************************************************************
+
+\begin{code}
+coercionType :: Coercion -> Type
+coercionType co = case coercionKind co of
+ Pair ty1 ty2 -> mkCoType ty1 ty2
+
+------------------
+-- | If it is the case that
+--
+-- > c :: (t1 ~ t2)
+--
+-- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
+coercionKind :: Coercion -> Pair Type
+coercionKind (Refl ty) = Pair ty ty
+coercionKind (TyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map coercionKind cos)
+coercionKind (AppCo co1 co2) = mkAppTy <$> coercionKind co1 <*> coercionKind co2
+coercionKind (ForAllCo tv co) = mkForAllTy tv <$> coercionKind co
+ -- BAY*: is the above still correct for equality
+ -- abstractions? the System FC paper seems to imply we can
+ -- only ever construct coercions between foralls whose
+ -- variables have *equal* kinds. But there was this comment
+ -- below suggesting otherwise:
+
+-- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
+-- ----------------------------------------------
+-- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2
+-- or
+-- forall (_:c1~c2)
+coercionKind (CoVarCo cv) = ASSERT( isCoVar cv ) toPair $ coVarKind cv
+coercionKind (AxiomInstCo ax cos) = let Pair tys1 tys2 = coercionKinds cos
+ in Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax))
+ (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax))
+coercionKind (UnsafeCo ty1 ty2) = Pair ty1 ty2
+coercionKind (SymCo co) = swap $ coercionKind co
+coercionKind (TransCo co1 co2) = Pair (pFst $ coercionKind co1) (pSnd $ coercionKind co2)
+coercionKind (NthCo d co) = getNth d <$> coercionKind co
+coercionKind (InstCo co ty) | Just ks <- splitForAllTy_maybe `traverse` coercionKind co
+ = (\(tv, body) -> substTyWith [tv] [ty] body) <$> ks
+ -- fall-through error case.
+coercionKind co = pprPanic "coercionKind" (ppr co)
+
+-- | Apply 'coercionKind' to multiple 'Coercion's
+coercionKinds :: [Coercion] -> Pair [Type]
+coercionKinds tys = sequenceA $ map coercionKind tys
+
+getNth :: Int -> Type -> Type
+getNth n ty | Just (_, tys) <- splitTyConApp_maybe ty
+ = ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n
+getNth n ty = pprPanic "getNth" (ppr n <+> ppr ty)
+\end{code}
+
+\begin{code}
+applyCo :: Type -> Coercion -> Type
+-- Gives the type of (e co) where e :: (a~b) => ty
+applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
+applyCo (FunTy _ ty) _ = ty
+applyCo _ _ = panic "applyCo"
+\end{code}
\ No newline at end of file