compiler/types/Coercion.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 Module for type coercions, as in System FC.
   6
   7 Coercions are represented as types, and their kinds tell what types the
   8 coercion works on.
   9
  10 The coercion kind constructor is a special TyCon that must always be saturated
  11
  12   typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
  13
  14 \begin{code}
  15 {-# OPTIONS -w #-}
  16 -- The above warning supression flag is a temporary kludge.
  17 -- While working on this module you are encouraged to remove it and fix
  18 -- any warnings in the module. See
  19 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
  20 -- for details
  21
  22 module Coercion (
  23         Coercion,
  24
  25         mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
  26         coercionKind, coercionKinds, coercionKindPredTy,
  27
  28         -- Equality predicates
  29         isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
  30
  31         -- Coercion transformations
  32         mkCoercion,
  33         mkSymCoercion, mkTransCoercion,
  34         mkLeftCoercion, mkRightCoercion, mkRightCoercions,
  35         mkInstCoercion, mkAppCoercion,
  36         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
  37         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
  38
  39         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
  40
  41         unsafeCoercionTyCon, symCoercionTyCon,
  42         transCoercionTyCon, leftCoercionTyCon,
  43         rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
  44
  45         -- CoercionI
  46         CoercionI(..),
  47         isIdentityCoercion,
  48         mkSymCoI, mkTransCoI,
  49         mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
  50         mkNoteTyCoI, mkForAllTyCoI,
  51         fromCoI, fromACo,
  52         mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
  53
  54        ) where
  55
  56 #include "HsVersions.h"
  57
  58 import TypeRep
  59 import Type
  60 import TyCon
  61 import Class
  62 import Var
  63 import Name
  64 import OccName
  65 import PrelNames
  66 import Util
  67 import Unique
  68 import BasicTypes
  69 import Outputable
  70
  71
  72 type Coercion     = Type
  73 type CoercionKind = Kind        -- A CoercionKind is always of form (ty1 :=: ty2)
  74
  75 ------------------------------
  76 decomposeCo :: Arity -> Coercion -> [Coercion]
  77 -- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]
  78 -- So this breaks a coercion with kind T A B C :=: T D E F into
  79 -- a list of coercions of kinds A :=: D, B :=: E and E :=: F
  80 decomposeCo n co
  81   = go n co []
  82   where
  83     go 0 co cos = cos
  84     go n co cos = go (n-1) (mkLeftCoercion co)
  85                            (mkRightCoercion co : cos)
  86
  87 ------------------------------
  88
  89 -------------------------------------------------------
  90 -- and some coercion kind stuff
  91
  92 isEqPredTy (PredTy pred) = isEqPred pred
  93 isEqPredTy other         = False
  94
  95 mkEqPred :: (Type, Type) -> PredType
  96 mkEqPred (ty1, ty2) = EqPred ty1 ty2
  97
  98 getEqPredTys :: PredType -> (Type,Type)
  99 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
 100 getEqPredTys other            = pprPanic "getEqPredTys" (ppr other)
 101
 102 mkCoKind :: Type -> Type -> CoercionKind
 103 mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
 104
 105 mkReflCoKind :: Type -> CoercionKind
 106 mkReflCoKind ty = mkCoKind ty ty
 107
 108 splitCoercionKind :: CoercionKind -> (Type, Type)
 109 splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co'
 110 splitCoercionKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)
 111
 112 splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
 113 splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
 114 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
 115 splitCoercionKind_maybe other = Nothing
 116
 117 coercionKind :: Coercion -> (Type, Type)
 118 --      c :: (t1 :=: t2)
 119 -- Then (coercionKind c) = (t1,t2)
 120 coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
 121                             | otherwise = (ty, ty)
 122 coercionKind (AppTy ty1 ty2)
 123   = let (t1, t2) = coercionKind ty1
 124         (s1, s2) = coercionKind ty2 in
 125     (mkAppTy t1 s1, mkAppTy t2 s2)
 126 coercionKind (TyConApp tc args)
 127   | Just (ar, rule) <- isCoercionTyCon_maybe tc
 128     -- CoercionTyCons carry their kinding rule, so we use it here
 129   = ASSERT( length args >= ar ) -- Always saturated
 130     let (ty1,ty2)    = rule (take ar args)      -- Apply the rule to the right number of args
 131         (tys1, tys2) = coercionKinds (drop ar args)
 132     in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)
 133
 134   | otherwise
 135   = let (lArgs, rArgs) = coercionKinds args in
 136     (TyConApp tc lArgs, TyConApp tc rArgs)
 137 coercionKind (FunTy ty1 ty2)
 138   = let (t1, t2) = coercionKind ty1
 139         (s1, s2) = coercionKind ty2 in
 140     (mkFunTy t1 s1, mkFunTy t2 s2)
 141 coercionKind (ForAllTy tv ty)
 142   = let (ty1, ty2) = coercionKind ty in
 143     (ForAllTy tv ty1, ForAllTy tv ty2)
 144 coercionKind (NoteTy _ ty) = coercionKind ty
 145 coercionKind (PredTy (EqPred c1 c2))
 146   = let k1 = coercionKindPredTy c1
 147         k2 = coercionKindPredTy c2 in
 148     (k1,k2)
 149 coercionKind (PredTy (ClassP cl args))
 150   = let (lArgs, rArgs) = coercionKinds args in
 151     (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
 152 coercionKind (PredTy (IParam name ty))
 153   = let (ty1, ty2) = coercionKind ty in
 154     (PredTy (IParam name ty1), PredTy (IParam name ty2))
 155
 156 coercionKindPredTy :: Coercion -> CoercionKind
 157 coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
 158
 159 coercionKinds :: [Coercion] -> ([Type], [Type])
 160 coercionKinds tys = unzip $ map coercionKind tys
 161
 162 -------------------------------------
 163 -- Coercion kind and type mk's
 164 -- (make saturated TyConApp CoercionTyCon{...} args)
 165
 166 mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
 167                         TyConApp coCon args
 168
 169 mkAppCoercion, mkFunCoercion, mkTransCoercion, mkInstCoercion :: Coercion -> Coercion -> Coercion
 170 mkSymCoercion, mkLeftCoercion, mkRightCoercion :: Coercion -> Coercion
 171
 172 mkAppCoercion    co1 co2 = mkAppTy co1 co2
 173 mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys
 174 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
 175 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
 176 mkFunCoercion    co1 co2 = mkFunTy co1 co2
 177
 178
 179 -------------------------------
 180 -- This smart constructor creates a sym'ed version its argument,
 181 -- but tries to push the sym's down to the leaves.  If we come to
 182 -- sym tv or sym tycon then we can drop the sym because tv and tycon
 183 -- are reflexive coercions
 184 mkSymCoercion co
 185   | Just co' <- coreView co = mkSymCoercion co'
 186
 187 mkSymCoercion (ForAllTy tv ty)  = ForAllTy tv (mkSymCoercion ty)
 188 mkSymCoercion (AppTy co1 co2)   = AppTy (mkSymCoercion co1) (mkSymCoercion co2)
 189 mkSymCoercion (FunTy co1 co2)   = FunTy (mkSymCoercion co1) (mkSymCoercion co2)
 190
 191 mkSymCoercion (TyConApp tc cos)
 192   | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos)
 193
 194 mkSymCoercion (TyConApp tc [co])
 195   | tc `hasKey` symCoercionTyConKey   = co    -- sym (sym co) --> co
 196   | tc `hasKey` leftCoercionTyConKey  = mkLeftCoercion (mkSymCoercion co)
 197   | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)
 198
 199 mkSymCoercion (TyConApp tc [co1,co2])
 200   | tc `hasKey` transCoercionTyConKey
 201      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
 202      -- Note reversal of arguments!
 203   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
 204
 205   | tc `hasKey` instCoercionTyConKey
 206      -- sym (co @ ty) --> (sym co) @ ty
 207      -- Note: sym is not applied to 'ty'
 208   = mkInstCoercion (mkSymCoercion co1) co2
 209
 210 mkSymCoercion (TyConApp tc cos)         -- Other coercion tycons, such as those
 211   = mkCoercion symCoercionTyCon [TyConApp tc cos]  -- arising from newtypes
 212
 213 mkSymCoercion (TyVarTy tv)
 214   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
 215   | otherwise  = TyVarTy tv     -- Reflexive
 216
 217 -------------------------------
 218 -- ToDo: we should be cleverer about transitivity
 219 mkTransCoercion g1 g2   -- sym g `trans` g = id
 220   | (t1,_) <- coercionKind g1
 221   , (_,t2) <- coercionKind g2
 222   , t1 `coreEqType` t2
 223   = t1
 224
 225   | otherwise
 226   = mkCoercion transCoercionTyCon [g1, g2]
 227
 228
 229 -------------------------------
 230 -- Smart constructors for left and right
 231 mkLeftCoercion co
 232   | Just (co', _) <- splitAppCoercion_maybe co = co'
 233   | otherwise = mkCoercion leftCoercionTyCon [co]
 234
 235 mkRightCoercion  co
 236   | Just (co1, co2) <- splitAppCoercion_maybe co = co2
 237   | otherwise = mkCoercion rightCoercionTyCon [co]
 238
 239 mkRightCoercions n co
 240   = go n co []
 241   where
 242     go n co acc
 243        | n > 0
 244        = case splitAppCoercion_maybe co of
 245           Just (co1,co2) -> go (n-1) co1 (co2:acc)
 246           Nothing        -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
 247        | otherwise
 248        = acc
 249
 250 mkInstCoercion co ty
 251   | Just (tv,co') <- splitForAllTy_maybe co
 252   = substTyWith [tv] [ty] co'   -- (forall a.co) @ ty  -->  co[ty/a]
 253   | otherwise
 254   = mkCoercion instCoercionTyCon  [co, ty]
 255
 256 mkInstsCoercion co tys = foldl mkInstCoercion co tys
 257
 258 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
 259 splitSymCoercion_maybe (TyConApp tc [co]) =
 260   if tc `hasKey` symCoercionTyConKey
 261   then Just co
 262   else Nothing
 263 splitSymCoercion_maybe co = Nothing
 264
 265 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 266 -- Splits a coercion application, being careful *not* to split (left c), etc
 267 -- which are really sytactic constructs, not applications
 268 splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
 269 splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 270 splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 271 splitAppCoercion_maybe (TyConApp tc tys)
 272    | not (isCoercionTyCon tc)
 273    = case snocView tys of
 274        Just (tys', ty') -> Just (TyConApp tc tys', ty')
 275        Nothing          -> Nothing
 276 splitAppCoercion_maybe co = Nothing
 277
 278 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 279 splitTransCoercion_maybe (TyConApp tc [ty1, ty2])
 280  = if tc `hasKey` transCoercionTyConKey then
 281        Just (ty1, ty2)
 282    else
 283        Nothing
 284 splitTransCoercion_maybe other = Nothing
 285
 286 splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
 287 splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
 288  = if tc `hasKey` instCoercionTyConKey then
 289        Just (ty1, ty2)
 290     else
 291        Nothing
 292 splitInstCoercion_maybe other = Nothing
 293
 294 splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
 295 splitLeftCoercion_maybe (TyConApp tc [co])
 296  = if tc `hasKey` leftCoercionTyConKey then
 297        Just co
 298    else
 299        Nothing
 300 splitLeftCoercion_maybe other = Nothing
 301
 302 splitRightCoercion_maybe :: Coercion -> Maybe Coercion
 303 splitRightCoercion_maybe (TyConApp tc [co])
 304  = if tc `hasKey` rightCoercionTyConKey then
 305        Just co
 306    else
 307        Nothing
 308 splitRightCoercion_maybe other = Nothing
 309
 310 -- Unsafe coercion is not safe, it is used when we know we are dealing with
 311 -- bottom, which is one case in which it is safe.  It is also used to
 312 -- implement the unsafeCoerce# primitive.
 313 mkUnsafeCoercion :: Type -> Type -> Coercion
 314 mkUnsafeCoercion ty1 ty2
 315   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 316
 317
 318 -- See note [Newtype coercions] in TyCon
 319 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 320 mkNewTypeCoercion name tycon tvs rhs_ty
 321   = mkCoercionTyCon name co_con_arity rule
 322   where
 323     co_con_arity = length tvs
 324
 325     rule args = ASSERT( co_con_arity == length args )
 326                 (TyConApp tycon args, substTyWith tvs args rhs_ty)
 327
 328 -- Coercion identifying a data/newtype/synonym representation type and its
 329 -- family instance.  It has the form `Co tvs :: F ts :=: R tvs', where `Co' is
 330 -- the coercion tycon built here, `F' the family tycon and `R' the (derived)
 331 -- representation tycon.
 332 --
 333 mkFamInstCoercion :: Name       -- unique name for the coercion tycon
 334                   -> [TyVar]    -- type parameters of the coercion (`tvs')
 335                   -> TyCon      -- family tycon (`F')
 336                   -> [Type]     -- type instance (`ts')
 337                   -> TyCon      -- representation tycon (`R')
 338                   -> TyCon      -- => coercion tycon (`Co')
 339 mkFamInstCoercion name tvs family instTys rep_tycon
 340   = mkCoercionTyCon name coArity rule
 341   where
 342     coArity = length tvs
 343     rule args = (substTyWith tvs args $              -- with sigma = [tys/tvs],
 344                    TyConApp family instTys,          --       sigma (F ts)
 345                  TyConApp rep_tycon args)            --   :=: R tys
 346
 347 --------------------------------------
 348 -- Coercion Type Constructors...
 349
 350 -- Example.  The coercion ((sym c) (sym d) (sym e))
 351 -- will be represented by (TyConApp sym [c, sym d, sym e])
 352 -- If sym c :: p1=q1
 353 --    sym d :: p2=q2
 354 --    sym e :: p3=q3
 355 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 356
 357 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon :: TyCon
 358 -- Each coercion TyCon is built with the special CoercionTyCon record and
 359 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 360 -- by any TyConApp in which they are applied, however they may also be over
 361 -- applied (see example above) and the kinding function must deal with this.
 362 symCoercionTyCon =
 363   mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
 364   where
 365     flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
 366         where
 367           (ty1, ty2) = coercionKind co
 368
 369 transCoercionTyCon =
 370   mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
 371   where
 372     composeCoercionKindsOf (co1:co2:rest)
 373       = ASSERT( null rest )
 374         WARN( not (r1 `coreEqType` a2),
 375               text "Strange! Type mismatch in trans coercion, probably a bug"
 376               $$
 377               ppr r1 <+> text "=/=" <+> ppr a2)
 378         (a1, r2)
 379       where
 380         (a1, r1) = coercionKind co1
 381         (a2, r2) = coercionKind co2
 382
 383 leftCoercionTyCon =
 384   mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
 385   where
 386     leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 387       where
 388         (ty1,ty2) = fst (splitCoercionKindOf co)
 389
 390 rightCoercionTyCon =
 391   mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
 392   where
 393     rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 394       where
 395         (ty1,ty2) = snd (splitCoercionKindOf co)
 396
 397 splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
 398 -- Helper for left and right.  Finds coercion kind of its input and
 399 -- returns the left and right projections of the coercion...
 400 --
 401 -- if c :: t1 s1 :=: t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 402 splitCoercionKindOf co
 403   | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
 404   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 405   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 406   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 407
 408 instCoercionTyCon
 409   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
 410   where
 411     instantiateCo t s =
 412       let Just (tv, ty) = splitForAllTy_maybe t in
 413       substTyWith [tv] [s] ty
 414
 415     instCoercionKind (co1:ty:rest) = ASSERT( null rest )
 416                                      (instantiateCo t1 ty, instantiateCo t2 ty)
 417       where (t1, t2) = coercionKind co1
 418
 419 unsafeCoercionTyCon
 420   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
 421   where
 422    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2)
 423
 424 --------------------------------------
 425 -- ...and their names
 426
 427 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
 428                             key (ATyCon coCon) BuiltInSyntax
 429
 430 transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
 431 symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon
 432 leftCoercionTyConName  = mkCoConName FSLIT("left") leftCoercionTyConKey leftCoercionTyCon
 433 rightCoercionTyConName = mkCoConName FSLIT("right") rightCoercionTyConKey rightCoercionTyCon
 434 instCoercionTyConName  = mkCoConName FSLIT("inst") instCoercionTyConKey instCoercionTyCon
 435 unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 436
 437
 438
 439 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
 440 -- instNewTyCon_maybe T ts
 441 --      = Just (rep_ty, co)     if   co : T ts ~ rep_ty
 442 instNewTyCon_maybe tc tys
 443   | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
 444   = ASSERT( tys `lengthIs` tyConArity tc )
 445     Just (substTyWith tvs tys ty,
 446           case mb_co_tc of
 447            Nothing    -> IdCo
 448            Just co_tc -> ACo (mkTyConApp co_tc tys))
 449   | otherwise
 450   = Nothing
 451
 452 -- this is here to avoid module loops
 453 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 454 -- Sometimes we want to look through a newtype and get its associated coercion
 455 -- It only strips *one layer* off, so the caller will usually call itself recursively
 456 -- Only applied to types of kind *, hence the newtype is always saturated
 457 --    splitNewTypeRepCo_maybe ty
 458 --      = Just (ty', co)  if   co : ty ~ ty'
 459 -- Returns Nothing for non-newtypes or fully-transparent newtypes
 460 splitNewTypeRepCo_maybe ty
 461   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 462 splitNewTypeRepCo_maybe (TyConApp tc tys)
 463   | Just (ty', coi) <- instNewTyCon_maybe tc tys
 464   = case coi of
 465         ACo co -> Just (ty', co)
 466         IdCo   -> panic "splitNewTypeRepCo_maybe"
 467                         -- This case handled by coreView
 468 splitNewTypeRepCo_maybe other
 469   = Nothing
 470 \end{code}
 471
 472
 473 --------------------------------------
 474 -- CoercionI smart constructors
 475 --      lifted smart constructors of ordinary coercions
 476
 477 \begin{code}
 478         -- CoercionI is either
 479         --      (a) proper coercion
 480         --      (b) the identity coercion
 481 data CoercionI = IdCo | ACo Coercion
 482
 483 isIdentityCoercion :: CoercionI -> Bool
 484 isIdentityCoercion IdCo = True
 485 isIdentityCoercion _    = False
 486
 487 allIdCos :: [CoercionI] -> Bool
 488 allIdCos = all isIdentityCoercion
 489
 490 zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
 491 zipCoArgs cois tys = zipWith fromCoI cois tys
 492
 493 fromCoI :: CoercionI -> Type -> Type
 494 fromCoI IdCo ty     = ty        -- Identity coercion represented
 495 fromCoI (ACo co) ty = co        --      by the type itself
 496
 497 mkSymCoI :: CoercionI -> CoercionI
 498 mkSymCoI IdCo = IdCo
 499 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
 500                                 -- the smart constructor
 501                                 -- is too smart with tyvars
 502
 503 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
 504 mkTransCoI IdCo aco = aco
 505 mkTransCoI aco IdCo = aco
 506 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
 507
 508 mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
 509 mkTyConAppCoI tyCon tys cois
 510   | allIdCos cois = IdCo
 511   | otherwise     = ACo (TyConApp tyCon (zipCoArgs cois tys))
 512
 513 mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 514 mkAppTyCoI ty1 IdCo ty2 IdCo = IdCo
 515 mkAppTyCoI ty1 coi1 ty2 coi2 =
 516         ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 517
 518 mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 519 mkFunTyCoI ty1 IdCo ty2 IdCo = IdCo
 520 mkFunTyCoI ty1 coi1 ty2 coi2 =
 521         ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 522
 523 mkNoteTyCoI :: TyNote -> CoercionI -> CoercionI
 524 mkNoteTyCoI _ IdCo = IdCo
 525 mkNoteTyCoI note (ACo co) = ACo $ NoteTy note co
 526
 527 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
 528 mkForAllTyCoI _ IdCo = IdCo
 529 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
 530
 531 fromACo (ACo co) = co
 532
 533
 534 mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
 535 -- mkClassPPredCoI cls tys cois = coi
 536 --    coi : PredTy (cls tys) ~ predTy (cls (tys `cast` cois))
 537 mkClassPPredCoI cls tys cois
 538   | allIdCos cois = IdCo
 539   | otherwise     = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
 540
 541 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
 542 -- Similar invariant to mkclassPPredCoI
 543 mkIParamPredCoI ipn IdCo     = IdCo
 544 mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
 545
 546 mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 547 -- Similar invariant to mkclassPPredCoI
 548 mkEqPredCoI _    IdCo     _   IdCo      = IdCo
 549 mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
 550 mkEqPredCoI ty1 (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
 551 \end{code}
 552