Merge remote-tracking branch 'origin/master' into type-nats
authorIavor S. Diatchki <iavor.diatchki@gmail.com>
Wed, 25 Jan 2012 03:40:06 +0000 (19:40 -0800)
committerIavor S. Diatchki <iavor.diatchki@gmail.com>
Wed, 25 Jan 2012 03:40:06 +0000 (19:40 -0800)
Conflicts:
compiler/typecheck/TcEvidence.lhs

18 files changed:
1  2 
compiler/deSugar/DsBinds.lhs
compiler/deSugar/DsExpr.lhs
compiler/deSugar/Match.lhs
compiler/iface/BinIface.hs
compiler/iface/TcIface.lhs
compiler/parser/Parser.y.pp
compiler/prelude/PrelNames.lhs
compiler/rename/RnTypes.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcEvidence.lhs
compiler/typecheck/TcForeign.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSplice.lhs
compiler/types/Coercion.lhs
compiler/vectorise/Vectorise/Type/Classify.hs
mk/validate-settings.mk

@@@ -64,11 -63,12 +64,13 @@@ import Maybe
  import OrdList
  import Bag
  import BasicTypes hiding ( TopLevel )
+ import DynFlags
  import FastString
+ import ErrUtils( MsgDoc )
  import Util
+ import Control.Monad( when )
  import MonadUtils
 +import Control.Monad(liftM)
  \end{code}
  
  %************************************************************************
@@@ -445,9 -427,12 +432,12 @@@ dsSpec mb_poly_rhs (L loc (SpecPrag pol
                                final_bndrs args
                                (mkVarApps (Var spec_id) bndrs)
  
 -             spec_rhs  = dsHsWrapper spec_co poly_rhs
 -             spec_pair = makeCorePair spec_id False (dictArity bndrs) spec_rhs
 +       ; spec_rhs <- dsHsWrapper spec_co poly_rhs
 +       ; let spec_pair = makeCorePair spec_id False (dictArity bndrs) spec_rhs
  
+        ; dflags <- getDynFlags
+        ; when (isInlinePragma id_inl && wopt Opt_WarnPointlessPragmas dflags)
+               (warnDs (specOnInline poly_name))
         ; return (Just (spec_pair `consOL` unf_pairs, rule))
         } } }
    where
