compiler/types/Coercion.lhs

   1 T%
   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, coVarKind,
  25         coercionKind, coercionKinds, 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         mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion,
  38
  39         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
  40
  41         unsafeCoercionTyCon, symCoercionTyCon,
  42         transCoercionTyCon, leftCoercionTyCon,
  43         rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
  44         csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon,
  45
  46         -- ** Optimisation
  47         optCoercion,
  48
  49         -- ** Comparison
  50         coreEqCoercion,
  51
  52         -- * CoercionI
  53         CoercionI(..),
  54         isIdentityCoI,
  55         mkSymCoI, mkTransCoI,
  56         mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
  57         mkForAllTyCoI,
  58         fromCoI, fromACo,
  59         mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
  60
  61        ) where
  62
  63 #include "HsVersions.h"
  64
  65 import TypeRep
  66 import Type
  67 import TyCon
  68 import Class
  69 import Var
  70 import Name
  71 import PrelNames
  72 import Util
  73 import BasicTypes
  74 import Outputable
  75 import FastString
  76
  77 -- | A 'Coercion' represents a 'Type' something should be coerced to.
  78 type Coercion     = Type
  79
  80 -- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
  81 -- types that a 'Coercion' will work on.
  82 type CoercionKind = Kind
  83
  84 ------------------------------
  85
  86 -- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
  87 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
  88 --
  89 -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
  90 decomposeCo :: Arity -> Coercion -> [Coercion]
  91 decomposeCo n co
  92   = go n co []
  93   where
  94     go 0 _  cos = cos
  95     go n co cos = go (n-1) (mkLeftCoercion co)
  96                            (mkRightCoercion co : cos)
  97
  98 ------------------------------
  99
 100 -------------------------------------------------------
 101 -- and some coercion kind stuff
 102
 103 coVarKind :: CoVar -> (Type,Type)
 104 -- c :: t1 ~ t2
 105 coVarKind cv = splitCoVarKind (tyVarKind cv)
 106
 107 -- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
 108 -- Panics if the argument is not a valid 'CoercionKind'
 109 splitCoVarKind :: Kind -> (Type, Type)
 110 splitCoVarKind co | Just co' <- kindView co = splitCoVarKind co'
 111 splitCoVarKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)
 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 -- | (mkCoPredTy s t r) produces the type:   (s~t) => r
 118 mkCoPredTy :: Type -> Type -> Type -> Type
 119 mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r
 120
 121 -- | Tests whether a type is just a type equality predicate
 122 isEqPredTy :: Type -> Bool
 123 isEqPredTy (PredTy pred) = isEqPred pred
 124 isEqPredTy _             = False
 125
 126 -- | Creates a type equality predicate
 127 mkEqPred :: (Type, Type) -> PredType
 128 mkEqPred (ty1, ty2) = EqPred ty1 ty2
 129
 130 -- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
 131 -- Panics otherwise
 132 getEqPredTys :: PredType -> (Type,Type)
 133 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
 134 getEqPredTys other            = pprPanic "getEqPredTys" (ppr other)
 135
 136 -- | Create a reflexive 'CoercionKind' that asserts that a type can be coerced to itself
 137 mkReflCoKind :: Type -> CoercionKind
 138 mkReflCoKind ty = mkCoKind ty ty
 139
 140 -- | If it is the case that
 141 --
 142 -- > c :: (t1 ~ t2)
 143 --
 144 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
 145 coercionKind :: Coercion -> (Type, Type)
 146 coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
 147                             | otherwise = (ty, ty)
 148 coercionKind (AppTy ty1 ty2)
 149   = let (t1, t2) = coercionKind ty1
 150         (s1, s2) = coercionKind ty2 in
 151     (mkAppTy t1 s1, mkAppTy t2 s2)
 152 coercionKind (TyConApp tc args)
 153   | Just (ar, rule) <- isCoercionTyCon_maybe tc
 154     -- CoercionTyCons carry their kinding rule, so we use it here
 155   = ASSERT( length args >= ar ) -- Always saturated
 156     let (ty1,ty2)    = rule (take ar args)      -- Apply the rule to the right number of args
 157         (tys1, tys2) = coercionKinds (drop ar args)
 158     in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)
 159
 160   | otherwise
 161   = let (lArgs, rArgs) = coercionKinds args in
 162     (TyConApp tc lArgs, TyConApp tc rArgs)
 163 coercionKind (FunTy ty1 ty2)
 164   = let (t1, t2) = coercionKind ty1
 165         (s1, s2) = coercionKind ty2 in
 166     (mkFunTy t1 s1, mkFunTy t2 s2)
 167
 168 coercionKind (ForAllTy tv ty)
 169   | isCoVar tv
 170 --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
 171 --    ----------------------------------------------
 172 --    c1~c2 => c3  ::  (s1~t1) => r1 ~ (s2~t2) => r2
 173 --      or
 174 --    forall (_:c1~c2)
 175   = let (c1,c2) = coVarKind tv
 176         (s1,s2) = coercionKind c1
 177         (t1,t2) = coercionKind c2
 178         (r1,r2) = coercionKind ty
 179     in
 180     (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
 181
 182   | otherwise
 183 --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
 184 --   ----------------------------------------------
 185 --    forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
 186   = let (ty1, ty2) = coercionKind ty in
 187     (ForAllTy tv ty1, ForAllTy tv ty2)
 188
 189 coercionKind (PredTy (EqPred c1 c2))
 190   = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
 191     let k1 = coercionKindPredTy c1
 192         k2 = coercionKindPredTy c2 in
 193     (k1,k2)
 194   -- These should not show up in coercions at all
 195   -- becuase they are in the form of for-alls
 196   where
 197     coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
 198
 199
 200
 201 coercionKind (PredTy (ClassP cl args))
 202   = let (lArgs, rArgs) = coercionKinds args in
 203     (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
 204 coercionKind (PredTy (IParam name ty))
 205   = let (ty1, ty2) = coercionKind ty in
 206     (PredTy (IParam name ty1), PredTy (IParam name ty2))
 207
 208 -- | Apply 'coercionKind' to multiple 'Coercion's
 209 coercionKinds :: [Coercion] -> ([Type], [Type])
 210 coercionKinds tys = unzip $ map coercionKind tys
 211
 212 -------------------------------------
 213 isIdentityCoercion :: Coercion -> Bool
 214 isIdentityCoercion co
 215   = case coercionKind co of
 216        (t1,t2) -> t1 `coreEqType` t2
 217 \end{code}
 218
 219 %************************************************************************
 220 %*                                                                      *
 221             Building coercions
 222 %*                                                                      *
 223 %************************************************************************
 224
 225 Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args)
 226
 227 \begin{code}
 228 -- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
 229 -- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
 230 -- if possible
 231 mkCoercion :: TyCon -> [Type] -> Coercion
 232 mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
 233                         TyConApp coCon args
 234
 235 -- | Apply a 'Coercion' to another 'Coercion', which is presumably a
 236 -- 'Coercion' constructor of some kind
 237 mkAppCoercion :: Coercion -> Coercion -> Coercion
 238 mkAppCoercion co1 co2 = mkAppTy co1 co2
 239
 240 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
 241 -- See also 'mkAppCoercion'
 242 mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
 243 mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
 244
 245 -- | Apply a type constructor to a list of coercions.
 246 mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
 247 mkTyConCoercion con cos = mkTyConApp con cos
 248
 249 -- | Make a function 'Coercion' between two other 'Coercion's
 250 mkFunCoercion :: Coercion -> Coercion -> Coercion
 251 mkFunCoercion co1 co2 = mkFunTy co1 co2
 252
 253 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
 254 mkForAllCoercion :: Var -> Coercion -> Coercion
 255 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
 256 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
 257
 258
 259 -------------------------------
 260
 261 mkSymCoercion :: Coercion -> Coercion
 262 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality
 263 -- between the same types but in the other "direction", so a kind of @t1 ~ t2@
 264 -- becomes the kind @t2 ~ t1@.
 265 --
 266 -- This function attempts to simplify the generated 'Coercion' by removing
 267 -- redundant applications of @sym@. This is done by pushing this new @sym@
 268 -- down into the 'Coercion' and exploiting the fact that @sym (sym co) = co@.
 269 mkSymCoercion co
 270   | Just co' <- coreView co = mkSymCoercion co'
 271
 272 mkSymCoercion (ForAllTy tv ty)  = ForAllTy tv (mkSymCoercion ty)
 273 mkSymCoercion (AppTy co1 co2)   = AppTy (mkSymCoercion co1) (mkSymCoercion co2)
 274 mkSymCoercion (FunTy co1 co2)   = FunTy (mkSymCoercion co1) (mkSymCoercion co2)
 275
 276 mkSymCoercion (TyConApp tc cos)
 277   | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos)
 278
 279 mkSymCoercion (TyConApp tc [co])
 280   | tc `hasKey` symCoercionTyConKey   = co    -- sym (sym co) --> co
 281   | tc `hasKey` leftCoercionTyConKey  = mkLeftCoercion (mkSymCoercion co)
 282   | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)
 283
 284 mkSymCoercion (TyConApp tc [co1,co2])
 285   | tc `hasKey` transCoercionTyConKey
 286      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
 287      -- Note reversal of arguments!
 288   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
 289
 290   | tc `hasKey` instCoercionTyConKey
 291      -- sym (co @ ty) --> (sym co) @ ty
 292      -- Note: sym is not applied to 'ty'
 293   = mkInstCoercion (mkSymCoercion co1) co2
 294
 295 mkSymCoercion (TyConApp tc cos)         -- Other coercion tycons, such as those
 296   = mkCoercion symCoercionTyCon [TyConApp tc cos]  -- arising from newtypes
 297
 298 mkSymCoercion (TyVarTy tv)
 299   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
 300   | otherwise  = TyVarTy tv     -- Reflexive
 301
 302 -------------------------------
 303 -- ToDo: we should be cleverer about transitivity
 304
 305 mkTransCoercion :: Coercion -> Coercion -> Coercion
 306 -- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
 307 --
 308 -- This function attempts to simplify the generated 'Coercion' by exploiting the fact that
 309 -- @sym g `trans` g = id@.
 310 mkTransCoercion g1 g2   -- sym g `trans` g = id
 311   | (t1,_) <- coercionKind g1
 312   , (_,t2) <- coercionKind g2
 313   , t1 `coreEqType` t2
 314   = t1
 315
 316   | otherwise
 317   = mkCoercion transCoercionTyCon [g1, g2]
 318
 319
 320 -------------------------------
 321 -- Smart constructors for left and right
 322
 323 mkLeftCoercion :: Coercion -> Coercion
 324 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
 325 -- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
 326 --
 327 -- > mkLeftCoercion c :: f ~ g
 328 mkLeftCoercion co
 329   | Just (co', _) <- splitAppCoercion_maybe co = co'
 330   | otherwise = mkCoercion leftCoercionTyCon [co]
 331
 332 mkRightCoercion :: Coercion -> Coercion
 333 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
 334 -- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
 335 --
 336 -- > mkLeftCoercion c :: x ~ y
 337 mkRightCoercion  co
 338   | Just (_, co2) <- splitAppCoercion_maybe co = co2
 339   | otherwise = mkCoercion rightCoercionTyCon [co]
 340
 341 mkRightCoercions :: Int -> Coercion -> [Coercion]
 342 -- ^ As 'mkRightCoercion', but finds the 'Coercion's available on the right side of @n@
 343 -- nested application 'Coercion's, manufacturing new left or right cooercions as necessary
 344 -- if suffficiently many are not directly available.
 345 mkRightCoercions n co
 346   = go n co []
 347   where
 348     go n co acc
 349        | n > 0
 350        = case splitAppCoercion_maybe co of
 351           Just (co1,co2) -> go (n-1) co1 (co2:acc)
 352           Nothing        -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
 353        | otherwise
 354        = acc
 355
 356
 357 mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
 358 mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
 359 mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
 360 mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co]
 361
 362 -------------------------------
 363 mkInstCoercion :: Coercion -> Type -> Coercion
 364 -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
 365 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
 366 mkInstCoercion co ty
 367   | Just (tv,co') <- splitForAllTy_maybe co
 368   = substTyWith [tv] [ty] co'   -- (forall a.co) @ ty  -->  co[ty/a]
 369   | otherwise
 370   = mkCoercion instCoercionTyCon  [co, ty]
 371
 372 mkInstsCoercion :: Coercion -> [Type] -> Coercion
 373 -- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right
 374 mkInstsCoercion co tys = foldl mkInstCoercion co tys
 375
 376 {-
 377 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
 378 splitSymCoercion_maybe (TyConApp tc [co]) =
 379   if tc `hasKey` symCoercionTyConKey
 380   then Just co
 381   else Nothing
 382 splitSymCoercion_maybe co = Nothing
 383 -}
 384
 385 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 386 -- ^ Splits a coercion application, being careful *not* to split @left c@ etc.
 387 -- This is because those are really syntactic constructs, not applications
 388 splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
 389 splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 390 splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 391 splitAppCoercion_maybe (TyConApp tc tys)
 392    | not (isCoercionTyCon tc)
 393    = case snocView tys of
 394        Just (tys', ty') -> Just (TyConApp tc tys', ty')
 395        Nothing          -> Nothing
 396 splitAppCoercion_maybe _ = Nothing
 397
 398 {-
 399 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 400 splitTransCoercion_maybe (TyConApp tc [ty1, ty2])
 401  = if tc `hasKey` transCoercionTyConKey then
 402        Just (ty1, ty2)
 403    else
 404        Nothing
 405 splitTransCoercion_maybe other = Nothing
 406
 407 splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
 408 splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
 409  = if tc `hasKey` instCoercionTyConKey then
 410        Just (ty1, ty2)
 411     else
 412        Nothing
 413 splitInstCoercion_maybe other = Nothing
 414
 415 splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
 416 splitLeftCoercion_maybe (TyConApp tc [co])
 417  = if tc `hasKey` leftCoercionTyConKey then
 418        Just co
 419    else
 420        Nothing
 421 splitLeftCoercion_maybe other = Nothing
 422
 423 splitRightCoercion_maybe :: Coercion -> Maybe Coercion
 424 splitRightCoercion_maybe (TyConApp tc [co])
 425  = if tc `hasKey` rightCoercionTyConKey then
 426        Just co
 427    else
 428        Nothing
 429 splitRightCoercion_maybe other = Nothing
 430 -}
 431
 432 -- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
 433 -- but it is used when we know we are dealing with bottom, which is one case in which
 434 -- it is safe.  This is also used implement the @unsafeCoerce#@ primitive.
 435 mkUnsafeCoercion :: Type -> Type -> Coercion
 436 mkUnsafeCoercion ty1 ty2
 437   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 438
 439
 440 -- See note [Newtype coercions] in TyCon
 441
 442 -- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a
 443 -- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the
 444 -- type the appropriate right hand side of the @newtype@, with the free variables
 445 -- a subset of those 'TyVar's.
 446 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 447 mkNewTypeCoercion name tycon tvs rhs_ty
 448   = mkCoercionTyCon name co_con_arity rule
 449   where
 450     co_con_arity = length tvs
 451
 452     rule args = ASSERT( co_con_arity == length args )
 453                 (TyConApp tycon args, substTyWith tvs args rhs_ty)
 454
 455 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
 456 -- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
 457 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
 458 -- representation tycon.
 459 mkFamInstCoercion :: Name       -- ^ Unique name for the coercion tycon
 460                   -> [TyVar]    -- ^ Type parameters of the coercion (@tvs@)
 461                   -> TyCon      -- ^ Family tycon (@F@)
 462                   -> [Type]     -- ^ Type instance (@ts@)
 463                   -> TyCon      -- ^ Representation tycon (@R@)
 464                   -> TyCon      -- ^ Coercion tycon (@Co@)
 465 mkFamInstCoercion name tvs family instTys rep_tycon
 466   = mkCoercionTyCon name coArity rule
 467   where
 468     coArity = length tvs
 469     rule args = (substTyWith tvs args $              -- with sigma = [tys/tvs],
 470                    TyConApp family instTys,          --       sigma (F ts)
 471                  TyConApp rep_tycon args)            --   ~ R tys
 472 \end{code}
 473
 474
 475 %************************************************************************
 476 %*                                                                      *
 477             Coercion Type Constructors
 478 %*                                                                      *
 479 %************************************************************************
 480
 481 Example.  The coercion ((sym c) (sym d) (sym e))
 482 will be represented by (TyConApp sym [c, sym d, sym e])
 483 If sym c :: p1=q1
 484    sym d :: p2=q2
 485    sym e :: p3=q3
 486 then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 487
 488 \begin{code}
 489 -- | Coercion type constructors: avoid using these directly and instead use
 490 -- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
 491 --
 492 -- Each coercion TyCon is built with the special CoercionTyCon record and
 493 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 494 -- by any TyConApp in which they are applied, however they may also be over
 495 -- applied (see example above) and the kinding function must deal with this.
 496 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon,
 497   rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
 498   csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
 499
 500 symCoercionTyCon =
 501   mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
 502   where
 503     flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
 504         where
 505           (ty1, ty2) = coercionKind co
 506
 507 transCoercionTyCon =
 508   mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
 509   where
 510     composeCoercionKindsOf (co1:co2:rest)
 511       = ASSERT( null rest )
 512         WARN( not (r1 `coreEqType` a2),
 513               text "Strange! Type mismatch in trans coercion, probably a bug"
 514               $$
 515               _err_stuff )
 516         (a1, r2)
 517       where
 518         (a1, r1) = coercionKind co1
 519         (a2, r2) = coercionKind co2
 520
 521         _err_stuff = vcat [ text "co1:" <+> ppr co1
 522                           , text "co1 kind left:"  <+> ppr a1
 523                           , text "co1 kind right:" <+> ppr r1
 524                           , text "co2:" <+> ppr co2
 525                           , text "co2 kind left:"  <+> ppr a2
 526                           , text "co2 kind right:" <+> ppr r2 ]
 527
 528 ---------------------------------------------------
 529 leftCoercionTyCon  = mkCoercionTyCon leftCoercionTyConName  1 (fst . decompLR)
 530 rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (snd . decompLR)
 531
 532 decompLR :: [Type] -> ((Type,Type), (Type,Type))
 533 -- Helper for left and right.  Finds coercion kind of its input and
 534 -- returns the left and right projections of the coercion...
 535 --
 536 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 537 decompLR (co : rest)
 538   | (ty1, ty2) <- coercionKind co
 539   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 540   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 541   = ASSERT( null rest)
 542     ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 543 decompLR cos
 544   = pprPanic "Coercion.decompLR"
 545              (ppr cos $$ vcat (map (pprEqPred .coercionKind) cos))
 546
 547 ---------------------------------------------------
 548 instCoercionTyCon
 549   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
 550   where
 551     instantiateCo t s =
 552       let Just (tv, ty) = splitForAllTy_maybe t in
 553       substTyWith [tv] [s] ty
 554
 555     instCoercionKind (co1:ty:rest) = ASSERT( null rest )
 556                                      (instantiateCo t1 ty, instantiateCo t2 ty)
 557       where (t1, t2) = coercionKind co1
 558
 559 ---------------------------------------------------
 560 unsafeCoercionTyCon
 561   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
 562   where
 563    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2)
 564
 565 ---------------------------------------------------
 566 -- The csel* family
 567 --   If         co :: (s1~t1 => r1) ~ (s2~t2 => r2)
 568 -- Then   csel1 co :: s1 ~ s2
 569 --        csel2 co :: t1 ~ t2
 570 --        cselR co :: r1 ~ r2
 571
 572 csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 (fstOf3   . decompCsel)
 573 csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 (sndOf3   . decompCsel)
 574 cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (thirdOf3 . decompCsel)
 575
 576 decompCsel :: [Coercion] -> ((Type,Type), (Type,Type), (Type,Type))
 577 decompCsel (co : rest)
 578   | (ty1,ty2) <- coercionKind co
 579   , Just (cv1, r1) <- splitForAllTy_maybe ty1
 580   , Just (cv2, r2) <- splitForAllTy_maybe ty2
 581   , (s1,t1) <- ASSERT( isCoVar cv1) coVarKind cv1
 582   , (s2,t2) <- ASSERT( isCoVar cv1) coVarKind cv2
 583   = ASSERT( null rest )
 584     ((s1,s2), (t1,t2), (r1,r2))
 585 decompCsel other = pprPanic "decompCsel" (ppr other)
 586
 587 fstOf3   :: (a,b,c) -> a
 588 sndOf3   :: (a,b,c) -> b
 589 thirdOf3 :: (a,b,c) -> c
 590 fstOf3      (a,_,_) =  a
 591 sndOf3      (_,b,_) =  b
 592 thirdOf3    (_,_,c) =  c
 593
 594 --------------------------------------
 595 -- Their Names
 596
 597 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
 598    rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
 599    csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
 600
 601 transCoercionTyConName  = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
 602 symCoercionTyConName    = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
 603 leftCoercionTyConName   = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
 604 rightCoercionTyConName  = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
 605 instCoercionTyConName   = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
 606 csel1CoercionTyConName  = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
 607 csel2CoercionTyConName  = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
 608 cselRCoercionTyConName  = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
 609 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 610
 611 mkCoConName :: FastString -> Unique -> TyCon -> Name
 612 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
 613                             key (ATyCon coCon) BuiltInSyntax
 614 \end{code}
 615
 616
 617 %************************************************************************
 618 %*                                                                      *
 619             Newtypes
 620 %*                                                                      *
 621 %************************************************************************
 622
 623 \begin{code}
 624 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
 625 -- ^ If @co :: T ts ~ rep_ty@ then:
 626 --
 627 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
 628 instNewTyCon_maybe tc tys
 629   | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
 630   = ASSERT( tys `lengthIs` tyConArity tc )
 631     Just (substTyWith tvs tys ty,
 632           case mb_co_tc of
 633            Nothing    -> IdCo
 634            Just co_tc -> ACo (mkTyConApp co_tc tys))
 635   | otherwise
 636   = Nothing
 637
 638 -- this is here to avoid module loops
 639 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 640 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
 641 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
 642 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
 643 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
 644 --
 645 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
 646 --
 647 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
 648 splitNewTypeRepCo_maybe ty
 649   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 650 splitNewTypeRepCo_maybe (TyConApp tc tys)
 651   | Just (ty', coi) <- instNewTyCon_maybe tc tys
 652   = case coi of
 653         ACo co -> Just (ty', co)
 654         IdCo   -> panic "splitNewTypeRepCo_maybe"
 655                         -- This case handled by coreView
 656 splitNewTypeRepCo_maybe _
 657   = Nothing
 658
 659 -- | Determines syntactic equality of coercions
 660 coreEqCoercion :: Coercion -> Coercion -> Bool
 661 coreEqCoercion = coreEqType
 662 \end{code}
 663
 664
 665 %************************************************************************
 666 %*                                                                      *
 667             CoercionI and its constructors
 668 %*                                                                      *
 669 %************************************************************************
 670
 671 --------------------------------------
 672 -- CoercionI smart constructors
 673 --      lifted smart constructors of ordinary coercions
 674
 675 \begin{code}
 676 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
 677 -- can represent either one of:
 678 --
 679 -- 1. A proper 'Coercion'
 680 --
 681 -- 2. The identity coercion
 682 data CoercionI = IdCo | ACo Coercion
 683
 684 instance Outputable CoercionI where
 685   ppr IdCo     = ptext (sLit "IdCo")
 686   ppr (ACo co) = ppr co
 687
 688 isIdentityCoI :: CoercionI -> Bool
 689 isIdentityCoI IdCo = True
 690 isIdentityCoI _    = False
 691
 692 -- | Tests whether all the given 'CoercionI's represent the identity coercion
 693 allIdCoIs :: [CoercionI] -> Bool
 694 allIdCoIs = all isIdentityCoI
 695
 696 -- | For each 'CoercionI' in the input list, return either the 'Coercion' it
 697 -- contains or the corresponding 'Type' from the other list
 698 zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
 699 zipCoArgs cois tys = zipWith fromCoI cois tys
 700
 701 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
 702 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
 703 fromCoI :: CoercionI -> Type -> Type
 704 fromCoI IdCo ty     = ty        -- Identity coercion represented
 705 fromCoI (ACo co) _  = co        --      by the type itself
 706
 707 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
 708 mkSymCoI :: CoercionI -> CoercionI
 709 mkSymCoI IdCo = IdCo
 710 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
 711                                 -- the smart constructor
 712                                 -- is too smart with tyvars
 713
 714 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
 715 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
 716 mkTransCoI IdCo aco = aco
 717 mkTransCoI aco IdCo = aco
 718 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
 719
 720 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
 721 mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
 722 mkTyConAppCoI tyCon tys cois
 723   | allIdCoIs cois = IdCo
 724   | otherwise      = ACo (TyConApp tyCon (zipCoArgs cois tys))
 725
 726 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
 727 mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 728 mkAppTyCoI _   IdCo _   IdCo = IdCo
 729 mkAppTyCoI ty1 coi1 ty2 coi2 =
 730         ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 731
 732 -- | Smart constructor for function-'Coercion's on 'CoercionI', see also 'mkFunCoercion'
 733 mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 734 mkFunTyCoI _   IdCo _   IdCo = IdCo
 735 mkFunTyCoI ty1 coi1 ty2 coi2 =
 736         ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 737
 738 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
 739 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
 740 mkForAllTyCoI _ IdCo = IdCo
 741 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
 742
 743 -- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
 744 -- panic
 745 fromACo :: CoercionI -> Coercion
 746 fromACo (ACo co) = co
 747
 748 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
 749 --
 750 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
 751 mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
 752 mkClassPPredCoI cls tys cois
 753   | allIdCoIs cois = IdCo
 754   | otherwise      = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
 755
 756 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 757 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
 758 mkIParamPredCoI _   IdCo     = IdCo
 759 mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
 760
 761 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 762 mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 763 mkEqPredCoI _    IdCo     _   IdCo      = IdCo
 764 mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
 765 mkEqPredCoI _   (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
 766 \end{code}
 767
 768 %************************************************************************
 769 %*                                                                      *
 770                  Optimising coercions
 771 %*                                                                      *
 772 %************************************************************************
 773
 774 \begin{code}
 775 optCoercion :: Coercion -> Coercion
 776 optCoercion co
 777   = ASSERT2( coercionKind co `eq` coercionKind result,
 778              ppr co $$ ppr result $$ ppr (coercionKind co) $$ ppr (coercionKind result) )
 779     result
 780   where
 781         (s1,t1) `eq` (s2,t2) = s1 `coreEqType` s2 && t1 `coreEqType` t2
 782
 783         (result,_,_) = go co
 784                          -- optimized, changed?, identity?
 785         go :: Coercion -> ( Coercion, Bool, Bool )
 786         -- traverse coercion term bottom up and return
 787         --
 788         --    1) equivalent coercion, in optimized form
 789         --
 790         --    2) whether the output coercion differs from
 791         --       the input coercion
 792         --
 793         --    3) whether the coercion is an identity coercion
 794         --
 795         -- Performs the following optimizations:
 796         --
 797         --      sym id          >->     id
 798         --      trans id co     >->     co
 799         --      trans co id     >->     co
 800         --      sym (sym co)    >->     co
 801         --      trans g (sym g) >->     id
 802         --      trans (sym g) g >->     id
 803         --
 804         go ty@(TyVarTy a) | isCoVar a = let (ty1,ty2) = coercionKind ty
 805                                         in (ty, False, ty1 `coreEqType` ty2)
 806                           | otherwise = (ty, False, True)
 807         go ty@(AppTy ty1 ty2)
 808           = let (ty1', chan1, id1) = go ty1
 809                 (ty2', chan2, id2) = go ty2
 810             in if chan1 || chan2
 811                  then (AppTy ty1' ty2', True,  id1 && id2)
 812                  else (ty             , False, id1 && id2)
 813         go ty@(TyConApp tc args)
 814           | tc == symCoercionTyCon, (ty1:tys) <- args
 815           = goSym ty ty1 tys
 816           | tc == transCoercionTyCon, [ty1,ty2] <- args
 817           = goTrans ty ty1 ty2
 818           | tc == leftCoercionTyCon, [ty1] <- args
 819           = goLeft ty ty1
 820           | tc == rightCoercionTyCon, [ty1] <- args
 821           = goRight ty ty1
 822           | tc == instCoercionTyCon, [ty1,ty2] <- args
 823           = goInst ty ty1 ty2
 824           | not (isCoercionTyCon tc)
 825           = let (args', chans, ids) = mapAndUnzip3 go args
 826             in  if or chans
 827                   then (TyConApp tc args', True , and ids)
 828                   else (ty               , False, and ids)
 829           | otherwise
 830           = (ty, False, False)
 831         go ty@(FunTy ty1 ty2)
 832           = let (ty1',chan1,id1) = go ty1
 833                 (ty2',chan2,id2) = go ty2
 834             in  if chan1 || chan2
 835                   then (FunTy ty1' ty2', True , id1 && id2)
 836                   else (ty             , False, id1 && id2)
 837         go ty@(ForAllTy tv ty1)
 838           = let (ty1', chan1, id1) = go ty1
 839             in if chan1
 840                  then (ForAllTy tv ty1', True , id1)
 841                  else (ty              , False, id1)
 842         go ty@(PredTy (EqPred ty1 ty2))
 843           = let (ty1', chan1, id1) = go ty1
 844                 (ty2', chan2, id2) = go ty2
 845             in if chan1 || chan2
 846                  then (PredTy (EqPred ty1' ty2'), True , id1 && id2)
 847                  else (ty                       , False, id1 && id2)
 848         go ty@(PredTy (ClassP cl args))
 849           = let (args', chans, ids) = mapAndUnzip3 go args
 850             in  if or chans
 851                   then (PredTy (ClassP cl args'), True , and ids)
 852                   else (ty                      , False, and ids)
 853         go ty@(PredTy (IParam name ty1))
 854           = let (ty1', chan1, id1) = go ty1
 855             in  if chan1
 856                   then (PredTy (IParam name ty1'), True , id1)
 857                   else (ty                       , False, id1)
 858
 859         goSym :: Coercion -> Coercion -> [Coercion] -> ( Coercion, Bool, Bool )
 860         --
 861         -- pushes the sym constructor inwards, if possible
 862         --
 863         --   takes original coercion term
 864         --                  first argument
 865         --                  rest of arguments
 866         goSym ty ty1 tys
 867           = case mkSymCoercion ty1 of
 868               (TyConApp tc _ ) | tc == symCoercionTyCon
 869                                -> let (tys',chans',ids) = mapAndUnzip3 go (ty1:tys)
 870                                   in  if or chans'
 871                                         then (TyConApp symCoercionTyCon tys', True , and ids)
 872                                         else (ty                            , False, and ids)
 873               ty1'             -> let (ty',_   ,id') = go (mkAppsCoercion ty1' tys)
 874                                   in  (ty',True,id')
 875
 876
 877         goRight :: Coercion -> Coercion -> ( Coercion, Bool, Bool )
 878         --
 879         -- reduces the right constructor, if possible
 880         --
 881         --   takes original coercion term
 882         --                  argument
 883         --
 884         goRight ty ty1
 885           = case mkRightCoercion ty1 of
 886               (TyConApp tc _ ) | tc == rightCoercionTyCon
 887                                -> let (ty1',chan1,id1) = go ty1
 888                                   in  if chan1
 889                                         then (TyConApp rightCoercionTyCon [ty1'], True , id1)
 890                                         else (ty                                , False, id1)
 891               ty1'             -> let (ty',_   ,id') = go ty1'
 892                                   in  (ty',True,id')
 893
 894         goLeft :: Coercion -> Coercion -> ( Coercion, Bool, Bool )
 895         --
 896         -- reduces the left constructor, if possible
 897         --
 898         --   takes original coercion term
 899         --                  argument
 900         --
 901         goLeft ty ty1
 902           = case mkLeftCoercion ty1 of
 903               (TyConApp tc _ ) | tc == leftCoercionTyCon
 904                                -> let (ty1',chan1,id1) = go ty1
 905                                   in  if chan1
 906                                         then (TyConApp leftCoercionTyCon [ty1'], True , id1)
 907                                         else (ty                                , False, id1)
 908               ty1'             -> let (ty',_   ,id') = go ty1'
 909                                   in  (ty',True,id')
 910
 911         goInst :: Coercion -> Coercion -> Coercion -> ( Coercion, Bool, Bool )
 912         --
 913         -- reduces the inst constructor, if possible
 914         --
 915         --   takes original coercion term
 916         --                  coercion argument
 917         --                  type argument
 918         --
 919         goInst ty ty1 ty2
 920           = case mkInstCoercion ty1 ty2 of
 921               (TyConApp tc _ ) | tc == instCoercionTyCon
 922                                -> let (ty1',chan1,id1) = go ty1
 923                                   in  if chan1
 924                                         then (TyConApp instCoercionTyCon [ty1',ty2], True , id1)
 925                                         else (ty                                   , False, id1)
 926               ty1'             -> let (ty',_   ,id') = go ty1'
 927                                   in  (ty',True,id')
 928
 929         goTrans :: Coercion -> Coercion -> Coercion -> ( Coercion, Bool, Bool )
 930         --
 931         --      trans id co     >->     co
 932         --      trans co id     >->     co
 933         --      trans g (sym g) >->     id
 934         --      trans (sym g) g >->     id
 935         --
 936         goTrans ty ty1 ty2
 937           | id1
 938           = (ty2', True, id2)
 939           | id2
 940           = (ty1', True, False)
 941           | chan1 || chan2
 942           = (TyConApp transCoercionTyCon [ty1',ty2'], True , False)
 943           | Just ty' <- mty'
 944           = (ty', True, True)
 945           | otherwise
 946           = (ty, False, False)
 947           where (ty1', chan1, id1) = go ty1
 948                 (ty2', chan2, id2) = go ty2
 949                 mty' = case mkTransCoercion ty1' ty2'
 950                          of (TyConApp tc _) | tc == transCoercionTyCon
 951                                              -> Nothing
 952                             ty'              -> Just ty'
 953 \end{code}