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