Simple merge
Simple merge
Simple merge
Simple merge
Simple merge
Simple merge
Simple merge
Simple merge
- %\r
- % (c) The University of Glasgow 2006\r
- %\r
\r
- \begin{code}\r
- module TcEvidence (\r
\r
-   -- HsWrapper\r
-   HsWrapper(..), \r
-   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, \r
-   idHsWrapper, isIdHsWrapper, pprHsWrapper,\r
\r
-   -- Evidence bindin\r
-   TcEvBinds(..), EvBindsVar(..), \r
-   EvBindMap(..), emptyEvBindMap, extendEvBinds, lookupEvBind, evBindMapBinds,\r
\r
-   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, \r
\r
-   EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,\r
\r
-   -- TcCoercion\r
-   TcCoercion(..), \r
-   mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,\r
-   mkTcAxInstCo, mkTcForAllCo, mkTcForAllCos, \r
-   mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcInstCos,\r
-   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, \r
-   isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,\r
-   liftTcCoSubstWith\r
\r
-   ) where\r
- #include "HsVersions.h"\r
\r
- import Var\r
\r
- import PprCore ()   -- Instance OutputableBndr TyVar\r
- import TypeRep  -- Knows type representation\r
- import TcType\r
- import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe )\r
- import TysPrim( funTyCon )\r
- import TyCon\r
- import PrelNames\r
- import VarEnv\r
- import VarSet\r
- import Name\r
\r
- import Util\r
- import Bag\r
- import Pair\r
- import Control.Applicative\r
- import Data.Traversable (traverse, sequenceA)\r
- import qualified Data.Data as Data \r
- import Outputable\r
- import FastString\r
- import Data.IORef( IORef )\r
- \end{code}\r
\r
\r
- Note [TcCoercions]\r
- ~~~~~~~~~~~~~~~~~~\r
- | LCoercions are a hack used by the typechecker. Normally,\r
- Coercions have free variables of type (a ~# b): we call these\r
- CoVars. However, the type checker passes around equality evidence\r
- (boxed up) at type (a ~ b).\r
\r
- An LCoercion is simply a Coercion whose free variables have the\r
- boxed type (a ~ b). After we are done with typechecking the\r
- desugarer finds the free variables, unboxes them, and creates a\r
- resulting real Coercion with kosher free variables.\r
\r
- We can use most of the Coercion "smart constructors" to build LCoercions. However,\r
- mkCoVarCo will not work! The equivalent is mkTcCoVarCo.\r
\r
- The data type is similar to Coercion.Coercion, with the following\r
- differences\r
-   * Most important, TcLetCo adds let-bindings for coercions.\r
-     This is what lets us unify two for-all types and generate\r
-     equality constraints underneath\r
\r
-   * The kind of a TcCoercion is  t1 ~  t2 \r
-              of a Coercion   is  t1 ~# t2\r
\r
-   * TcAxiomInstCo takes Types, not Coecions as arguments;\r
-     the generality is required only in the Simplifier\r
\r
-   * UnsafeCo aren't required\r
\r
-   * Reprsentation invariants are weaker:\r
-      - we are allowed to have type synonyms in TcTyConAppCo\r
-      - the first arg of a TcAppCo can be a TcTyConAppCo\r
-     Reason: they'll get established when we desugar to Coercion\r
\r
- \begin{code}\r
- data TcCoercion \r
-   = TcRefl TcType\r
-   | TcTyConAppCo TyCon [TcCoercion]\r
-   | TcAppCo TcCoercion TcCoercion\r
-   | TcForAllCo TyVar TcCoercion \r
-   | TcInstCo TcCoercion TcType\r
-   | TcCoVarCo EqVar\r
-   | TcAxiomInstCo CoAxiom [TcType]\r
-   | TcSymCo TcCoercion\r
-   | TcTransCo TcCoercion TcCoercion\r
-   | TcNthCo Int TcCoercion\r
-   | TcLetCo TcEvBinds TcCoercion\r
-   deriving (Data.Data, Data.Typeable)\r
\r
- isEqVar :: Var -> Bool \r
- -- Is lifted coercion variable (only!)\r
- isEqVar v = case tyConAppTyCon_maybe (varType v) of\r
-                Just tc -> tc `hasKey` eqTyConKey\r
-                Nothing -> False\r
\r
- isTcReflCo_maybe :: TcCoercion -> Maybe TcType\r
- isTcReflCo_maybe (TcRefl ty) = Just ty\r
- isTcReflCo_maybe _             = Nothing\r
\r
- isTcReflCo :: TcCoercion -> Bool\r
- isTcReflCo (TcRefl {}) = True\r
- isTcReflCo _           = False\r
\r
- getTcCoVar_maybe :: TcCoercion -> Maybe CoVar\r
- getTcCoVar_maybe (TcCoVarCo v) = Just v\r
- getTcCoVar_maybe _             = Nothing\r
\r
- mkTcReflCo :: TcType -> TcCoercion\r
- mkTcReflCo = TcRefl\r
\r
- mkTcFunCo :: TcCoercion -> TcCoercion -> TcCoercion\r
- mkTcFunCo co1 co2 = mkTcTyConAppCo funTyCon [co1, co2]\r
\r
- mkTcTyConAppCo :: TyCon -> [TcCoercion] -> TcCoercion\r
- mkTcTyConAppCo tc cos   -- No need to expand type synonyms\r
-                         -- See Note [TcCoercions]\r
-   | Just tys <- traverse isTcReflCo_maybe cos \r
-   = TcRefl (mkTyConApp tc tys)    -- See Note [Refl invariant]\r
\r
-   | otherwise = TcTyConAppCo tc cos\r
\r
- mkTcAxInstCo :: CoAxiom -> [TcType] -> TcCoercion\r
- mkTcAxInstCo ax tys\r
-   | arity == n_tys = TcAxiomInstCo ax tys\r
-   | otherwise      = ASSERT( arity < n_tys )\r
-                      foldl TcAppCo (TcAxiomInstCo ax (take arity tys))\r
-                                    (map TcRefl (drop arity tys))\r
-   where\r
-     n_tys = length tys\r
-     arity = coAxiomArity ax\r
\r
- mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion\r
- -- No need to deal with TyConApp on the left; see Note [TcCoercions]\r
- mkTcAppCo (TcRefl ty1) (TcRefl ty2)     = TcRefl (mkAppTy ty1 ty2)\r
- mkTcAppCo co1 co2                       = TcAppCo co1 co2\r
\r
- mkTcSymCo :: TcCoercion -> TcCoercion\r
- mkTcSymCo co@(TcRefl {})  = co\r
- mkTcSymCo    (TcSymCo co) = co\r
- mkTcSymCo co              = TcSymCo co\r
\r
- mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion\r
- mkTcTransCo (TcRefl _) co = co\r
- mkTcTransCo co (TcRefl _) = co\r
- mkTcTransCo co1 co2       = TcTransCo co1 co2\r
\r
- mkTcNthCo :: Int -> TcCoercion -> TcCoercion\r
- mkTcNthCo n (TcRefl ty) = TcRefl (tyConAppArgN n ty)\r
- mkTcNthCo n co          = TcNthCo n co\r
\r
- mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion\r
- mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys\r
\r
- mkTcForAllCo :: Var -> TcCoercion -> TcCoercion\r
- -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)\r
- mkTcForAllCo tv (TcRefl ty) = ASSERT( isTyVar tv ) TcRefl (mkForAllTy tv ty)\r
- mkTcForAllCo tv  co         = ASSERT( isTyVar tv ) TcForAllCo tv co\r
\r
- mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion\r
- mkTcForAllCos tvs (TcRefl ty) = ASSERT( all isTyVar tvs ) TcRefl (mkForAllTys tvs ty)\r
- mkTcForAllCos tvs co          = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs\r
\r
- mkTcInstCos :: TcCoercion -> [TcType] -> TcCoercion\r
- mkTcInstCos (TcRefl ty) tys = TcRefl (applyTys ty tys)\r
- mkTcInstCos co tys          = foldl TcInstCo co tys\r
\r
- mkTcCoVarCo :: EqVar -> TcCoercion\r
- -- ipv :: s ~ t  (the boxed equality type)\r
- mkTcCoVarCo ipv\r
-   | ty1 `eqType` ty2 = TcRefl ty1\r
-   | otherwise        = TcCoVarCo ipv\r
-   where\r
-     (ty1, ty2) = case getEqPredTys_maybe (varType ipv) of\r
-         Nothing  -> pprPanic "mkCoVarLCo" (ppr ipv)\r
-         Just tys -> tys\r
- \end{code}\r
\r
- \begin{code}\r
- tcCoercionKind :: TcCoercion -> Pair Type\r
- tcCoercionKind co = go co \r
-   where \r
-     go (TcRefl ty)            = Pair ty ty\r
-     go (TcLetCo _ co)         = go co\r
-     go (TcTyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)\r
-     go (TcAppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2\r
-     go (TcForAllCo tv co)     = mkForAllTy tv <$> go co\r
-     go (TcInstCo co ty)       = go_inst co [ty]\r
-     go (TcCoVarCo cv)         = eqVarKind cv\r
-     go (TcAxiomInstCo ax tys) = Pair (substTyWith (co_ax_tvs ax) tys (co_ax_lhs ax)) \r
-                                      (substTyWith (co_ax_tvs ax) tys (co_ax_rhs ax))\r
-     go (TcSymCo co)           = swap $ go co\r
-     go (TcTransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)\r
-     go (TcNthCo d co)         = tyConAppArgN d <$> go co\r
\r
-     -- c.f. Coercion.coercionKind\r
-     go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)\r
-     go_inst co               tys = (`applyTys` tys) <$> go co\r
\r
- eqVarKind :: EqVar -> Pair Type\r
- eqVarKind cv\r
-  | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)\r
-  = ASSERT (tc `hasKey` eqTyConKey)\r
-    Pair ty1 ty2\r
-  | otherwise = panic "eqVarKind, non coercion variable"\r
\r
- coVarsOfTcCo :: TcCoercion -> VarSet\r
- -- Only works on *zonked* coercions, because of TcLetCo\r
- coVarsOfTcCo tc_co\r
-   = go tc_co\r
-   where\r
-     go (TcRefl _)                = emptyVarSet\r
-     go (TcTyConAppCo _ cos)      = foldr (unionVarSet . go) emptyVarSet cos\r
-     go (TcAppCo co1 co2)         = go co1 `unionVarSet` go co2\r
-     go (TcForAllCo _ co)         = go co\r
-     go (TcInstCo co _)           = go co\r
-     go (TcCoVarCo v)             = unitVarSet v\r
-     go (TcAxiomInstCo {})        = emptyVarSet\r
-     go (TcSymCo co)              = go co\r
-     go (TcTransCo co1 co2)       = go co1 `unionVarSet` go co2\r
-     go (TcNthCo _ co)            = go co\r
-     go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs\r
-                                    `minusVarSet` get_bndrs bs\r
-     go (TcLetCo {}) = pprPanic "coVarsOfTcCo called on non-zonked TcCoercion" (ppr tc_co)\r
\r
-     -- We expect only coercion bindings\r
-     go_bind :: EvBind -> VarSet\r
-     go_bind (EvBind _ (EvCoercion co)) = go co\r
-     go_bind (EvBind _ (EvId v))        = unitVarSet v\r
-     go_bind other = pprPanic "coVarsOfTcCo:Bind" (ppr other)\r
\r
-     get_bndrs :: Bag EvBind -> VarSet\r
-     get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet \r
\r
- liftTcCoSubstWith :: [TyVar] -> [TcCoercion] -> TcType -> TcCoercion\r
- -- This version can ignore capture; the free varialbes of the \r
- -- TcCoerion are all fresh.  Result is mush simpler code\r
- liftTcCoSubstWith tvs cos ty\r
-   = ASSERT( equalLength tvs cos )\r
-     go ty\r
-   where\r
-     env = zipVarEnv tvs cos\r
\r
-     go ty@(TyVarTy tv)   = case lookupVarEnv env tv of\r
-                              Just co -> co\r
-                              Nothing -> mkTcReflCo ty\r
-     go (AppTy t1 t2)     = mkTcAppCo (go t1) (go t2)\r
-     go (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)\r
+ %
+ % (c) The University of Glasgow 2006
+ %
+ \begin{code}
+ module TcEvidence (
+   -- HsWrapper
+   HsWrapper(..), 
+   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, 
+   idHsWrapper, isIdHsWrapper, pprHsWrapper,
+   -- Evidence bindin
+   TcEvBinds(..), EvBindsVar(..), 
+   EvBindMap(..), emptyEvBindMap, extendEvBinds, lookupEvBind, evBindMapBinds,
+   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, 
+   EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,
+   -- TcCoercion
+   TcCoercion(..), 
+   mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
+   mkTcAxInstCo, mkTcForAllCo, mkTcForAllCos, 
+   mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcInstCos,
+   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, 
+   isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
+   liftTcCoSubstWith
+   ) where
+ #include "HsVersions.h"
+ import Var
+ import PprCore ()   -- Instance OutputableBndr TyVar
+ import TypeRep  -- Knows type representation
+ import TcType
+ import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe )
+ import TysPrim( funTyCon )
+ import TyCon
+ import PrelNames
+ import VarEnv
+ import VarSet
+ import Name
+ import Util
+ import Bag
+ import Pair
+ import Control.Applicative
+ import Data.Traversable (traverse, sequenceA)
+ import qualified Data.Data as Data 
+ import Outputable
+ import FastString
+ import Data.IORef( IORef )
+ \end{code}
+ Note [TcCoercions]
+ ~~~~~~~~~~~~~~~~~~
+ | LCoercions are a hack used by the typechecker. Normally,
+ Coercions have free variables of type (a ~# b): we call these
+ CoVars. However, the type checker passes around equality evidence
+ (boxed up) at type (a ~ b).
+ An LCoercion is simply a Coercion whose free variables have the
+ boxed type (a ~ b). After we are done with typechecking the
+ desugarer finds the free variables, unboxes them, and creates a
+ resulting real Coercion with kosher free variables.
+ We can use most of the Coercion "smart constructors" to build LCoercions. However,
+ mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
+ The data type is similar to Coercion.Coercion, with the following
+ differences
+   * Most important, TcLetCo adds let-bindings for coercions.
+     This is what lets us unify two for-all types and generate
+     equality constraints underneath
+   * The kind of a TcCoercion is  t1 ~  t2 
+              of a Coercion   is  t1 ~# t2
+   * TcAxiomInstCo takes Types, not Coecions as arguments;
+     the generality is required only in the Simplifier
+   * UnsafeCo aren't required
+   * Reprsentation invariants are weaker:
+      - we are allowed to have type synonyms in TcTyConAppCo
+      - the first arg of a TcAppCo can be a TcTyConAppCo
+     Reason: they'll get established when we desugar to Coercion
+ \begin{code}
+ data TcCoercion 
+   = TcRefl TcType
+   | TcTyConAppCo TyCon [TcCoercion]
+   | TcAppCo TcCoercion TcCoercion
+   | TcForAllCo TyVar TcCoercion 
+   | TcInstCo TcCoercion TcType
+   | TcCoVarCo EqVar
+   | TcAxiomInstCo CoAxiom [TcType]
+   | TcSymCo TcCoercion
+   | TcTransCo TcCoercion TcCoercion
+   | TcNthCo Int TcCoercion
+   | TcLetCo TcEvBinds TcCoercion
+   deriving (Data.Data, Data.Typeable)
+ isEqVar :: Var -> Bool 
+ -- Is lifted coercion variable (only!)
+ isEqVar v = case tyConAppTyCon_maybe (varType v) of
+                Just tc -> tc `hasKey` eqTyConKey
+                Nothing -> False
+ isTcReflCo_maybe :: TcCoercion -> Maybe TcType
+ isTcReflCo_maybe (TcRefl ty) = Just ty
+ isTcReflCo_maybe _             = Nothing
+ isTcReflCo :: TcCoercion -> Bool
+ isTcReflCo (TcRefl {}) = True
+ isTcReflCo _           = False
+ getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
+ getTcCoVar_maybe (TcCoVarCo v) = Just v
+ getTcCoVar_maybe _             = Nothing
+ mkTcReflCo :: TcType -> TcCoercion
+ mkTcReflCo = TcRefl
+ mkTcFunCo :: TcCoercion -> TcCoercion -> TcCoercion
+ mkTcFunCo co1 co2 = mkTcTyConAppCo funTyCon [co1, co2]
+ mkTcTyConAppCo :: TyCon -> [TcCoercion] -> TcCoercion
+ mkTcTyConAppCo tc cos   -- No need to expand type synonyms
+                         -- See Note [TcCoercions]
+   | Just tys <- traverse isTcReflCo_maybe cos 
+   = TcRefl (mkTyConApp tc tys)    -- See Note [Refl invariant]
+   | otherwise = TcTyConAppCo tc cos
+ mkTcAxInstCo :: CoAxiom -> [TcType] -> TcCoercion
+ mkTcAxInstCo ax tys
+   | arity == n_tys = TcAxiomInstCo ax tys
+   | otherwise      = ASSERT( arity < n_tys )
+                      foldl TcAppCo (TcAxiomInstCo ax (take arity tys))
+                                    (map TcRefl (drop arity tys))
+   where
+     n_tys = length tys
+     arity = coAxiomArity ax
+ mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
+ -- No need to deal with TyConApp on the left; see Note [TcCoercions]
+ mkTcAppCo (TcRefl ty1) (TcRefl ty2)     = TcRefl (mkAppTy ty1 ty2)
+ mkTcAppCo co1 co2                       = TcAppCo co1 co2
+ mkTcSymCo :: TcCoercion -> TcCoercion
+ mkTcSymCo co@(TcRefl {})  = co
+ mkTcSymCo    (TcSymCo co) = co
+ mkTcSymCo co              = TcSymCo co
+ mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
+ mkTcTransCo (TcRefl _) co = co
+ mkTcTransCo co (TcRefl _) = co
+ mkTcTransCo co1 co2       = TcTransCo co1 co2
+ mkTcNthCo :: Int -> TcCoercion -> TcCoercion
+ mkTcNthCo n (TcRefl ty) = TcRefl (tyConAppArgN n ty)
+ mkTcNthCo n co          = TcNthCo n co
+ mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
+ mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
+ mkTcForAllCo :: Var -> TcCoercion -> TcCoercion
+ -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
+ mkTcForAllCo tv (TcRefl ty) = ASSERT( isTyVar tv ) TcRefl (mkForAllTy tv ty)
+ mkTcForAllCo tv  co         = ASSERT( isTyVar tv ) TcForAllCo tv co
+ mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion
+ mkTcForAllCos tvs (TcRefl ty) = ASSERT( all isTyVar tvs ) TcRefl (mkForAllTys tvs ty)
+ mkTcForAllCos tvs co          = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs
+ mkTcInstCos :: TcCoercion -> [TcType] -> TcCoercion
+ mkTcInstCos (TcRefl ty) tys = TcRefl (applyTys ty tys)
+ mkTcInstCos co tys          = foldl TcInstCo co tys
+ mkTcCoVarCo :: EqVar -> TcCoercion
+ -- ipv :: s ~ t  (the boxed equality type)
+ mkTcCoVarCo ipv
+   | ty1 `eqType` ty2 = TcRefl ty1
+   | otherwise        = TcCoVarCo ipv
+   where
+     (ty1, ty2) = case getEqPredTys_maybe (varType ipv) of
+         Nothing  -> pprPanic "mkCoVarLCo" (ppr ipv)
+         Just tys -> tys
+ \end{code}
+ \begin{code}
+ tcCoercionKind :: TcCoercion -> Pair Type
+ tcCoercionKind co = go co 
+   where 
+     go (TcRefl ty)            = Pair ty ty
+     go (TcLetCo _ co)         = go co
+     go (TcTyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
+     go (TcAppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
+     go (TcForAllCo tv co)     = mkForAllTy tv <$> go co
+     go (TcInstCo co ty)       = go_inst co [ty]
+     go (TcCoVarCo cv)         = eqVarKind cv
+     go (TcAxiomInstCo ax tys) = Pair (substTyWith (co_ax_tvs ax) tys (co_ax_lhs ax)) 
+                                      (substTyWith (co_ax_tvs ax) tys (co_ax_rhs ax))
+     go (TcSymCo co)           = swap $ go co
+     go (TcTransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)
+     go (TcNthCo d co)         = tyConAppArgN d <$> go co
+     -- c.f. Coercion.coercionKind
+     go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)
+     go_inst co               tys = (`applyTys` tys) <$> go co
+ eqVarKind :: EqVar -> Pair Type
+ eqVarKind cv
+  | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
+  = ASSERT (tc `hasKey` eqTyConKey)
+    Pair ty1 ty2
+  | otherwise = panic "eqVarKind, non coercion variable"
+ coVarsOfTcCo :: TcCoercion -> VarSet
+ -- Only works on *zonked* coercions, because of TcLetCo
+ coVarsOfTcCo tc_co
+   = go tc_co
+   where
+     go (TcRefl _)                = emptyVarSet
+     go (TcTyConAppCo _ cos)      = foldr (unionVarSet . go) emptyVarSet cos
+     go (TcAppCo co1 co2)         = go co1 `unionVarSet` go co2
+     go (TcForAllCo _ co)         = go co
+     go (TcInstCo co _)           = go co
+     go (TcCoVarCo v)             = unitVarSet v
+     go (TcAxiomInstCo {})        = emptyVarSet
+     go (TcSymCo co)              = go co
+     go (TcTransCo co1 co2)       = go co1 `unionVarSet` go co2
+     go (TcNthCo _ co)            = go co
+     go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
+                                    `minusVarSet` get_bndrs bs
+     go (TcLetCo {}) = pprPanic "coVarsOfTcCo called on non-zonked TcCoercion" (ppr tc_co)
+     -- We expect only coercion bindings
+     go_bind :: EvBind -> VarSet
+     go_bind (EvBind _ (EvCoercion co)) = go co
+     go_bind (EvBind _ (EvId v))        = unitVarSet v
+     go_bind other = pprPanic "coVarsOfTcCo:Bind" (ppr other)
+     get_bndrs :: Bag EvBind -> VarSet
+     get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet 
+ liftTcCoSubstWith :: [TyVar] -> [TcCoercion] -> TcType -> TcCoercion
+ -- This version can ignore capture; the free varialbes of the 
+ -- TcCoerion are all fresh.  Result is mush simpler code
+ liftTcCoSubstWith tvs cos ty
+   = ASSERT( equalLength tvs cos )
+     go ty
+   where
+     env = zipVarEnv tvs cos
+     go ty@(TyVarTy tv)   = case lookupVarEnv env tv of
+                              Just co -> co
+                              Nothing -> mkTcReflCo ty
+     go (AppTy t1 t2)     = mkTcAppCo (go t1) (go t2)
+     go (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)
 +    go ty@(LitTy {})     = mkTcReflCo ty\r
-     go (ForAllTy tv ty)  = mkTcForAllCo tv (go ty)\r
-     go (FunTy t1 t2)     = mkTcFunCo (go t1) (go t2)\r
- \end{code}\r
\r
- Pretty printing\r
\r
- \begin{code}\r
- instance Outputable TcCoercion where\r
-   ppr = pprTcCo\r
\r
- pprTcCo, pprParendTcCo :: TcCoercion -> SDoc\r
- pprTcCo       co = ppr_co TopPrec   co\r
- pprParendTcCo co = ppr_co TyConPrec co\r
\r
- ppr_co :: Prec -> TcCoercion -> SDoc\r
- ppr_co _ (TcRefl ty) = angleBrackets (ppr ty)\r
\r
- ppr_co p co@(TcTyConAppCo tc [_,_])\r
-   | tc `hasKey` funTyConKey = ppr_fun_co p co\r
\r
- ppr_co p (TcTyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos\r
- ppr_co p (TcLetCo bs co)         = maybeParen p TopPrec $\r
-                                    sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]\r
- ppr_co p (TcAppCo co1 co2)       = maybeParen p TyConPrec $\r
-                                    pprTcCo co1 <+> ppr_co TyConPrec co2\r
- ppr_co p co@(TcForAllCo {})      = ppr_forall_co p co\r
- ppr_co p (TcInstCo co ty)        = maybeParen p TyConPrec $\r
-                                    pprParendTcCo co <> ptext (sLit "@") <> pprType ty\r
-                      \r
- ppr_co _ (TcCoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)\r
- ppr_co p (TcAxiomInstCo con cos) = pprTypeNameApp p ppr_type (getName con) cos\r
\r
- ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $\r
-                                ppr_co FunPrec co1\r
-                                <+> ptext (sLit ";")\r
-                                <+> ppr_co FunPrec co2\r
- ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]\r
- ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]\r
\r
- ppr_fun_co :: Prec -> TcCoercion -> SDoc\r
- ppr_fun_co p co = pprArrowChain p (split co)\r
-   where\r
-     split :: TcCoercion -> [SDoc]\r
-     split (TcTyConAppCo f [arg,res])\r
-       | f `hasKey` funTyConKey\r
-       = ppr_co FunPrec arg : split res\r
-     split co = [ppr_co TopPrec co]\r
\r
- ppr_forall_co :: Prec -> TcCoercion -> SDoc\r
- ppr_forall_co p ty\r
-   = maybeParen p FunPrec $\r
-     sep [pprForAll tvs, ppr_co TopPrec rho]\r
-   where\r
-     (tvs,  rho) = split1 [] ty\r
-     split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty\r
-     split1 tvs ty                 = (reverse tvs, ty)\r
- \end{code}\r
\r
- %************************************************************************\r
- %*                                                                      *\r
-                   HsWrapper\r
- %*                                                                      *\r
- %************************************************************************\r
\r
- \begin{code}\r
- data HsWrapper\r
-   = WpHole                      -- The identity coercion\r
\r
-   | WpCompose HsWrapper HsWrapper\r
-        -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]\r
-        --\r
-        -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])\r
-        -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)\r
\r
-   | WpCast TcCoercion         -- A cast:  [] `cast` co\r
-                               -- Guaranteed not the identity coercion\r
\r
-         -- Evidence abstraction and application\r
-         -- (both dictionaries and coercions)\r
-   | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable\r
-   | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint\r
\r
-         -- Kind and Type abstraction and application\r
-   | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)\r
-   | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)\r
\r
\r
-   | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,\r
-                                 -- so that the identity coercion is always exactly WpHole\r
-   deriving (Data.Data, Data.Typeable)\r
\r
\r
- (<.>) :: HsWrapper -> HsWrapper -> HsWrapper\r
- WpHole <.> c = c\r
- c <.> WpHole = c\r
- c1 <.> c2    = c1 `WpCompose` c2\r
\r
- mkWpTyApps :: [Type] -> HsWrapper\r
- mkWpTyApps tys = mk_co_app_fn WpTyApp tys\r
\r
- mkWpEvApps :: [EvTerm] -> HsWrapper\r
- mkWpEvApps args = mk_co_app_fn WpEvApp args\r
\r
- mkWpEvVarApps :: [EvVar] -> HsWrapper\r
- mkWpEvVarApps vs = mkWpEvApps (map EvId vs)\r
\r
- mkWpTyLams :: [TyVar] -> HsWrapper\r
- mkWpTyLams ids = mk_co_lam_fn WpTyLam ids\r
\r
- mkWpLams :: [Var] -> HsWrapper\r
- mkWpLams ids = mk_co_lam_fn WpEvLam ids\r
\r
- mkWpLet :: TcEvBinds -> HsWrapper\r
- -- This no-op is a quite a common case\r
- mkWpLet (EvBinds b) | isEmptyBag b = WpHole\r
- mkWpLet ev_binds                   = WpLet ev_binds\r
\r
- mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper\r
- mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as\r
\r
- mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper\r
- -- For applications, the *first* argument must\r
- -- come *last* in the composition sequence\r
- mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as\r
\r
- idHsWrapper :: HsWrapper\r
- idHsWrapper = WpHole\r
\r
- isIdHsWrapper :: HsWrapper -> Bool\r
- isIdHsWrapper WpHole = True\r
- isIdHsWrapper _      = False\r
- \end{code}\r
\r
\r
- %************************************************************************\r
- %*                                                                      *\r
-                   Evidence bindings\r
- %*                                                                      *\r
- %************************************************************************\r
\r
- \begin{code}\r
- data TcEvBinds\r
-   = TcEvBinds           -- Mutable evidence bindings\r
-        EvBindsVar       -- Mutable because they are updated "later"\r
-                         --    when an implication constraint is solved\r
\r
-   | EvBinds             -- Immutable after zonking\r
-        (Bag EvBind)\r
\r
-   deriving( Data.Typeable )\r
\r
- data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique\r
-      -- The Unique is only for debug printing\r
\r
- instance Data.Data TcEvBinds where\r
-   -- Placeholder; we can't travers into TcEvBinds\r
-   toConstr _   = abstractConstr "TcEvBinds"\r
-   gunfold _ _  = error "gunfold"\r
-   dataTypeOf _ = Data.mkNoRepType "TcEvBinds"\r
\r
- -----------------\r
- newtype EvBindMap \r
-   = EvBindMap { \r
-        ev_bind_varenv :: VarEnv EvBind\r
-     }       -- Map from evidence variables to evidence terms\r
\r
- emptyEvBindMap :: EvBindMap\r
- emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }\r
\r
- extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap\r
- extendEvBinds bs v t \r
-   = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) }\r
\r
- lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind\r
- lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)\r
\r
- evBindMapBinds :: EvBindMap -> Bag EvBind\r
- evBindMapBinds bs \r
-   = foldVarEnv consBag emptyBag (ev_bind_varenv bs)\r
\r
- -----------------\r
- -- All evidence is bound by EvBinds; no side effects\r
- data EvBind = EvBind EvVar EvTerm\r
\r
- data EvTerm\r
-   = EvId EvId                    -- Term-level variable-to-variable bindings\r
-                                  -- (no coercion variables! they come via EvCoercion)\r
\r
-   | EvCoercion TcCoercion        -- (Boxed) coercion bindings\r
\r
-   | EvCast EvVar TcCoercion      -- d |> co\r
\r
-   | EvDFunApp DFunId             -- Dictionary instance application\r
-        [Type] [EvVar]\r
\r
-   | EvTupleSel EvId  Int         -- n'th component of the tuple\r
\r
-   | EvTupleMk [EvId]             -- tuple built from this stuff\r
\r
-   | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors\r
-                                -- See Note [Deferring coercion errors to runtime]\r
-                                -- in TcSimplify\r
\r
-   | EvSuperClass DictId Int      -- n'th superclass. Used for both equalities and\r
-                                  -- dictionaries, even though the former have no\r
-                                  -- selector Id.  We count up from _0_\r
-   | EvKindCast EvVar TcCoercion  -- See Note [EvKindCast]\r
+     go (ForAllTy tv ty)  = mkTcForAllCo tv (go ty)
+     go (FunTy t1 t2)     = mkTcFunCo (go t1) (go t2)
+ \end{code}
+ Pretty printing
+ \begin{code}
+ instance Outputable TcCoercion where
+   ppr = pprTcCo
+ pprTcCo, pprParendTcCo :: TcCoercion -> SDoc
+ pprTcCo       co = ppr_co TopPrec   co
+ pprParendTcCo co = ppr_co TyConPrec co
+ ppr_co :: Prec -> TcCoercion -> SDoc
+ ppr_co _ (TcRefl ty) = angleBrackets (ppr ty)
+ ppr_co p co@(TcTyConAppCo tc [_,_])
+   | tc `hasKey` funTyConKey = ppr_fun_co p co
+ ppr_co p (TcTyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos
+ ppr_co p (TcLetCo bs co)         = maybeParen p TopPrec $
+                                    sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
+ ppr_co p (TcAppCo co1 co2)       = maybeParen p TyConPrec $
+                                    pprTcCo co1 <+> ppr_co TyConPrec co2
+ ppr_co p co@(TcForAllCo {})      = ppr_forall_co p co
+ ppr_co p (TcInstCo co ty)        = maybeParen p TyConPrec $
+                                    pprParendTcCo co <> ptext (sLit "@") <> pprType ty
+                      
+ ppr_co _ (TcCoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
+ ppr_co p (TcAxiomInstCo con cos) = pprTypeNameApp p ppr_type (getName con) cos
+ ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
+                                ppr_co FunPrec co1
+                                <+> ptext (sLit ";")
+                                <+> ppr_co FunPrec co2
+ ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
+ ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
+ ppr_fun_co :: Prec -> TcCoercion -> SDoc
+ ppr_fun_co p co = pprArrowChain p (split co)
+   where
+     split :: TcCoercion -> [SDoc]
+     split (TcTyConAppCo f [arg,res])
+       | f `hasKey` funTyConKey
+       = ppr_co FunPrec arg : split res
+     split co = [ppr_co TopPrec co]
+ ppr_forall_co :: Prec -> TcCoercion -> SDoc
+ ppr_forall_co p ty
+   = maybeParen p FunPrec $
+     sep [pprForAll tvs, ppr_co TopPrec rho]
+   where
+     (tvs,  rho) = split1 [] ty
+     split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty
+     split1 tvs ty                 = (reverse tvs, ty)
+ \end{code}
+ %************************************************************************
+ %*                                                                      *
+                   HsWrapper
+ %*                                                                      *
+ %************************************************************************
+ \begin{code}
+ data HsWrapper
+   = WpHole                      -- The identity coercion
+   | WpCompose HsWrapper HsWrapper
+        -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
+        --
+        -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
+        -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)
+   | WpCast TcCoercion         -- A cast:  [] `cast` co
+                               -- Guaranteed not the identity coercion
+         -- Evidence abstraction and application
+         -- (both dictionaries and coercions)
+   | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable
+   | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint
+         -- Kind and Type abstraction and application
+   | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)
+   | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)
+   | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,
+                                 -- so that the identity coercion is always exactly WpHole
+   deriving (Data.Data, Data.Typeable)
+ (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
+ WpHole <.> c = c
+ c <.> WpHole = c
+ c1 <.> c2    = c1 `WpCompose` c2
+ mkWpTyApps :: [Type] -> HsWrapper
+ mkWpTyApps tys = mk_co_app_fn WpTyApp tys
+ mkWpEvApps :: [EvTerm] -> HsWrapper
+ mkWpEvApps args = mk_co_app_fn WpEvApp args
+ mkWpEvVarApps :: [EvVar] -> HsWrapper
+ mkWpEvVarApps vs = mkWpEvApps (map EvId vs)
+ mkWpTyLams :: [TyVar] -> HsWrapper
+ mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
+ mkWpLams :: [Var] -> HsWrapper
+ mkWpLams ids = mk_co_lam_fn WpEvLam ids
+ mkWpLet :: TcEvBinds -> HsWrapper
+ -- This no-op is a quite a common case
+ mkWpLet (EvBinds b) | isEmptyBag b = WpHole
+ mkWpLet ev_binds                   = WpLet ev_binds
+ mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
+ mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
+ mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
+ -- For applications, the *first* argument must
+ -- come *last* in the composition sequence
+ mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
+ idHsWrapper :: HsWrapper
+ idHsWrapper = WpHole
+ isIdHsWrapper :: HsWrapper -> Bool
+ isIdHsWrapper WpHole = True
+ isIdHsWrapper _      = False
+ \end{code}
+ %************************************************************************
+ %*                                                                      *
+                   Evidence bindings
+ %*                                                                      *
+ %************************************************************************
+ \begin{code}
+ data TcEvBinds
+   = TcEvBinds           -- Mutable evidence bindings
+        EvBindsVar       -- Mutable because they are updated "later"
+                         --    when an implication constraint is solved
+   | EvBinds             -- Immutable after zonking
+        (Bag EvBind)
+   deriving( Data.Typeable )
+ data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
+      -- The Unique is only for debug printing
+ instance Data.Data TcEvBinds where
+   -- Placeholder; we can't travers into TcEvBinds
+   toConstr _   = abstractConstr "TcEvBinds"
+   gunfold _ _  = error "gunfold"
+   dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
+ -----------------
+ newtype EvBindMap 
+   = EvBindMap { 
+        ev_bind_varenv :: VarEnv EvBind
+     }       -- Map from evidence variables to evidence terms
+ emptyEvBindMap :: EvBindMap
+ emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }
+ extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap
+ extendEvBinds bs v t 
+   = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) }
+ lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
+ lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)
+ evBindMapBinds :: EvBindMap -> Bag EvBind
+ evBindMapBinds bs 
+   = foldVarEnv consBag emptyBag (ev_bind_varenv bs)
+ -----------------
+ -- All evidence is bound by EvBinds; no side effects
+ data EvBind = EvBind EvVar EvTerm
+ data EvTerm
+   = EvId EvId                    -- Term-level variable-to-variable bindings
+                                  -- (no coercion variables! they come via EvCoercion)
+   | EvCoercion TcCoercion        -- (Boxed) coercion bindings
+   | EvCast EvVar TcCoercion      -- d |> co
+   | EvDFunApp DFunId             -- Dictionary instance application
+        [Type] [EvVar]
+   | EvTupleSel EvId  Int         -- n'th component of the tuple
+   | EvTupleMk [EvId]             -- tuple built from this stuff
+   | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors
+                                -- See Note [Deferring coercion errors to runtime]
+                                -- in TcSimplify
+   | EvSuperClass DictId Int      -- n'th superclass. Used for both equalities and
+                                  -- dictionaries, even though the former have no
+                                  -- selector Id.  We count up from _0_
+   | EvKindCast EvVar TcCoercion  -- See Note [EvKindCast]
 +\r
 +  | EvInteger Integer            -- The dictionary for class "NatI"\r
 +                                 -- Note [EvInteger]\r
