compiler/types/Coercion.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 \begin{code}
   6 {-# OPTIONS -fno-warn-tabs #-}
   7 -- The above warning supression flag is a temporary kludge.
   8 -- While working on this module you are encouraged to remove it and
   9 -- detab the module (please do the detabbing in a separate patch). See
  10 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
  11 -- for details
  12
  13 -- | Module for (a) type kinds and (b) type coercions,
  14 -- as used in System FC. See 'CoreSyn.Expr' for
  15 -- more on System FC and how coercions fit into it.
  16 --
  17 module Coercion (
  18         -- * Main data type
  19         Coercion(..), Var, CoVar,
  20
  21         -- ** Functions over coercions
  22         coVarKind,
  23         coercionType, coercionKind, coercionKinds, isReflCo,
  24         isReflCo_maybe,
  25         mkCoercionType,
  26
  27         -- ** Functions over coercion axioms
  28         coAxiomSplitLHS,
  29
  30         -- ** Constructing coercions
  31         mkReflCo, mkCoVarCo,
  32         mkAxInstCo, mkAxInstRHS,
  33         mkPiCo, mkPiCos,
  34         mkSymCo, mkTransCo, mkNthCo,
  35         mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
  36         mkForAllCo, mkUnsafeCo,
  37         mkNewTypeCo,
  38
  39         -- ** Decomposition
  40         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
  41         getCoVar_maybe,
  42
  43         splitTyConAppCo_maybe,
  44         splitAppCo_maybe,
  45         splitForAllCo_maybe,
  46
  47         -- ** Coercion variables
  48         mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
  49
  50         -- ** Free variables
  51         tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize,
  52
  53         -- ** Substitution
  54         CvSubstEnv, emptyCvSubstEnv,
  55         CvSubst(..), emptyCvSubst, Coercion.lookupTyVar, lookupCoVar,
  56         isEmptyCvSubst, zapCvSubstEnv, getCvInScope,
  57         substCo, substCos, substCoVar, substCoVars,
  58         substCoWithTy, substCoWithTys,
  59         cvTvSubst, tvCvSubst, mkCvSubst, zipOpenCvSubst,
  60         substTy, extendTvSubst, extendCvSubstAndInScope,
  61         substTyVarBndr, substCoVarBndr,
  62
  63         -- ** Lifting
  64         liftCoMatch, liftCoSubstTyVar, liftCoSubstWith,
  65
  66         -- ** Comparison
  67         coreEqCoercion, coreEqCoercion2,
  68
  69         -- ** Forcing evaluation of coercions
  70         seqCo,
  71
  72         -- * Pretty-printing
  73         pprCo, pprParendCo, pprCoAxiom,
  74
  75         -- * Other
  76         applyCo
  77        ) where
  78
  79 #include "HsVersions.h"
  80
  81 import Unify    ( MatchEnv(..), matchList )
  82 import TypeRep
  83 import qualified Type
  84 import Type hiding( substTy, substTyVarBndr, extendTvSubst )
  85 import TyCon
  86 import Var
  87 import VarEnv
  88 import VarSet
  89 import Maybes   ( orElse )
  90 import Name     ( Name, NamedThing(..), nameUnique )
  91 import OccName  ( parenSymOcc )
  92 import Util
  93 import BasicTypes
  94 import Outputable
  95 import Unique
  96 import Pair
  97 import PrelNames        ( funTyConKey, eqPrimTyConKey )
  98 import Control.Applicative
  99 import Data.Traversable (traverse, sequenceA)
 100 import Control.Arrow (second)
 101 import FastString
 102
 103 import qualified Data.Data as Data hiding ( TyCon )
 104 \end{code}
 105
 106 %************************************************************************
 107 %*                                                                      *
 108             Coercions
 109 %*                                                                      *
 110 %************************************************************************
 111
 112 \begin{code}
 113 -- | A 'Coercion' is concrete evidence of the equality/convertibility
 114 -- of two types.
 115
 116 data Coercion
 117   -- These ones mirror the shape of types
 118   = Refl Type  -- See Note [Refl invariant]
 119           -- Invariant: applications of (Refl T) to a bunch of identity coercions
 120           --            always show up as Refl.
 121           -- For example  (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
 122
 123           -- Applications of (Refl T) to some coercions, at least one of
 124           -- which is NOT the identity, show up as TyConAppCo.
 125           -- (They may not be fully saturated however.)
 126           -- ConAppCo coercions (like all coercions other than Refl)
 127           -- are NEVER the identity.
 128
 129   -- These ones simply lift the correspondingly-named
 130   -- Type constructors into Coercions
 131   | TyConAppCo TyCon [Coercion]    -- lift TyConApp
 132                -- The TyCon is never a synonym;
 133                -- we expand synonyms eagerly
 134                -- But it can be a type function
 135
 136   | AppCo Coercion Coercion        -- lift AppTy
 137
 138   -- See Note [Forall coercions]
 139   | ForAllCo TyVar Coercion       -- forall a. g
 140
 141   -- These are special
 142   | CoVarCo CoVar
 143   | AxiomInstCo CoAxiom [Coercion]  -- The coercion arguments always *precisely*
 144                                     -- saturate arity of CoAxiom.
 145                                     -- See [Coercion axioms applied to coercions]
 146   | UnsafeCo Type Type
 147   | SymCo Coercion
 148   | TransCo Coercion Coercion
 149
 150   -- These are destructors
 151   | NthCo Int Coercion          -- Zero-indexed
 152   | InstCo Coercion Type
 153   deriving (Data.Data, Data.Typeable)
 154 \end{code}
 155
 156
 157 Note [Refl invariant]
 158 ~~~~~~~~~~~~~~~~~~~~~
 159 Coercions have the following invariant
 160      Refl is always lifted as far as possible.
 161
 162 You might think that a consequencs is:
 163      Every identity coercions has Refl at the root
 164
 165 But that's not quite true because of coercion variables.  Consider
 166      g         where g :: Int~Int
 167      Left h    where h :: Maybe Int ~ Maybe Int
 168 etc.  So the consequence is only true of coercions that
 169 have no coercion variables.
 170
 171 Note [Coercion axioms applied to coercions]
 172 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 173 The reason coercion axioms can be applied to coercions and not just
 174 types is to allow for better optimization.  There are some cases where
 175 we need to be able to "push transitivity inside" an axiom in order to
 176 expose further opportunities for optimization.
 177
 178 For example, suppose we have
 179
 180   C a : t[a] ~ F a
 181   g   : b ~ c
 182
 183 and we want to optimize
 184
 185   sym (C b) ; t[g] ; C c
 186
 187 which has the kind
 188
 189   F b ~ F c
 190
 191 (stopping through t[b] and t[c] along the way).
 192
 193 We'd like to optimize this to just F g -- but how?  The key is
 194 that we need to allow axioms to be instantiated by *coercions*,
 195 not just by types.  Then we can (in certain cases) push
 196 transitivity inside the axiom instantiations, and then react
 197 opposite-polarity instantiations of the same axiom.  In this
 198 case, e.g., we match t[g] against the LHS of (C c)'s kind, to
 199 obtain the substitution  a |-> g  (note this operation is sort
 200 of the dual of lifting!) and hence end up with
 201
 202   C g : t[b] ~ F c
 203
 204 which indeed has the same kind as  t[g] ; C c.
 205
 206 Now we have
 207
 208   sym (C b) ; C g
 209
 210 which can be optimized to F g.
 211
 212
 213 Note [Forall coercions]
 214 ~~~~~~~~~~~~~~~~~~~~~~~
 215 Constructing coercions between forall-types can be a bit tricky.
 216 Currently, the situation is as follows:
 217
 218   ForAllCo TyVar Coercion
 219
 220 represents a coercion between polymorphic types, with the rule
 221
 222            v : k       g : t1 ~ t2
 223   ----------------------------------------------
 224   ForAllCo v g : (all v:k . t1) ~ (all v:k . t2)
 225
 226 Note that it's only necessary to coerce between polymorphic types
 227 where the type variables have identical kinds, because equality on
 228 kinds is trivial.
 229
 230 Note [Predicate coercions]
 231 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 232 Suppose we have
 233    g :: a~b
 234 How can we coerce between types
 235    ([c]~a) => [a] -> c
 236 and
 237    ([c]~b) => [b] -> c
 238 where the equality predicate *itself* differs?
 239
 240 Answer: we simply treat (~) as an ordinary type constructor, so these
 241 types really look like
 242
 243    ((~) [c] a) -> [a] -> c
 244    ((~) [c] b) -> [b] -> c
 245
 246 So the coercion between the two is obviously
 247
 248    ((~) [c] g) -> [g] -> c
 249
 250 Another way to see this to say that we simply collapse predicates to
 251 their representation type (see Type.coreView and Type.predTypeRep).
 252
 253 This collapse is done by mkPredCo; there is no PredCo constructor
 254 in Coercion.  This is important because we need Nth to work on
 255 predicates too:
 256     Nth 1 ((~) [c] g) = g
 257 See Simplify.simplCoercionF, which generates such selections.
 258
 259 Note [Kind coercions]
 260 ~~~~~~~~~~~~~~~~~~~~~
 261 Suppose T :: * -> *, and g :: A ~ B
 262 Then the coercion
 263    TyConAppCo T [g]      T g : T A ~ T B
 264
 265 Now suppose S :: forall k. k -> *, and g :: A ~ B
 266 Then the coercion
 267    TyConAppCo S [Refl *, g]   T <*> g : T * A ~ T * B
 268
 269 Notice that the arguments to TyConAppCo are coercions, but the first
 270 represents a *kind* coercion. Now, we don't allow any non-trivial kind
 271 coercions, so it's an invariant that any such kind coercions are Refl.
 272 Lint checks this.
 273
 274 However it's inconvenient to insist that these kind coercions are always
 275 *structurally* (Refl k), because the key function exprIsConApp_maybe
 276 pushes coercions into constructor arguments, so
 277        C k ty e |> g
 278 may turn into
 279        C (Nth 0 g) ....
 280 Now (Nth 0 g) will optimise to Refl, but perhaps not instantly.
 281
 282
 283 %************************************************************************
 284 %*                                                                      *
 285 \subsection{Coercion axioms}
 286 %*                                                                      *
 287 %************************************************************************
 288 These functions are not in TyCon because they need knowledge about
 289 the type representation (from TypeRep)
 290
 291 \begin{code}
 292 -- If `ax :: F a ~ b`, and `F` is a family instance, returns (F, [a])
 293 coAxiomSplitLHS :: CoAxiom -> (TyCon, [Type])
 294 coAxiomSplitLHS ax
 295   = case splitTyConApp_maybe (coAxiomLHS ax) of
 296       Just (tc,tys) -> (tc,tys)
 297       Nothing       -> pprPanic "coAxiomSplitLHS" (ppr ax)
 298 \end{code}
 299
 300 %************************************************************************
 301 %*                                                                      *
 302 \subsection{Coercion variables}
 303 %*                                                                      *
 304 %************************************************************************
 305
 306 \begin{code}
 307 coVarName :: CoVar -> Name
 308 coVarName = varName
 309
 310 setCoVarUnique :: CoVar -> Unique -> CoVar
 311 setCoVarUnique = setVarUnique
 312
 313 setCoVarName :: CoVar -> Name -> CoVar
 314 setCoVarName   = setVarName
 315
 316 isCoVar :: Var -> Bool
 317 isCoVar v = isCoVarType (varType v)
 318
 319 isCoVarType :: Type -> Bool
 320 isCoVarType ty      -- Tests for t1 ~# t2, the unboxed equality
 321   | Just tc <- tyConAppTyCon_maybe ty = tc `hasKey` eqPrimTyConKey
 322   | otherwise                         = False
 323 \end{code}
 324
 325
 326 \begin{code}
 327 tyCoVarsOfCo :: Coercion -> VarSet
 328 -- Extracts type and coercion variables from a coercion
 329 tyCoVarsOfCo (Refl ty)           = tyVarsOfType ty
 330 tyCoVarsOfCo (TyConAppCo _ cos)  = tyCoVarsOfCos cos
 331 tyCoVarsOfCo (AppCo co1 co2)     = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
 332 tyCoVarsOfCo (ForAllCo tv co)    = tyCoVarsOfCo co `delVarSet` tv
 333 tyCoVarsOfCo (CoVarCo v)         = unitVarSet v
 334 tyCoVarsOfCo (AxiomInstCo _ cos) = tyCoVarsOfCos cos
 335 tyCoVarsOfCo (UnsafeCo ty1 ty2)  = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
 336 tyCoVarsOfCo (SymCo co)          = tyCoVarsOfCo co
 337 tyCoVarsOfCo (TransCo co1 co2)   = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
 338 tyCoVarsOfCo (NthCo _ co)        = tyCoVarsOfCo co
 339 tyCoVarsOfCo (InstCo co ty)      = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
 340
 341 tyCoVarsOfCos :: [Coercion] -> VarSet
 342 tyCoVarsOfCos cos = foldr (unionVarSet . tyCoVarsOfCo) emptyVarSet cos
 343
 344 coVarsOfCo :: Coercion -> VarSet
 345 -- Extract *coerction* variables only.  Tiresome to repeat the code, but easy.
 346 coVarsOfCo (Refl _)            = emptyVarSet
 347 coVarsOfCo (TyConAppCo _ cos)  = coVarsOfCos cos
 348 coVarsOfCo (AppCo co1 co2)     = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
 349 coVarsOfCo (ForAllCo _ co)     = coVarsOfCo co
 350 coVarsOfCo (CoVarCo v)         = unitVarSet v
 351 coVarsOfCo (AxiomInstCo _ cos) = coVarsOfCos cos
 352 coVarsOfCo (UnsafeCo _ _)      = emptyVarSet
 353 coVarsOfCo (SymCo co)          = coVarsOfCo co
 354 coVarsOfCo (TransCo co1 co2)   = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
 355 coVarsOfCo (NthCo _ co)        = coVarsOfCo co
 356 coVarsOfCo (InstCo co _)       = coVarsOfCo co
 357
 358 coVarsOfCos :: [Coercion] -> VarSet
 359 coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos
 360
 361 coercionSize :: Coercion -> Int
 362 coercionSize (Refl ty)           = typeSize ty
 363 coercionSize (TyConAppCo _ cos)  = 1 + sum (map coercionSize cos)
 364 coercionSize (AppCo co1 co2)     = coercionSize co1 + coercionSize co2
 365 coercionSize (ForAllCo _ co)     = 1 + coercionSize co
 366 coercionSize (CoVarCo _)         = 1
 367 coercionSize (AxiomInstCo _ cos) = 1 + sum (map coercionSize cos)
 368 coercionSize (UnsafeCo ty1 ty2)  = typeSize ty1 + typeSize ty2
 369 coercionSize (SymCo co)          = 1 + coercionSize co
 370 coercionSize (TransCo co1 co2)   = 1 + coercionSize co1 + coercionSize co2
 371 coercionSize (NthCo _ co)        = 1 + coercionSize co
 372 coercionSize (InstCo co ty)      = 1 + coercionSize co + typeSize ty
 373 \end{code}
 374
 375 %************************************************************************
 376 %*                                                                      *
 377                    Pretty-printing coercions
 378 %*                                                                      *
 379 %************************************************************************
 380
 381 @pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
 382 function is defined to use this.  @pprParendCo@ is the same, except it
 383 puts parens around the type, except for the atomic cases.
 384 @pprParendCo@ works just by setting the initial context precedence
 385 very high.
 386
 387 \begin{code}
 388 instance Outputable Coercion where
 389   ppr = pprCo
 390
 391 pprCo, pprParendCo :: Coercion -> SDoc
 392 pprCo       co = ppr_co TopPrec   co
 393 pprParendCo co = ppr_co TyConPrec co
 394
 395 ppr_co :: Prec -> Coercion -> SDoc
 396 ppr_co _ (Refl ty) = angleBrackets (ppr ty)
 397
 398 ppr_co p co@(TyConAppCo tc [_,_])
 399   | tc `hasKey` funTyConKey = ppr_fun_co p co
 400
 401 ppr_co p (TyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos
 402 ppr_co p (AppCo co1 co2)       = maybeParen p TyConPrec $
 403                                  pprCo co1 <+> ppr_co TyConPrec co2
 404 ppr_co p co@(ForAllCo {})      = ppr_forall_co p co
 405 ppr_co _ (CoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
 406 ppr_co p (AxiomInstCo con cos) = pprTypeNameApp p ppr_co (getName con) cos
 407
 408 ppr_co p (TransCo co1 co2) = maybeParen p FunPrec $
 409                              ppr_co FunPrec co1
 410                              <+> ptext (sLit ";")
 411                              <+> ppr_co FunPrec co2
 412 ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
 413                           pprParendCo co <> ptext (sLit "@") <> pprType ty
 414
 415 ppr_co p (UnsafeCo ty1 ty2) = pprPrefixApp p (ptext (sLit "UnsafeCo"))
 416                                            [pprParendType ty1, pprParendType ty2]
 417 ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
 418 ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendCo co]
 419
 420
 421 ppr_fun_co :: Prec -> Coercion -> SDoc
 422 ppr_fun_co p co = pprArrowChain p (split co)
 423   where
 424     split :: Coercion -> [SDoc]
 425     split (TyConAppCo f [arg,res])
 426       | f `hasKey` funTyConKey
 427       = ppr_co FunPrec arg : split res
 428     split co = [ppr_co TopPrec co]
 429
 430 ppr_forall_co :: Prec -> Coercion -> SDoc
 431 ppr_forall_co p ty
 432   = maybeParen p FunPrec $
 433     sep [pprForAll tvs, ppr_co TopPrec rho]
 434   where
 435     (tvs,  rho) = split1 [] ty
 436     split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
 437     split1 tvs ty               = (reverse tvs, ty)
 438 \end{code}
 439
 440 \begin{code}
 441 pprCoAxiom :: CoAxiom -> SDoc
 442 pprCoAxiom ax
 443   = sep [ ptext (sLit "axiom") <+> ppr ax <+> ppr (co_ax_tvs ax)
 444         , nest 2 (dcolon <+> pprEqPred (Pair (co_ax_lhs ax) (co_ax_rhs ax))) ]
 445 \end{code}
 446
 447 %************************************************************************
 448 %*                                                                      *
 449         Functions over Kinds
 450 %*                                                                      *
 451 %************************************************************************
 452
 453 \begin{code}
 454 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
 455 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
 456 --
 457 -- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
 458 decomposeCo :: Arity -> Coercion -> [Coercion]
 459 decomposeCo arity co = [mkNthCo n co | n <- [0..(arity-1)] ]
 460                        -- Remember, Nth is zero-indexed
 461
 462 -- | Attempts to obtain the type variable underlying a 'Coercion'
 463 getCoVar_maybe :: Coercion -> Maybe CoVar
 464 getCoVar_maybe (CoVarCo cv) = Just cv
 465 getCoVar_maybe _            = Nothing
 466
 467 -- | Attempts to tease a coercion apart into a type constructor and the application
 468 -- of a number of coercion arguments to that constructor
 469 splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
 470 splitTyConAppCo_maybe (Refl ty)           = (fmap . second . map) Refl (splitTyConApp_maybe ty)
 471 splitTyConAppCo_maybe (TyConAppCo tc cos) = Just (tc, cos)
 472 splitTyConAppCo_maybe _                   = Nothing
 473
 474 splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
 475 -- ^ Attempt to take a coercion application apart.
 476 splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
 477 splitAppCo_maybe (TyConAppCo tc cos)
 478   | isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc
 479   , Just (cos', co') <- snocView cos
 480   = Just (mkTyConAppCo tc cos', co')    -- Never create unsaturated type family apps!
 481        -- Use mkTyConAppCo to preserve the invariant
 482        --  that identity coercions are always represented by Refl
 483 splitAppCo_maybe (Refl ty)
 484   | Just (ty1, ty2) <- splitAppTy_maybe ty
 485   = Just (Refl ty1, Refl ty2)
 486 splitAppCo_maybe _ = Nothing
 487
 488 splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
 489 splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
 490 splitForAllCo_maybe _                = Nothing
 491
 492 -------------------------------------------------------
 493 -- and some coercion kind stuff
 494
 495 coVarKind :: CoVar -> (Type,Type)
 496 coVarKind cv
 497  | Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
 498  = ASSERT (tc `hasKey` eqPrimTyConKey)
 499    (ty1,ty2)
 500  | otherwise = panic "coVarKind, non coercion variable"
 501
 502 -- | Makes a coercion type from two types: the types whose equality
 503 -- is proven by the relevant 'Coercion'
 504 mkCoercionType :: Type -> Type -> Type
 505 mkCoercionType = curry mkPrimEqType
 506
 507 isReflCo :: Coercion -> Bool
 508 isReflCo (Refl {}) = True
 509 isReflCo _         = False
 510
 511 isReflCo_maybe :: Coercion -> Maybe Type
 512 isReflCo_maybe (Refl ty) = Just ty
 513 isReflCo_maybe _         = Nothing
 514 \end{code}
 515
 516 %************************************************************************
 517 %*                                                                      *
 518             Building coercions
 519 %*                                                                      *
 520 %************************************************************************
 521
 522 \begin{code}
 523 mkCoVarCo :: CoVar -> Coercion
 524 -- cv :: s ~# t
 525 mkCoVarCo cv
 526   | ty1 `eqType` ty2 = Refl ty1
 527   | otherwise        = CoVarCo cv
 528   where
 529     (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
 530
 531 mkReflCo :: Type -> Coercion
 532 mkReflCo = Refl
 533
 534 mkAxInstCo :: CoAxiom -> [Type] -> Coercion
 535 -- mkAxInstCo can legitimately be called over-staturated;
 536 -- i.e. with more type arguments than the coercion requires
 537 mkAxInstCo ax tys
 538   | arity == n_tys = AxiomInstCo ax rtys
 539   | otherwise      = ASSERT( arity < n_tys )
 540                      foldl AppCo (AxiomInstCo ax (take arity rtys))
 541                                  (drop arity rtys)
 542   where
 543     n_tys = length tys
 544     arity = coAxiomArity ax
 545     rtys  = map Refl tys
 546
 547 mkAxInstRHS :: CoAxiom -> [Type] -> Type
 548 -- Instantiate the axiom with specified types,
 549 -- returning the instantiated RHS
 550 -- A companion to mkAxInstCo:
 551 --    mkAxInstRhs ax tys = snd (coercionKind (mkAxInstCo ax tys))
 552 mkAxInstRHS ax tys
 553   = ASSERT( tvs `equalLength` tys1 )
 554     mkAppTys rhs' tys2
 555   where
 556     tvs          = coAxiomTyVars ax
 557     (tys1, tys2) = splitAtList tvs tys
 558     rhs'         = substTyWith tvs tys1 (coAxiomRHS ax)
 559
 560 -- | Apply a 'Coercion' to another 'Coercion'.
 561 mkAppCo :: Coercion -> Coercion -> Coercion
 562 mkAppCo (Refl ty1) (Refl ty2)       = Refl (mkAppTy ty1 ty2)
 563 mkAppCo (Refl (TyConApp tc tys)) co = TyConAppCo tc (map Refl tys ++ [co])
 564 mkAppCo (TyConAppCo tc cos) co      = TyConAppCo tc (cos ++ [co])
 565 mkAppCo co1 co2                     = AppCo co1 co2
 566 -- Note, mkAppCo is careful to maintain invariants regarding
 567 -- where Refl constructors appear; see the comments in the definition
 568 -- of Coercion and the Note [Refl invariant] in types/TypeRep.lhs.
 569
 570 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
 571 -- See also 'mkAppCo'
 572 mkAppCos :: Coercion -> [Coercion] -> Coercion
 573 mkAppCos co1 tys = foldl mkAppCo co1 tys
 574
 575 -- | Apply a type constructor to a list of coercions.
 576 mkTyConAppCo :: TyCon -> [Coercion] -> Coercion
 577 mkTyConAppCo tc cos
 578                -- Expand type synonyms
 579   | Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos
 580   = mkAppCos (liftCoSubst tv_co_prs rhs_ty) leftover_cos
 581
 582   | Just tys <- traverse isReflCo_maybe cos
 583   = Refl (mkTyConApp tc tys)    -- See Note [Refl invariant]
 584
 585   | otherwise = TyConAppCo tc cos
 586
 587 -- | Make a function 'Coercion' between two other 'Coercion's
 588 mkFunCo :: Coercion -> Coercion -> Coercion
 589 mkFunCo co1 co2 = mkTyConAppCo funTyCon [co1, co2]
 590
 591 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
 592 mkForAllCo :: Var -> Coercion -> Coercion
 593 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
 594 mkForAllCo tv (Refl ty) = ASSERT( isTyVar tv ) Refl (mkForAllTy tv ty)
 595 mkForAllCo tv  co       = ASSERT ( isTyVar tv ) ForAllCo tv co
 596
 597 -------------------------------
 598
 599 -- | Create a symmetric version of the given 'Coercion' that asserts
 600 --   equality between the same types but in the other "direction", so
 601 --   a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
 602 mkSymCo :: Coercion -> Coercion
 603
 604 -- Do a few simple optimizations, but don't bother pushing occurrences
 605 -- of symmetry to the leaves; the optimizer will take care of that.
 606 mkSymCo co@(Refl {})              = co
 607 mkSymCo    (UnsafeCo ty1 ty2)    = UnsafeCo ty2 ty1
 608 mkSymCo    (SymCo co)            = co
 609 mkSymCo co                       = SymCo co
 610
 611 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
 612 mkTransCo :: Coercion -> Coercion -> Coercion
 613 mkTransCo (Refl _) co = co
 614 mkTransCo co (Refl _) = co
 615 mkTransCo co1 co2     = TransCo co1 co2
 616
 617 mkNthCo :: Int -> Coercion -> Coercion
 618 mkNthCo n (Refl ty) = Refl (tyConAppArgN n ty)
 619 mkNthCo n co        = NthCo n co
 620
 621 -- | Instantiates a 'Coercion' with a 'Type' argument.
 622 mkInstCo :: Coercion -> Type -> Coercion
 623 mkInstCo co ty = InstCo co ty
 624
 625 -- | Manufacture a coercion from thin air. Needless to say, this is
 626 --   not usually safe, but it is used when we know we are dealing with
 627 --   bottom, which is one case in which it is safe.  This is also used
 628 --   to implement the @unsafeCoerce#@ primitive.  Optimise by pushing
 629 --   down through type constructors.
 630 mkUnsafeCo :: Type -> Type -> Coercion
 631 mkUnsafeCo ty1 ty2 | ty1 `eqType` ty2 = Refl ty1
 632 mkUnsafeCo (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 633   | tc1 == tc2
 634   = mkTyConAppCo tc1 (zipWith mkUnsafeCo tys1 tys2)
 635
 636 mkUnsafeCo (FunTy a1 r1) (FunTy a2 r2)
 637   = mkFunCo (mkUnsafeCo a1 a2) (mkUnsafeCo r1 r2)
 638
 639 mkUnsafeCo ty1 ty2 = UnsafeCo ty1 ty2
 640
 641 -- See note [Newtype coercions] in TyCon
 642
 643 -- | Create a coercion constructor (axiom) suitable for the given
 644 --   newtype 'TyCon'. The 'Name' should be that of a new coercion
 645 --   'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
 646 --   the type the appropriate right hand side of the @newtype@, with
 647 --   the free variables a subset of those 'TyVar's.
 648 mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom
 649 mkNewTypeCo name tycon tvs rhs_ty
 650   = CoAxiom { co_ax_unique   = nameUnique name
 651             , co_ax_name     = name
 652             , co_ax_implicit = True  -- See Note [Implicit axioms] in TyCon
 653             , co_ax_tvs      = tvs
 654             , co_ax_lhs      = mkTyConApp tycon (mkTyVarTys tvs)
 655             , co_ax_rhs      = rhs_ty }
 656
 657 mkPiCos :: [Var] -> Coercion -> Coercion
 658 mkPiCos vs co = foldr mkPiCo co vs
 659
 660 mkPiCo  :: Var -> Coercion -> Coercion
 661 mkPiCo v co | isTyVar v = mkForAllCo v co
 662             | otherwise = mkFunCo (mkReflCo (varType v)) co
 663 \end{code}
 664
 665 %************************************************************************
 666 %*                                                                      *
 667             Newtypes
 668 %*                                                                      *
 669 %************************************************************************
 670
 671 \begin{code}
 672 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
 673 -- ^ If @co :: T ts ~ rep_ty@ then:
 674 --
 675 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
 676 instNewTyCon_maybe tc tys
 677   | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc
 678   = ASSERT( tys `lengthIs` tyConArity tc )
 679     Just (substTyWith tvs tys ty, mkAxInstCo co_tc tys)
 680   | otherwise
 681   = Nothing
 682
 683 -- this is here to avoid module loops
 684 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 685 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
 686 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
 687 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
 688 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
 689 --
 690 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
 691 --
 692 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
 693 splitNewTypeRepCo_maybe ty
 694   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 695 splitNewTypeRepCo_maybe (TyConApp tc tys)
 696   | Just (ty', co) <- instNewTyCon_maybe tc tys
 697   = case co of
 698         Refl _ -> panic "splitNewTypeRepCo_maybe"
 699                         -- This case handled by coreView
 700         _      -> Just (ty', co)
 701 splitNewTypeRepCo_maybe _
 702   = Nothing
 703
 704 -- | Determines syntactic equality of coercions
 705 coreEqCoercion :: Coercion -> Coercion -> Bool
 706 coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
 707   where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
 708
 709 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
 710 coreEqCoercion2 env (Refl ty1) (Refl ty2) = eqTypeX env ty1 ty2
 711 coreEqCoercion2 env (TyConAppCo tc1 cos1) (TyConAppCo tc2 cos2)
 712   = tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2
 713
 714 coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22)
 715   = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
 716
 717 coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2)
 718   = coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2
 719
 720 coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2)
 721   = rnOccL env cv1 == rnOccR env cv2
 722
 723 coreEqCoercion2 env (AxiomInstCo con1 cos1) (AxiomInstCo con2 cos2)
 724   = con1 == con2
 725     && all2 (coreEqCoercion2 env) cos1 cos2
 726
 727 coreEqCoercion2 env (UnsafeCo ty11 ty12) (UnsafeCo ty21 ty22)
 728   = eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
 729
 730 coreEqCoercion2 env (SymCo co1) (SymCo co2)
 731   = coreEqCoercion2 env co1 co2
 732
 733 coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
 734   = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
 735
 736 coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
 737   = d1 == d2 && coreEqCoercion2 env co1 co2
 738
 739 coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
 740   = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
 741
 742 coreEqCoercion2 _ _ _ = False
 743 \end{code}
 744
 745 %************************************************************************
 746 %*                                                                      *
 747                    Substitution of coercions
 748 %*                                                                      *
 749 %************************************************************************
 750
 751 \begin{code}
 752 -- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
 753 --   doing a \"lifting\" substitution)
 754 type CvSubstEnv = VarEnv Coercion
 755
 756 emptyCvSubstEnv :: CvSubstEnv
 757 emptyCvSubstEnv = emptyVarEnv
 758
 759 data CvSubst
 760   = CvSubst InScopeSet  -- The in-scope type variables
 761             TvSubstEnv  -- Substitution of types
 762             CvSubstEnv  -- Substitution of coercions
 763
 764 instance Outputable CvSubst where
 765   ppr (CvSubst ins tenv cenv)
 766     = brackets $ sep[ ptext (sLit "CvSubst"),
 767                       nest 2 (ptext (sLit "In scope:") <+> ppr ins),
 768                       nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
 769                       nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
 770
 771 emptyCvSubst :: CvSubst
 772 emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
 773
 774 isEmptyCvSubst :: CvSubst -> Bool
 775 isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
 776
 777 getCvInScope :: CvSubst -> InScopeSet
 778 getCvInScope (CvSubst in_scope _ _) = in_scope
 779
 780 zapCvSubstEnv :: CvSubst -> CvSubst
 781 zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
 782
 783 cvTvSubst :: CvSubst -> TvSubst
 784 cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
 785
 786 tvCvSubst :: TvSubst -> CvSubst
 787 tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
 788
 789 extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
 790 extendTvSubst (CvSubst in_scope tenv cenv) tv ty
 791   = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
 792
 793 extendCvSubstAndInScope :: CvSubst -> CoVar -> Coercion -> CvSubst
 794 -- Also extends the in-scope set
 795 extendCvSubstAndInScope (CvSubst in_scope tenv cenv) cv co
 796   = CvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfCo co)
 797             tenv
 798             (extendVarEnv cenv cv co)
 799
 800 substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
 801 substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
 802   = ASSERT( isCoVar old_var )
 803     (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
 804   where
 805     -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
 806     -- In that case, mkCoVarCo will return a ReflCoercion, and
 807     -- we want to substitute that (not new_var) for old_var
 808     new_co    = mkCoVarCo new_var
 809     no_change = new_var == old_var && not (isReflCo new_co)
 810
 811     new_cenv | no_change = delVarEnv cenv old_var
 812              | otherwise = extendVarEnv cenv old_var new_co
 813
 814     new_var = uniqAway in_scope subst_old_var
 815     subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
 816                   -- It's important to do the substitution for coercions,
 817                   -- because they can have free type variables
 818
 819 substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
 820 substTyVarBndr (CvSubst in_scope tenv cenv) old_var
 821   = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
 822       (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
 823
 824 mkCvSubst :: InScopeSet -> [(Var,Coercion)] -> CvSubst
 825 mkCvSubst in_scope prs = CvSubst in_scope Type.emptyTvSubstEnv (mkVarEnv prs)
 826
 827 zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
 828 zipOpenCvSubst vs cos
 829   | debugIsOn && (length vs /= length cos)
 830   = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
 831   | otherwise
 832   = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
 833
 834 substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
 835 substCoWithTy in_scope tv ty = substCoWithTys in_scope [tv] [ty]
 836
 837 substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
 838 substCoWithTys in_scope tvs tys co
 839   | debugIsOn && (length tvs /= length tys)
 840   = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
 841   | otherwise
 842   = ASSERT( length tvs == length tys )
 843     substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
 844
 845 -- | Substitute within a 'Coercion'
 846 substCo :: CvSubst -> Coercion -> Coercion
 847 substCo subst co | isEmptyCvSubst subst = co
 848                  | otherwise            = subst_co subst co
 849
 850 -- | Substitute within several 'Coercion's
 851 substCos :: CvSubst -> [Coercion] -> [Coercion]
 852 substCos subst cos | isEmptyCvSubst subst = cos
 853                    | otherwise            = map (substCo subst) cos
 854
 855 substTy :: CvSubst -> Type -> Type
 856 substTy subst = Type.substTy (cvTvSubst subst)
 857
 858 subst_co :: CvSubst -> Coercion -> Coercion
 859 subst_co subst co
 860   = go co
 861   where
 862     go_ty :: Type -> Type
 863     go_ty = Coercion.substTy subst
 864
 865     go :: Coercion -> Coercion
 866     go (Refl ty)             = Refl $! go_ty ty
 867     go (TyConAppCo tc cos)   = let args = map go cos
 868                                in  args `seqList` TyConAppCo tc args
 869     go (AppCo co1 co2)       = mkAppCo (go co1) $! go co2
 870     go (ForAllCo tv co)      = case substTyVarBndr subst tv of
 871                                  (subst', tv') ->
 872                                    ForAllCo tv' $! subst_co subst' co
 873     go (CoVarCo cv)          = substCoVar subst cv
 874     go (AxiomInstCo con cos) = AxiomInstCo con $! map go cos
 875     go (UnsafeCo ty1 ty2)    = (UnsafeCo $! go_ty ty1) $! go_ty ty2
 876     go (SymCo co)            = mkSymCo (go co)
 877     go (TransCo co1 co2)     = mkTransCo (go co1) (go co2)
 878     go (NthCo d co)          = mkNthCo d (go co)
 879     go (InstCo co ty)        = mkInstCo (go co) $! go_ty ty
 880
 881 substCoVar :: CvSubst -> CoVar -> Coercion
 882 substCoVar (CvSubst in_scope _ cenv) cv
 883   | Just co  <- lookupVarEnv cenv cv      = co
 884   | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
 885   | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope)
 886                 ASSERT( isCoVar cv ) CoVarCo cv
 887
 888 substCoVars :: CvSubst -> [CoVar] -> [Coercion]
 889 substCoVars subst cvs = map (substCoVar subst) cvs
 890
 891 lookupTyVar :: CvSubst -> TyVar  -> Maybe Type
 892 lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
 893
 894 lookupCoVar :: CvSubst -> Var  -> Maybe Coercion
 895 lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
 896 \end{code}
 897
 898 %************************************************************************
 899 %*                                                                      *
 900                    "Lifting" substitution
 901            [(TyVar,Coercion)] -> Type -> Coercion
 902 %*                                                                      *
 903 %************************************************************************
 904
 905 \begin{code}
 906 data LiftCoSubst = LCS InScopeSet LiftCoEnv
 907
 908 type LiftCoEnv = VarEnv Coercion
 909      -- Maps *type variables* to *coercions*
 910      -- That's the whole point of this function!
 911
 912 liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
 913 liftCoSubstWith tvs cos ty
 914   = liftCoSubst (zipEqual "liftCoSubstWith" tvs cos) ty
 915
 916 liftCoSubst :: [(TyVar,Coercion)] -> Type -> Coercion
 917 liftCoSubst prs ty
 918  | null prs  = Refl ty
 919  | otherwise = ty_co_subst (LCS (mkInScopeSet (tyCoVarsOfCos (map snd prs)))
 920                                 (mkVarEnv prs)) ty
 921
 922 -- | The \"lifting\" operation which substitutes coercions for type
 923 --   variables in a type to produce a coercion.
 924 --
 925 --   For the inverse operation, see 'liftCoMatch'
 926 ty_co_subst :: LiftCoSubst -> Type -> Coercion
 927 ty_co_subst subst ty
 928   = go ty
 929   where
 930     go (TyVarTy tv)      = liftCoSubstTyVar subst tv `orElse` Refl (TyVarTy tv)
 931                              -- A type variable from a non-cloned forall
 932                              -- won't be in the substitution
 933     go (AppTy ty1 ty2)   = mkAppCo (go ty1) (go ty2)
 934     go (TyConApp tc tys) = mkTyConAppCo tc (map go tys)
 935                            -- IA0_NOTE: Do we need to do anything
 936                            -- about kind instantiations? I don't think
 937                            -- so.  see Note [Kind coercions]
 938     go (FunTy ty1 ty2)   = mkFunCo (go ty1) (go ty2)
 939     go (ForAllTy v ty)   = mkForAllCo v' $! (ty_co_subst subst' ty)
 940                          where
 941                            (subst', v') = liftCoSubstTyVarBndr subst v
 942
 943 liftCoSubstTyVar :: LiftCoSubst -> TyVar -> Maybe Coercion
 944 liftCoSubstTyVar (LCS _ cenv) tv = lookupVarEnv cenv tv
 945
 946 liftCoSubstTyVarBndr :: LiftCoSubst -> TyVar -> (LiftCoSubst, TyVar)
 947 liftCoSubstTyVarBndr (LCS in_scope cenv) old_var
 948   = (LCS (in_scope `extendInScopeSet` new_var) new_cenv, new_var)
 949   where
 950     new_cenv | no_change = delVarEnv cenv old_var
 951              | otherwise = extendVarEnv cenv old_var (Refl (TyVarTy new_var))
 952
 953     no_change = new_var == old_var
 954     new_var = uniqAway in_scope old_var
 955 \end{code}
 956
 957 \begin{code}
 958 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
 959 --   @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
 960 --   That is, it matches a type against a coercion of the same
 961 --   "shape", and returns a lifting substitution which could have been
 962 --   used to produce the given coercion from the given type.
 963 liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst
 964 liftCoMatch tmpls ty co
 965   = case ty_co_match menv emptyVarEnv ty co of
 966       Just cenv -> Just (LCS in_scope cenv)
 967       Nothing   -> Nothing
 968   where
 969     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
 970     in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
 971     -- Like tcMatchTy, assume all the interesting variables
 972     -- in ty are in tmpls
 973
 974 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
 975 ty_co_match :: MatchEnv -> LiftCoEnv -> Type -> Coercion -> Maybe LiftCoEnv
 976 ty_co_match menv subst ty co
 977   | Just ty' <- coreView ty = ty_co_match menv subst ty' co
 978
 979   -- Match a type variable against a non-refl coercion
 980 ty_co_match menv cenv (TyVarTy tv1) co
 981   | Just co1' <- lookupVarEnv cenv tv1'      -- tv1' is already bound to co1
 982   = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
 983     then Just cenv
 984     else Nothing       -- no match since tv1 matches two different coercions
 985
 986   | tv1' `elemVarSet` me_tmpls menv           -- tv1' is a template var
 987   = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
 988     then Nothing      -- occurs check failed
 989     else return (extendVarEnv cenv tv1' co)
 990         -- BAY: I don't think we need to do any kind matching here yet
 991         -- (compare 'match'), but we probably will when moving to SHE.
 992
 993   | otherwise    -- tv1 is not a template ty var, so the only thing it
 994                  -- can match is a reflexivity coercion for itself.
 995                  -- But that case is dealt with already
 996   = Nothing
 997
 998   where
 999     rn_env = me_env menv
1000     tv1' = rnOccL rn_env tv1
1001
1002 ty_co_match menv subst (AppTy ty1 ty2) co
1003   | Just (co1, co2) <- splitAppCo_maybe co      -- c.f. Unify.match on AppTy
1004   = do { subst' <- ty_co_match menv subst ty1 co1
1005        ; ty_co_match menv subst' ty2 co2 }
1006
1007 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo tc2 cos)
1008   | tc1 == tc2 = ty_co_matches menv subst tys cos
1009
1010 ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos)
1011   | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
1012
1013 ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co)
1014   = ty_co_match menv' subst ty co
1015   where
1016     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
1017
1018 ty_co_match menv subst ty co
1019   | Just co' <- pushRefl co = ty_co_match menv subst ty co'
1020   | otherwise               = Nothing
1021
1022 ty_co_matches :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion] -> Maybe LiftCoEnv
1023 ty_co_matches menv = matchList (ty_co_match menv)
1024
1025 pushRefl :: Coercion -> Maybe Coercion
1026 pushRefl (Refl (AppTy ty1 ty2))   = Just (AppCo (Refl ty1) (Refl ty2))
1027 pushRefl (Refl (FunTy ty1 ty2))   = Just (TyConAppCo funTyCon [Refl ty1, Refl ty2])
1028 pushRefl (Refl (TyConApp tc tys)) = Just (TyConAppCo tc (map Refl tys))
1029 pushRefl (Refl (ForAllTy tv ty))  = Just (ForAllCo tv (Refl ty))
1030 pushRefl _                        = Nothing
1031 \end{code}
1032
1033 %************************************************************************
1034 %*                                                                      *
1035             Sequencing on coercions
1036 %*                                                                      *
1037 %************************************************************************
1038
1039 \begin{code}
1040 seqCo :: Coercion -> ()
1041 seqCo (Refl ty)             = seqType ty
1042 seqCo (TyConAppCo tc cos)   = tc `seq` seqCos cos
1043 seqCo (AppCo co1 co2)       = seqCo co1 `seq` seqCo co2
1044 seqCo (ForAllCo tv co)      = tv `seq` seqCo co
1045 seqCo (CoVarCo cv)          = cv `seq` ()
1046 seqCo (AxiomInstCo con cos) = con `seq` seqCos cos
1047 seqCo (UnsafeCo ty1 ty2)    = seqType ty1 `seq` seqType ty2
1048 seqCo (SymCo co)            = seqCo co
1049 seqCo (TransCo co1 co2)     = seqCo co1 `seq` seqCo co2
1050 seqCo (NthCo _ co)          = seqCo co
1051 seqCo (InstCo co ty)        = seqCo co `seq` seqType ty
1052
1053 seqCos :: [Coercion] -> ()
1054 seqCos []       = ()
1055 seqCos (co:cos) = seqCo co `seq` seqCos cos
1056 \end{code}
1057
1058
1059 %************************************************************************
1060 %*                                                                      *
1061              The kind of a type, and of a coercion
1062 %*                                                                      *
1063 %************************************************************************
1064
1065 \begin{code}
1066 coercionType :: Coercion -> Type
1067 coercionType co = case coercionKind co of
1068                     Pair ty1 ty2 -> mkCoercionType ty1 ty2
1069
1070 ------------------
1071 -- | If it is the case that
1072 --
1073 -- > c :: (t1 ~ t2)
1074 --
1075 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
1076
1077 coercionKind :: Coercion -> Pair Type
1078 coercionKind co = go co
1079   where
1080     go (Refl ty)            = Pair ty ty
1081     go (TyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
1082     go (AppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
1083     go (ForAllCo tv co)     = mkForAllTy tv <$> go co
1084     go (CoVarCo cv)         = toPair $ coVarKind cv
1085     go (AxiomInstCo ax cos) = let Pair tys1 tys2 = sequenceA $ map go cos
1086                               in  Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax))
1087                                        (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax))
1088     go (UnsafeCo ty1 ty2)   = Pair ty1 ty2
1089     go (SymCo co)           = swap $ go co
1090     go (TransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)
1091     go (NthCo d co)         = tyConAppArgN d <$> go co
1092     go (InstCo aco ty)      = go_app aco [ty]
1093
1094     go_app :: Coercion -> [Type] -> Pair Type
1095     -- Collect up all the arguments and apply all at once
1096     -- See Note [Nested InstCos]
1097     go_app (InstCo co ty) tys = go_app co (ty:tys)
1098     go_app co             tys = (`applyTys` tys) <$> go co
1099
1100 -- | Apply 'coercionKind' to multiple 'Coercion's
1101 coercionKinds :: [Coercion] -> Pair [Type]
1102 coercionKinds tys = sequenceA $ map coercionKind tys
1103 \end{code}
1104
1105 Note [Nested InstCos]
1106 ~~~~~~~~~~~~~~~~~~~~~
1107 In Trac #5631 we found that 70% of the entire compilation time was
1108 being spent in coercionKind!  The reason was that we had
1109    (g @ ty1 @ ty2 .. @ ty100)    -- The "@s" are InstCos
1110 where
1111    g :: forall a1 a2 .. a100. phi
1112 If we deal with the InstCos one at a time, we'll do this:
1113    1.  Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
1114    2.  Substitute phi'[ ty100/a100 ], a single tyvar->type subst
1115 But this is a *quadratic* algorithm, and the blew up Trac #5631.
1116 So it's very important to do the substitution simultaneously.
1117
1118 cf Type.applyTys (which in fact we call here)
1119
1120
1121 \begin{code}
1122 applyCo :: Type -> Coercion -> Type
1123 -- Gives the type of (e co) where e :: (a~b) => ty
1124 applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
1125 applyCo (FunTy _ ty) _ = ty
1126 applyCo _            _ = panic "applyCo"
1127 \end{code}
1128
1129 Note [Kind coercions]
1130 ~~~~~~~~~~~~~~~~~~~~~
1131 Kind coercions are only of the form: Refl kind. They are only used to
1132 instantiate kind polymorphic type constructors in TyConAppCo. Remember
1133 that kind instantiation only happens with TyConApp, not AppTy.