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