-            \r
-   deriving( Data.Data, Data.Typeable)\r
- \end{code}\r
\r
- Note [EvKindCast] \r
- ~~~~~~~~~~~~~~~~~ \r
\r
- EvKindCast g kco is produced when we have a constraint (g : s1 ~ s2) \r
- but the kinds of s1 and s2 (k1 and k2 respectively) don't match but \r
- are rather equal by a coercion. You may think that this coercion will\r
- always turn out to be ReflCo, so why is this needed? Because sometimes\r
- we will want to defer kind errors until the runtime and in these cases\r
- that coercion will be an 'error' term, which we want to evaluate rather\r
- than silently forget about!\r
\r
- The relevant (and only) place where such a coercion is produced in \r
- the simplifier is in emit_kind_constraint in TcCanonical.\r
\r
\r
- Note [EvBinds/EvTerm]\r
- ~~~~~~~~~~~~~~~~~~~~~\r
- How evidence is created and updated. Bindings for dictionaries,\r
- and coercions and implicit parameters are carried around in TcEvBinds\r
- which during constraint generation and simplification is always of the\r
- form (TcEvBinds ref). After constraint simplification is finished it\r
- will be transformed to t an (EvBinds ev_bag).\r
\r
- Evidence for coercions *SHOULD* be filled in using the TcEvBinds\r
- However, all EvVars that correspond to *wanted* coercion terms in\r
- an EvBind must be mutable variables so that they can be readily\r
- inlined (by zonking) after constraint simplification is finished.\r
\r
- Conclusion: a new wanted coercion variable should be made mutable.\r
- [Notice though that evidence variables that bind coercion terms\r
-  from super classes will be "given" and hence rigid]\r
\r
\r
+            
+   deriving( Data.Data, Data.Typeable)
+ \end{code}
+ Note [EvKindCast] 
+ ~~~~~~~~~~~~~~~~~ 
+ EvKindCast g kco is produced when we have a constraint (g : s1 ~ s2) 
+ but the kinds of s1 and s2 (k1 and k2 respectively) don't match but 
+ are rather equal by a coercion. You may think that this coercion will
+ always turn out to be ReflCo, so why is this needed? Because sometimes
+ we will want to defer kind errors until the runtime and in these cases
+ that coercion will be an 'error' term, which we want to evaluate rather
+ than silently forget about!
+ The relevant (and only) place where such a coercion is produced in 
+ the simplifier is in emit_kind_constraint in TcCanonical.
+ Note [EvBinds/EvTerm]
+ ~~~~~~~~~~~~~~~~~~~~~
+ How evidence is created and updated. Bindings for dictionaries,
+ and coercions and implicit parameters are carried around in TcEvBinds
+ which during constraint generation and simplification is always of the
+ form (TcEvBinds ref). After constraint simplification is finished it
+ will be transformed to t an (EvBinds ev_bag).
+ Evidence for coercions *SHOULD* be filled in using the TcEvBinds
+ However, all EvVars that correspond to *wanted* coercion terms in
+ an EvBind must be mutable variables so that they can be readily
+ inlined (by zonking) after constraint simplification is finished.
+ Conclusion: a new wanted coercion variable should be made mutable.
+ [Notice though that evidence variables that bind coercion terms
+  from super classes will be "given" and hence rigid]
 +Note [EvInteger]\r
 +~~~~~~~~~~~~~~~~\r
 +A part of the type-level naturals implementation is the class "NatI",\r
 +which provides a "smart" constructor for defining singleton values.\r
 +\r
 +newtype NatS (n :: Nat) = NatS Integer\r
 +\r
 +class NatI n where\r
 +  natS :: NatS n\r
 +\r
 +Conceptually, this class has infinitely many instances:\r
 +\r
 +instance NatI 0 where natS = NatS 0\r
 +instance NatI 1 where natS = NatS 1\r
 +instance NatI 2 where natS = NatS 2\r
 +...\r
 +\r
 +In practice, we solve "NatI" predicates in the type-checker because we can't\r
 +have infinately many instances.  The evidence (aka "dictionary")\r
 +for "NatI n" is of the form "EvInteger n".\r
 +\r
 +We make the following assumptions about dictionaries in GHC:\r
 +  1. The "dictionary" for classes with a single method---like NatI---is\r
 +     a newtype for the type of the method, so using a evidence amounts\r
 +     to a coercion, and\r
 +  2. Newtypes use the same representation as their definition types.\r
 +\r
 +So, the evidence for "NatI" is just an integer wrapped in 2 newtypes:\r
 +one to make it into a "NatS" value, and another to make it into "NatI" evidence.\r
 +\r
 +\r
 +\r
