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