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