compiler/types/Coercion.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 \begin{code}
   6 -- The above warning supression flag is a temporary kludge.
   7 -- While working on this module you are encouraged to remove it and fix
   8 -- any warnings in the module. See
   9 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
  10 -- for details
  11
  12 -- | Module for type coercions, as used in System FC. See 'CoreSyn.Expr' for
  13 -- more on System FC and how coercions fit into it.
  14 --
  15 -- Coercions are represented as types, and their kinds tell what types the
  16 -- coercion works on. The coercion kind constructor is a special TyCon that must always be saturated, like so:
  17 --
  18 -- > typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
  19 module Coercion (
  20         -- * Main data type
  21         Coercion,
  22
  23         mkCoKind, mkCoPredTy, coVarKind, coVarKind_maybe,
  24         coercionKind, coercionKinds, isIdentityCoercion,
  25
  26         -- ** Equality predicates
  27         isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
  28
  29         -- ** Coercion transformations
  30         mkCoercion,
  31         mkSymCoercion, mkTransCoercion,
  32         mkLeftCoercion, mkRightCoercion,
  33         mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
  34         mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
  35         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
  36         mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion,
  37
  38         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
  39
  40         unsafeCoercionTyCon, symCoercionTyCon,
  41         transCoercionTyCon, leftCoercionTyCon,
  42         rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
  43         csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon,
  44
  45         -- ** Decomposition
  46         decompLR_maybe, decompCsel_maybe, decompInst_maybe,
  47
  48         -- ** Optimisation
  49         optCoercion,
  50
  51         -- ** Comparison
  52         coreEqCoercion, coreEqCoercion2,
  53
  54         -- * CoercionI
  55         CoercionI(..),
  56         isIdentityCoI,
  57         mkSymCoI, mkTransCoI,
  58         mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
  59         mkForAllTyCoI,
  60         fromCoI, fromACo,
  61         mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
  62
  63        ) where
  64
  65 #include "HsVersions.h"
  66
  67 import TypeRep
  68 import Type
  69 import TyCon
  70 import Class
  71 import Var
  72 import VarEnv
  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 _   [] = 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     kc_sym _ _ _ _ = panic "kc_sym"
 414
 415 transCoercionTyCon
 416   = mkCoercionTyCon transCoercionTyConName 2 kc_trans
 417   where
 418     kc_trans :: CoTyConKindChecker
 419     kc_trans _kc_ty kc_co checking (co1:co2:_)
 420       = do { (a1, r1) <- kc_co co1
 421            ; (a2, r2) <- kc_co co2
 422            ; unless (not checking || (r1 `coreEqType` a2))
 423                     (fail "Trans coercion mis-match")
 424            ; return (a1, r2) }
 425     kc_trans _ _ _ _ = panic "kc_sym"
 426
 427 ---------------------------------------------------
 428 leftCoercionTyCon  = mkCoercionTyCon leftCoercionTyConName  1 (kcLR_help fst)
 429 rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (kcLR_help snd)
 430
 431 kcLR_help :: (forall a. (a,a)->a) -> CoTyConKindChecker
 432 kcLR_help select _kc_ty kc_co _checking (co : _)
 433   = do { (ty1, ty2)  <- kc_co co
 434        ; case decompLR_maybe ty1 ty2 of
 435            Nothing  -> fail "decompLR"
 436            Just res -> return (select res) }
 437 kcLR_help _ _ _ _ _ = panic "kcLR_help"
 438
 439 decompLR_maybe :: Type -> Type -> Maybe ((Type,Type), (Type,Type))
 440 -- Helper for left and right.  Finds coercion kind of its input and
 441 -- returns the left and right projections of the coercion...
 442 --
 443 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 444 decompLR_maybe ty1 ty2
 445   | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 446   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 447   = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 448 decompLR_maybe _ _ = Nothing
 449
 450 ---------------------------------------------------
 451 instCoercionTyCon
 452   =  mkCoercionTyCon instCoercionTyConName 2 kcInst_help
 453   where
 454     kcInst_help :: CoTyConKindChecker
 455     kcInst_help kc_ty kc_co checking (co : ty : _)
 456       = do { (t1,t2) <- kc_co co
 457            ; k <- kc_ty ty
 458            ; case decompInst_maybe t1 t2 of
 459                Nothing -> fail "decompInst"
 460                Just ((tv1,tv2), (ty1,ty2)) -> do
 461            { unless (not checking || (k `isSubKind` tyVarKind tv1))
 462                     (fail "Coercion instantation kind mis-match")
 463            ; return (substTyWith [tv1] [ty] ty1,
 464                      substTyWith [tv2] [ty] ty2) } }
 465     kcInst_help _ _ _ _ = panic "kcInst_help"
 466
 467 decompInst_maybe :: Type -> Type -> Maybe ((TyVar,TyVar), (Type,Type))
 468 decompInst_maybe ty1 ty2
 469   | Just (tv1,r1) <- splitForAllTy_maybe ty1
 470   , Just (tv2,r2) <- splitForAllTy_maybe ty2
 471   = Just ((tv1,tv2), (r1,r2))
 472 decompInst_maybe _ _ = Nothing
 473
 474 ---------------------------------------------------
 475 unsafeCoercionTyCon
 476   = mkCoercionTyCon unsafeCoercionTyConName 2 kc_unsafe
 477   where
 478    kc_unsafe kc_ty _kc_co _checking (ty1:ty2:_)
 479     = do { _ <- kc_ty ty1
 480          ; _ <- kc_ty ty2
 481          ; return (ty1,ty2) }
 482    kc_unsafe _ _ _ _ = panic "kc_unsafe"
 483
 484 ---------------------------------------------------
 485 -- The csel* family
 486
 487 csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 (kcCsel_help fstOf3)
 488 csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 (kcCsel_help sndOf3)
 489 cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (kcCsel_help thirdOf3)
 490
 491 kcCsel_help :: (forall a. (a,a,a) -> a) -> CoTyConKindChecker
 492 kcCsel_help select _kc_ty kc_co _checking (co : _)
 493   = do { (ty1,ty2) <- kc_co co
 494        ; case decompCsel_maybe ty1 ty2 of
 495            Nothing  -> fail "decompCsel"
 496            Just res -> return (select res) }
 497 kcCsel_help _ _ _ _ _ = panic "kcCsel_help"
 498
 499 decompCsel_maybe :: Type -> Type -> Maybe ((Type,Type), (Type,Type), (Type,Type))
 500 --   If         co :: (s1~t1 => r1) ~ (s2~t2 => r2)
 501 -- Then   csel1 co ::            s1 ~ s2
 502 --        csel2 co ::            t1 ~ t2
 503 --        cselR co ::            r1 ~ r2
 504 decompCsel_maybe ty1 ty2
 505   | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
 506   , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
 507   = Just ((s1,s2), (t1,t2), (r1,r2))
 508 decompCsel_maybe _ _ = Nothing
 509
 510 fstOf3   :: (a,b,c) -> a
 511 sndOf3   :: (a,b,c) -> b
 512 thirdOf3 :: (a,b,c) -> c
 513 fstOf3      (a,_,_) =  a
 514 sndOf3      (_,b,_) =  b
 515 thirdOf3    (_,_,c) =  c
 516
 517 --------------------------------------
 518 -- Their Names
 519
 520 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
 521    rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
 522    csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
 523
 524 transCoercionTyConName  = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
 525 symCoercionTyConName    = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
 526 leftCoercionTyConName   = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
 527 rightCoercionTyConName  = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
 528 instCoercionTyConName   = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
 529 csel1CoercionTyConName  = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
 530 csel2CoercionTyConName  = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
 531 cselRCoercionTyConName  = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
 532 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 533
 534 mkCoConName :: FastString -> Unique -> TyCon -> Name
 535 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
 536                             key (ATyCon coCon) BuiltInSyntax
 537 \end{code}
 538
 539
 540 %************************************************************************
 541 %*                                                                      *
 542             Newtypes
 543 %*                                                                      *
 544 %************************************************************************
 545
 546 \begin{code}
 547 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
 548 -- ^ If @co :: T ts ~ rep_ty@ then:
 549 --
 550 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
 551 instNewTyCon_maybe tc tys
 552   | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
 553   = ASSERT( tys `lengthIs` tyConArity tc )
 554     Just (substTyWith tvs tys ty,
 555           case mb_co_tc of
 556            Nothing    -> IdCo
 557            Just co_tc -> ACo (mkTyConApp co_tc tys))
 558   | otherwise
 559   = Nothing
 560
 561 -- this is here to avoid module loops
 562 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 563 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
 564 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
 565 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
 566 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
 567 --
 568 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
 569 --
 570 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
 571 splitNewTypeRepCo_maybe ty
 572   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 573 splitNewTypeRepCo_maybe (TyConApp tc tys)
 574   | Just (ty', coi) <- instNewTyCon_maybe tc tys
 575   = case coi of
 576         ACo co -> Just (ty', co)
 577         IdCo   -> panic "splitNewTypeRepCo_maybe"
 578                         -- This case handled by coreView
 579 splitNewTypeRepCo_maybe _
 580   = Nothing
 581
 582 -- | Determines syntactic equality of coercions
 583 coreEqCoercion :: Coercion -> Coercion -> Bool
 584 coreEqCoercion = coreEqType
 585
 586 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
 587 coreEqCoercion2 = coreEqType2
 588 \end{code}
 589
 590
 591 %************************************************************************
 592 %*                                                                      *
 593             CoercionI and its constructors
 594 %*                                                                      *
 595 %************************************************************************
 596
 597 --------------------------------------
 598 -- CoercionI smart constructors
 599 --      lifted smart constructors of ordinary coercions
 600
 601 \begin{code}
 602 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
 603 -- can represent either one of:
 604 --
 605 -- 1. A proper 'Coercion'
 606 --
 607 -- 2. The identity coercion
 608 data CoercionI = IdCo | ACo Coercion
 609
 610 instance Outputable CoercionI where
 611   ppr IdCo     = ptext (sLit "IdCo")
 612   ppr (ACo co) = ppr co
 613
 614 isIdentityCoI :: CoercionI -> Bool
 615 isIdentityCoI IdCo = True
 616 isIdentityCoI _    = False
 617
 618 -- | Tests whether all the given 'CoercionI's represent the identity coercion
 619 allIdCoIs :: [CoercionI] -> Bool
 620 allIdCoIs = all isIdentityCoI
 621
 622 -- | For each 'CoercionI' in the input list, return either the 'Coercion' it
 623 -- contains or the corresponding 'Type' from the other list
 624 zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
 625 zipCoArgs cois tys = zipWith fromCoI cois tys
 626
 627 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
 628 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
 629 fromCoI :: CoercionI -> Type -> Type
 630 fromCoI IdCo ty     = ty        -- Identity coercion represented
 631 fromCoI (ACo co) _  = co        --      by the type itself
 632
 633 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
 634 mkSymCoI :: CoercionI -> CoercionI
 635 mkSymCoI IdCo = IdCo
 636 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
 637                                 -- the smart constructor
 638                                 -- is too smart with tyvars
 639
 640 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
 641 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
 642 mkTransCoI IdCo aco = aco
 643 mkTransCoI aco IdCo = aco
 644 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
 645
 646 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
 647 mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
 648 mkTyConAppCoI tyCon tys cois
 649   | allIdCoIs cois = IdCo
 650   | otherwise      = ACo (TyConApp tyCon (zipCoArgs cois tys))
 651
 652 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
 653 mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 654 mkAppTyCoI _   IdCo _   IdCo = IdCo
 655 mkAppTyCoI ty1 coi1 ty2 coi2 =
 656         ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 657
 658
 659 mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 660 mkFunTyCoI _   IdCo _   IdCo = IdCo
 661 mkFunTyCoI ty1 coi1 ty2 coi2 =
 662         ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 663
 664 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
 665 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
 666 mkForAllTyCoI _ IdCo = IdCo
 667 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
 668
 669 -- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
 670 -- panic
 671 fromACo :: CoercionI -> Coercion
 672 fromACo (ACo co)  = co
 673 fromACo (IdCo {}) = panic "fromACo"
 674
 675 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
 676 --
 677 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
 678 mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
 679 mkClassPPredCoI cls tys cois
 680   | allIdCoIs cois = IdCo
 681   | otherwise      = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
 682
 683 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 684 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
 685 mkIParamPredCoI _   IdCo     = IdCo
 686 mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
 687
 688 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 689 mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 690 mkEqPredCoI _    IdCo     _   IdCo      = IdCo
 691 mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
 692 mkEqPredCoI _   (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
 693 \end{code}
 694
 695 %************************************************************************
 696 %*                                                                      *
 697                  Optimising coercions
 698 %*                                                                      *
 699 %************************************************************************
 700
 701 \begin{code}
 702 type NormalCo = Coercion
 703   -- Invariants:
 704   --  * For trans coercions (co1 `trans` co2)
 705   --       co1 is not a trans, and neither co1 nor co2 is identity
 706   --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
 707
 708 type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity
 709
 710 optCoercion :: Coercion -> NormalCo
 711 optCoercion co = opt_co False co
 712
 713 opt_co :: Bool         -- True <=> return (sym co)
 714        -> Coercion
 715        -> NormalCo
 716 opt_co = opt_co'
 717 -- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $
 718 --                      co1 `seq`
 719 --                pprTrace "opt_co done }" (ppr co1)
 720 --               WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (s1,t1)
 721 --                                     $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )
 722 --                co1
 723 --  where
 724 --    co1 = opt_co' sym co
 725 --    same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2
 726 --    (s,t) = coercionKind co
 727 --    (s1,t1) | sym = (t,s)
 728 --            | otherwise = (s,t)
 729 --    (s2,t2) = coercionKind co1
 730
 731 opt_co' sym (AppTy ty1 ty2)           = mkAppTy (opt_co sym ty1) (opt_co sym ty2)
 732 opt_co' sym (FunTy ty1 ty2)           = FunTy (opt_co sym ty1) (opt_co sym ty2)
 733 opt_co' sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co sym) tys))
 734 opt_co' sym (PredTy (IParam n ty))    = PredTy (IParam n (opt_co sym ty))
 735
 736 opt_co' sym co@(TyVarTy tv)
 737   | not (isCoVar tv)     = co   -- Identity; does not mention a CoVar
 738   | ty1 `coreEqType` ty2 = ty1  -- Identity; ..ditto..
 739   | not sym              = co
 740   | otherwise            = mkSymCoercion co
 741   where
 742     (ty1,ty2) = coVarKind tv
 743
 744 opt_co' sym (ForAllTy tv cor)
 745   | isCoVar tv = mkCoPredTy (opt_co sym co1) (opt_co sym co2) (opt_co sym cor)
 746   | otherwise  = ForAllTy tv (opt_co sym cor)
 747   where
 748     (co1,co2) = coVarKind tv
 749
 750 opt_co' sym (TyConApp tc cos)
 751   | isCoercionTyCon tc
 752   = foldl mkAppTy opt_co_tc
 753           (map (opt_co sym) (drop arity cos))
 754   | otherwise
 755   = TyConApp tc (map (opt_co sym) cos)
 756   where
 757     arity = tyConArity tc
 758     opt_co_tc :: NormalCo
 759     opt_co_tc = opt_co_tc_app sym tc (take arity cos)
 760
 761 --------
 762 opt_co_tc_app :: Bool -> TyCon -> [Type] -> NormalCo
 763 -- Used for CoercionTyCons only
 764 opt_co_tc_app sym tc cos
 765   | tc `hasKey` symCoercionTyConKey
 766   = opt_co (not sym) co1
 767
 768   | tc `hasKey` transCoercionTyConKey
 769   = if sym then opt_trans opt_co2 opt_co1
 770            else opt_trans opt_co1 opt_co2
 771
 772   | tc `hasKey` leftCoercionTyConKey
 773   , Just (co1, _) <- splitAppTy_maybe opt_co1
 774   = co1
 775
 776   | tc `hasKey` rightCoercionTyConKey
 777   , Just (_, co2) <- splitAppTy_maybe opt_co1
 778   = co2
 779
 780   | tc `hasKey` csel1CoercionTyConKey
 781   , Just (s1,_,_) <- splitCoPredTy_maybe opt_co1
 782   = s1
 783
 784   | tc `hasKey` csel2CoercionTyConKey
 785   , Just (_,s2,_) <- splitCoPredTy_maybe opt_co1
 786   = s2
 787
 788   | tc `hasKey` cselRCoercionTyConKey
 789   , Just (_,_,r) <- splitCoPredTy_maybe opt_co1
 790   = r
 791
 792   | tc `hasKey` instCoercionTyConKey
 793   , Just (tv, co'') <- splitForAllTy_maybe opt_co1
 794   , let ty = co2
 795   = substTyWith [tv] [ty] co''
 796
 797   | otherwise     -- Do not push sym inside top-level axioms
 798                   -- e.g. if g is a top-level axiom
 799                   --   g a : F a ~ a
 800                   -- Then (sym (g ty)) /= g (sym ty) !!
 801   = if sym then mkSymCoercion the_co
 802            else the_co
 803   where
 804     the_co = TyConApp tc cos
 805     (co1 : cos1) = cos
 806     (co2 : _)    = cos1
 807     opt_co1 = opt_co sym co1
 808     opt_co2 = opt_co sym co2
 809
 810 -------------
 811 opt_trans :: NormalCo -> NormalCo -> NormalCo
 812 opt_trans co1 co2
 813   | isIdNormCo co1 = co2
 814   | otherwise      = opt_trans1 co1 co2
 815
 816 opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
 817 -- First arg is not the identity
 818 opt_trans1 co1 co2
 819   | isIdNormCo co2 = co1
 820   | otherwise      = opt_trans2 co1 co2
 821
 822 opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
 823 -- Neither arg is the identity
 824 opt_trans2 (TyConApp tc [co1a,co1b]) co2
 825   | tc `hasKey` transCoercionTyConKey
 826   = opt_trans1 co1a (opt_trans2 co1b co2)
 827
 828 opt_trans2 co1 co2
 829   | Just co <- opt_trans_rule co1 co2
 830   = co
 831
 832 opt_trans2 co1 (TyConApp tc [co2a,co2b])
 833   | tc `hasKey` transCoercionTyConKey
 834   , Just co1_2a <- opt_trans_rule co1 co2a
 835   = if isIdNormCo co1_2a
 836     then co2b
 837     else opt_trans2 co1_2a co2b
 838
 839 opt_trans2 co1 co2
 840   = mkTransCoercion co1 co2
 841
 842 ------
 843 opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
 844 opt_trans_rule (TyConApp tc [co1]) co2
 845   | tc `hasKey` symCoercionTyConKey
 846   , co1 `coreEqType` co2
 847   , (_,ty2) <- coercionKind co2
 848   = Just ty2
 849
 850 opt_trans_rule co1 (TyConApp tc [co2])
 851   | tc `hasKey` symCoercionTyConKey
 852   , co1 `coreEqType` co2
 853   , (ty1,_) <- coercionKind co1
 854   = Just ty1
 855
 856 opt_trans_rule (TyConApp tc1 [co1,ty1]) (TyConApp tc2 [co2,ty2])
 857   | tc1 `hasKey` instCoercionTyConKey
 858   , tc1 == tc2
 859   , ty1 `coreEqType` ty2
 860   = Just (mkInstCoercion (opt_trans2 co1 co2) ty1)
 861
 862 opt_trans_rule (TyConApp tc1 cos1) (TyConApp tc2 cos2)
 863   | not (isCoercionTyCon tc1) ||
 864     getUnique tc1 `elem` [ leftCoercionTyConKey, rightCoercionTyConKey
 865                          , csel1CoercionTyConKey, csel2CoercionTyConKey
 866                          , cselRCoercionTyConKey ]      --Yuk!
 867   , tc1 == tc2           -- Works for left,right, and csel* family
 868                          -- BUT NOT equality axioms
 869                          -- E.g.        (g Int) `trans` (g Bool)
 870                          --        /= g (Int . Bool)
 871   = Just (TyConApp tc1 (zipWith opt_trans cos1 cos2))
 872
 873 opt_trans_rule co1 co2
 874   | Just (co1a, co1b) <- splitAppTy_maybe co1
 875   , Just (co2a, co2b) <- splitAppTy_maybe co2
 876   = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))
 877
 878   | Just (s1,t1,r1) <- splitCoPredTy_maybe co1
 879   , Just (s2,t2,r2) <- splitCoPredTy_maybe co1
 880   = Just (mkCoPredTy (opt_trans s1 s2)
 881                      (opt_trans t1 t2)
 882                      (opt_trans r1 r2))
 883
 884   | Just (tv1,r1) <- splitForAllTy_maybe co1
 885   , Just (tv2,r2) <- splitForAllTy_maybe co2
 886   , not (isCoVar tv1)                -- Both have same kind
 887   , let r2' = substTyWith [tv2] [TyVarTy tv1] r2
 888   = Just (ForAllTy tv1 (opt_trans2 r1 r2'))
 889
 890 opt_trans_rule _ _ = Nothing
 891
 892
 893 -------------
 894 isIdNormCo :: NormalCo -> Bool
 895 -- Cheap identity test: look for coercions with no coercion variables at all
 896 -- So it'll return False for (sym g `trans` g)
 897 isIdNormCo ty = go ty
 898   where
 899     go (TyVarTy tv)            = not (isCoVar tv)
 900     go (AppTy t1 t2)           = go t1 && go t2
 901     go (FunTy t1 t2)           = go t1 && go t2
 902     go (ForAllTy tv ty)        = go (tyVarKind tv) && go ty
 903     go (TyConApp tc tys)       = not (isCoercionTyCon tc) && all go tys
 904     go (PredTy (IParam _ ty))  = go ty
 905     go (PredTy (ClassP _ tys)) = all go tys
 906     go (PredTy (EqPred t1 t2)) = go t1 && go t2
 907 \end{code}