- \begin{code}\r
- mkEvCast :: EvVar -> TcCoercion -> EvTerm\r
- mkEvCast ev lco\r
-   | isTcReflCo lco = EvId ev\r
-   | otherwise      = EvCast ev lco\r
\r
- mkEvKindCast :: EvVar -> TcCoercion -> EvTerm\r
- mkEvKindCast ev lco\r
-   | isTcReflCo lco = EvId ev\r
-   | otherwise      = EvKindCast ev lco\r
\r
- emptyTcEvBinds :: TcEvBinds\r
- emptyTcEvBinds = EvBinds emptyBag\r
\r
- isEmptyTcEvBinds :: TcEvBinds -> Bool\r
- isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b\r
- isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"\r
\r
\r
- evVarsOfTerm :: EvTerm -> [EvVar]\r
- evVarsOfTerm (EvId v) = [v]\r
- evVarsOfTerm (EvCoercion co)      = varSetElems (coVarsOfTcCo co)\r
- evVarsOfTerm (EvDFunApp _ _ evs)  = evs\r
- evVarsOfTerm (EvTupleSel v _)     = [v]\r
- evVarsOfTerm (EvSuperClass v _)   = [v]\r
- evVarsOfTerm (EvCast v co)        = v : varSetElems (coVarsOfTcCo co)\r
- evVarsOfTerm (EvTupleMk evs)      = evs\r
- evVarsOfTerm (EvDelayedError _ _) = []\r
- evVarsOfTerm (EvKindCast v co)   = v : varSetElems (coVarsOfTcCo co)\r
+ \begin{code}
+ mkEvCast :: EvVar -> TcCoercion -> EvTerm
+ mkEvCast ev lco
+   | isTcReflCo lco = EvId ev
+   | otherwise      = EvCast ev lco
+ mkEvKindCast :: EvVar -> TcCoercion -> EvTerm
+ mkEvKindCast ev lco
+   | isTcReflCo lco = EvId ev
+   | otherwise      = EvKindCast ev lco
+ emptyTcEvBinds :: TcEvBinds
+ emptyTcEvBinds = EvBinds emptyBag
+ isEmptyTcEvBinds :: TcEvBinds -> Bool
+ isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b
+ isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
+ evVarsOfTerm :: EvTerm -> [EvVar]
+ evVarsOfTerm (EvId v) = [v]
+ evVarsOfTerm (EvCoercion co)      = varSetElems (coVarsOfTcCo co)
+ evVarsOfTerm (EvDFunApp _ _ evs)  = evs
+ evVarsOfTerm (EvTupleSel v _)     = [v]
+ evVarsOfTerm (EvSuperClass v _)   = [v]
+ evVarsOfTerm (EvCast v co)        = v : varSetElems (coVarsOfTcCo co)
+ evVarsOfTerm (EvTupleMk evs)      = evs
+ evVarsOfTerm (EvDelayedError _ _) = []
+ evVarsOfTerm (EvKindCast v co)   = v : varSetElems (coVarsOfTcCo co)
 +evVarsOfTerm (EvInteger _)       = []\r
