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