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