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,
  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         isIdentityCoercion,
  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 -- Coercion kind and type mk's
 188 -- (make saturated TyConApp CoercionTyCon{...} args)
 189
 190 -- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
 191 -- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
 192 -- if possible
 193 mkCoercion :: TyCon -> [Type] -> Coercion
 194 mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
 195                         TyConApp coCon args
 196
 197 -- | Apply a 'Coercion' to another 'Coercion', which is presumably a 'Coercion' constructor of some
 198 -- kind
 199 mkAppCoercion :: Coercion -> Coercion -> Coercion
 200 mkAppCoercion    co1 co2 = mkAppTy co1 co2
 201
 202 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
 203 -- See also 'mkAppCoercion'
 204 mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
 205 mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys
 206
 207 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
 208 mkForAllCoercion :: Var -> Coercion -> Coercion
 209 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
 210 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
 211
 212 -- | Make a function 'Coercion' between two other 'Coercion's
 213 mkFunCoercion :: Coercion -> Coercion -> Coercion
 214 mkFunCoercion    co1 co2 = mkFunTy co1 co2
 215
 216
 217 -------------------------------
 218
 219 mkSymCoercion :: Coercion -> Coercion
 220 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality between
 221 -- the same types but in the other "direction", so a kind of @t1 ~ t2@ becomes the
 222 -- kind @t2 ~ t1@.
 223 --
 224 -- This function attempts to simplify the generated 'Coercion' by removing redundant applications
 225 -- of @sym@. This is done by pushing this new @sym@ down into the 'Coercion' and exploiting the fact that
 226 -- @sym (sym co) = co@.
 227 mkSymCoercion co
 228   | Just co' <- coreView co = mkSymCoercion co'
 229
 230 mkSymCoercion (ForAllTy tv ty)  = ForAllTy tv (mkSymCoercion ty)
 231 mkSymCoercion (AppTy co1 co2)   = AppTy (mkSymCoercion co1) (mkSymCoercion co2)
 232 mkSymCoercion (FunTy co1 co2)   = FunTy (mkSymCoercion co1) (mkSymCoercion co2)
 233
 234 mkSymCoercion (TyConApp tc cos)
 235   | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos)
 236
 237 mkSymCoercion (TyConApp tc [co])
 238   | tc `hasKey` symCoercionTyConKey   = co    -- sym (sym co) --> co
 239   | tc `hasKey` leftCoercionTyConKey  = mkLeftCoercion (mkSymCoercion co)
 240   | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)
 241
 242 mkSymCoercion (TyConApp tc [co1,co2])
 243   | tc `hasKey` transCoercionTyConKey
 244      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
 245      -- Note reversal of arguments!
 246   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
 247
 248   | tc `hasKey` instCoercionTyConKey
 249      -- sym (co @ ty) --> (sym co) @ ty
 250      -- Note: sym is not applied to 'ty'
 251   = mkInstCoercion (mkSymCoercion co1) co2
 252
 253 mkSymCoercion (TyConApp tc cos)         -- Other coercion tycons, such as those
 254   = mkCoercion symCoercionTyCon [TyConApp tc cos]  -- arising from newtypes
 255
 256 mkSymCoercion (TyVarTy tv)
 257   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
 258   | otherwise  = TyVarTy tv     -- Reflexive
 259
 260 -------------------------------
 261 -- ToDo: we should be cleverer about transitivity
 262
 263 mkTransCoercion :: Coercion -> Coercion -> Coercion
 264 -- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
 265 --
 266 -- This function attempts to simplify the generated 'Coercion' by exploiting the fact that
 267 -- @sym g `trans` g = id@.
 268 mkTransCoercion g1 g2   -- sym g `trans` g = id
 269   | (t1,_) <- coercionKind g1
 270   , (_,t2) <- coercionKind g2
 271   , t1 `coreEqType` t2
 272   = t1
 273
 274   | otherwise
 275   = mkCoercion transCoercionTyCon [g1, g2]
 276
 277
 278 -------------------------------
 279 -- Smart constructors for left and right
 280
 281 mkLeftCoercion :: Coercion -> Coercion
 282 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
 283 -- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
 284 --
 285 -- > mkLeftCoercion c :: f ~ g
 286 mkLeftCoercion co
 287   | Just (co', _) <- splitAppCoercion_maybe co = co'
 288   | otherwise = mkCoercion leftCoercionTyCon [co]
 289
 290 mkRightCoercion :: Coercion -> Coercion
 291 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
 292 -- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
 293 --
 294 -- > mkLeftCoercion c :: x ~ y
 295 mkRightCoercion  co
 296   | Just (_, co2) <- splitAppCoercion_maybe co = co2
 297   | otherwise = mkCoercion rightCoercionTyCon [co]
 298
 299 mkRightCoercions :: Int -> Coercion -> [Coercion]
 300 -- ^ As 'mkRightCoercion', but finds the 'Coercion's available on the right side of @n@
 301 -- nested application 'Coercion's, manufacturing new left or right cooercions as necessary
 302 -- if suffficiently many are not directly available.
 303 mkRightCoercions n co
 304   = go n co []
 305   where
 306     go n co acc
 307        | n > 0
 308        = case splitAppCoercion_maybe co of
 309           Just (co1,co2) -> go (n-1) co1 (co2:acc)
 310           Nothing        -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
 311        | otherwise
 312        = acc
 313
 314
 315 mkInstCoercion :: Coercion -> Type -> Coercion
 316 -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
 317 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
 318 mkInstCoercion co ty
 319   | Just (tv,co') <- splitForAllTy_maybe co
 320   = substTyWith [tv] [ty] co'   -- (forall a.co) @ ty  -->  co[ty/a]
 321   | otherwise
 322   = mkCoercion instCoercionTyCon  [co, ty]
 323
 324 mkInstsCoercion :: Coercion -> [Type] -> Coercion
 325 -- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right
 326 mkInstsCoercion co tys = foldl mkInstCoercion co tys
 327
 328 {-
 329 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
 330 splitSymCoercion_maybe (TyConApp tc [co]) =
 331   if tc `hasKey` symCoercionTyConKey
 332   then Just co
 333   else Nothing
 334 splitSymCoercion_maybe co = Nothing
 335 -}
 336
 337 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 338 -- ^ Splits a coercion application, being careful *not* to split @left c@ etc.
 339 -- This is because those are really syntactic constructs, not applications
 340 splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
 341 splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 342 splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 343 splitAppCoercion_maybe (TyConApp tc tys)
 344    | not (isCoercionTyCon tc)
 345    = case snocView tys of
 346        Just (tys', ty') -> Just (TyConApp tc tys', ty')
 347        Nothing          -> Nothing
 348 splitAppCoercion_maybe _ = Nothing
 349
 350 {-
 351 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 352 splitTransCoercion_maybe (TyConApp tc [ty1, ty2])
 353  = if tc `hasKey` transCoercionTyConKey then
 354        Just (ty1, ty2)
 355    else
 356        Nothing
 357 splitTransCoercion_maybe other = Nothing
 358
 359 splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
 360 splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
 361  = if tc `hasKey` instCoercionTyConKey then
 362        Just (ty1, ty2)
 363     else
 364        Nothing
 365 splitInstCoercion_maybe other = Nothing
 366
 367 splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
 368 splitLeftCoercion_maybe (TyConApp tc [co])
 369  = if tc `hasKey` leftCoercionTyConKey then
 370        Just co
 371    else
 372        Nothing
 373 splitLeftCoercion_maybe other = Nothing
 374
 375 splitRightCoercion_maybe :: Coercion -> Maybe Coercion
 376 splitRightCoercion_maybe (TyConApp tc [co])
 377  = if tc `hasKey` rightCoercionTyConKey then
 378        Just co
 379    else
 380        Nothing
 381 splitRightCoercion_maybe other = Nothing
 382 -}
 383
 384 -- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
 385 -- but it is used when we know we are dealing with bottom, which is one case in which
 386 -- it is safe.  This is also used implement the @unsafeCoerce#@ primitive.
 387 mkUnsafeCoercion :: Type -> Type -> Coercion
 388 mkUnsafeCoercion ty1 ty2
 389   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 390
 391
 392 -- See note [Newtype coercions] in TyCon
 393
 394 -- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a
 395 -- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the
 396 -- type the appropriate right hand side of the @newtype@, with the free variables
 397 -- a subset of those 'TyVar's.
 398 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 399 mkNewTypeCoercion name tycon tvs rhs_ty
 400   = mkCoercionTyCon name co_con_arity rule
 401   where
 402     co_con_arity = length tvs
 403
 404     rule args = ASSERT( co_con_arity == length args )
 405                 (TyConApp tycon args, substTyWith tvs args rhs_ty)
 406
 407 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
 408 -- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
 409 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
 410 -- representation tycon.
 411 mkFamInstCoercion :: Name       -- ^ Unique name for the coercion tycon
 412                   -> [TyVar]    -- ^ Type parameters of the coercion (@tvs@)
 413                   -> TyCon      -- ^ Family tycon (@F@)
 414                   -> [Type]     -- ^ Type instance (@ts@)
 415                   -> TyCon      -- ^ Representation tycon (@R@)
 416                   -> TyCon      -- ^ Coercion tycon (@Co@)
 417 mkFamInstCoercion name tvs family instTys rep_tycon
 418   = mkCoercionTyCon name coArity rule
 419   where
 420     coArity = length tvs
 421     rule args = (substTyWith tvs args $              -- with sigma = [tys/tvs],
 422                    TyConApp family instTys,          --       sigma (F ts)
 423                  TyConApp rep_tycon args)            --   ~ R tys
 424
 425 --------------------------------------
 426 -- Coercion Type Constructors...
 427
 428 -- Example.  The coercion ((sym c) (sym d) (sym e))
 429 -- will be represented by (TyConApp sym [c, sym d, sym e])
 430 -- If sym c :: p1=q1
 431 --    sym d :: p2=q2
 432 --    sym e :: p3=q3
 433 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 434
 435 -- | Coercion type constructors: avoid using these directly and instead use the @mk*Coercion@ and @split*Coercion@ family
 436 -- of functions if possible.
 437 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon :: TyCon
 438 -- Each coercion TyCon is built with the special CoercionTyCon record and
 439 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 440 -- by any TyConApp in which they are applied, however they may also be over
 441 -- applied (see example above) and the kinding function must deal with this.
 442 symCoercionTyCon =
 443   mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
 444   where
 445     flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
 446         where
 447           (ty1, ty2) = coercionKind co
 448
 449 transCoercionTyCon =
 450   mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
 451   where
 452     composeCoercionKindsOf (co1:co2:rest)
 453       = ASSERT( null rest )
 454         WARN( not (r1 `coreEqType` a2),
 455               text "Strange! Type mismatch in trans coercion, probably a bug"
 456               $$
 457               ppr r1 <+> text "=/=" <+> ppr a2)
 458         (a1, r2)
 459       where
 460         (a1, r1) = coercionKind co1
 461         (a2, r2) = coercionKind co2
 462
 463 leftCoercionTyCon =
 464   mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
 465   where
 466     leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 467       where
 468         (ty1,ty2) = fst (splitCoercionKindOf co)
 469
 470 rightCoercionTyCon =
 471   mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
 472   where
 473     rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 474       where
 475         (ty1,ty2) = snd (splitCoercionKindOf co)
 476
 477 splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
 478 -- Helper for left and right.  Finds coercion kind of its input and
 479 -- returns the left and right projections of the coercion...
 480 --
 481 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 482 splitCoercionKindOf co
 483   | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
 484   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 485   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 486   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 487 splitCoercionKindOf co
 488   = pprPanic "Coercion.splitCoercionKindOf"
 489              (ppr co $$ ppr (coercionKindPredTy co))
 490
 491 instCoercionTyCon
 492   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
 493   where
 494     instantiateCo t s =
 495       let Just (tv, ty) = splitForAllTy_maybe t in
 496       substTyWith [tv] [s] ty
 497
 498     instCoercionKind (co1:ty:rest) = ASSERT( null rest )
 499                                      (instantiateCo t1 ty, instantiateCo t2 ty)
 500       where (t1, t2) = coercionKind co1
 501
 502 unsafeCoercionTyCon
 503   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
 504   where
 505    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2)
 506
 507 --------------------------------------
 508 -- ...and their names
 509
 510 mkCoConName :: FastString -> Unique -> TyCon -> Name
 511 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
 512                             key (ATyCon coCon) BuiltInSyntax
 513
 514 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: Name
 515
 516 transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
 517 symCoercionTyConName   = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
 518 leftCoercionTyConName  = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
 519 rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
 520 instCoercionTyConName  = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
 521 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 522
 523
 524
 525 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
 526 -- ^ If @co :: T ts ~ rep_ty@ then:
 527 --
 528 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
 529 instNewTyCon_maybe tc tys
 530   | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
 531   = ASSERT( tys `lengthIs` tyConArity tc )
 532     Just (substTyWith tvs tys ty,
 533           case mb_co_tc of
 534            Nothing    -> IdCo
 535            Just co_tc -> ACo (mkTyConApp co_tc tys))
 536   | otherwise
 537   = Nothing
 538
 539 -- this is here to avoid module loops
 540 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 541 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
 542 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
 543 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
 544 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
 545 --
 546 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
 547 --
 548 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
 549 splitNewTypeRepCo_maybe ty
 550   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 551 splitNewTypeRepCo_maybe (TyConApp tc tys)
 552   | Just (ty', coi) <- instNewTyCon_maybe tc tys
 553   = case coi of
 554         ACo co -> Just (ty', co)
 555         IdCo   -> panic "splitNewTypeRepCo_maybe"
 556                         -- This case handled by coreView
 557 splitNewTypeRepCo_maybe _
 558   = Nothing
 559
 560 -- | Determines syntactic equality of coercions
 561 coreEqCoercion :: Coercion -> Coercion -> Bool
 562 coreEqCoercion = coreEqType
 563 \end{code}
 564
 565
 566 --------------------------------------
 567 -- CoercionI smart constructors
 568 --      lifted smart constructors of ordinary coercions
 569
 570 \begin{code}
 571 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
 572 -- can represent either one of:
 573 --
 574 -- 1. A proper 'Coercion'
 575 --
 576 -- 2. The identity coercion
 577 data CoercionI = IdCo | ACo Coercion
 578
 579 isIdentityCoercion :: CoercionI -> Bool
 580 isIdentityCoercion IdCo = True
 581 isIdentityCoercion _    = False
 582
 583 -- | Tests whether all the given 'CoercionI's represent the identity coercion
 584 allIdCos :: [CoercionI] -> Bool
 585 allIdCos = all isIdentityCoercion
 586
 587 -- | For each 'CoercionI' in the input list, return either the 'Coercion' it
 588 -- contains or the corresponding 'Type' from the other list
 589 zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
 590 zipCoArgs cois tys = zipWith fromCoI cois tys
 591
 592 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
 593 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
 594 fromCoI :: CoercionI -> Type -> Type
 595 fromCoI IdCo ty     = ty        -- Identity coercion represented
 596 fromCoI (ACo co) _  = co        --      by the type itself
 597
 598 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
 599 mkSymCoI :: CoercionI -> CoercionI
 600 mkSymCoI IdCo = IdCo
 601 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
 602                                 -- the smart constructor
 603                                 -- is too smart with tyvars
 604
 605 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
 606 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
 607 mkTransCoI IdCo aco = aco
 608 mkTransCoI aco IdCo = aco
 609 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
 610
 611 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
 612 mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
 613 mkTyConAppCoI tyCon tys cois
 614   | allIdCos cois = IdCo
 615   | otherwise     = ACo (TyConApp tyCon (zipCoArgs cois tys))
 616
 617 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
 618 mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 619 mkAppTyCoI _   IdCo _   IdCo = IdCo
 620 mkAppTyCoI ty1 coi1 ty2 coi2 =
 621         ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 622
 623 -- | Smart constructor for function-'Coercion's on 'CoercionI', see also 'mkFunCoercion'
 624 mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 625 mkFunTyCoI _   IdCo _   IdCo = IdCo
 626 mkFunTyCoI ty1 coi1 ty2 coi2 =
 627         ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 628
 629 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
 630 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
 631 mkForAllTyCoI _ IdCo = IdCo
 632 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
 633
 634 -- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
 635 -- panic
 636 fromACo :: CoercionI -> Coercion
 637 fromACo (ACo co) = co
 638
 639 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
 640 --
 641 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
 642 mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
 643 mkClassPPredCoI cls tys cois
 644   | allIdCos cois = IdCo
 645   | otherwise     = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
 646
 647 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 648 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
 649 mkIParamPredCoI _   IdCo     = IdCo
 650 mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
 651
 652 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 653 mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 654 mkEqPredCoI _    IdCo     _   IdCo      = IdCo
 655 mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
 656 mkEqPredCoI _   (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
 657 \end{code}