- \end{code}\r
\r
\r
- %************************************************************************\r
- %*                                                                      *\r
-                   Pretty printing\r
- %*                                                                      *\r
- %************************************************************************\r
\r
- \begin{code}\r
- instance Outputable HsWrapper where\r
-   ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn\r
\r
- pprHsWrapper :: SDoc -> HsWrapper -> SDoc\r
- -- In debug mode, print the wrapper\r
- -- otherwise just print what's inside\r
- pprHsWrapper doc wrap\r
-   = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)\r
-   where\r
-     help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc\r
-     -- True  <=> appears in function application position\r
-     -- False <=> appears as body of let or lambda\r
-     help it WpHole             = it\r
-     help it (WpCompose f1 f2)  = help (help it f2) f1\r
-     help it (WpCast co)   = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")\r
-                                               <+> pprParendTcCo co)]\r
-     help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]\r
-     help it (WpTyApp ty)  = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]\r
-     help it (WpEvLam id)  = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]\r
-     help it (WpTyLam tv)  = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]\r
-     help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]\r
\r
-     pp_bndr v = pprBndr LambdaBind v <> dot\r
\r
-     add_parens, no_parens :: SDoc -> Bool -> SDoc\r
-     add_parens d True  = parens d\r
-     add_parens d False = d\r
-     no_parens d _ = d\r
\r
- instance Outputable TcEvBinds where\r
-   ppr (TcEvBinds v) = ppr v\r
-   ppr (EvBinds bs)  = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))\r
\r
- instance Outputable EvBindsVar where\r
-   ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)\r
\r
- instance Outputable EvBind where\r
-   ppr (EvBind v e)   = sep [ ppr v, nest 2 $ equals <+> ppr e ]\r
-    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing\r
\r
- instance Outputable EvTerm where\r
-   ppr (EvId v)                = ppr v\r
-   ppr (EvCast v co)           = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co\r
-   ppr (EvKindCast v co)       = ppr v <+> (ptext (sLit "`kind-cast`")) <+> pprParendTcCo co\r
-   ppr (EvCoercion co)         = ptext (sLit "CO") <+> ppr co\r
-   ppr (EvTupleSel v n)        = ptext (sLit "tupsel") <> parens (ppr (v,n))\r
-   ppr (EvTupleMk vs)          = ptext (sLit "tupmk") <+> ppr vs\r
-   ppr (EvSuperClass d n)      = ptext (sLit "sc") <> parens (ppr (d,n))\r
-   ppr (EvDFunApp df tys ts)   = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]\r
-   ppr (EvInteger n)           = integer n\r
-   ppr (EvDelayedError ty msg) = ptext (sLit "error") \r
-                                 <+> sep [ char '@' <> ppr ty, ppr msg ]\r
- \end{code}\r
\r
+ \end{code}
+ %************************************************************************
+ %*                                                                      *
+                   Pretty printing
+ %*                                                                      *
+ %************************************************************************
+ \begin{code}
+ instance Outputable HsWrapper where
+   ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn
+ pprHsWrapper :: SDoc -> HsWrapper -> SDoc
+ -- In debug mode, print the wrapper
+ -- otherwise just print what's inside
+ pprHsWrapper doc wrap
+   = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)
+   where
+     help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
+     -- True  <=> appears in function application position
+     -- False <=> appears as body of let or lambda
+     help it WpHole             = it
+     help it (WpCompose f1 f2)  = help (help it f2) f1
+     help it (WpCast co)   = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
+                                               <+> pprParendTcCo co)]
+     help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]
+     help it (WpTyApp ty)  = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
+     help it (WpEvLam id)  = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
+     help it (WpTyLam tv)  = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
+     help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
+     pp_bndr v = pprBndr LambdaBind v <> dot
+     add_parens, no_parens :: SDoc -> Bool -> SDoc
+     add_parens d True  = parens d
+     add_parens d False = d
+     no_parens d _ = d
+ instance Outputable TcEvBinds where
+   ppr (TcEvBinds v) = ppr v
+   ppr (EvBinds bs)  = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))
+ instance Outputable EvBindsVar where
+   ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
+ instance Outputable EvBind where
+   ppr (EvBind v e)   = sep [ ppr v, nest 2 $ equals <+> ppr e ]
+    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
+ instance Outputable EvTerm where
+   ppr (EvId v)           = ppr v
+   ppr (EvCast v co)      = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
+   ppr (EvKindCast v co)  = ppr v <+> (ptext (sLit "`kind-cast`")) <+> pprParendTcCo co
+   ppr (EvCoercion co)    = ptext (sLit "CO") <+> ppr co
+   ppr (EvTupleSel v n)   = ptext (sLit "tupsel") <> parens (ppr (v,n))
+   ppr (EvTupleMk vs)     = ptext (sLit "tupmk") <+> ppr vs
+   ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
+   ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
++  ppr (EvInteger n)           = integer n
+   ppr (EvDelayedError ty msg) =     ptext (sLit "error") 
+                                 <+> sep [ char '@' <> ppr ty, ppr msg ]
+ \end{code}
Simple merge
Simple merge
Simple merge
Simple merge
Simple merge
Simple merge
Simple merge