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