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