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