compiler/types/Coercion.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 \begin{code}
   6 {-# OPTIONS -fno-warn-incomplete-patterns #-}
   7 -- The above warning supression flag is a temporary kludge.
   8 -- While working on this module you are encouraged to remove it and fix
   9 -- any warnings in the module. See
  10 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
  11 -- for details
  12
  13 -- | Module for type coercions, as used in System FC. See 'CoreSyn.Expr' for
  14 -- more on System FC and how coercions fit into it.
  15 --
  16 -- Coercions are represented as types, and their kinds tell what types the
  17 -- coercion works on. The coercion kind constructor is a special TyCon that must always be saturated, like so:
  18 --
  19 -- > typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
  20 module Coercion (
  21         -- * Main data type
  22         Coercion,
  23
  24         mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
  25         coercionKind, coercionKinds, coercionKindPredTy, isIdentityCoercion,
  26
  27         -- ** Equality predicates
  28         isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
  29
  30         -- ** Coercion transformations
  31         mkCoercion,
  32         mkSymCoercion, mkTransCoercion,
  33         mkLeftCoercion, mkRightCoercion, mkRightCoercions,
  34         mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
  35         mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
  36         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
  37
  38         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
  39
  40         unsafeCoercionTyCon, symCoercionTyCon,
  41         transCoercionTyCon, leftCoercionTyCon,
  42         rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
  43
  44         -- ** Optimisation
  45         optCoercion,
  46
  47         -- ** Comparison
  48         coreEqCoercion,
  49
  50         -- * CoercionI
  51         CoercionI(..),
  52         isIdentityCoI,
  53         mkSymCoI, mkTransCoI,
  54         mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
  55         mkForAllTyCoI,
  56         fromCoI, fromACo,
  57         mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
  58
  59        ) where
  60
  61 #include "HsVersions.h"
  62
  63 import TypeRep
  64 import Type
  65 import TyCon
  66 import Class
  67 import Var
  68 import Name
  69 import PrelNames
  70 import Util
  71 import BasicTypes
  72 import Outputable
  73 import FastString
  74
  75 -- | A 'Coercion' represents a 'Type' something should be coerced to.
  76 type Coercion     = Type
  77
  78 -- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
  79 -- types that a 'Coercion' will work on.
  80 type CoercionKind = Kind
  81
  82 ------------------------------
  83
  84 -- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
  85 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
  86 --
  87 -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
  88 decomposeCo :: Arity -> Coercion -> [Coercion]
  89 decomposeCo n co
  90   = go n co []
  91   where
  92     go 0 _  cos = cos
  93     go n co cos = go (n-1) (mkLeftCoercion co)
  94                            (mkRightCoercion co : cos)
  95
  96 ------------------------------
  97
  98 -------------------------------------------------------
  99 -- and some coercion kind stuff
 100
 101 -- | Tests whether a type is just a type equality predicate
 102 isEqPredTy :: Type -> Bool
 103 isEqPredTy (PredTy pred) = isEqPred pred
 104 isEqPredTy _             = False
 105
 106 -- | Creates a type equality predicate
 107 mkEqPred :: (Type, Type) -> PredType
 108 mkEqPred (ty1, ty2) = EqPred ty1 ty2
 109
 110 -- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
 111 -- Panics otherwise
 112 getEqPredTys :: PredType -> (Type,Type)
 113 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
 114 getEqPredTys other            = pprPanic "getEqPredTys" (ppr other)
 115
 116 -- | Makes a 'CoercionKind' from two types: the types whose equality is proven by the relevant 'Coercion'
 117 mkCoKind :: Type -> Type -> CoercionKind
 118 mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
 119
 120 -- | Create a reflexive 'CoercionKind' that asserts that a type can be coerced to itself
 121 mkReflCoKind :: Type -> CoercionKind
 122 mkReflCoKind ty = mkCoKind ty ty
 123
 124 -- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
 125 -- Panics if the argument is not a valid 'CoercionKind'
 126 splitCoercionKind :: CoercionKind -> (Type, Type)
 127 splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co'
 128 splitCoercionKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)
 129
 130 -- | Take a 'CoercionKind' apart into the two types it relates, if possible. See also 'splitCoercionKind'
 131 splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
 132 splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
 133 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
 134 splitCoercionKind_maybe _ = Nothing
 135
 136 -- | If it is the case that
 137 --
 138 -- > c :: (t1 ~ t2)
 139 --
 140 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
 141 -- See also 'coercionKindPredTy'
 142 coercionKind :: Coercion -> (Type, Type)
 143 coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
 144                             | otherwise = (ty, ty)
 145 coercionKind (AppTy ty1 ty2)
 146   = let (t1, t2) = coercionKind ty1
 147         (s1, s2) = coercionKind ty2 in
 148     (mkAppTy t1 s1, mkAppTy t2 s2)
 149 coercionKind (TyConApp tc args)
 150   | Just (ar, rule) <- isCoercionTyCon_maybe tc
 151     -- CoercionTyCons carry their kinding rule, so we use it here
 152   = ASSERT( length args >= ar ) -- Always saturated
 153     let (ty1,ty2)    = rule (take ar args)      -- Apply the rule to the right number of args
 154         (tys1, tys2) = coercionKinds (drop ar args)
 155     in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)
 156
 157   | otherwise
 158   = let (lArgs, rArgs) = coercionKinds args in
 159     (TyConApp tc lArgs, TyConApp tc rArgs)
 160 coercionKind (FunTy ty1 ty2)
 161   = let (t1, t2) = coercionKind ty1
 162         (s1, s2) = coercionKind ty2 in
 163     (mkFunTy t1 s1, mkFunTy t2 s2)
 164 coercionKind (ForAllTy tv ty)
 165   = let (ty1, ty2) = coercionKind ty in
 166     (ForAllTy tv ty1, ForAllTy tv ty2)
 167 coercionKind (PredTy (EqPred c1 c2))
 168   = let k1 = coercionKindPredTy c1
 169         k2 = coercionKindPredTy c2 in
 170     (k1,k2)
 171 coercionKind (PredTy (ClassP cl args))
 172   = let (lArgs, rArgs) = coercionKinds args in
 173     (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
 174 coercionKind (PredTy (IParam name ty))
 175   = let (ty1, ty2) = coercionKind ty in
 176     (PredTy (IParam name ty1), PredTy (IParam name ty2))
 177
 178 -- | Recover the 'CoercionKind' corresponding to a particular 'Coerceion'. See also 'coercionKind'
 179 -- and 'mkCoKind'
 180 coercionKindPredTy :: Coercion -> CoercionKind
 181 coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
 182
 183 -- | Apply 'coercionKind' to multiple 'Coercion's
 184 coercionKinds :: [Coercion] -> ([Type], [Type])
 185 coercionKinds tys = unzip $ map coercionKind tys
 186
 187 -------------------------------------
 188 isIdentityCoercion :: Coercion -> Bool
 189 isIdentityCoercion co
 190   = case coercionKind co of
 191        (t1,t2) -> t1 `coreEqType` t2
 192
 193 -------------------------------------
 194 -- Coercion kind and type mk's
 195 -- (make saturated TyConApp CoercionTyCon{...} args)
 196
 197 -- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
 198 -- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
 199 -- if possible
 200 mkCoercion :: TyCon -> [Type] -> Coercion
 201 mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
 202                         TyConApp coCon args
 203
 204 -- | Apply a 'Coercion' to another 'Coercion', which is presumably a
 205 -- 'Coercion' constructor of some kind
 206 mkAppCoercion :: Coercion -> Coercion -> Coercion
 207 mkAppCoercion co1 co2 = mkAppTy co1 co2
 208
 209 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
 210 -- See also 'mkAppCoercion'
 211 mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
 212 mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
 213
 214 -- | Apply a type constructor to a list of coercions.
 215 mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
 216 mkTyConCoercion con cos = mkTyConApp con cos
 217
 218 -- | Make a function 'Coercion' between two other 'Coercion's
 219 mkFunCoercion :: Coercion -> Coercion -> Coercion
 220 mkFunCoercion co1 co2 = mkFunTy co1 co2
 221
 222 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
 223 mkForAllCoercion :: Var -> Coercion -> Coercion
 224 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
 225 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
 226
 227
 228 -------------------------------
 229
 230 mkSymCoercion :: Coercion -> Coercion
 231 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality
 232 -- between the same types but in the other "direction", so a kind of @t1 ~ t2@
 233 -- becomes the kind @t2 ~ t1@.
 234 --
 235 -- This function attempts to simplify the generated 'Coercion' by removing
 236 -- redundant applications of @sym@. This is done by pushing this new @sym@
 237 -- down into the 'Coercion' and exploiting the fact that @sym (sym co) = co@.
 238 mkSymCoercion co
 239   | Just co' <- coreView co = mkSymCoercion co'
 240
 241 mkSymCoercion (ForAllTy tv ty)  = ForAllTy tv (mkSymCoercion ty)
 242 mkSymCoercion (AppTy co1 co2)   = AppTy (mkSymCoercion co1) (mkSymCoercion co2)
 243 mkSymCoercion (FunTy co1 co2)   = FunTy (mkSymCoercion co1) (mkSymCoercion co2)
 244
 245 mkSymCoercion (TyConApp tc cos)
 246   | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos)
 247
 248 mkSymCoercion (TyConApp tc [co])
 249   | tc `hasKey` symCoercionTyConKey   = co    -- sym (sym co) --> co
 250   | tc `hasKey` leftCoercionTyConKey  = mkLeftCoercion (mkSymCoercion co)
 251   | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)
 252
 253 mkSymCoercion (TyConApp tc [co1,co2])
 254   | tc `hasKey` transCoercionTyConKey
 255      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
 256      -- Note reversal of arguments!
 257   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
 258
 259   | tc `hasKey` instCoercionTyConKey
 260      -- sym (co @ ty) --> (sym co) @ ty
 261      -- Note: sym is not applied to 'ty'
 262   = mkInstCoercion (mkSymCoercion co1) co2
 263
 264 mkSymCoercion (TyConApp tc cos)         -- Other coercion tycons, such as those
 265   = mkCoercion symCoercionTyCon [TyConApp tc cos]  -- arising from newtypes
 266
 267 mkSymCoercion (TyVarTy tv)
 268   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
 269   | otherwise  = TyVarTy tv     -- Reflexive
 270
 271 -------------------------------
 272 -- ToDo: we should be cleverer about transitivity
 273
 274 mkTransCoercion :: Coercion -> Coercion -> Coercion
 275 -- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
 276 --
 277 -- This function attempts to simplify the generated 'Coercion' by exploiting the fact that
 278 -- @sym g `trans` g = id@.
 279 mkTransCoercion g1 g2   -- sym g `trans` g = id
 280   | (t1,_) <- coercionKind g1
 281   , (_,t2) <- coercionKind g2
 282   , t1 `coreEqType` t2
 283   = t1
 284
 285   | otherwise
 286   = mkCoercion transCoercionTyCon [g1, g2]
 287
 288
 289 -------------------------------
 290 -- Smart constructors for left and right
 291
 292 mkLeftCoercion :: Coercion -> Coercion
 293 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
 294 -- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
 295 --
 296 -- > mkLeftCoercion c :: f ~ g
 297 mkLeftCoercion co
 298   | Just (co', _) <- splitAppCoercion_maybe co = co'
 299   | otherwise = mkCoercion leftCoercionTyCon [co]
 300
 301 mkRightCoercion :: Coercion -> Coercion
 302 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
 303 -- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
 304 --
 305 -- > mkLeftCoercion c :: x ~ y
 306 mkRightCoercion  co
 307   | Just (_, co2) <- splitAppCoercion_maybe co = co2
 308   | otherwise = mkCoercion rightCoercionTyCon [co]
 309
 310 mkRightCoercions :: Int -> Coercion -> [Coercion]
 311 -- ^ As 'mkRightCoercion', but finds the 'Coercion's available on the right side of @n@
 312 -- nested application 'Coercion's, manufacturing new left or right cooercions as necessary
 313 -- if suffficiently many are not directly available.
 314 mkRightCoercions n co
 315   = go n co []
 316   where
 317     go n co acc
 318        | n > 0
 319        = case splitAppCoercion_maybe co of
 320           Just (co1,co2) -> go (n-1) co1 (co2:acc)
 321           Nothing        -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
 322        | otherwise
 323        = acc
 324
 325
 326 mkInstCoercion :: Coercion -> Type -> Coercion
 327 -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
 328 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
 329 mkInstCoercion co ty
 330   | Just (tv,co') <- splitForAllTy_maybe co
 331   = substTyWith [tv] [ty] co'   -- (forall a.co) @ ty  -->  co[ty/a]
 332   | otherwise
 333   = mkCoercion instCoercionTyCon  [co, ty]
 334
 335 mkInstsCoercion :: Coercion -> [Type] -> Coercion
 336 -- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right
 337 mkInstsCoercion co tys = foldl mkInstCoercion co tys
 338
 339 {-
 340 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
 341 splitSymCoercion_maybe (TyConApp tc [co]) =
 342   if tc `hasKey` symCoercionTyConKey
 343   then Just co
 344   else Nothing
 345 splitSymCoercion_maybe co = Nothing
 346 -}
 347
 348 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 349 -- ^ Splits a coercion application, being careful *not* to split @left c@ etc.
 350 -- This is because those are really syntactic constructs, not applications
 351 splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
 352 splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 353 splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 354 splitAppCoercion_maybe (TyConApp tc tys)
 355    | not (isCoercionTyCon tc)
 356    = case snocView tys of
 357        Just (tys', ty') -> Just (TyConApp tc tys', ty')
 358        Nothing          -> Nothing
 359 splitAppCoercion_maybe _ = Nothing
 360
 361 {-
 362 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 363 splitTransCoercion_maybe (TyConApp tc [ty1, ty2])
 364  = if tc `hasKey` transCoercionTyConKey then
 365        Just (ty1, ty2)
 366    else
 367        Nothing
 368 splitTransCoercion_maybe other = Nothing
 369
 370 splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
 371 splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
 372  = if tc `hasKey` instCoercionTyConKey then
 373        Just (ty1, ty2)
 374     else
 375        Nothing
 376 splitInstCoercion_maybe other = Nothing
 377
 378 splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
 379 splitLeftCoercion_maybe (TyConApp tc [co])
 380  = if tc `hasKey` leftCoercionTyConKey then
 381        Just co
 382    else
 383        Nothing
 384 splitLeftCoercion_maybe other = Nothing
 385
 386 splitRightCoercion_maybe :: Coercion -> Maybe Coercion
 387 splitRightCoercion_maybe (TyConApp tc [co])
 388  = if tc `hasKey` rightCoercionTyConKey then
 389        Just co
 390    else
 391        Nothing
 392 splitRightCoercion_maybe other = Nothing
 393 -}
 394
 395 -- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
 396 -- but it is used when we know we are dealing with bottom, which is one case in which
 397 -- it is safe.  This is also used implement the @unsafeCoerce#@ primitive.
 398 mkUnsafeCoercion :: Type -> Type -> Coercion
 399 mkUnsafeCoercion ty1 ty2
 400   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 401
 402
 403 -- See note [Newtype coercions] in TyCon
 404
 405 -- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a
 406 -- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the
 407 -- type the appropriate right hand side of the @newtype@, with the free variables
 408 -- a subset of those 'TyVar's.
 409 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 410 mkNewTypeCoercion name tycon tvs rhs_ty
 411   = mkCoercionTyCon name co_con_arity rule
 412   where
 413     co_con_arity = length tvs
 414
 415     rule args = ASSERT( co_con_arity == length args )
 416                 (TyConApp tycon args, substTyWith tvs args rhs_ty)
 417
 418 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
 419 -- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
 420 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
 421 -- representation tycon.
 422 mkFamInstCoercion :: Name       -- ^ Unique name for the coercion tycon
 423                   -> [TyVar]    -- ^ Type parameters of the coercion (@tvs@)
 424                   -> TyCon      -- ^ Family tycon (@F@)
 425                   -> [Type]     -- ^ Type instance (@ts@)
 426                   -> TyCon      -- ^ Representation tycon (@R@)
 427                   -> TyCon      -- ^ Coercion tycon (@Co@)
 428 mkFamInstCoercion name tvs family instTys rep_tycon
 429   = mkCoercionTyCon name coArity rule
 430   where
 431     coArity = length tvs
 432     rule args = (substTyWith tvs args $              -- with sigma = [tys/tvs],
 433                    TyConApp family instTys,          --       sigma (F ts)
 434                  TyConApp rep_tycon args)            --   ~ R tys
 435
 436 --------------------------------------
 437 -- Coercion Type Constructors...
 438
 439 -- Example.  The coercion ((sym c) (sym d) (sym e))
 440 -- will be represented by (TyConApp sym [c, sym d, sym e])
 441 -- If sym c :: p1=q1
 442 --    sym d :: p2=q2
 443 --    sym e :: p3=q3
 444 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 445
 446 -- | Coercion type constructors: avoid using these directly and instead use the @mk*Coercion@ and @split*Coercion@ family
 447 -- of functions if possible.
 448 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon :: TyCon
 449 -- Each coercion TyCon is built with the special CoercionTyCon record and
 450 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 451 -- by any TyConApp in which they are applied, however they may also be over
 452 -- applied (see example above) and the kinding function must deal with this.
 453 symCoercionTyCon =
 454   mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
 455   where
 456     flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
 457         where
 458           (ty1, ty2) = coercionKind co
 459
 460 transCoercionTyCon =
 461   mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
 462   where
 463     composeCoercionKindsOf (co1:co2:rest)
 464       = ASSERT( null rest )
 465         WARN( not (r1 `coreEqType` a2),
 466               text "Strange! Type mismatch in trans coercion, probably a bug"
 467               $$
 468               ppr r1 <+> text "=/=" <+> ppr a2)
 469         (a1, r2)
 470       where
 471         (a1, r1) = coercionKind co1
 472         (a2, r2) = coercionKind co2
 473
 474 leftCoercionTyCon =
 475   mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
 476   where
 477     leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 478       where
 479         (ty1,ty2) = fst (splitCoercionKindOf co)
 480
 481 rightCoercionTyCon =
 482   mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
 483   where
 484     rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 485       where
 486         (ty1,ty2) = snd (splitCoercionKindOf co)
 487
 488 splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
 489 -- Helper for left and right.  Finds coercion kind of its input and
 490 -- returns the left and right projections of the coercion...
 491 --
 492 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 493 splitCoercionKindOf co
 494   | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
 495   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 496   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 497   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 498 splitCoercionKindOf co
 499   = pprPanic "Coercion.splitCoercionKindOf"
 500              (ppr co $$ ppr (coercionKindPredTy co))
 501
 502 instCoercionTyCon
 503   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
 504   where
 505     instantiateCo t s =
 506       let Just (tv, ty) = splitForAllTy_maybe t in
 507       substTyWith [tv] [s] ty
 508
 509     instCoercionKind (co1:ty:rest) = ASSERT( null rest )
 510                                      (instantiateCo t1 ty, instantiateCo t2 ty)
 511       where (t1, t2) = coercionKind co1
 512
 513 unsafeCoercionTyCon
 514   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
 515   where
 516    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2)
 517
 518 --------------------------------------
 519 -- ...and their names
 520
 521 mkCoConName :: FastString -> Unique -> TyCon -> Name
 522 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
 523                             key (ATyCon coCon) BuiltInSyntax
 524
 525 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: Name
 526
 527 transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
 528 symCoercionTyConName   = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
 529 leftCoercionTyConName  = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
 530 rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
 531 instCoercionTyConName  = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
 532 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 533
 534
 535
 536 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
 537 -- ^ If @co :: T ts ~ rep_ty@ then:
 538 --
 539 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
 540 instNewTyCon_maybe tc tys
 541   | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
 542   = ASSERT( tys `lengthIs` tyConArity tc )
 543     Just (substTyWith tvs tys ty,
 544           case mb_co_tc of
 545            Nothing    -> IdCo
 546            Just co_tc -> ACo (mkTyConApp co_tc tys))
 547   | otherwise
 548   = Nothing
 549
 550 -- this is here to avoid module loops
 551 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 552 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
 553 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
 554 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
 555 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
 556 --
 557 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
 558 --
 559 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
 560 splitNewTypeRepCo_maybe ty
 561   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 562 splitNewTypeRepCo_maybe (TyConApp tc tys)
 563   | Just (ty', coi) <- instNewTyCon_maybe tc tys
 564   = case coi of
 565         ACo co -> Just (ty', co)
 566         IdCo   -> panic "splitNewTypeRepCo_maybe"
 567                         -- This case handled by coreView
 568 splitNewTypeRepCo_maybe _
 569   = Nothing
 570
 571 -- | Determines syntactic equality of coercions
 572 coreEqCoercion :: Coercion -> Coercion -> Bool
 573 coreEqCoercion = coreEqType
 574 \end{code}
 575
 576
 577 --------------------------------------
 578 -- CoercionI smart constructors
 579 --      lifted smart constructors of ordinary coercions
 580
 581 \begin{code}
 582 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
 583 -- can represent either one of:
 584 --
 585 -- 1. A proper 'Coercion'
 586 --
 587 -- 2. The identity coercion
 588 data CoercionI = IdCo | ACo Coercion
 589
 590 instance Outputable CoercionI where
 591   ppr IdCo     = ptext (sLit "IdCo")
 592   ppr (ACo co) = ppr co
 593
 594 isIdentityCoI :: CoercionI -> Bool
 595 isIdentityCoI IdCo = True
 596 isIdentityCoI _    = False
 597
 598 -- | Tests whether all the given 'CoercionI's represent the identity coercion
 599 allIdCoIs :: [CoercionI] -> Bool
 600 allIdCoIs = all isIdentityCoI
 601
 602 -- | For each 'CoercionI' in the input list, return either the 'Coercion' it
 603 -- contains or the corresponding 'Type' from the other list
 604 zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
 605 zipCoArgs cois tys = zipWith fromCoI cois tys
 606
 607 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
 608 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
 609 fromCoI :: CoercionI -> Type -> Type
 610 fromCoI IdCo ty     = ty        -- Identity coercion represented
 611 fromCoI (ACo co) _  = co        --      by the type itself
 612
 613 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
 614 mkSymCoI :: CoercionI -> CoercionI
 615 mkSymCoI IdCo = IdCo
 616 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
 617                                 -- the smart constructor
 618                                 -- is too smart with tyvars
 619
 620 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
 621 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
 622 mkTransCoI IdCo aco = aco
 623 mkTransCoI aco IdCo = aco
 624 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
 625
 626 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
 627 mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
 628 mkTyConAppCoI tyCon tys cois
 629   | allIdCoIs cois = IdCo
 630   | otherwise      = ACo (TyConApp tyCon (zipCoArgs cois tys))
 631
 632 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
 633 mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 634 mkAppTyCoI _   IdCo _   IdCo = IdCo
 635 mkAppTyCoI ty1 coi1 ty2 coi2 =
 636         ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 637
 638 -- | Smart constructor for function-'Coercion's on 'CoercionI', see also 'mkFunCoercion'
 639 mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
 640 mkFunTyCoI _   IdCo _   IdCo = IdCo
 641 mkFunTyCoI ty1 coi1 ty2 coi2 =
 642         ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
 643
 644 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
 645 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
 646 mkForAllTyCoI _ IdCo = IdCo
 647 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
 648
 649 -- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
 650 -- panic
 651 fromACo :: CoercionI -> Coercion
 652 fromACo (ACo co) = co
 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                  Optimising coercions
 677 %*                                                                      *
 678 %************************************************************************
 679
 680 \begin{code}
 681 optCoercion :: Coercion -> Coercion
 682 optCoercion co = co
 683 {-
 684   = pprTrace "optCoercion" (ppr co $$ ppr (coercionKind co)) $
 685     ASSERT2( coercionKind co `eq` coercionKind result, ppr co $$ ppr result )
 686     result
 687   where
 688         (s1,t1) `eq` (s2,t2) = s1 `coreEqType` s2 && t1 `coreEqType` t2
 689
 690         (result,_,_) = go co
 691                          -- optimized, changed?, identity?
 692         go :: Coercion -> ( Coercion, Bool, Bool )
 693         -- traverse coercion term bottom up and return
 694         --
 695         --    1) equivalent coercion, in optimized form
 696         --
 697         --    2) whether the output coercion differs from
 698         --       the input coercion
 699         --
 700         --    3) whether the coercion is an identity coercion
 701         --
 702         -- Performs the following optimizations:
 703         --
 704         --      sym id          >->     id
 705         --      trans id co     >->     co
 706         --      trans co id     >->     co
 707         --
 708         go ty@(TyVarTy a) | isCoVar a = let (ty1,ty2) = coercionKind ty
 709                                         in (ty, False, ty1 `coreEqType` ty2)
 710                           | otherwise = (ty, False, True)
 711         go ty@(AppTy ty1 ty2)
 712           = let (ty1', chan1, id1) = go ty1
 713                 (ty2', chan2, id2) = go ty2
 714             in if chan1 || chan2
 715                  then (AppTy ty1' ty2', True,  id1 && id2)
 716                  else (ty             , False, id1 && id2)
 717         go ty@(TyConApp tc args)
 718           | tc == symCoercionTyCon, [ty1] <- args
 719           = case go ty1 of
 720               (ty1', _   ,    True) -> (ty1', True, True)
 721               (ty1', True, _      ) -> (TyConApp tc [ty1'], True, False)
 722               (_   , _   , _      ) -> (ty, False, False)
 723           | tc == transCoercionTyCon, [ty1,ty2] <- args
 724           = let (ty1', chan1, id1) = go ty1
 725                 (ty2', chan2, id2) = go ty2
 726             in  if id1
 727                   then (ty2', True, id2)
 728                   else if id2
 729                          then (ty1', True, False)
 730                          else if chan1 || chan2
 731                                 then (TyConApp tc [ty1',ty2'], True , False)
 732                                 else (ty                     , False, False)
 733           | otherwise
 734           = let (args', chans, ids) = mapAndUnzip3 go args
 735             in  if or chans
 736                   then (TyConApp tc args', True , and ids)
 737                   else (ty               , False, and ids)
 738         go ty@(FunTy ty1 ty2)
 739           = let (ty1',chan1,id1) = go ty1
 740                 (ty2',chan2,id2) = go ty2
 741             in  if chan1 || chan2
 742                   then (FunTy ty1' ty2', True , id1 && id2)
 743                   else (ty             , False, id1 && id2)
 744         go ty@(ForAllTy tv ty1)
 745           = let (ty1', chan1, id1) = go ty1
 746             in if chan1
 747                  then (ForAllTy tv ty1', True , id1)
 748                  else (ty              , False, id1)
 749         go ty@(PredTy (EqPred ty1 ty2))
 750           = let (ty1', chan1, id1) = go ty1
 751                 (ty2', chan2, id2) = go ty2
 752             in if chan1 || chan2
 753                  then (PredTy (EqPred ty1' ty2'), True , id1 && id2)
 754                  else (ty                       , False, id1 && id2)
 755         go ty@(PredTy (ClassP cl args))
 756           = let (args', chans, ids) = mapAndUnzip3 go args
 757             in  if or chans
 758                   then (PredTy (ClassP cl args'), True , and ids)
 759                   else (ty                      , False, and ids)
 760         go ty@(PredTy (IParam name ty1))
 761           = let (ty1', chan1, id1) = go ty1
 762             in  if chan1
 763                   then (PredTy (IParam name ty1'), True , id1)
 764                   else (ty                       , False, id1)
 765 -}
 766 \end{code}