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