-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 (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