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