compiler/types/Coercion.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 \begin{code}
   6 {-# OPTIONS -fno-warn-incomplete-patterns #-}
   7 -- The above warning supression flag is a temporary kludge.
   8 -- While working on this module you are encouraged to remove it and fix
   9 -- any warnings in the module. See
  10 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
  11 -- for details
  12
  13 -- | Module for type coercions, as used in System FC. See 'CoreSyn.Expr' for
  14 -- more on System FC and how coercions fit into it.
  15 --
  16 -- Coercions are represented as types, and their kinds tell what types the
  17 -- coercion works on. The coercion kind constructor is a special TyCon that must always be saturated, like so:
  18 --
  19 -- > typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
  20 module Coercion (
  21         -- * Main data type
  22         Coercion,
  23
  24         mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
  25         coercionKind, coercionKinds, coercionKindPredTy, isIdentityCoercion,
  26
  27         -- ** Equality predicates
  28         isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
  29
  30         -- ** Coercion transformations
  31         mkCoercion,
  32         mkSymCoercion, mkTransCoercion,
  33         mkLeftCoercion, mkRightCoercion, mkRightCoercions,
  34         mkInstCoercion, mkAppCoercion,
  35         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
  36         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
  37
  38         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
  39
  40         unsafeCoercionTyCon, symCoercionTyCon,
  41         transCoercionTyCon, leftCoercionTyCon,
  42         rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
  43
  44         -- ** Comparison
  45         coreEqCoercion,
  46
  47         -- * CoercionI
  48         CoercionI(..),
  49         isIdentityCoI,
  50         mkSymCoI, mkTransCoI,
  51         mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
  52         mkForAllTyCoI,
  53         fromCoI, fromACo,
  54         mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
  55
  56        ) where
  57
  58 #include "HsVersions.h"
  59
  60 import TypeRep
  61 import Type
  62 import TyCon
  63 import Class
  64 import Var
  65 import Name
  66 import OccName
  67 import PrelNames
  68 import Util
  69 import Unique
  70 import BasicTypes
  71 import Outputable
  72 import FastString
  73
  74 -- | A 'Coercion' represents a 'Type' something should be coerced to.
  75 type Coercion     = Type
  76
  77 -- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
  78 -- types that a 'Coercion' will work on.
  79 type CoercionKind = Kind
  80
  81 ------------------------------
  82
  83 -- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
  84 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
  85 --
  86 -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
  87 decomposeCo :: Arity -> Coercion -> [Coercion]
  88 decomposeCo n co
  89   = go n co []
  90   where
  91     go 0 _  cos = cos
  92     go n co cos = go (n-1) (mkLeftCoercion co)
  93                            (mkRightCoercion co : cos)
  94
  95 ------------------------------
  96
  97 -------------------------------------------------------
  98 -- and some coercion kind stuff
  99
 100 -- | Tests whether a type is just a type equality predicate
 101 isEqPredTy :: Type -> Bool
 102 isEqPredTy (PredTy pred) = isEqPred pred
 103 isEqPredTy _             = False
 104
 105 -- | Creates a type equality predicate
 106 mkEqPred :: (Type, Type) -> PredType
 107 mkEqPred (ty1, ty2) = EqPred ty1 ty2
 108
 109 -- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
 110 -- Panics otherwise
 111 getEqPredTys :: PredType -> (Type,Type)
 112 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
 113 getEqPredTys other            = pprPanic "getEqPredTys" (ppr other)
 114
 115 -- | Makes a 'CoercionKind' from two types: the types whose equality is proven by the relevant 'Coercion'
 116 mkCoKind :: Type -> Type -> CoercionKind
 117 mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
 118
 119 -- | Create a reflexive 'CoercionKind' that asserts that a type can be coerced to itself
 120 mkReflCoKind :: Type -> CoercionKind
 121 mkReflCoKind ty = mkCoKind ty ty
 122
 123 -- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
 124 -- Panics if the argument is not a valid 'CoercionKind'
 125 splitCoercionKind :: CoercionKind -> (Type, Type)
 126 splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co'
 127 splitCoercionKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)
 128
 129 -- | Take a 'CoercionKind' apart into the two types it relates, if possible. See also 'splitCoercionKind'
 130 splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
 131 splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
 132 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
 133 splitCoercionKind_maybe _ = Nothing
 134
 135 -- | If it is the case that
 136 --
 137 -- > c :: (t1 ~ t2)
 138 --
 139 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
 140 -- See also 'coercionKindPredTy'
 141 coercionKind :: Coercion -> (Type, Type)
 142 coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
 143                             | otherwise = (ty, ty)
 144 coercionKind (AppTy ty1 ty2)
 145   = let (t1, t2) = coercionKind ty1
 146         (s1, s2) = coercionKind ty2 in
 147     (mkAppTy t1 s1, mkAppTy t2 s2)
 148 coercionKind (TyConApp tc args)
 149   | Just (ar, rule) <- isCoercionTyCon_maybe tc
 150     -- CoercionTyCons carry their kinding rule, so we use it here
 151   = ASSERT( length args >= ar ) -- Always saturated
 152     let (ty1,ty2)    = rule (take ar args)      -- Apply the rule to the right number of args
 153         (tys1, tys2) = coercionKinds (drop ar args)
 154     in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)
 155
 156   | otherwise
 157   = let (lArgs, rArgs) = coercionKinds args in
 158     (TyConApp tc lArgs, TyConApp tc rArgs)
 159 coercionKind (FunTy ty1 ty2)
 160   = let (t1, t2) = coercionKind ty1
 161         (s1, s2) = coercionKind ty2 in
 162     (mkFunTy t1 s1, mkFunTy t2 s2)
 163 coercionKind (ForAllTy tv ty)
 164   = let (ty1, ty2) = coercionKind ty in
 165     (ForAllTy tv ty1, ForAllTy tv ty2)
 166 coercionKind (PredTy (EqPred c1 c2))
 167   = let k1 = coercionKindPredTy c1
 168         k2 = coercionKindPredTy c2 in
 169     (k1,k2)
 170 coercionKind (PredTy (ClassP cl args))
 171   = let (lArgs, rArgs) = coercionKinds args in
 172     (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
 173 coercionKind (PredTy (IParam name ty))
 174   = let (ty1, ty2) = coercionKind ty in
 175     (PredTy (IParam name ty1), PredTy (IParam name ty2))
 176
 177 -- | Recover the 'CoercionKind' corresponding to a particular 'Coerceion'. See also 'coercionKind'
 178 -- and 'mkCoKind'
 179 coercionKindPredTy :: Coercion -> CoercionKind
 180 coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
 181
 182 -- | Apply 'coercionKind' to multiple 'Coercion's
 183 coercionKinds :: [Coercion] -> ([Type], [Type])
 184 coercionKinds tys = unzip $ map coercionKind tys
 185
 186 -------------------------------------
 187 isIdentityCoercion :: Coercion -> Bool
 188 isIdentityCoercion co
 189   = case coercionKind co of
 190        (t1,t2) -> t1 `coreEqType` t2
 191
 192 -------------------------------------
 193 -- Coercion kind and type mk's
 194 -- (make saturated TyConApp CoercionTyCon{...} args)
 195
 196 -- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
 197 -- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
 198 -- if possible
 199 mkCoercion :: TyCon -> [Type] -> Coercion
 200 mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
 201                         TyConApp coCon args
 202
 203 -- | Apply a 'Coercion' to another 'Coercion', which is presumably a 'Coercion' constructor of some
 204 -- kind
 205 mkAppCoercion :: Coercion -> Coercion -> Coercion
 206 mkAppCoercion    co1 co2 = mkAppTy co1 co2
 207
 208 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
 209 -- See also 'mkAppCoercion'
 210 mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
 211 mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys
 212
 213 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
 214 mkForAllCoercion :: Var -> Coercion -> Coercion
 215 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
 216 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
 217
 218 -- | Make a function 'Coercion' between two other 'Coercion's
 219 mkFunCoercion :: Coercion -> Coercion -> Coercion
 220 mkFunCoercion    co1 co2 = mkFunTy co1 co2
 221
 222
 223 -------------------------------
 224
 225 mkSymCoercion :: Coercion -> Coercion
 226 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality between
 227 -- the same types but in the other "direction", so a kind of @t1 ~ t2@ becomes the
 228 -- kind @t2 ~ t1@.
 229 --
 230 -- This function attempts to simplify the generated 'Coercion' by removing redundant applications
 231 -- of @sym@. This is done by pushing this new @sym@ down into the 'Coercion' and exploiting the fact that
 232 -- @sym (sym co) = co@.
 233 mkSymCoercion co
 234   | Just co' <- coreView co = mkSymCoercion co'
 235
 236 mkSymCoercion (ForAllTy tv ty)  = ForAllTy tv (mkSymCoercion ty)
 237 mkSymCoercion (AppTy co1 co2)   = AppTy (mkSymCoercion co1) (mkSymCoercion co2)
 238 mkSymCoercion (FunTy co1 co2)   = FunTy (mkSymCoercion co1) (mkSymCoercion co2)
 239
 240 mkSymCoercion (TyConApp tc cos)
 241   | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos)
 242
 243 mkSymCoercion (TyConApp tc [co])
 244   | tc `hasKey` symCoercionTyConKey   = co    -- sym (sym co) --> co
 245   | tc `hasKey` leftCoercionTyConKey  = mkLeftCoercion (mkSymCoercion co)
 246   | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)
 247
 248 mkSymCoercion (TyConApp tc [co1,co2])
 249   | tc `hasKey` transCoercionTyConKey
 250      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
 251      -- Note reversal of arguments!
 252   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
 253
 254   | tc `hasKey` instCoercionTyConKey
 255      -- sym (co @ ty) --> (sym co) @ ty
 256      -- Note: sym is not applied to 'ty'
 257   = mkInstCoercion (mkSymCoercion co1) co2
 258
 259 mkSymCoercion (TyConApp tc cos)         -- Other coercion tycons, such as those
 260   = mkCoercion symCoercionTyCon [TyConApp tc cos]  -- arising from newtypes
 261
 262 mkSymCoercion (TyVarTy tv)
 263   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
 264   | otherwise  = TyVarTy tv     -- Reflexive
 265
 266 -------------------------------
 267 -- ToDo: we should be cleverer about transitivity
 268
 269 mkTransCoercion :: Coercion -> Coercion -> Coercion
 270 -- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
 271 --
 272 -- This function attempts to simplify the generated 'Coercion' by exploiting the fact that
 273 -- @sym g `trans` g = id@.
 274 mkTransCoercion g1 g2   -- sym g `trans` g = id
 275   | (t1,_) <- coercionKind g1
 276   , (_,t2) <- coercionKind g2
 277   , t1 `coreEqType` t2
 278   = t1
 279
 280   | otherwise
 281   = mkCoercion transCoercionTyCon [g1, g2]
 282
 283
 284 -------------------------------
 285 -- Smart constructors for left and right
 286
 287 mkLeftCoercion :: Coercion -> Coercion
 288 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
 289 -- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
 290 --
 291 -- > mkLeftCoercion c :: f ~ g
 292 mkLeftCoercion co
 293   | Just (co', _) <- splitAppCoercion_maybe co = co'
 294   | otherwise = mkCoercion leftCoercionTyCon [co]
 295
 296 mkRightCoercion :: Coercion -> Coercion
 297 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
 298 -- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
 299 --
 300 -- > mkLeftCoercion c :: x ~ y
 301 mkRightCoercion  co
 302   | Just (_, co2) <- splitAppCoercion_maybe co = co2
 303   | otherwise = mkCoercion rightCoercionTyCon [co]
 304
 305 mkRightCoercions :: Int -> Coercion -> [Coercion]
 306 -- ^ As 'mkRightCoercion', but finds the 'Coercion's available on the right side of @n@
 307 -- nested application 'Coercion's, manufacturing new left or right cooercions as necessary
 308 -- if suffficiently many are not directly available.
 309 mkRightCoercions n co
 310   = go n co []
 311   where
 312     go n co acc
 313        | n > 0
 314        = case splitAppCoercion_maybe co of
 315           Just (co1,co2) -> go (n-1) co1 (co2:acc)
 316           Nothing        -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
 317        | otherwise
 318        = acc
 319
 320
 321 mkInstCoercion :: Coercion -> Type -> Coercion
 322 -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
 323 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
 324 mkInstCoercion co ty
 325   | Just (tv,co') <- splitForAllTy_maybe co
 326   = substTyWith [tv] [ty] co'   -- (forall a.co) @ ty  -->  co[ty/a]
 327   | otherwise
 328   = mkCoercion instCoercionTyCon  [co, ty]
 329
 330 mkInstsCoercion :: Coercion -> [Type] -> Coercion
 331 -- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right
 332 mkInstsCoercion co tys = foldl mkInstCoercion co tys
 333
 334 {-
 335 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
 336 splitSymCoercion_maybe (TyConApp tc [co]) =
 337   if tc `hasKey` symCoercionTyConKey
 338   then Just co
 339   else Nothing
 340 splitSymCoercion_maybe co = Nothing
 341 -}
 342
 343 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 344 -- ^ Splits a coercion application, being careful *not* to split @left c@ etc.
 345 -- This is because those are really syntactic constructs, not applications
 346 splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
 347 splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 348 splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 349 splitAppCoercion_maybe (TyConApp tc tys)
 350    | not (isCoercionTyCon tc)
 351    = case snocView tys of
 352        Just (tys', ty') -> Just (TyConApp tc tys', ty')
 353        Nothing          -> Nothing
 354 splitAppCoercion_maybe _ = Nothing
 355
 356 {-
 357 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 358 splitTransCoercion_maybe (TyConApp tc [ty1, ty2])
 359  = if tc `hasKey` transCoercionTyConKey then
 360        Just (ty1, ty2)
 361    else
 362        Nothing
 363 splitTransCoercion_maybe other = Nothing
 364
 365 splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
 366 splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
 367  = if tc `hasKey` instCoercionTyConKey then
 368        Just (ty1, ty2)
 369     else
 370        Nothing
 371 splitInstCoercion_maybe other = Nothing
 372
 373 splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
 374 splitLeftCoercion_maybe (TyConApp tc [co])
 375  = if tc `hasKey` leftCoercionTyConKey then
 376        Just co
 377    else
 378        Nothing
 379 splitLeftCoercion_maybe other = Nothing
 380
 381 splitRightCoercion_maybe :: Coercion -> Maybe Coercion
 382 splitRightCoercion_maybe (TyConApp tc [co])
 383  = if tc `hasKey` rightCoercionTyConKey then
 384        Just co
 385    else
 386        Nothing
 387 splitRightCoercion_maybe other = Nothing
 388 -}
 389
 390 -- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
 391 -- but it is used when we know we are dealing with bottom, which is one case in which
 392 -- it is safe.  This is also used implement the @unsafeCoerce#@ primitive.
 393 mkUnsafeCoercion :: Type -> Type -> Coercion
 394 mkUnsafeCoercion ty1 ty2
 395   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 396
 397
 398 -- See note [Newtype coercions] in TyCon
 399
 400 -- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a
 401 -- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the
 402 -- type the appropriate right hand side of the @newtype@, with the free variables
 403 -- a subset of those 'TyVar's.
 404 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 405 mkNewTypeCoercion name tycon tvs rhs_ty
 406   = mkCoercionTyCon name co_con_arity rule
 407   where
 408     co_con_arity = length tvs
 409
 410     rule args = ASSERT( co_con_arity == length args )
 411                 (TyConApp tycon args, substTyWith tvs args rhs_ty)
 412
 413 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
 414 -- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
 415 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
 416 -- representation tycon.
 417 mkFamInstCoercion :: Name       -- ^ Unique name for the coercion tycon
 418                   -> [TyVar]    -- ^ Type parameters of the coercion (@tvs@)
 419                   -> TyCon      -- ^ Family tycon (@F@)
 420                   -> [Type]     -- ^ Type instance (@ts@)
 421                   -> TyCon      -- ^ Representation tycon (@R@)
 422                   -> TyCon      -- ^ Coercion tycon (@Co@)
 423 mkFamInstCoercion name tvs family instTys rep_tycon
 424   = mkCoercionTyCon name coArity rule
 425   where
 426     coArity = length tvs
 427     rule args = (substTyWith tvs args $              -- with sigma = [tys/tvs],
 428                    TyConApp family instTys,          --       sigma (F ts)
 429                  TyConApp rep_tycon args)            --   ~ R tys
 430
 431 --------------------------------------
 432 -- Coercion Type Constructors...
 433
 434 -- Example.  The coercion ((sym c) (sym d) (sym e))
 435 -- will be represented by (TyConApp sym [c, sym d, sym e])
 436 -- If sym c :: p1=q1
 437 --    sym d :: p2=q2
 438 --    sym e :: p3=q3
 439 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 440
 441 -- | Coercion type constructors: avoid using these directly and instead use the @mk*Coercion@ and @split*Coercion@ family
 442 -- of functions if possible.
 443 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon :: TyCon
 444 -- Each coercion TyCon is built with the special CoercionTyCon record and
 445 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 446 -- by any TyConApp in which they are applied, however they may also be over
 447 -- applied (see example above) and the kinding function must deal with this.
 448 symCoercionTyCon =
 449   mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
 450   where
 451     flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
 452         where
 453           (ty1, ty2) = coercionKind co
 454
 455 transCoercionTyCon =
 456   mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
 457   where
 458     composeCoercionKindsOf (co1:co2:rest)
 459       = ASSERT( null rest )
 460         WARN( not (r1 `coreEqType` a2),
 461               text "Strange! Type mismatch in trans coercion, probably a bug"
 462               $$
 463               ppr r1 <+> text "=/=" <+> ppr a2)
 464         (a1, r2)
 465       where
 466         (a1, r1) = coercionKind co1
 467         (a2, r2) = coercionKind co2
 468
 469 leftCoercionTyCon =
 470   mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
 471   where
 472     leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 473       where
 474         (ty1,ty2) = fst (splitCoercionKindOf co)
 475
 476 rightCoercionTyCon =
 477   mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
 478   where
 479     rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 480       where
 481         (ty1,ty2) = snd (splitCoercionKindOf co)
 482
 483 splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
 484 -- Helper for left and right.  Finds coercion kind of its input and
 485 -- returns the left and right projections of the coercion...
 486 --
 487 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 488 splitCoercionKindOf co
 489   | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
 490   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 491   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 492   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 493 splitCoercionKindOf co
 494   = pprPanic "Coercion.splitCoercionKindOf"
 495              (ppr co $$ ppr (coercionKindPredTy co))
 496
 497 instCoercionTyCon
 498   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
 499   where
 500     instantiateCo t s =
 501       let Just (tv, ty) = splitForAllTy_maybe t in
 502       substTyWith [tv] [s] ty
 503
 504     instCoercionKind (co1:ty:rest) = ASSERT( null rest )
 505                                      (instantiateCo t1 ty, instantiateCo t2 ty)
 506       where (t1, t2) = coercionKind co1
 507
 508 unsafeCoercionTyCon
 509   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
 510   where
 511    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2)
 512
 513 --------------------------------------
 514 -- ...and their names
 515
 516 mkCoConName :: FastString -> Unique -> TyCon -> Name
 517 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
 518                             key (ATyCon coCon) BuiltInSyntax
 519
 520 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: Name
 521
 522 transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
 523 symCoercionTyConName   = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
 524 leftCoercionTyConName  = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
 525 rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
 526 instCoercionTyConName  = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
 527 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 528
 529
 530
 531 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
 532 -- ^ If @co :: T ts ~ rep_ty@ then:
 533 --
 534 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
 535 instNewTyCon_maybe tc tys
 536   | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
 537   = ASSERT( tys `lengthIs` tyConArity tc )
 538     Just (substTyWith tvs tys ty,
 539           case mb_co_tc of
 540            Nothing    -> IdCo
 541            Just co_tc -> ACo (mkTyConApp co_tc tys))
 542   | otherwise
 543   = Nothing
 544
 545 -- this is here to avoid module loops
 546 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 547 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
 548 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
 549 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
 550 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
 551 --
 552 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
 553 --
 554 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
 555 splitNewTypeRepCo_maybe ty
 556   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 557 splitNewTypeRepCo_maybe (TyConApp tc tys)
 558   | Just (ty', coi) <- instNewTyCon_maybe tc tys
 559   = case coi of
 560         ACo co -> Just (ty', co)
 561         IdCo   -> panic "splitNewTypeRepCo_maybe"
 562                         -- This case handled by coreView
 563 splitNewTypeRepCo_maybe _
 564   = Nothing
 565
 566 -- | Determines syntactic equality of coercions
 567 coreEqCoercion :: Coercion -> Coercion -> Bool
 568 coreEqCoercion = coreEqType
 569 \end{code}
 570
 571
 572 --------------------------------------
 573 -- CoercionI smart constructors
 574 --      lifted smart constructors of ordinary coercions
 575
 576 \begin{code}
 577 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
 578 -- can represent either one of:
 579 --
 580 -- 1. A proper 'Coercion'
 581 --
 582 -- 2. The identity coercion
 583 data CoercionI = IdCo | ACo Coercion
 584
 585 instance Outputable CoercionI where
 586   ppr IdCo     = ptext (sLit "IdCo")
 587   ppr (ACo co) = ppr co
 588
 589 isIdentityCoI :: CoercionI -> Bool
 590 isIdentityCoI IdCo = True
 591 isIdentityCoI _    = False
 592
 593 -- | Tests whether all the given 'CoercionI's represent the identity coercion
 594 allIdCoIs :: [CoercionI] -> Bool
 595 allIdCoIs = all isIdentityCoI
 596
 597 -- | For each 'CoercionI' in the input list, return either the 'Coercion' it
 598 -- contains or the corresponding 'Type' from the other list
 599 zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
 600 zipCoArgs cois tys = zipWith fromCoI cois tys
 601
 602 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
 603 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
 604 fromCoI :: CoercionI -> Type -> Type
 605 fromCoI IdCo ty     = ty        -- Identity coercion represented
 606 fromCoI (ACo co) _  = co        --      by the type itself
 607
 608 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
 609 mkSymCoI :: CoercionI -> CoercionI
 610 mkSymCoI IdCo = IdCo
 611 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
 612                                 -- the smart constructor
 613                                 -- is too smart with tyvars
 614
 615 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
 616 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
 617 mkTransCoI IdCo aco = aco
 618 mkTransCoI aco IdCo = aco
 619 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
 620
 621 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
 622 mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
 623 mkTyConAppCoI tyCon tys cois
 624   | allIdCoIs cois = IdCo
 625   | otherwise      = ACo (TyConApp tyCon (zipCoArgs cois tys))
 626
 627 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
 628 mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 629 mkAppTyCoI _   IdCo _   IdCo = IdCo
 630 mkAppTyCoI ty1 coi1 ty2 coi2 =
 631         ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 632
 633 -- | Smart constructor for function-'Coercion's on 'CoercionI', see also 'mkFunCoercion'
 634 mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 635 mkFunTyCoI _   IdCo _   IdCo = IdCo
 636 mkFunTyCoI ty1 coi1 ty2 coi2 =
 637         ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 638
 639 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
 640 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
 641 mkForAllTyCoI _ IdCo = IdCo
 642 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
 643
 644 -- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
 645 -- panic
 646 fromACo :: CoercionI -> Coercion
 647 fromACo (ACo co) = co
 648
 649 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
 650 --
 651 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
 652 mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
 653 mkClassPPredCoI cls tys cois
 654   | allIdCoIs cois = IdCo
 655   | otherwise      = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
 656
 657 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 658 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
 659 mkIParamPredCoI _   IdCo     = IdCo
 660 mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
 661
 662 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 663 mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 664 mkEqPredCoI _    IdCo     _   IdCo      = IdCo
 665 mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
 666 mkEqPredCoI _   (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
 667 \end{code}