compiler/types/Coercion.lhs

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