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, mkEqPredCo,
  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 mkEqPredCo :: Coercion -> Coercion -> Coercion
 462 mkEqPredCo co1 co2 = PredTy (EqPred co1 co2)
 463
 464
 465 \end{code}
 466
 467
 468 %************************************************************************
 469 %*                                                                      *
 470             Coercion Type Constructors
 471 %*                                                                      *
 472 %************************************************************************
 473
 474 Example.  The coercion ((sym c) (sym d) (sym e))
 475 will be represented by (TyConApp sym [c, sym d, sym e])
 476 If sym c :: p1=q1
 477    sym d :: p2=q2
 478    sym e :: p3=q3
 479 then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 480
 481 \begin{code}
 482 -- | Coercion type constructors: avoid using these directly and instead use
 483 -- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
 484 --
 485 -- Each coercion TyCon is built with the special CoercionTyCon record and
 486 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 487 -- by any TyConApp in which they are applied, however they may also be over
 488 -- applied (see example above) and the kinding function must deal with this.
 489 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon,
 490   rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
 491   csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
 492
 493 symCoercionTyCon    = mkCoercionTyCon symCoercionTyConName   1 CoSym
 494 transCoercionTyCon  = mkCoercionTyCon transCoercionTyConName 2 CoTrans
 495 leftCoercionTyCon   = mkCoercionTyCon leftCoercionTyConName  1 CoLeft
 496 rightCoercionTyCon  = mkCoercionTyCon rightCoercionTyConName 1 CoRight
 497 instCoercionTyCon   =  mkCoercionTyCon instCoercionTyConName 2 CoInst
 498 csel1CoercionTyCon  = mkCoercionTyCon csel1CoercionTyConName 1 CoCsel1
 499 csel2CoercionTyCon  = mkCoercionTyCon csel2CoercionTyConName 1 CoCsel2
 500 cselRCoercionTyCon  = mkCoercionTyCon cselRCoercionTyConName 1 CoCselR
 501 unsafeCoercionTyCon = mkCoercionTyCon unsafeCoercionTyConName 2 CoUnsafe
 502
 503 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
 504    rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
 505    csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
 506
 507 transCoercionTyConName  = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
 508 symCoercionTyConName    = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
 509 leftCoercionTyConName   = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
 510 rightCoercionTyConName  = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
 511 instCoercionTyConName   = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
 512 csel1CoercionTyConName  = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
 513 csel2CoercionTyConName  = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
 514 cselRCoercionTyConName  = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
 515 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 516
 517 mkCoConName :: FastString -> Unique -> TyCon -> Name
 518 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
 519                             key (ATyCon coCon) BuiltInSyntax
 520 \end{code}
 521
 522 \begin{code}
 523 ------------
 524 decompLR_maybe :: (Type,Type) -> Maybe ((Type,Type), (Type,Type))
 525 -- Helper for left and right.  Finds coercion kind of its input and
 526 -- returns the left and right projections of the coercion...
 527 --
 528 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 529 decompLR_maybe (ty1,ty2)
 530   | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 531   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 532   = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 533 decompLR_maybe _ = Nothing
 534
 535 ------------
 536 decompInst_maybe :: (Type, Type) -> Maybe ((TyVar,TyVar), (Type,Type))
 537 decompInst_maybe (ty1, ty2)
 538   | Just (tv1,r1) <- splitForAllTy_maybe ty1
 539   , Just (tv2,r2) <- splitForAllTy_maybe ty2
 540   = Just ((tv1,tv2), (r1,r2))
 541 decompInst_maybe _ = Nothing
 542
 543 ------------
 544 decompCsel_maybe :: (Type, Type) -> Maybe ((Type,Type), (Type,Type), (Type,Type))
 545 --   If         co :: (s1~t1 => r1) ~ (s2~t2 => r2)
 546 -- Then   csel1 co ::            s1 ~ s2
 547 --        csel2 co ::            t1 ~ t2
 548 --        cselR co ::            r1 ~ r2
 549 decompCsel_maybe (ty1, ty2)
 550   | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
 551   , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
 552   = Just ((s1,s2), (t1,t2), (r1,r2))
 553 decompCsel_maybe _ = Nothing
 554 \end{code}
 555
 556
 557 %************************************************************************
 558 %*                                                                      *
 559             Newtypes
 560 %*                                                                      *
 561 %************************************************************************
 562
 563 \begin{code}
 564 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
 565 -- ^ If @co :: T ts ~ rep_ty@ then:
 566 --
 567 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
 568 instNewTyCon_maybe tc tys
 569   | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
 570   = ASSERT( tys `lengthIs` tyConArity tc )
 571     Just (substTyWith tvs tys ty,
 572           case mb_co_tc of
 573              Nothing    -> IdCo (mkTyConApp tc    tys)
 574              Just co_tc -> ACo  (mkTyConApp co_tc tys))
 575   | otherwise
 576   = Nothing
 577
 578 -- this is here to avoid module loops
 579 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 580 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
 581 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
 582 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
 583 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
 584 --
 585 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
 586 --
 587 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
 588 splitNewTypeRepCo_maybe ty
 589   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 590 splitNewTypeRepCo_maybe (TyConApp tc tys)
 591   | Just (ty', coi) <- instNewTyCon_maybe tc tys
 592   = case coi of
 593         ACo co -> Just (ty', co)
 594         IdCo _ -> panic "splitNewTypeRepCo_maybe"
 595                         -- This case handled by coreView
 596 splitNewTypeRepCo_maybe _
 597   = Nothing
 598
 599 -- | Determines syntactic equality of coercions
 600 coreEqCoercion :: Coercion -> Coercion -> Bool
 601 coreEqCoercion = coreEqType
 602
 603 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
 604 coreEqCoercion2 = coreEqType2
 605 \end{code}
 606
 607
 608 %************************************************************************
 609 %*                                                                      *
 610             CoercionI and its constructors
 611 %*                                                                      *
 612 %************************************************************************
 613
 614 --------------------------------------
 615 -- CoercionI smart constructors
 616 --      lifted smart constructors of ordinary coercions
 617
 618 \begin{code}
 619 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
 620 -- can represent either one of:
 621 --
 622 -- 1. A proper 'Coercion'
 623 --
 624 -- 2. The identity coercion
 625 data CoercionI = IdCo Type | ACo Coercion
 626
 627 liftCoI :: (Type -> Type) -> CoercionI -> CoercionI
 628 liftCoI f (IdCo ty) = IdCo (f ty)
 629 liftCoI f (ACo ty)  = ACo (f ty)
 630
 631 liftCoI2 :: (Type -> Type -> Type) -> CoercionI -> CoercionI -> CoercionI
 632 liftCoI2 f (IdCo ty1) (IdCo ty2) = IdCo (f ty1 ty2)
 633 liftCoI2 f coi1       coi2       = ACo (f (fromCoI coi1) (fromCoI coi2))
 634
 635 liftCoIs :: ([Type] -> Type) -> [CoercionI] -> CoercionI
 636 liftCoIs f cois = go_id [] cois
 637   where
 638     go_id rev_tys []               = IdCo (f (reverse rev_tys))
 639     go_id rev_tys (IdCo ty : cois) = go_id  (ty:rev_tys) cois
 640     go_id rev_tys (ACo  co : cois) = go_aco (co:rev_tys) cois
 641
 642     go_aco rev_tys []               = ACo (f (reverse rev_tys))
 643     go_aco rev_tys (IdCo ty : cois) = go_aco (ty:rev_tys) cois
 644     go_aco rev_tys (ACo  co : cois) = go_aco (co:rev_tys) cois
 645
 646 instance Outputable CoercionI where
 647   ppr (IdCo _) = ptext (sLit "IdCo")
 648   ppr (ACo co) = ppr co
 649
 650 isIdentityCoI :: CoercionI -> Bool
 651 isIdentityCoI (IdCo _) = True
 652 isIdentityCoI (ACo _)  = False
 653
 654 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
 655 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
 656 fromCoI :: CoercionI -> Type
 657 fromCoI (IdCo ty) = ty  -- Identity coercion represented
 658 fromCoI (ACo co)  = co  --      by the type itself
 659
 660 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
 661 mkSymCoI :: CoercionI -> CoercionI
 662 mkSymCoI (IdCo ty) = IdCo ty
 663 mkSymCoI (ACo co)  = ACo $ mkCoercion symCoercionTyCon [co]
 664                                 -- the smart constructor
 665                                 -- is too smart with tyvars
 666
 667 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
 668 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
 669 mkTransCoI (IdCo _) aco = aco
 670 mkTransCoI aco (IdCo _) = aco
 671 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
 672
 673 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
 674 mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI
 675 mkTyConAppCoI tyCon cois = liftCoIs (mkTyConApp tyCon) cois
 676
 677 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
 678 mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI
 679 mkAppTyCoI = liftCoI2 mkAppTy
 680
 681 mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI
 682 mkFunTyCoI = liftCoI2 mkFunTy
 683
 684 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
 685 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
 686 mkForAllTyCoI tv = liftCoI (ForAllTy tv)
 687
 688 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
 689 --
 690 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
 691 mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI
 692 mkClassPPredCoI cls = liftCoIs (PredTy . ClassP cls)
 693
 694 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 695 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
 696 mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn)
 697
 698 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 699 mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
 700 mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
 701
 702 mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI
 703 mkCoPredCoI coi1 coi2 coi3 =   mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3
 704
 705
 706 \end{code}
 707
 708 %************************************************************************
 709 %*                                                                      *
 710              The kind of a type, and of a coercion
 711 %*                                                                      *
 712 %************************************************************************
 713
 714 \begin{code}
 715 typeKind :: Type -> Kind
 716 typeKind ty@(TyConApp tc tys)
 717   | isCoercionTyCon tc = typeKind (fst (coercionKind ty))
 718   | otherwise          = kindAppResult (tyConKind tc) tys
 719         -- During coercion optimisation we *do* match a type
 720         -- against a coercion (see OptCoercion.matchesAxiomLhs)
 721         -- So the use of typeKind in Unify.match_kind must work on coercions too
 722         -- Hence the isCoercionTyCon case above
 723
 724 typeKind (PredTy pred)        = predKind pred
 725 typeKind (AppTy fun _)        = kindFunResult (typeKind fun)
 726 typeKind (ForAllTy _ ty)      = typeKind ty
 727 typeKind (TyVarTy tyvar)      = tyVarKind tyvar
 728 typeKind (FunTy _arg res)
 729     -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*),
 730     --              not unliftedTypKind (#)
 731     -- The only things that can be after a function arrow are
 732     --   (a) types (of kind openTypeKind or its sub-kinds)
 733     --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
 734     | isTySuperKind k         = k
 735     | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind
 736     where
 737       k = typeKind res
 738
 739 ------------------
 740 predKind :: PredType -> Kind
 741 predKind (EqPred {}) = coSuperKind      -- A coercion kind!
 742 predKind (ClassP {}) = liftedTypeKind   -- Class and implicitPredicates are
 743 predKind (IParam {}) = liftedTypeKind   -- always represented by lifted types
 744
 745 ------------------
 746 -- | If it is the case that
 747 --
 748 -- > c :: (t1 ~ t2)
 749 --
 750 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@,
 751 -- then @coercionKind c = (t1, t2)@.
 752 coercionKind :: Coercion -> (Type, Type)
 753 coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
 754                             | otherwise = (ty, ty)
 755 coercionKind (AppTy ty1 ty2)
 756   = let (s1, t1) = coercionKind ty1
 757         (s2, t2) = coercionKind ty2 in
 758     (mkAppTy s1 s2, mkAppTy t1 t2)
 759 coercionKind co@(TyConApp tc args)
 760   | Just (ar, desc) <- isCoercionTyCon_maybe tc
 761     -- CoercionTyCons carry their kinding rule, so we use it here
 762   = WARN( not (length args >= ar), ppr co )     -- Always saturated
 763     (let (ty1,  ty2)  = coTyConAppKind desc (take ar args)
 764          (tys1, tys2) = coercionKinds (drop ar args)
 765      in (mkAppTys ty1 tys1, mkAppTys ty2 tys2))
 766
 767   | otherwise
 768   = let (lArgs, rArgs) = coercionKinds args in
 769     (TyConApp tc lArgs, TyConApp tc rArgs)
 770
 771 coercionKind (FunTy ty1 ty2)
 772   = let (t1, t2) = coercionKind ty1
 773         (s1, s2) = coercionKind ty2 in
 774     (mkFunTy t1 s1, mkFunTy t2 s2)
 775
 776 coercionKind (ForAllTy tv ty)
 777   | isCoVar tv
 778 --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
 779 --    ----------------------------------------------
 780 --    c1~c2 => c3  ::  (s1~t1) => r1 ~ (s2~t2) => r2
 781 --      or
 782 --    forall (_:c1~c2)
 783   = let (c1,c2) = coVarKind tv
 784         (s1,s2) = coercionKind c1
 785         (t1,t2) = coercionKind c2
 786         (r1,r2) = coercionKind ty
 787     in
 788     (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
 789
 790   | otherwise
 791 --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
 792 --   ----------------------------------------------
 793 --    forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
 794   = let (ty1, ty2) = coercionKind ty in
 795     (ForAllTy tv ty1, ForAllTy tv ty2)
 796
 797 coercionKind (PredTy (ClassP cl args))
 798   = let (lArgs, rArgs) = coercionKinds args in
 799     (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
 800 coercionKind (PredTy (IParam name ty))
 801   = let (ty1, ty2) = coercionKind ty in
 802     (PredTy (IParam name ty1), PredTy (IParam name ty2))
 803 coercionKind (PredTy (EqPred c1 c2))
 804   = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
 805   -- These should not show up in coercions at all
 806   -- becuase they are in the form of for-alls
 807     let k1 = coercionKindPredTy c1
 808         k2 = coercionKindPredTy c2 in
 809     (k1,k2)
 810   where
 811     coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
 812
 813 ------------------
 814 -- | Apply 'coercionKind' to multiple 'Coercion's
 815 coercionKinds :: [Coercion] -> ([Type], [Type])
 816 coercionKinds tys = unzip $ map coercionKind tys
 817
 818 ------------------
 819 -- | 'coTyConAppKind' is given a list of the type arguments to the 'CoTyCon',
 820 -- and constructs the types that the resulting coercion relates.
 821 -- Fails (in the monad) if ill-kinded.
 822 -- Typically the monad is
 823 --   either the Lint monad (with the consistency-check flag = True),
 824 --   or the ID monad with a panic on failure (and the consistency-check flag = False)
 825 coTyConAppKind
 826     :: CoTyConDesc
 827     -> [Type]                   -- Exactly right number of args
 828     -> (Type, Type)             -- Kind of this application
 829 coTyConAppKind CoUnsafe (ty1:ty2:_)
 830   = (ty1,ty2)
 831 coTyConAppKind CoSym (co:_)
 832   | (ty1,ty2) <- coercionKind co = (ty2,ty1)
 833 coTyConAppKind CoTrans (co1:co2:_)
 834   = (fst (coercionKind co1), snd (coercionKind co2))
 835 coTyConAppKind CoLeft (co:_)
 836   | Just (res,_) <- decompLR_maybe (coercionKind co) = res
 837 coTyConAppKind CoRight (co:_)
 838   | Just (_,res) <- decompLR_maybe (coercionKind co) = res
 839 coTyConAppKind CoCsel1 (co:_)
 840   | Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res
 841 coTyConAppKind CoCsel2 (co:_)
 842   | Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res
 843 coTyConAppKind CoCselR (co:_)
 844   | Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res
 845 coTyConAppKind CoInst (co:ty:_)
 846   | Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co)
 847   = (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2)
 848 coTyConAppKind (CoAxiom { co_ax_tvs = tvs
 849                         , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
 850   = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
 851   where
 852     (tys1, tys2) = coercionKinds cos
 853 coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat
 854                              [ ppr co <+> dcolon <+> pprEqPred (coercionKind co)
 855                              | co <- cos ])) $
 856                           coercionKind (head cos)
 857 \end{code}