compiler/types/Coercion.lhs

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