compiler/types/Coercion.lhs

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