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