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), text "Strange! Type mismatch in trans coercion, probably a bug")
 375         (a1, r2)
 376       where
 377         (a1, r1) = coercionKind co1
 378         (a2, r2) = coercionKind co2
 379
 380 leftCoercionTyCon =
 381   mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
 382   where
 383     leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 384       where
 385         (ty1,ty2) = fst (splitCoercionKindOf co)
 386
 387 rightCoercionTyCon =
 388   mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
 389   where
 390     rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 391       where
 392         (ty1,ty2) = snd (splitCoercionKindOf co)
 393
 394 splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
 395 -- Helper for left and right.  Finds coercion kind of its input and
 396 -- returns the left and right projections of the coercion...
 397 --
 398 -- if c :: t1 s1 :=: t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 399 splitCoercionKindOf co
 400   | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
 401   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 402   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 403   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 404
 405 instCoercionTyCon
 406   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
 407   where
 408     instantiateCo t s =
 409       let Just (tv, ty) = splitForAllTy_maybe t in
 410       substTyWith [tv] [s] ty
 411
 412     instCoercionKind (co1:ty:rest) = ASSERT( null rest )
 413                                      (instantiateCo t1 ty, instantiateCo t2 ty)
 414       where (t1, t2) = coercionKind co1
 415
 416 unsafeCoercionTyCon
 417   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
 418   where
 419    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2)
 420
 421 --------------------------------------
 422 -- ...and their names
 423
 424 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
 425                             key (ATyCon coCon) BuiltInSyntax
 426
 427 transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
 428 symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon
 429 leftCoercionTyConName  = mkCoConName FSLIT("left") leftCoercionTyConKey leftCoercionTyCon
 430 rightCoercionTyConName = mkCoConName FSLIT("right") rightCoercionTyConKey rightCoercionTyCon
 431 instCoercionTyConName  = mkCoConName FSLIT("inst") instCoercionTyConKey instCoercionTyCon
 432 unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 433
 434
 435
 436 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
 437 -- instNewTyCon_maybe T ts
 438 --      = Just (rep_ty, co)     if   co : T ts ~ rep_ty
 439 instNewTyCon_maybe tc tys
 440   | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
 441   = ASSERT( tys `lengthIs` tyConArity tc )
 442     Just (substTyWith tvs tys ty,
 443           case mb_co_tc of
 444            Nothing    -> IdCo
 445            Just co_tc -> ACo (mkTyConApp co_tc tys))
 446   | otherwise
 447   = Nothing
 448
 449 -- this is here to avoid module loops
 450 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 451 -- Sometimes we want to look through a newtype and get its associated coercion
 452 -- It only strips *one layer* off, so the caller will usually call itself recursively
 453 -- Only applied to types of kind *, hence the newtype is always saturated
 454 --    splitNewTypeRepCo_maybe ty
 455 --      = Just (ty', co)  if   co : ty ~ ty'
 456 -- Returns Nothing for non-newtypes or fully-transparent newtypes
 457 splitNewTypeRepCo_maybe ty
 458   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 459 splitNewTypeRepCo_maybe (TyConApp tc tys)
 460   | Just (ty', coi) <- instNewTyCon_maybe tc tys
 461   = case coi of
 462         ACo co -> Just (ty', co)
 463         IdCo   -> panic "splitNewTypeRepCo_maybe"
 464                         -- This case handled by coreView
 465 splitNewTypeRepCo_maybe other
 466   = Nothing
 467 \end{code}
 468
 469
 470 --------------------------------------
 471 -- CoercionI smart constructors
 472 --      lifted smart constructors of ordinary coercions
 473
 474 \begin{code}
 475         -- CoercionI is either
 476         --      (a) proper coercion
 477         --      (b) the identity coercion
 478 data CoercionI = IdCo | ACo Coercion
 479
 480 isIdentityCoercion :: CoercionI -> Bool
 481 isIdentityCoercion IdCo = True
 482 isIdentityCoercion _    = False
 483
 484 allIdCos :: [CoercionI] -> Bool
 485 allIdCos = all isIdentityCoercion
 486
 487 zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
 488 zipCoArgs cois tys = zipWith fromCoI cois tys
 489
 490 fromCoI :: CoercionI -> Type -> Type
 491 fromCoI IdCo ty     = ty        -- Identity coercion represented
 492 fromCoI (ACo co) ty = co        --      by the type itself
 493
 494 mkSymCoI :: CoercionI -> CoercionI
 495 mkSymCoI IdCo = IdCo
 496 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
 497                                 -- the smart constructor
 498                                 -- is too smart with tyvars
 499
 500 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
 501 mkTransCoI IdCo aco = aco
 502 mkTransCoI aco IdCo = aco
 503 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
 504
 505 mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
 506 mkTyConAppCoI tyCon tys cois
 507   | allIdCos cois = IdCo
 508   | otherwise     = ACo (TyConApp tyCon (zipCoArgs cois tys))
 509
 510 mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 511 mkAppTyCoI ty1 IdCo ty2 IdCo = IdCo
 512 mkAppTyCoI ty1 coi1 ty2 coi2 =
 513         ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 514
 515 mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 516 mkFunTyCoI ty1 IdCo ty2 IdCo = IdCo
 517 mkFunTyCoI ty1 coi1 ty2 coi2 =
 518         ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 519
 520 mkNoteTyCoI :: TyNote -> CoercionI -> CoercionI
 521 mkNoteTyCoI _ IdCo = IdCo
 522 mkNoteTyCoI note (ACo co) = ACo $ NoteTy note co
 523
 524 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
 525 mkForAllTyCoI _ IdCo = IdCo
 526 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
 527
 528 fromACo (ACo co) = co
 529
 530
 531 mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
 532 -- mkClassPPredCoI cls tys cois = coi
 533 --    coi : PredTy (cls tys) ~ predTy (cls (tys `cast` cois))
 534 mkClassPPredCoI cls tys cois
 535   | allIdCos cois = IdCo
 536   | otherwise     = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
 537
 538 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
 539 -- Similar invariant to mkclassPPredCoI
 540 mkIParamPredCoI ipn IdCo     = IdCo
 541 mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
 542
 543 mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 544 -- Similar invariant to mkclassPPredCoI
 545 mkEqPredCoI _    IdCo     _   IdCo      = IdCo
 546 mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
 547 mkEqPredCoI ty1 (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
 548 \end{code}
 549