compiler/types/Coercion.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 \begin{code}
   6 -- | Module for (a) type kinds and (b) type coercions,
   7 -- as used in System FC. See 'CoreSyn.Expr' for
   8 -- more on System FC and how coercions fit into it.
   9 --
  10 -- Coercions are represented as types, and their kinds tell what types the
  11 -- coercion works on. The coercion kind constructor is a special TyCon that
  12 -- must always be saturated, like so:
  13 --
  14 -- > typeKind (symCoercion type) :: TyConApp CoTyCon{...} [type, type]
  15 module Coercion (
  16         -- * Main data type
  17         Coercion, Kind,
  18         typeKind,
  19
  20         -- ** Deconstructing Kinds
  21         kindFunResult, kindAppResult, synTyConResKind,
  22         splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
  23
  24         -- ** Predicates on Kinds
  25         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
  26         isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
  27         isCoSuperKind, isSuperKind, isCoercionKind,
  28         mkArrowKind, mkArrowKinds,
  29
  30         isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
  31         isSubKindCon,
  32
  33         mkCoKind, mkCoPredTy, coVarKind, coVarKind_maybe,
  34         coercionKind, coercionKinds, isIdentityCoercion,
  35
  36         -- ** Equality predicates
  37         isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
  38
  39         -- ** Coercion transformations
  40         mkCoercion,
  41         mkSymCoercion, mkTransCoercion,
  42         mkLeftCoercion, mkRightCoercion,
  43         mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
  44         mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
  45         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
  46         mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion,
  47
  48         mkCoVarCoercion,
  49
  50
  51         unsafeCoercionTyCon, symCoercionTyCon,
  52         transCoercionTyCon, leftCoercionTyCon,
  53         rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
  54         csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon,
  55
  56         -- ** Decomposition
  57         decompLR_maybe, decompCsel_maybe, decompInst_maybe,
  58         splitCoPredTy_maybe,
  59         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
  60
  61         -- ** Comparison
  62         coreEqCoercion, coreEqCoercion2,
  63
  64         -- * CoercionI
  65         CoercionI(..),
  66         isIdentityCoI,
  67         mkSymCoI, mkTransCoI,
  68         mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
  69         mkForAllTyCoI,
  70         fromCoI,
  71         mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
  72
  73        ) where
  74
  75 #include "HsVersions.h"
  76
  77 import TypeRep
  78 import Type
  79 import TyCon
  80 import Class
  81 import Var
  82 import VarEnv
  83 import Name
  84 import PrelNames
  85 import Util
  86 import BasicTypes
  87 import Outputable
  88 import FastString
  89 \end{code}
  90
  91 %************************************************************************
  92 %*                                                                      *
  93         Functions over Kinds
  94 %*                                                                      *
  95 %************************************************************************
  96
  97 \begin{code}
  98 -- | Essentially 'funResultTy' on kinds
  99 kindFunResult :: Kind -> Kind
 100 kindFunResult k = funResultTy k
 101
 102 kindAppResult :: Kind -> [arg] -> Kind
 103 kindAppResult k []     = k
 104 kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
 105
 106 -- | Essentially 'splitFunTys' on kinds
 107 splitKindFunTys :: Kind -> ([Kind],Kind)
 108 splitKindFunTys k = splitFunTys k
 109
 110 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
 111 splitKindFunTy_maybe = splitFunTy_maybe
 112
 113 -- | Essentially 'splitFunTysN' on kinds
 114 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
 115 splitKindFunTysN k = splitFunTysN k
 116
 117 -- | Find the result 'Kind' of a type synonym,
 118 -- after applying it to its 'arity' number of type variables
 119 -- Actually this function works fine on data types too,
 120 -- but they'd always return '*', so we never need to ask
 121 synTyConResKind :: TyCon -> Kind
 122 synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
 123
 124 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
 125 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
 126 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
 127         isUnliftedTypeKindCon, isSubArgTypeKindCon      :: TyCon -> Bool
 128
 129 isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
 130
 131 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
 132 isOpenTypeKind _               = False
 133
 134 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
 135
 136 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
 137 isUbxTupleKind _               = False
 138
 139 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
 140
 141 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
 142 isArgTypeKind _               = False
 143
 144 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
 145
 146 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
 147 isUnliftedTypeKind _               = False
 148
 149 isSubOpenTypeKind :: Kind -> Bool
 150 -- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
 151 isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
 152                                      ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
 153                                      False
 154 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
 155 isSubOpenTypeKind other            = ASSERT( isKind other ) False
 156          -- This is a conservative answer
 157          -- It matters in the call to isSubKind in
 158          -- checkExpectedKind.
 159
 160 isSubArgTypeKindCon kc
 161   | isUnliftedTypeKindCon kc = True
 162   | isLiftedTypeKindCon kc   = True
 163   | isArgTypeKindCon kc      = True
 164   | otherwise                = False
 165
 166 isSubArgTypeKind :: Kind -> Bool
 167 -- ^ True of any sub-kind of ArgTypeKind
 168 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
 169 isSubArgTypeKind _                = False
 170
 171 -- | Is this a super-kind (i.e. a type-of-kinds)?
 172 isSuperKind :: Type -> Bool
 173 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
 174 isSuperKind _                   = False
 175
 176 -- | Is this a kind (i.e. a type-of-types)?
 177 isKind :: Kind -> Bool
 178 isKind k = isSuperKind (typeKind k)
 179
 180 isSubKind :: Kind -> Kind -> Bool
 181 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
 182 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
 183 isSubKind (FunTy a1 r1) (FunTy a2 r2)         = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
 184 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
 185   = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
 186 isSubKind _             _                     = False
 187
 188 eqKind :: Kind -> Kind -> Bool
 189 eqKind = tcEqType
 190
 191 isSubKindCon :: TyCon -> TyCon -> Bool
 192 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
 193 isSubKindCon kc1 kc2
 194   | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
 195   | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
 196   | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
 197   | isOpenTypeKindCon kc2                                  = True
 198                            -- we already know kc1 is not a fun, its a TyCon
 199   | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
 200   | otherwise                                              = False
 201
 202 defaultKind :: Kind -> Kind
 203 -- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
 204 -- information on what that means
 205
 206 -- When we generalise, we make generic type variables whose kind is
 207 -- simple (* or *->* etc).  So generic type variables (other than
 208 -- built-in constants like 'error') always have simple kinds.  This is important;
 209 -- consider
 210 --      f x = True
 211 -- We want f to get type
 212 --      f :: forall (a::*). a -> Bool
 213 -- Not
 214 --      f :: forall (a::??). a -> Bool
 215 -- because that would allow a call like (f 3#) as well as (f True),
 216 --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
 217 defaultKind k
 218   | isSubOpenTypeKind k = liftedTypeKind
 219   | isSubArgTypeKind k  = liftedTypeKind
 220   | otherwise        = k
 221 \end{code}
 222
 223 %************************************************************************
 224 %*                                                                      *
 225             Coercions
 226 %*                                                                      *
 227 %************************************************************************
 228
 229
 230 \begin{code}
 231 -- | A 'Coercion' represents a 'Type' something should be coerced to.
 232 type Coercion     = Type
 233
 234 -- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
 235 -- types that a 'Coercion' will work on.
 236 type CoercionKind = Kind
 237
 238 ------------------------------
 239
 240 -- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
 241 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
 242 --
 243 -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
 244 decomposeCo :: Arity -> Coercion -> [Coercion]
 245 decomposeCo n co
 246   = go n co []
 247   where
 248     go 0 _  cos = cos
 249     go n co cos = go (n-1) (mkLeftCoercion co)
 250                            (mkRightCoercion co : cos)
 251
 252
 253 -------------------------------------------------------
 254 -- and some coercion kind stuff
 255
 256 coVarKind :: CoVar -> (Type,Type)
 257 -- c :: t1 ~ t2
 258 coVarKind cv = case coVarKind_maybe cv of
 259                  Just ts -> ts
 260                  Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv))
 261
 262 coVarKind_maybe :: CoVar -> Maybe (Type,Type)
 263 coVarKind_maybe cv = splitCoKind_maybe (tyVarKind cv)
 264
 265 -- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
 266 -- Panics if the argument is not a valid 'CoercionKind'
 267 splitCoKind_maybe :: Kind -> Maybe (Type, Type)
 268 splitCoKind_maybe co | Just co' <- kindView co = splitCoKind_maybe co'
 269 splitCoKind_maybe (PredTy (EqPred ty1 ty2))    = Just (ty1, ty2)
 270 splitCoKind_maybe _                            = Nothing
 271
 272 -- | Makes a 'CoercionKind' from two types: the types whose equality
 273 -- is proven by the relevant 'Coercion'
 274 mkCoKind :: Type -> Type -> CoercionKind
 275 mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
 276
 277 -- | (mkCoPredTy s t r) produces the type:   (s~t) => r
 278 mkCoPredTy :: Type -> Type -> Type -> Type
 279 mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r
 280
 281 splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
 282 splitCoPredTy_maybe ty
 283   | Just (cv,r) <- splitForAllTy_maybe ty
 284   , isCoVar cv
 285   , Just (s,t) <- coVarKind_maybe cv
 286   = Just (s,t,r)
 287   | otherwise
 288   = Nothing
 289
 290 -- | Tests whether a type is just a type equality predicate
 291 isEqPredTy :: Type -> Bool
 292 isEqPredTy (PredTy pred) = isEqPred pred
 293 isEqPredTy _             = False
 294
 295 -- | Creates a type equality predicate
 296 mkEqPred :: (Type, Type) -> PredType
 297 mkEqPred (ty1, ty2) = EqPred ty1 ty2
 298
 299 -- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
 300 -- Panics otherwise
 301 getEqPredTys :: PredType -> (Type,Type)
 302 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
 303 getEqPredTys other            = pprPanic "getEqPredTys" (ppr other)
 304
 305 isIdentityCoercion :: Coercion -> Bool
 306 isIdentityCoercion co
 307   = case coercionKind co of
 308        (t1,t2) -> t1 `coreEqType` t2
 309 \end{code}
 310
 311 %************************************************************************
 312 %*                                                                      *
 313             Building coercions
 314 %*                                                                      *
 315 %************************************************************************
 316
 317 Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args)
 318
 319 \begin{code}
 320 -- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
 321 -- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
 322 -- if possible
 323 mkCoercion :: TyCon -> [Type] -> Coercion
 324 mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
 325                         TyConApp coCon args
 326
 327 mkCoVarCoercion :: CoVar -> Coercion
 328 mkCoVarCoercion cv = mkTyVarTy cv
 329
 330 -- | Apply a 'Coercion' to another 'Coercion', which is presumably a
 331 -- 'Coercion' constructor of some kind
 332 mkAppCoercion :: Coercion -> Coercion -> Coercion
 333 mkAppCoercion co1 co2 = mkAppTy co1 co2
 334
 335 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
 336 -- See also 'mkAppCoercion'
 337 mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
 338 mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
 339
 340 -- | Apply a type constructor to a list of coercions.
 341 mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
 342 mkTyConCoercion con cos = mkTyConApp con cos
 343
 344 -- | Make a function 'Coercion' between two other 'Coercion's
 345 mkFunCoercion :: Coercion -> Coercion -> Coercion
 346 mkFunCoercion co1 co2 = mkFunTy co1 co2
 347
 348 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
 349 mkForAllCoercion :: Var -> Coercion -> Coercion
 350 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
 351 mkForAllCoercion tv  co  = ASSERT ( isTyCoVar tv ) mkForAllTy tv co
 352
 353
 354 -------------------------------
 355
 356 mkSymCoercion :: Coercion -> Coercion
 357 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality
 358 -- between the same types but in the other "direction", so a kind of @t1 ~ t2@
 359 -- becomes the kind @t2 ~ t1@.
 360 mkSymCoercion g = mkCoercion symCoercionTyCon [g]
 361
 362 mkTransCoercion :: Coercion -> Coercion -> Coercion
 363 -- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
 364 mkTransCoercion g1 g2 = mkCoercion transCoercionTyCon [g1, g2]
 365
 366 mkLeftCoercion :: Coercion -> Coercion
 367 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
 368 -- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
 369 --
 370 -- > mkLeftCoercion c :: f ~ g
 371 mkLeftCoercion co = mkCoercion leftCoercionTyCon [co]
 372
 373 mkRightCoercion :: Coercion -> Coercion
 374 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
 375 -- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
 376 --
 377 -- > mkLeftCoercion c :: x ~ y
 378 mkRightCoercion co = mkCoercion rightCoercionTyCon [co]
 379
 380 mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
 381 mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
 382 mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
 383 mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co]
 384
 385 -------------------------------
 386 mkInstCoercion :: Coercion -> Type -> Coercion
 387 -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
 388 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
 389 mkInstCoercion co ty = mkCoercion instCoercionTyCon  [co, ty]
 390
 391 mkInstsCoercion :: Coercion -> [Type] -> Coercion
 392 -- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right
 393 mkInstsCoercion co tys = foldl mkInstCoercion co tys
 394
 395 -- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
 396 -- but it is used when we know we are dealing with bottom, which is one case in which
 397 -- it is safe.  This is also used implement the @unsafeCoerce#@ primitive.
 398 -- Optimise by pushing down through type constructors
 399 mkUnsafeCoercion :: Type -> Type -> Coercion
 400 mkUnsafeCoercion (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 401   | tc1 == tc2
 402   = TyConApp tc1 (zipWith mkUnsafeCoercion tys1 tys2)
 403
 404 mkUnsafeCoercion (FunTy a1 r1) (FunTy a2 r2)
 405   = FunTy (mkUnsafeCoercion a1 a2) (mkUnsafeCoercion r1 r2)
 406
 407 mkUnsafeCoercion ty1 ty2
 408   | ty1 `coreEqType` ty2 = ty1
 409   | otherwise            = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 410
 411 -- See note [Newtype coercions] in TyCon
 412
 413 -- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a
 414 -- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the
 415 -- type the appropriate right hand side of the @newtype@, with the free variables
 416 -- a subset of those 'TyVar's.
 417 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 418 mkNewTypeCoercion name tycon tvs rhs_ty
 419   = mkCoercionTyCon name arity desc
 420   where
 421     arity = length tvs
 422     desc = CoAxiom { co_ax_tvs = tvs
 423                    , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs)
 424                    , co_ax_rhs = rhs_ty }
 425
 426 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
 427 -- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
 428 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
 429 -- representation tycon.
 430 mkFamInstCoercion :: Name       -- ^ Unique name for the coercion tycon
 431                   -> [TyVar]    -- ^ Type parameters of the coercion (@tvs@)
 432                   -> TyCon      -- ^ Family tycon (@F@)
 433                   -> [Type]     -- ^ Type instance (@ts@)
 434                   -> TyCon      -- ^ Representation tycon (@R@)
 435                   -> TyCon      -- ^ Coercion tycon (@Co@)
 436 mkFamInstCoercion name tvs family inst_tys rep_tycon
 437   = mkCoercionTyCon name arity desc
 438   where
 439     arity = length tvs
 440     desc = CoAxiom { co_ax_tvs = tvs
 441                    , co_ax_lhs = mkTyConApp family inst_tys
 442                    , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
 443 \end{code}
 444
 445
 446 %************************************************************************
 447 %*                                                                      *
 448             Coercion Type Constructors
 449 %*                                                                      *
 450 %************************************************************************
 451
 452 Example.  The coercion ((sym c) (sym d) (sym e))
 453 will be represented by (TyConApp sym [c, sym d, sym e])
 454 If sym c :: p1=q1
 455    sym d :: p2=q2
 456    sym e :: p3=q3
 457 then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 458
 459 \begin{code}
 460 -- | Coercion type constructors: avoid using these directly and instead use
 461 -- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
 462 --
 463 -- Each coercion TyCon is built with the special CoercionTyCon record and
 464 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 465 -- by any TyConApp in which they are applied, however they may also be over
 466 -- applied (see example above) and the kinding function must deal with this.
 467 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon,
 468   rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
 469   csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
 470
 471 symCoercionTyCon    = mkCoercionTyCon symCoercionTyConName   1 CoSym
 472 transCoercionTyCon  = mkCoercionTyCon transCoercionTyConName 2 CoTrans
 473 leftCoercionTyCon   = mkCoercionTyCon leftCoercionTyConName  1 CoLeft
 474 rightCoercionTyCon  = mkCoercionTyCon rightCoercionTyConName 1 CoRight
 475 instCoercionTyCon   =  mkCoercionTyCon instCoercionTyConName 2 CoInst
 476 csel1CoercionTyCon  = mkCoercionTyCon csel1CoercionTyConName 1 CoCsel1
 477 csel2CoercionTyCon  = mkCoercionTyCon csel2CoercionTyConName 1 CoCsel2
 478 cselRCoercionTyCon  = mkCoercionTyCon cselRCoercionTyConName 1 CoCselR
 479 unsafeCoercionTyCon = mkCoercionTyCon unsafeCoercionTyConName 2 CoUnsafe
 480
 481 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
 482    rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
 483    csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
 484
 485 transCoercionTyConName  = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
 486 symCoercionTyConName    = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
 487 leftCoercionTyConName   = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
 488 rightCoercionTyConName  = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
 489 instCoercionTyConName   = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
 490 csel1CoercionTyConName  = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
 491 csel2CoercionTyConName  = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
 492 cselRCoercionTyConName  = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
 493 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 494
 495 mkCoConName :: FastString -> Unique -> TyCon -> Name
 496 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
 497                             key (ATyCon coCon) BuiltInSyntax
 498 \end{code}
 499
 500 \begin{code}
 501 ------------
 502 decompLR_maybe :: (Type,Type) -> Maybe ((Type,Type), (Type,Type))
 503 -- Helper for left and right.  Finds coercion kind of its input and
 504 -- returns the left and right projections of the coercion...
 505 --
 506 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 507 decompLR_maybe (ty1,ty2)
 508   | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 509   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 510   = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 511 decompLR_maybe _ = Nothing
 512
 513 ------------
 514 decompInst_maybe :: (Type, Type) -> Maybe ((TyVar,TyVar), (Type,Type))
 515 decompInst_maybe (ty1, ty2)
 516   | Just (tv1,r1) <- splitForAllTy_maybe ty1
 517   , Just (tv2,r2) <- splitForAllTy_maybe ty2
 518   = Just ((tv1,tv2), (r1,r2))
 519 decompInst_maybe _ = Nothing
 520
 521 ------------
 522 decompCsel_maybe :: (Type, Type) -> Maybe ((Type,Type), (Type,Type), (Type,Type))
 523 --   If         co :: (s1~t1 => r1) ~ (s2~t2 => r2)
 524 -- Then   csel1 co ::            s1 ~ s2
 525 --        csel2 co ::            t1 ~ t2
 526 --        cselR co ::            r1 ~ r2
 527 decompCsel_maybe (ty1, ty2)
 528   | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
 529   , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
 530   = Just ((s1,s2), (t1,t2), (r1,r2))
 531 decompCsel_maybe _ = Nothing
 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 (mkTyConApp tc    tys)
 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 Type | ACo Coercion
 604
 605 liftCoI :: (Type -> Type) -> CoercionI -> CoercionI
 606 liftCoI f (IdCo ty) = IdCo (f ty)
 607 liftCoI f (ACo ty)  = ACo (f ty)
 608
 609 liftCoI2 :: (Type -> Type -> Type) -> CoercionI -> CoercionI -> CoercionI
 610 liftCoI2 f (IdCo ty1) (IdCo ty2) = IdCo (f ty1 ty2)
 611 liftCoI2 f coi1       coi2       = ACo (f (fromCoI coi1) (fromCoI coi2))
 612
 613 liftCoIs :: ([Type] -> Type) -> [CoercionI] -> CoercionI
 614 liftCoIs f cois = go_id [] cois
 615   where
 616     go_id rev_tys []               = IdCo (f (reverse rev_tys))
 617     go_id rev_tys (IdCo ty : cois) = go_id  (ty:rev_tys) cois
 618     go_id rev_tys (ACo  co : cois) = go_aco (co:rev_tys) cois
 619
 620     go_aco rev_tys []               = ACo (f (reverse rev_tys))
 621     go_aco rev_tys (IdCo ty : cois) = go_aco (ty:rev_tys) cois
 622     go_aco rev_tys (ACo  co : cois) = go_aco (co:rev_tys) cois
 623
 624 instance Outputable CoercionI where
 625   ppr (IdCo _) = ptext (sLit "IdCo")
 626   ppr (ACo co) = ppr co
 627
 628 isIdentityCoI :: CoercionI -> Bool
 629 isIdentityCoI (IdCo _) = True
 630 isIdentityCoI (ACo _)  = False
 631
 632 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
 633 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
 634 fromCoI :: CoercionI -> Type
 635 fromCoI (IdCo ty) = ty  -- Identity coercion represented
 636 fromCoI (ACo co)  = co  --      by the type itself
 637
 638 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
 639 mkSymCoI :: CoercionI -> CoercionI
 640 mkSymCoI (IdCo ty) = IdCo ty
 641 mkSymCoI (ACo co)  = ACo $ mkCoercion symCoercionTyCon [co]
 642                                 -- the smart constructor
 643                                 -- is too smart with tyvars
 644
 645 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
 646 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
 647 mkTransCoI (IdCo _) aco = aco
 648 mkTransCoI aco (IdCo _) = aco
 649 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
 650
 651 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
 652 mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI
 653 mkTyConAppCoI tyCon cois = liftCoIs (mkTyConApp tyCon) cois
 654
 655 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
 656 mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI
 657 mkAppTyCoI = liftCoI2 mkAppTy
 658
 659 mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI
 660 mkFunTyCoI = liftCoI2 mkFunTy
 661
 662 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
 663 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
 664 mkForAllTyCoI tv = liftCoI (ForAllTy tv)
 665
 666 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
 667 --
 668 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
 669 mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI
 670 mkClassPPredCoI cls = liftCoIs (PredTy . ClassP cls)
 671
 672 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 673 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
 674 mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn)
 675
 676 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 677 mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
 678 mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
 679 \end{code}
 680
 681 %************************************************************************
 682 %*                                                                      *
 683              The kind of a type, and of a coercion
 684 %*                                                                      *
 685 %************************************************************************
 686
 687 \begin{code}
 688 typeKind :: Type -> Kind
 689 typeKind ty@(TyConApp tc tys)
 690   | isCoercionTyCon tc = typeKind (fst (coercionKind ty))
 691   | otherwise          = kindAppResult (tyConKind tc) tys
 692         -- During coercion optimisation we *do* match a type
 693         -- against a coercion (see OptCoercion.matchesAxiomLhs)
 694         -- So the use of typeKind in Unify.match_kind must work on coercions too
 695         -- Hence the isCoercionTyCon case above
 696
 697 typeKind (PredTy pred)        = predKind pred
 698 typeKind (AppTy fun _)        = kindFunResult (typeKind fun)
 699 typeKind (ForAllTy _ ty)      = typeKind ty
 700 typeKind (TyVarTy tyvar)      = tyVarKind tyvar
 701 typeKind (FunTy _arg res)
 702     -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*),
 703     --              not unliftedTypKind (#)
 704     -- The only things that can be after a function arrow are
 705     --   (a) types (of kind openTypeKind or its sub-kinds)
 706     --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
 707     | isTySuperKind k         = k
 708     | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind
 709     where
 710       k = typeKind res
 711
 712 ------------------
 713 predKind :: PredType -> Kind
 714 predKind (EqPred {}) = coSuperKind      -- A coercion kind!
 715 predKind (ClassP {}) = liftedTypeKind   -- Class and implicitPredicates are
 716 predKind (IParam {}) = liftedTypeKind   -- always represented by lifted types
 717
 718 ------------------
 719 -- | If it is the case that
 720 --
 721 -- > c :: (t1 ~ t2)
 722 --
 723 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
 724 coercionKind :: Coercion -> (Type, Type)
 725 coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
 726                             | otherwise = (ty, ty)
 727 coercionKind (AppTy ty1 ty2)
 728   = let (s1, t1) = coercionKind ty1
 729         (s2, t2) = coercionKind ty2 in
 730     (mkAppTy s1 s2, mkAppTy t1 t2)
 731 coercionKind co@(TyConApp tc args)
 732   | Just (ar, desc) <- isCoercionTyCon_maybe tc
 733     -- CoercionTyCons carry their kinding rule, so we use it here
 734   = WARN( not (length args >= ar), ppr co )     -- Always saturated
 735     (let (ty1,  ty2)  = coTyConAppKind desc (take ar args)
 736          (tys1, tys2) = coercionKinds (drop ar args)
 737      in (mkAppTys ty1 tys1, mkAppTys ty2 tys2))
 738
 739   | otherwise
 740   = let (lArgs, rArgs) = coercionKinds args in
 741     (TyConApp tc lArgs, TyConApp tc rArgs)
 742
 743 coercionKind (FunTy ty1 ty2)
 744   = let (t1, t2) = coercionKind ty1
 745         (s1, s2) = coercionKind ty2 in
 746     (mkFunTy t1 s1, mkFunTy t2 s2)
 747
 748 coercionKind (ForAllTy tv ty)
 749   | isCoVar tv
 750 --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
 751 --    ----------------------------------------------
 752 --    c1~c2 => c3  ::  (s1~t1) => r1 ~ (s2~t2) => r2
 753 --      or
 754 --    forall (_:c1~c2)
 755   = let (c1,c2) = coVarKind tv
 756         (s1,s2) = coercionKind c1
 757         (t1,t2) = coercionKind c2
 758         (r1,r2) = coercionKind ty
 759     in
 760     (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
 761
 762   | otherwise
 763 --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
 764 --   ----------------------------------------------
 765 --    forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
 766   = let (ty1, ty2) = coercionKind ty in
 767     (ForAllTy tv ty1, ForAllTy tv ty2)
 768
 769 coercionKind (PredTy (ClassP cl args))
 770   = let (lArgs, rArgs) = coercionKinds args in
 771     (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
 772 coercionKind (PredTy (IParam name ty))
 773   = let (ty1, ty2) = coercionKind ty in
 774     (PredTy (IParam name ty1), PredTy (IParam name ty2))
 775 coercionKind (PredTy (EqPred c1 c2))
 776   = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
 777   -- These should not show up in coercions at all
 778   -- becuase they are in the form of for-alls
 779     let k1 = coercionKindPredTy c1
 780         k2 = coercionKindPredTy c2 in
 781     (k1,k2)
 782   where
 783     coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
 784
 785 ------------------
 786 -- | Apply 'coercionKind' to multiple 'Coercion's
 787 coercionKinds :: [Coercion] -> ([Type], [Type])
 788 coercionKinds tys = unzip $ map coercionKind tys
 789
 790 ------------------
 791 -- | 'coTyConAppKind' is given a list of the type arguments to the 'CoTyCon',
 792 -- and constructs the types that the resulting coercion relates.
 793 -- Fails (in the monad) if ill-kinded.
 794 -- Typically the monad is
 795 --   either the Lint monad (with the consistency-check flag = True),
 796 --   or the ID monad with a panic on failure (and the consistency-check flag = False)
 797 coTyConAppKind
 798     :: CoTyConDesc
 799     -> [Type]                   -- Exactly right number of args
 800     -> (Type, Type)             -- Kind of this application
 801 coTyConAppKind CoUnsafe (ty1:ty2:_)
 802   = (ty1,ty2)
 803 coTyConAppKind CoSym (co:_)
 804   | (ty1,ty2) <- coercionKind co = (ty2,ty1)
 805 coTyConAppKind CoTrans (co1:co2:_)
 806   = (fst (coercionKind co1), snd (coercionKind co2))
 807 coTyConAppKind CoLeft (co:_)
 808   | Just (res,_) <- decompLR_maybe (coercionKind co) = res
 809 coTyConAppKind CoRight (co:_)
 810   | Just (_,res) <- decompLR_maybe (coercionKind co) = res
 811 coTyConAppKind CoCsel1 (co:_)
 812   | Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res
 813 coTyConAppKind CoCsel2 (co:_)
 814   | Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res
 815 coTyConAppKind CoCselR (co:_)
 816   | Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res
 817 coTyConAppKind CoInst (co:ty:_)
 818   | Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co)
 819   = (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2)
 820 coTyConAppKind (CoAxiom { co_ax_tvs = tvs
 821                         , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
 822   = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
 823   where
 824     (tys1, tys2) = coercionKinds cos
 825 coTyConAppKind desc cos = pprPanic "coTyConAppKind" (ppr desc $$ ppr cos)
 826 \end{code}