Allow full constraint solving under a for-all (Trac #5595)
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 5 Dec 2011 04:44:13 +0000 (04:44 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 5 Dec 2011 04:44:13 +0000 (04:44 +0000)
The main idea is that when we unify
    forall a. t1  ~  forall a. t2
we get constraints from unifying t1~t2 that mention a.
We are producing a coercion witnessing the equivalence of
the for-alls, and inside *that* coercion we need bindings
for the solved constraints arising from t1~t2.

We didn't have way to do this before.  The big change is
that here's a new type TcEvidence.TcCoercion, which is
much like Coercion.Coercion except that there's a slot
for TcEvBinds in it.

This has a wave of follow-on changes. Not deep but broad.

* New module TcEvidence, which now contains the HsWrapper
  TcEvBinds, EvTerm etc types that used to be in HsBinds

* The typechecker works exclusively in terms of TcCoercion.

* The desugarer converts TcCoercion to Coercion

* The main payload is in TcUnify.unifySigmaTy. This is the
  function that had a gross hack before, but is now beautiful.

* LCoercion is gone!  Hooray.

Many many fiddly changes in conssequence.  But it's nice.

46 files changed:
compiler/deSugar/Desugar.lhs
compiler/deSugar/DsArrows.lhs
compiler/deSugar/DsBinds.lhs
compiler/deSugar/DsExpr.lhs
compiler/deSugar/DsListComp.lhs
compiler/deSugar/Match.lhs
compiler/deSugar/MatchCon.lhs
compiler/ghc.cabal.in
compiler/hsSyn/HsBinds.lhs
compiler/hsSyn/HsExpr.lhs
compiler/hsSyn/HsPat.lhs
compiler/hsSyn/HsUtils.lhs
compiler/main/GHC.hs
compiler/main/GhcMake.hs
compiler/parser/Parser.y.pp
compiler/parser/RdrHsSyn.lhs
compiler/rename/RnBinds.lhs
compiler/typecheck/Inst.lhs
compiler/typecheck/TcArrows.lhs
compiler/typecheck/TcBinds.lhs
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcClassDcl.lhs
compiler/typecheck/TcDeriv.lhs
compiler/typecheck/TcEnv.lhs
compiler/typecheck/TcEvidence.lhs [new file with mode: 0644]
compiler/typecheck/TcExpr.lhs
compiler/typecheck/TcForeign.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMatches.lhs
compiler/typecheck/TcMatches.lhs-boot
compiler/typecheck/TcPat.lhs
compiler/typecheck/TcRnDriver.lhs
compiler/typecheck/TcRnMonad.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcSplice.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs
compiler/typecheck/TcUnify.lhs-boot
compiler/types/Coercion.lhs
compiler/types/Type.lhs
compiler/types/TypeRep.lhs

index cb23075..cb482ea 100644 (file)
@@ -120,7 +120,7 @@ deSugar hsc_env
                               else return (binds, hpcInfo, emptyModBreaks)
 
                      initDs hsc_env mod rdr_env type_env $ do
-                       do { ds_ev_binds <- dsEvBinds ev_binds
+                       do { let ds_ev_binds = dsEvBinds ev_binds
                           ; core_prs <- dsTopLHsBinds binds_cvr
                           ; (spec_prs, spec_rules) <- dsImpSpecs imp_specs
                           ; (ds_fords, foreign_prs) <- dsForeigns fords
index d276baf..1748ce7 100644 (file)
@@ -32,6 +32,7 @@ import TcHsSyn
 import {-# SOURCE #-} DsExpr ( dsExpr, dsLExpr, dsLocalBinds )
 
 import TcType
+import TcEvidence
 import Type
 import CoreSyn
 import CoreFVs
index b6a5e3e..d44943c 100644 (file)
@@ -18,7 +18,7 @@ lower levels it is preserved with @let@/@letrec@s).
 -- for details
 
 module DsBinds ( dsTopLHsBinds, dsLHsBinds, decomposeRuleLhs, dsSpec,
-                 dsHsWrapper, dsTcEvBinds, dsEvBinds,
+                 dsHsWrapper, dsTcEvBinds, dsEvBinds, dsTcCoercion
   ) where
 
 #include "HsVersions.h"
@@ -41,6 +41,7 @@ import CoreFVs
 import Digraph
 
 import TyCon      ( isTupleTyCon, tyConDataCons_maybe )
+import TcEvidence
 import TcType
 import Type
 import Coercion hiding (substCo)
@@ -107,8 +108,7 @@ dsHsBind (FunBind { fun_id = L _ fun, fun_matches = matches
                   , fun_infix = inf })
  = do  { (args, body) <- matchWrapper (FunRhs (idName fun) inf) matches
         ; let body' = mkOptTickBox tick body
-        ; wrap_fn' <- dsHsWrapper co_fn
-        ; let rhs = wrap_fn' (mkLams args body')
+              rhs = dsHsWrapper co_fn (mkLams args body')
         ; {- pprTrace "dsHsBind" (ppr fun <+> ppr (idInlinePragma fun)) $ -}
            return (unitOL (makeCorePair fun False 0 rhs)) }
 
@@ -131,12 +131,10 @@ dsHsBind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts
   | ABE { abe_wrap = wrap, abe_poly = global
         , abe_mono = local, abe_prags = prags } <- export
   = do  { bind_prs    <- ds_lhs_binds binds
-        ; ds_ev_binds <- dsTcEvBinds ev_binds
-        ; wrap_fn <- dsHsWrapper wrap
        ; let   core_bind = Rec (fromOL bind_prs)
-                rhs       = wrap_fn $  -- Usually the identity
+                rhs       = dsHsWrapper wrap $  -- Usually the identity
                            mkLams tyvars $ mkLams dicts $ 
-                           mkCoreLets ds_ev_binds $
+                           mkCoreLets (dsTcEvBinds ev_binds) $
                             Let core_bind $
                             Var local
     
@@ -152,14 +150,13 @@ dsHsBind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts
                    , abs_exports = exports, abs_ev_binds = ev_binds
                    , abs_binds = binds })
   = do  { bind_prs    <- ds_lhs_binds binds
-        ; ds_ev_binds <- dsTcEvBinds ev_binds
         ; let core_bind = Rec (fromOL bind_prs)
                -- Monomorphic recursion possible, hence Rec
 
              tup_expr     = mkBigCoreVarTup locals
              tup_ty       = exprType tup_expr
              poly_tup_rhs = mkLams tyvars $ mkLams dicts $
-                            mkCoreLets ds_ev_binds $
+                            mkCoreLets (dsTcEvBinds ev_binds) $
                             Let core_bind $
                             tup_expr
              locals       = map abe_mono exports
@@ -168,9 +165,9 @@ dsHsBind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts
 
        ; let mk_bind (ABE { abe_wrap = wrap, abe_poly = global
                            , abe_mono = local, abe_prags = spec_prags })
-               = do { wrap_fn <- dsHsWrapper wrap
-                    ; tup_id  <- newSysLocalDs tup_ty
-                    ; let rhs = wrap_fn $ mkLams tyvars $ mkLams dicts $
+               = do { tup_id  <- newSysLocalDs tup_ty
+                    ; let rhs = dsHsWrapper wrap $ 
+                                 mkLams tyvars $ mkLams dicts $
                                 mkTupleSelector locals local tup_id $
                                 mkVarApps (Var poly_tup_id) (tyvars ++ dicts)
                            rhs_for_spec = Let (NonRec poly_tup_id poly_tup_rhs) rhs
@@ -183,104 +180,6 @@ dsHsBind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts
        ; return ((poly_tup_id, poly_tup_rhs) `consOL` 
                    concatOL export_binds_s) }
 
---------------------------------------
-dsTcEvBinds :: TcEvBinds -> DsM [CoreBind]
-dsTcEvBinds (TcEvBinds {}) = panic "dsEvBinds" -- Zonker has got rid of this
-dsTcEvBinds (EvBinds bs)   = -- pprTrace "EvBinds bs = "  (ppr bs) $ 
-                             dsEvBinds bs
-
-dsEvBinds :: Bag EvBind -> DsM [CoreBind]
-dsEvBinds bs = do { let core_binds = map dsEvSCC sccs 
---                   ; pprTrace "dsEvBinds, result = " (vcat (map ppr core_binds)) $ 
-                  ; return core_binds }
---                   ; return (map dsEvGroup sccs)
-  where
-    sccs :: [SCC EvBind]
-    sccs = stronglyConnCompFromEdgedVertices edges
-
-    edges :: [(EvBind, EvVar, [EvVar])]
-    edges = foldrBag ((:) . mk_node) [] bs 
-
-    mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
-    mk_node b@(EvBind var term) = (b, var, free_vars_of term)
-
-    free_vars_of :: EvTerm -> [EvVar]
-    free_vars_of (EvId v)           = [v]
-    free_vars_of (EvCast v co)      = v : varSetElems (coVarsOfCo co)
-    free_vars_of (EvCoercionBox co) = varSetElems (coVarsOfCo co)
-    free_vars_of (EvDFunApp _ _ vs) = vs
-    free_vars_of (EvTupleSel v _)   = [v]
-    free_vars_of (EvTupleMk vs)     = vs
-    free_vars_of (EvSuperClass d _) = [d]
-
-dsEvSCC :: SCC EvBind -> CoreBind
-
-dsEvSCC (AcyclicSCC (EvBind v r))
-  = NonRec v (dsEvTerm r)
-
-dsEvSCC (CyclicSCC bs)
-  = Rec (map ds_pair bs)
-  where
-    ds_pair (EvBind v r) = (v, dsEvTerm r)
-
----------------------------------------
-dsLCoercion :: LCoercion -> (Coercion -> CoreExpr) -> CoreExpr
--- This is the crucial function that moves 
--- from LCoercions to Coercions; see Note [LCoercions] in Coercion
--- e.g.  dsLCoercion (trans g1 g2) k
---       = case g1 of EqBox g1# ->
---         case g2 of EqBox g2# ->
---         k (trans g1# g2#)
-dsLCoercion co k 
-  = foldr wrap_in_case result_expr eqvs_covs
-  where
-    result_expr = k (substCo subst co)
-    result_ty   = exprType result_expr
-
-    -- We use the same uniques for the EqVars and the CoVars, and just change
-    -- the type. So the CoVars shadow the EqVars
-    --
-    -- NB: DON'T try to cheat and not substitute into the LCoercion to change the
-    -- types of the free variables: -ddump-ds will panic if you do this since it
-    -- runs Lint before we substitute CoVar occurrences out for their binding sites.
-    eqvs_covs = [(eqv, eqv `setIdType` mkCoercionType ty1 ty2)
-                | eqv <- varSetElems (coVarsOfCo co)
-                , let (ty1, ty2) = getEqPredTys (evVarPred eqv)]
-
-    subst = extendCvSubstList (mkEmptySubst (mkInScopeSet (tyCoVarsOfCo co)))
-                              [(eqv, mkCoVarCo cov) | (eqv, cov) <- eqvs_covs]
-
-    wrap_in_case (eqv, cov) body 
-      = Case (Var eqv) eqv result_ty [(DataAlt eqBoxDataCon, [cov], body)]
-
----------------------------------------
-dsEvTerm :: EvTerm -> CoreExpr
-dsEvTerm (EvId v) = Var v
-
-dsEvTerm (EvCast v co) 
-  = dsLCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is
-                                    -- unnecessary to call varToCoreExpr v here.
-
-dsEvTerm (EvDFunApp df tys vars) = Var df `mkTyApps` tys `mkVarApps` vars
-dsEvTerm (EvCoercionBox co)      = dsLCoercion co mkEqBox
-dsEvTerm (EvTupleSel v n)
-   = ASSERT( isTupleTyCon tc )
-     Case (Var v) (mkWildValBinder (varType v)) (tys !! n) [(DataAlt dc, xs, Var v')]
-  where
-    (tc, tys) = splitTyConApp (evVarPred v)
-    Just [dc] = tyConDataCons_maybe tc
-    v' = v `setVarType` ty_want
-    xs = map mkWildValBinder tys_before ++ v' : map mkWildValBinder tys_after
-    (tys_before, ty_want:tys_after) = splitAt n tys
-dsEvTerm (EvTupleMk vs) = Var (dataConWorkId dc) `mkTyApps` tys `mkVarApps` vs
-  where dc = tupleCon ConstraintTuple (length vs)
-        tys = map varType vs
-dsEvTerm (EvSuperClass d n)
-  = Var sc_sel_id `mkTyApps` tys `App` Var d
-  where
-    sc_sel_id  = classSCSelId cls n    -- Zero-indexed
-    (cls, tys) = getClassPredTys (evVarPred d)    
-    
 ------------------------
 makeCorePair :: Id -> Bool -> Arity -> CoreExpr -> (Id, CoreExpr)
 makeCorePair gbl_id is_default_method dict_arity rhs
@@ -500,14 +399,13 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl))
   = putSrcSpanDs loc $ 
     do { let poly_name = idName poly_id
        ; spec_name <- newLocalName poly_name
-       ; wrap_fn   <- dsHsWrapper spec_co
-       ; let (bndrs, ds_lhs) = collectBinders (wrap_fn (Var poly_id))
+       ; let (bndrs, ds_lhs) = collectBinders (dsHsWrapper spec_co (Var poly_id))
              spec_ty = mkPiTypes bndrs (exprType ds_lhs)
        ; case decomposeRuleLhs bndrs ds_lhs of {
            Left msg -> do { warnDs msg; return Nothing } ;
            Right (final_bndrs, _fn, args) -> do
 
-       { (spec_unf, unf_pairs) <- specUnfolding wrap_fn spec_ty (realIdUnfolding poly_id)
+       { (spec_unf, unf_pairs) <- specUnfolding spec_co spec_ty (realIdUnfolding poly_id)
 
        ; let spec_id  = mkLocalId spec_name spec_ty 
                            `setInlinePragma` inl_prag
@@ -540,7 +438,7 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl))
                                final_bndrs args
                                (mkVarApps (Var spec_id) bndrs)
 
-             spec_rhs  = wrap_fn poly_rhs
+             spec_rhs  = dsHsWrapper spec_co poly_rhs
              spec_pair = makeCorePair spec_id False (dictArity bndrs) spec_rhs
 
        ; return (Just (spec_pair `consOL` unf_pairs, rule))
@@ -557,7 +455,7 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl))
              | otherwise = pprPanic "dsImpSpecs" (ppr poly_id)
                            -- The type checker has checked that it *has* an unfolding
 
-specUnfolding :: (CoreExpr -> CoreExpr) -> Type 
+specUnfolding :: HsWrapper -> Type 
               -> Unfolding -> DsM (Unfolding, OrdList (Id,CoreExpr))
 {-   [Dec 10: TEMPORARILY commented out, until we can straighten out how to
               generate unfoldings for specialised DFuns
@@ -740,25 +638,138 @@ as the old one, but with an Internal name and no IdInfo.
 
 %************************************************************************
 %*                                                                     *
-               Desugaring coercions
+               Desugaring evidence
 %*                                                                     *
 %************************************************************************
 
 
 \begin{code}
-dsHsWrapper :: HsWrapper -> DsM (CoreExpr -> CoreExpr)
-dsHsWrapper WpHole           = return (\e -> e)
-dsHsWrapper (WpTyApp ty)      = return (\e -> App e (Type ty))
-dsHsWrapper (WpLet ev_binds)  = do { ds_ev_binds <- dsTcEvBinds ev_binds
---                                   ; pprTrace "Desugared core bindings = " (vcat (map ppr ds_ev_binds)) $ 
-                                   ; return (mkCoreLets ds_ev_binds) }
-dsHsWrapper (WpCompose c1 c2) = do { k1 <- dsHsWrapper c1 
-                                   ; k2 <- dsHsWrapper c2
-                                   ; return (k1 . k2) }
-dsHsWrapper (WpCast co)
-  = return (\e -> dsLCoercion co (mkCast e)) 
-dsHsWrapper (WpEvLam ev)      = return (\e -> Lam ev e) 
-dsHsWrapper (WpTyLam tv)      = return (\e -> Lam tv e) 
-dsHsWrapper (WpEvApp evtrm)
-  = return (\e -> App e (dsEvTerm evtrm))
+dsHsWrapper :: HsWrapper -> CoreExpr -> CoreExpr
+dsHsWrapper WpHole           e = e
+dsHsWrapper (WpTyApp ty)      e = App e (Type ty)
+dsHsWrapper (WpLet ev_binds)  e = mkCoreLets (dsTcEvBinds ev_binds) e
+dsHsWrapper (WpCompose c1 c2) e = dsHsWrapper c1 (dsHsWrapper c2 e) 
+dsHsWrapper (WpCast co)       e = dsTcCoercion co (mkCast e) 
+dsHsWrapper (WpEvLam ev)      e = Lam ev e 
+dsHsWrapper (WpTyLam tv)      e = Lam tv e 
+dsHsWrapper (WpEvApp evtrm)   e = App e (dsEvTerm evtrm)
+
+--------------------------------------
+dsTcEvBinds :: TcEvBinds -> [CoreBind]
+dsTcEvBinds (TcEvBinds {}) = panic "dsEvBinds" -- Zonker has got rid of this
+dsTcEvBinds (EvBinds bs)   = dsEvBinds bs
+
+dsEvBinds :: Bag EvBind -> [CoreBind]
+dsEvBinds bs = map ds_scc (sccEvBinds bs)
+  where
+    ds_scc (AcyclicSCC (EvBind v r)) = NonRec v (dsEvTerm r)
+    ds_scc (CyclicSCC bs)            = Rec (map ds_pair bs)
+
+    ds_pair (EvBind v r) = (v, dsEvTerm r)
+
+sccEvBinds :: Bag EvBind -> [SCC EvBind]
+sccEvBinds bs = stronglyConnCompFromEdgedVertices edges
+  where
+    edges :: [(EvBind, EvVar, [EvVar])]
+    edges = foldrBag ((:) . mk_node) [] bs 
+
+    mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
+    mk_node b@(EvBind var term) = (b, var, evVarsOfTerm term)
+
+
+---------------------------------------
+dsEvTerm :: EvTerm -> CoreExpr
+dsEvTerm (EvId v) = Var v
+
+dsEvTerm (EvCast v co) 
+  = dsTcCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is
+                                    -- unnecessary to call varToCoreExpr v here.
+
+dsEvTerm (EvDFunApp df tys vars) = Var df `mkTyApps` tys `mkVarApps` vars
+dsEvTerm (EvCoercion co)         = dsTcCoercion co mkEqBox
+dsEvTerm (EvTupleSel v n)
+   = ASSERT( isTupleTyCon tc )
+     Case (Var v) (mkWildValBinder (varType v)) (tys !! n) [(DataAlt dc, xs, Var v')]
+  where
+    (tc, tys) = splitTyConApp (evVarPred v)
+    Just [dc] = tyConDataCons_maybe tc
+    v' = v `setVarType` ty_want
+    xs = map mkWildValBinder tys_before ++ v' : map mkWildValBinder tys_after
+    (tys_before, ty_want:tys_after) = splitAt n tys
+dsEvTerm (EvTupleMk vs) = Var (dataConWorkId dc) `mkTyApps` tys `mkVarApps` vs
+  where dc = tupleCon ConstraintTuple (length vs)
+        tys = map varType vs
+dsEvTerm (EvSuperClass d n)
+  = Var sc_sel_id `mkTyApps` tys `App` Var d
+  where
+    sc_sel_id  = classSCSelId cls n    -- Zero-indexed
+    (cls, tys) = getClassPredTys (evVarPred d)    
+
+---------------------------------------
+dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> CoreExpr
+-- This is the crucial function that moves 
+-- from LCoercions to Coercions; see Note [TcCoercions] in Coercion
+-- e.g.  dsTcCoercion (trans g1 g2) k
+--       = case g1 of EqBox g1# ->
+--         case g2 of EqBox g2# ->
+--         k (trans g1# g2#)
+dsTcCoercion co thing_inside
+  = foldr wrap_in_case result_expr eqvs_covs
+  where
+    result_expr = thing_inside (ds_tc_coercion subst co)
+    result_ty   = exprType result_expr
+
+    -- We use the same uniques for the EqVars and the CoVars, and just change
+    -- the type. So the CoVars shadow the EqVars
+
+    eqvs_covs :: [(EqVar,CoVar)]
+    eqvs_covs = [(eqv, eqv `setIdType` mkCoercionType ty1 ty2)
+                | eqv <- varSetElems (coVarsOfTcCo co)
+                , let (ty1, ty2) = getEqPredTys (evVarPred eqv)]
+
+    subst = mkCvSubst emptyInScopeSet [(eqv, mkCoVarCo cov) | (eqv, cov) <- eqvs_covs]
+
+    wrap_in_case (eqv, cov) body 
+      = Case (Var eqv) eqv result_ty [(DataAlt eqBoxDataCon, [cov], body)]
+
+ds_tc_coercion :: CvSubst -> TcCoercion -> Coercion
+-- If the incoming TcCoercion if of type (a ~ b), 
+--                 the result is of type (a ~# b)
+-- The VarEnv maps EqVars of type (a ~ b) to Coercions of type (a ~# b)
+-- No need for InScope set etc because the 
+ds_tc_coercion subst tc_co
+  = go tc_co
+  where
+    go (TcRefl ty)            = Refl (Coercion.substTy subst ty)
+    go (TcTyConAppCo tc cos)  = mkTyConAppCo tc (map go cos)
+    go (TcAppCo co1 co2)      = mkAppCo (go co1) (go co2)
+    go (TcForAllCo tv co)     = mkForAllCo tv' (ds_tc_coercion subst' co)
+                              where
+                                (subst', tv') = Coercion.substTyVarBndr subst tv
+    go (TcAxiomInstCo ax tys) = mkAxInstCo ax (map (Coercion.substTy subst) tys)
+    go (TcSymCo co)           = mkSymCo (go co)
+    go (TcTransCo co1 co2)    = mkTransCo (go co1) (go co2)
+    go (TcNthCo n co)         = mkNthCo n (go co)
+    go (TcInstCo co ty)       = mkInstCo (go co) ty
+    go (TcLetCo bs co)        = ds_tc_coercion (ds_co_binds bs) co
+    go (TcCoVarCo v)          = ds_ev_id subst v
+
+    ds_co_binds :: TcEvBinds -> CvSubst
+    ds_co_binds (EvBinds bs)      = foldl ds_scc subst (sccEvBinds bs)
+    ds_co_binds eb@(TcEvBinds {}) = pprPanic "ds_co_binds" (ppr eb)
+
+    ds_scc :: CvSubst -> SCC EvBind -> CvSubst
+    ds_scc subst (AcyclicSCC (EvBind v ev_term))
+      = extendCvSubstAndInScope subst v (ds_ev_term subst ev_term)
+    ds_scc _ (CyclicSCC other) = pprPanic "ds_scc:cyclic" (ppr other $$ ppr tc_co)
+
+    ds_ev_term :: CvSubst -> EvTerm -> Coercion
+    ds_ev_term subst (EvCoercion tc_co) = ds_tc_coercion subst tc_co
+    ds_ev_term subst (EvId v)           = ds_ev_id subst v
+    ds_ev_term _ other = pprPanic "ds_ev_term" (ppr other $$ ppr tc_co)
+
+    ds_ev_id :: CvSubst -> EqVar -> Coercion
+    ds_ev_id subst v
+     | Just co <- Coercion.lookupCoVar subst v = co
+     | otherwise  = pprPanic "ds_tc_coercion" (ppr v $$ ppr tc_co)
 \end{code}
index 8b41d3a..74644dd 100644 (file)
@@ -31,8 +31,8 @@ import HsSyn
 -- NB: The desugarer, which straddles the source and Core worlds, sometimes
 --     needs to see source types
 import TcType
+import TcEvidence
 import Type
-import Coercion
 import CoreSyn
 import CoreUtils
 import CoreFVs
@@ -79,8 +79,7 @@ dsValBinds (ValBindsIn  _     _) _    = panic "dsValBinds ValBindsIn"
 -------------------------
 dsIPBinds :: HsIPBinds Id -> CoreExpr -> DsM CoreExpr
 dsIPBinds (IPBinds ip_binds ev_binds) body
-  = do  { ds_ev_binds <- dsTcEvBinds ev_binds
-        ; let inner = mkCoreLets ds_ev_binds body
+  = do  { let inner = mkCoreLets (dsTcEvBinds ev_binds) body
                 -- The dict bindings may not be in 
                 -- dependency order; hence Rec
         ; foldrM ds_ip_bind inner ip_binds }
@@ -128,12 +127,11 @@ dsStrictBind (AbsBinds { abs_tvs = [], abs_ev_vars = []
                , abs_exports = exports
                , abs_ev_binds = ev_binds
                , abs_binds = binds }) body
-  = do { ds_ev_binds <- dsTcEvBinds ev_binds
-       ; let body1 = foldr bind_export body exports
+  = do { let body1 = foldr bind_export body exports
              bind_export export b = bindNonRec (abe_poly export) (Var (abe_mono export)) b
        ; body2 <- foldlBagM (\body bind -> dsStrictBind (unLoc bind) body) 
                             body1 binds 
-       ; return (mkCoreLets ds_ev_binds body2) }
+       ; return (mkCoreLets (dsTcEvBinds ev_binds) body2) }
 
 dsStrictBind (FunBind { fun_id = L _ fun, fun_matches = matches, fun_co_fn = co_fn 
                       , fun_tick = tick, fun_infix = inf }) body
@@ -217,11 +215,11 @@ dsExpr (HsLit lit)            = dsLit lit
 dsExpr (HsOverLit lit)        = dsOverLit lit
 
 dsExpr (HsWrap co_fn e)
-  = do { co_fn' <- dsHsWrapper co_fn
-       ; e' <- dsExpr e
+  = do { e' <- dsExpr e
+       ; let wrapped_e = dsHsWrapper co_fn e'
        ; warn_id <- woptDs Opt_WarnIdentities
-       ; when warn_id $ warnAboutIdentities e' co_fn'
-       ; return (co_fn' e') }
+       ; when warn_id $ warnAboutIdentities e' wrapped_e
+       ; return wrapped_e }
 
 dsExpr (NegApp expr neg_expr) 
   = App <$> dsExpr neg_expr <*> dsLExpr expr
@@ -545,12 +543,12 @@ dsExpr expr@(RecordUpd record_expr (HsRecFields { rec_flds = fields })
 
                         -- Tediously wrap the application in a cast
                         -- Note [Update for GADTs]
-                 wrap_co = mkTyConAppCo tycon
+                 wrap_co = mkTcTyConAppCo tycon
                                 [ lookup tv ty | (tv,ty) <- univ_tvs `zip` out_inst_tys ]
                  lookup univ_tv ty = case lookupVarEnv wrap_subst univ_tv of
                                         Just co' -> co'
-                                        Nothing  -> mkReflCo ty
-                 wrap_subst = mkVarEnv [ (tv, mkSymCo (mkEqVarLCo eq_var))
+                                        Nothing  -> mkTcReflCo ty
+                 wrap_subst = mkVarEnv [ (tv, mkTcSymCo (mkTcCoVarCo eq_var))
                                        | ((tv,_),eq_var) <- eq_spec `zip` eqs_vars ]
 
                  pat = noLoc $ ConPatOut { pat_con = noLoc con, pat_tvs = ex_tvs
@@ -805,14 +803,15 @@ mk_fail_msg pat = "Pattern match failure in do expression at " ++
 %*                                                                      *
 %************************************************************************
 
-Warn about functions that convert between one type and another
-when the to- and from- types are the same.  Then it's probably
-(albeit not definitely) the identity
+Warn about functions like toInteger, fromIntegral, that convert
+between one type and another when the to- and from- types are the
+same.  Then it's probably (albeit not definitely) the identity
+
 \begin{code}
-warnAboutIdentities :: CoreExpr -> (CoreExpr -> CoreExpr) -> DsM ()
-warnAboutIdentities (Var v) co_fn
+warnAboutIdentities :: CoreExpr -> CoreExpr -> DsM ()
+warnAboutIdentities (Var v) wrapped_fun
   | idName v `elem` conversionNames
-  , let fun_ty = exprType (co_fn (Var v))
+  , let fun_ty = exprType wrapped_fun
   , Just (arg_ty, res_ty) <- splitFunTy_maybe fun_ty
   , arg_ty `eqType` res_ty  -- So we are converting  ty -> ty
   = warnDs (vcat [ ptext (sLit "Call of") <+> ppr v <+> dcolon <+> ppr fun_ty
index 63d96fd..4ad8006 100644 (file)
@@ -19,6 +19,7 @@ import TcHsSyn
 import CoreSyn
 import MkCore
 
+import TcEvidence
 import DsMonad          -- the monadery used in the desugarer
 import DsUtils
 
index 236a05b..cd0153e 100644 (file)
@@ -22,6 +22,7 @@ import {-#SOURCE#-} DsExpr (dsLExpr)
 import DynFlags
 import HsSyn           
 import TcHsSyn
+import TcEvidence
 import Check
 import CoreSyn
 import Literal
@@ -36,7 +37,6 @@ import DataCon
 import MatchCon
 import MatchLit
 import Type
-import Coercion
 import TysWiredIn
 import ListSetOps
 import SrcLoc
@@ -356,8 +356,7 @@ matchCoercion (var:vars) ty (eqns@(eqn1:_))
        ; var' <- newUniqueId var (hsPatType pat)
        ; match_result <- match (var':vars) ty $
                           map (decomposeFirstPat getCoPat) eqns
-       ; co' <- dsHsWrapper co
-        ; let rhs' = co' (Var var)
+        ; let rhs' = dsHsWrapper co (Var var)
        ; return (mkCoLetMatchResult (NonRec var' rhs') match_result) }
 matchCoercion _ _ _ = panic "matchCoercion"
 
@@ -919,7 +918,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
     --        equating different ways of writing a coercion)
     wrap WpHole WpHole = True
     wrap (WpCompose w1 w2) (WpCompose w1' w2') = wrap w1 w1' && wrap w2 w2'
-    wrap (WpCast co)       (WpCast co')        = co `coreEqCoercion` co'
+    wrap (WpCast co)       (WpCast co')        = co `eq_co` co'
     wrap (WpEvApp et1)     (WpEvApp et2)       = et1 `ev_term` et2
     wrap (WpTyApp t)       (WpTyApp t')        = eqType t t'
     -- Enhancement: could implement equality for more wrappers
@@ -928,8 +927,8 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
 
     ---------
     ev_term :: EvTerm -> EvTerm -> Bool
-    ev_term (EvId a)          (EvId b)          = a==b
-    ev_term (EvCoercionBox a) (EvCoercionBox b) = coreEqCoercion a b
+    ev_term (EvId a)       (EvId b)       = a==b
+    ev_term (EvCoercion a) (EvCoercion b) = a `eq_co` b
     ev_term _ _ = False        
 
     ---------
@@ -939,6 +938,15 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
     eq_list _  (_:_)  []     = False
     eq_list eq (x:xs) (y:ys) = eq x y && eq_list eq xs ys
 
+    ---------
+    eq_co :: TcCoercion -> TcCoercion -> Bool 
+    -- Just some simple cases
+    eq_co (TcRefl t1)             (TcRefl t2)             = eqType t1 t2
+    eq_co (TcCoVarCo v1)         (TcCoVarCo v2)          = v1==v2
+    eq_co (TcSymCo co1)          (TcSymCo co2)           = co1 `eq_co` co2
+    eq_co (TcTyConAppCo tc1 cos1) (TcTyConAppCo tc2 cos2) = tc1==tc2 && eq_list eq_co cos1 cos2
+    eq_co _ _ = False
+
 patGroup :: Pat Id -> PatGroup
 patGroup (WildPat {})                = PgAny
 patGroup (BangPat {})                = PgBang  
index 989008a..f3b613f 100644 (file)
@@ -131,19 +131,18 @@ matchOneCon vars ty (eqn1 : eqns) -- All eqns for a single constructor
     match_group :: [Id] -> [(ConArgPats, EquationInfo)] -> DsM MatchResult
     -- All members of the group have compatible ConArgPats
     match_group arg_vars arg_eqn_prs
-      = do { (wraps, eqns') <- mapAndUnzipM shift arg_eqn_prs
-          ; let group_arg_vars = select_arg_vars arg_vars arg_eqn_prs
+      = do { let (wraps, eqns') = unzip (map shift arg_eqn_prs)
+                group_arg_vars = select_arg_vars arg_vars arg_eqn_prs
           ; match_result <- match (group_arg_vars ++ vars) ty eqns'
           ; return (adjustMatchResult (foldr1 (.) wraps) match_result) }
 
     shift (_, eqn@(EqnInfo { eqn_pats = ConPatOut{ pat_tvs = tvs, pat_dicts = ds, 
                                                   pat_binds = bind, pat_args = args
                                        } : pats }))
-      = do { ds_ev_binds <- dsTcEvBinds bind
-          ; return (wrapBinds (tvs `zip` tvs1) 
-                   . wrapBinds (ds  `zip` dicts1)
-                   . mkCoreLets ds_ev_binds,
-                   eqn { eqn_pats = conArgPats arg_tys args ++ pats }) }
+      = ( wrapBinds (tvs `zip` tvs1) 
+         . wrapBinds (ds  `zip` dicts1)
+         . mkCoreLets (dsTcEvBinds bind)
+       , eqn { eqn_pats = conArgPats arg_tys args ++ pats }) 
     shift (_, (EqnInfo { eqn_pats = ps })) = pprPanic "matchOneCon/shift" (ppr ps)
 
     -- Choose the right arg_vars in the right order for this group
index a976efa..15b9943 100644 (file)
@@ -411,6 +411,7 @@ Library
         TcTyClsDecls
         TcTyDecls
         TcType
+        TcEvidence
         TcUnify
         TcInteract
         TcCanonical
index b6bc0c7..bb8b337 100644 (file)
@@ -27,7 +27,7 @@ import HsLit
 import HsTypes
 import PprCore ()
 import CoreSyn
-import Coercion
+import TcEvidence
 import Type
 import Name
 import NameSet
@@ -35,15 +35,11 @@ import BasicTypes
 import Outputable      
 import SrcLoc
 import Util
-import VarEnv
 import Var
 import Bag
-import Unique
 import FastString
 
-import Data.IORef( IORef )
 import Data.Data hiding ( Fixity )
-
 import Data.List ( intersect )
 \end{code}
 
@@ -440,227 +436,6 @@ instance (OutputableBndr id) => Outputable (IPBind id) where
 
 %************************************************************************
 %*                                                                      *
-\subsection{Coercion functions}
-%*                                                                      *
-%************************************************************************
-
-\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 LCoercion          -- 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, Typeable)
-
-
-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( Typeable )
-
-data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
-     -- The Unique is only for debug printing
-
------------------
-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)
-
------------------
-instance Data TcEvBinds where
-  -- Placeholder; we can't travers into TcEvBinds
-  toConstr _   = abstractConstr "TcEvBinds"
-  gunfold _ _  = error "gunfold"
-  dataTypeOf _ = mkNoRepType "TcEvBinds"
-
--- 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 EvCoercionBox)
-
-  | EvCoercionBox LCoercion    -- (Boxed) coercion bindings
-
-  | EvCast EvVar LCoercion     -- 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
-
-  | 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_
-
-  deriving( Data, Typeable)
-\end{code}
-
-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]
-
-
-\begin{code}
-mkEvCast :: EvVar -> LCoercion -> EvTerm
-mkEvCast ev lco
-  | isReflCo lco = EvId ev
-  | otherwise    = EvCast ev lco
-
-emptyTcEvBinds :: TcEvBinds
-emptyTcEvBinds = EvBinds emptyBag
-
-isEmptyTcEvBinds :: TcEvBinds -> Bool
-isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b
-isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
-
-(<.>) :: 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}
-
-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 "|>")
-                                              <+> pprParendCo 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 (ppr bs)
-
-instance Outputable EvBindsVar where
-  ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
-
-instance Outputable EvBind where
-  ppr (EvBind v e)   = ppr v <+> 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`")) <+> pprParendCo co
-  ppr (EvCoercionBox 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 ]
-\end{code}
-
-%************************************************************************
-%*                                                                      *
 \subsection{@Sig@: type signatures and value-modifying user pragmas}
 %*                                                                      *
 %************************************************************************
index af2de9f..5a18fc6 100644 (file)
@@ -25,6 +25,7 @@ import HsTypes
 import HsBinds
 
 -- others:
+import TcEvidence
 import CoreSyn
 import Var
 import Name
index 236f211..3180d24 100644 (file)
@@ -29,6 +29,7 @@ import {-# SOURCE #-} HsExpr            (SyntaxExpr, LHsExpr, pprLExpr)
 import HsBinds
 import HsLit
 import HsTypes
+import TcEvidence
 import BasicTypes
 -- others:
 import PprCore          ( {- instance OutputableBndr TyVar -} )
index 358f8bb..234791d 100644 (file)
@@ -82,9 +82,9 @@ import HsPat
 import HsTypes 
 import HsLit
 
+import TcEvidence
 import RdrName
 import Var
-import Coercion
 import TypeRep
 import DataCon
 import Name
@@ -172,37 +172,6 @@ mkParPat :: LPat name -> LPat name
 mkParPat lp@(L loc p) | hsPatNeedsParens p = L loc (ParPat lp)
                       | otherwise          = lp
 
---------- HsWrappers: type args, dict args, casts ---------
-mkLHsWrap :: HsWrapper -> LHsExpr id -> LHsExpr id
-mkLHsWrap co_fn (L loc e) = L loc (mkHsWrap co_fn e)
-
-mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id
-mkHsWrap co_fn e | isIdHsWrapper co_fn = e
-                | otherwise           = HsWrap co_fn e
-
-mkHsWrapCo :: LCoercion -> HsExpr id -> HsExpr id
-mkHsWrapCo (Refl _) e = e
-mkHsWrapCo co       e = mkHsWrap (WpCast co) e
-
-mkLHsWrapCo :: LCoercion -> LHsExpr id -> LHsExpr id
-mkLHsWrapCo (Refl _) e         = e
-mkLHsWrapCo co       (L loc e) = L loc (mkHsWrap (WpCast co) e)
-
-coToHsWrapper :: LCoercion -> HsWrapper
-coToHsWrapper (Refl _) = idHsWrapper
-coToHsWrapper co       = WpCast co
-
-mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id
-mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
-                      | otherwise           = CoPat co_fn p ty
-
-mkHsWrapPatCo :: LCoercion -> Pat id -> Type -> Pat id
-mkHsWrapPatCo (Refl _) pat _  = pat
-mkHsWrapPatCo co       pat ty = CoPat (WpCast co) pat ty
-
-mkHsDictLet :: TcEvBinds -> LHsExpr Id -> LHsExpr Id
-mkHsDictLet ev_binds expr = mkLHsWrap (mkWpLet ev_binds) expr
-
 
 -------------------------------
 -- These are the bits of syntax that contain rebindable names
@@ -404,6 +373,39 @@ missingTupArg :: HsTupArg a
 missingTupArg = Missing placeHolderType
 \end{code}
 
+\begin{code}
+--------- HsWrappers: type args, dict args, casts ---------
+mkLHsWrap :: HsWrapper -> LHsExpr id -> LHsExpr id
+mkLHsWrap co_fn (L loc e) = L loc (mkHsWrap co_fn e)
+
+mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id
+mkHsWrap co_fn e | isIdHsWrapper co_fn = e
+                | otherwise           = HsWrap co_fn e
+
+mkHsWrapCo :: TcCoercion -> HsExpr id -> HsExpr id
+mkHsWrapCo co e | isTcReflCo co = e
+                | otherwise     = mkHsWrap (WpCast co) e
+
+mkLHsWrapCo :: TcCoercion -> LHsExpr id -> LHsExpr id
+mkLHsWrapCo co (L loc e) | isTcReflCo co = L loc e
+                         | otherwise     = L loc (mkHsWrap (WpCast co) e)
+
+coToHsWrapper :: TcCoercion -> HsWrapper
+coToHsWrapper co | isTcReflCo co = idHsWrapper
+                 | otherwise     = WpCast co
+
+mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id
+mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
+                      | otherwise           = CoPat co_fn p ty
+
+mkHsWrapPatCo :: TcCoercion -> Pat id -> Type -> Pat id
+mkHsWrapPatCo co pat ty | isTcReflCo co = pat
+                        | otherwise     = CoPat (WpCast co) pat ty
+
+mkHsDictLet :: TcEvBinds -> LHsExpr Id -> LHsExpr Id
+mkHsDictLet ev_binds expr = mkLHsWrap (mkWpLet ev_binds) expr
+\end{code}
+l
 %************************************************************************
 %*                                                                     *
                Bindings; with a location at the top
index c731b0a..7b82b11 100644 (file)
@@ -262,7 +262,7 @@ import Packages
 import NameSet
 import RdrName
 import qualified HsSyn -- hack as we want to reexport the whole module
-import HsSyn hiding ((<.>))
+import HsSyn
 import Type     hiding( typeKind )
 import Kind            ( synTyConResKind )
 import TcType          hiding( typeKind )
index abbaa1f..3db9205 100644 (file)
@@ -38,7 +38,7 @@ import Module
 import HscTypes
 import ErrUtils
 import DynFlags
-import HsSyn hiding ((<.>))
+import HsSyn
 import Finder
 import HeaderInfo
 import TcIface         ( typecheckIface )
index 8a57504..855a428 100644 (file)
@@ -32,6 +32,7 @@ import RdrHsSyn
 import HscTypes         ( IsBootInterface, WarningTxt(..) )
 import Lexer
 import RdrName
+import TcEvidence       ( emptyTcEvBinds )
 import TysPrim          ( liftedTypeKindTyConName, eqPrimTyCon )
 import TysWiredIn       ( unitTyCon, unitDataCon, tupleTyCon, tupleCon, nilDataCon,
                           unboxedSingletonTyCon, unboxedSingletonDataCon,
index 3b1a289..10e731b 100644 (file)
@@ -54,6 +54,7 @@ import RdrName          ( RdrName, isRdrTyVar, isRdrTc, mkUnqual, rdrNameOcc,
 import Name             ( Name )
 import BasicTypes       ( maxPrecedence, Activation(..), RuleMatchInfo,
                           InlinePragma(..), InlineSpec(..) )
+import TcEvidence       ( idHsWrapper )
 import Lexer
 import TysWiredIn       ( unitTyCon )
 import ForeignCall
index 51cd09f..0da8070 100644 (file)
@@ -35,6 +35,7 @@ import {-# SOURCE #-} RnExpr( rnLExpr, rnStmts )
 import HsSyn
 import RnHsSyn
 import TcRnMonad
+import TcEvidence     ( emptyTcEvBinds )
 import RnTypes        ( rnIPName, rnHsSigType, rnLHsType, checkPrecMatch )
 import RnPat
 import RnEnv
index 40d0d2b..34f6818 100644 (file)
@@ -48,6 +48,7 @@ import HsSyn
 import TcHsSyn
 import TcRnMonad
 import TcEnv
+import TcEvidence
 import InstEnv
 import FunDeps
 import TcMType
@@ -223,7 +224,7 @@ instCallConstraints origin (pred : preds)
   = do  { traceTc "instCallConstraints" $ ppr (mkEqPred (ty1, ty2))
         ; co <- unifyType ty1 ty2
        ; co_fn <- instCallConstraints origin preds
-        ; return (co_fn <.> WpEvApp (EvCoercionBox co)) }
+        ; return (co_fn <.> WpEvApp (EvCoercion co)) }
 
   | otherwise
   = do { ev_var <- emitWanted origin pred
index e6943ea..f58c566 100644 (file)
@@ -25,7 +25,7 @@ import TcPat
 import TcUnify
 import TcRnMonad
 import TcEnv
-import Coercion
+import TcEvidence
 import Id( mkLocalId )
 import Inst
 import Name
@@ -50,7 +50,7 @@ import Control.Monad
 \begin{code}
 tcProc :: InPat Name -> LHsCmdTop Name         -- proc pat -> expr
        -> TcRhoType                            -- Expected type of whole proc expression
-       -> TcM (OutPat TcId, LHsCmdTop TcId, LCoercion)
+       -> TcM (OutPat TcId, LHsCmdTop TcId, TcCoercion)
 
 tcProc pat cmd exp_ty
   = newArrowScope $
@@ -59,7 +59,7 @@ tcProc pat cmd exp_ty
        ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
         ; (pat', cmd') <- tcPat ProcExpr pat arg_ty $
                          tcCmdTop cmd_env cmd [] res_ty
-        ; let res_co = mkTransCo co (mkAppCo co1 (mkReflCo res_ty))
+        ; let res_co = mkTcTransCo co (mkTcAppCo co1 (mkTcReflCo res_ty))
         ; return (pat', cmd', res_co) }
 \end{code}
 
index 9f5257a..5e128c7 100644 (file)
@@ -21,6 +21,7 @@ import TcRnMonad
 import TcEnv
 import TcUnify
 import TcSimplify
+import TcEvidence
 import TcHsType
 import TcPat
 import TcMType
index d13b793..f2b6527 100644 (file)
@@ -24,7 +24,7 @@ import qualified TcMType as TcM
 import TcType
 import Type
 import Kind
-import Coercion
+import TcEvidence
 import Class
 import TyCon
 import TypeRep
@@ -38,7 +38,6 @@ import Control.Applicative ( (<|>) )
 
 import TrieMap
 import VarSet
-import HsBinds
 import TcSMonad
 import FastString
 
@@ -257,7 +256,7 @@ canIP d fl v nm ty
        -- possible in principle to not flatten, but since flattening applies 
        -- the inert substitution we choose to flatten anyway.
     do { (xi,co) <- flatten d fl (mkIPPred nm ty)
-       ; let no_flattening = isReflCo co 
+       ; let no_flattening = isTcReflCo co 
        ; if no_flattening then
             let IPPred _ xi_in = classifyPredType xi 
             in continueWith $ CIPCan { cc_id = v, cc_flavor = fl
@@ -268,7 +267,7 @@ canIP d fl v nm ty
                        IPPred _ ip_xi = classifyPredType xi
                  ; fl_new <- case fl of 
                                Wanted {}  -> setEvBind v (EvCast v_new co) fl 
-                               Given {}   -> setEvBind v_new (EvCast v (mkSymCo co)) fl
+                               Given {}   -> setEvBind v_new (EvCast v (mkTcSymCo co)) fl
                                Derived {} -> return fl
                  ; if isNewEvVar evc then
                        continueWith $ CIPCan { cc_id     = v_new
@@ -301,10 +300,10 @@ canClass :: SubGoalDepth -- Depth
 canClass d fl v cls tys
   = do { -- sctx <- getTcSContext
        ; (xis, cos) <- flattenMany d fl tys
-       ; let co = mkTyConAppCo (classTyCon cls) cos 
+       ; let co = mkTcTyConAppCo (classTyCon cls) cos 
              xi = mkClassPred cls xis
 
-       ; let no_flattening = all isReflCo cos
+       ; let no_flattening = all isTcReflCo cos
                   -- No flattening, continue with canonical
        ; if no_flattening then 
              continueWith $ CDictCan { cc_id = v, cc_flavor = fl
@@ -315,7 +314,7 @@ canClass d fl v cls tys
                  ; let v_new = evc_the_evvar evc
                  ; fl_new <- case fl of
                      Wanted  {} -> setEvBind v (EvCast v_new co) fl
-                     Given   {} -> setEvBind v_new (EvCast v (mkSymCo co)) fl
+                     Given   {} -> setEvBind v_new (EvCast v (mkTcSymCo co)) fl
                      Derived {} -> return fl
                     -- Continue only if flat constraint is new
                  ; if isNewEvVar evc then
@@ -463,7 +462,7 @@ canIrred d fl v ty
        ; (xi,co) <- flatten d fl ty -- co :: xi ~ ty
        ; let no_flattening = xi `eqType` ty 
                              -- In this particular case it is not safe to 
-                             -- say 'isReflCo' because the new constraint may
+                             -- say 'isTcReflCo' because the new constraint may
                              -- be reducible!
        ; if no_flattening then
             continueWith $ CIrredEvCan { cc_id = v, cc_flavor = fl
@@ -476,7 +475,7 @@ canIrred d fl v ty
       ; let v' = evc_the_evvar evc
       ; fl' <- case fl of 
           Wanted  {} -> setEvBind v (EvCast v' co) fl
-          Given   {} -> setEvBind v' (EvCast v (mkSymCo co)) fl
+          Given   {} -> setEvBind v' (EvCast v (mkTcSymCo co)) fl
           Derived {} -> return fl
       
       ; if isNewEvVar evc then 
@@ -536,7 +535,7 @@ unexpanded synonym.
 
 -- Flatten a bunch of types all at once.
 flattenMany :: SubGoalDepth -- Depth
-            -> CtFlavor -> [Type] -> TcS ([Xi], [LCoercion])
+            -> CtFlavor -> [Type] -> TcS ([Xi], [TcCoercion])
 -- Coercions :: Xi ~ Type 
 -- Returns True iff (no flattening happened)
 flattenMany d ctxt tys 
@@ -551,7 +550,7 @@ flattenMany d ctxt tys
 -- the new type-function-free type, and a collection of new equality
 -- constraints.  See Note [Flattening] for more detail.
 flatten :: SubGoalDepth -- Depth
-        -> CtFlavor -> TcType -> TcS (Xi, LCoercion)
+        -> CtFlavor -> TcType -> TcS (Xi, TcCoercion)
 -- Postcondition: Coercion :: Xi ~ TcType
 flatten d ctxt ty 
   | Just ty' <- tcView ty
@@ -561,21 +560,21 @@ flatten d ctxt ty
        -- DV: The following is tedious to do but maybe we should return to this
        -- Preserve type synonyms if possible
        -- ; if no_flattening
-       --   then return (xi, mkReflCo xi,no_flattening) -- Importantly, not xi!
+       --   then return (xi, mkTcReflCo xi,no_flattening) -- Importantly, not xi!
        --   else return (xi,co,no_flattening) 
        -- }
 
 flatten d ctxt v@(TyVarTy _)
   = do { ieqs <- getInertEqs
        ; let co = liftInertEqsTy ieqs ctxt v           -- co : v ~ ty
-             ty = pSnd (liftedCoercionKind co)
+             ty = pSnd (tcCoercionKind co)
        ; if v `eqType` ty then
-             return (ty,mkReflCo ty)
+             return (ty,mkTcReflCo ty)
          else -- NB recursive call. Why? See Note [Non-idempotent inert substitution]
               -- Actually I believe that applying the substition only *twice* will suffice
          
              do { (ty_final,co') <- flatten d ctxt ty  -- co' : ty_final ~ ty
-                ; return (ty_final,co' `mkTransCo` mkSymCo co) } }
+                ; return (ty_final,co' `mkTcTransCo` mkTcSymCo co) } }
 
 \end{code}
 
@@ -613,19 +612,19 @@ This insufficient rewriting was the reason for #5668.
 flatten d ctxt (AppTy ty1 ty2)
   = do { (xi1,co1) <- flatten d ctxt ty1
        ; (xi2,co2) <- flatten d ctxt ty2
-       ; return (mkAppTy xi1 xi2, mkAppCo co1 co2) }
+       ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
 
 flatten d ctxt (FunTy ty1 ty2)
   = do { (xi1,co1) <- flatten d ctxt ty1
        ; (xi2,co2) <- flatten d ctxt ty2
-       ; return (mkFunTy xi1 xi2, mkFunCo co1 co2) }
+       ; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) }
 
 flatten d fl (TyConApp tc tys)
   -- For a normal type constructor or data family application, we just
   -- recursively flatten the arguments.
   | not (isSynFamilyTyCon tc)
     = do { (xis,cos) <- flattenMany d fl tys
-         ; return (mkTyConApp tc xis, mkTyConAppCo tc cos) }
+         ; return (mkTyConApp tc xis, mkTcTyConAppCo tc cos) }
 
   -- Otherwise, it's a type function application, and we have to
   -- flatten it away as well, and generate a new given equality constraint
@@ -648,7 +647,7 @@ flatten d fl (TyConApp tc tys)
                         | isGivenOrSolved fl ->
                             do { rhs_xi_var <- newFlattenSkolemTy fam_ty
                                ; (fl',eqv) 
-                                   <- newGivenEqVar fl fam_ty rhs_xi_var (mkReflCo fam_ty)
+                                   <- newGivenEqVar fl fam_ty rhs_xi_var (mkTcReflCo fam_ty)
                                ; let ct  = CFunEqCan { cc_id     = eqv
                                                      , cc_flavor = fl' -- Given
                                                      , cc_fun    = tc 
@@ -657,7 +656,7 @@ flatten d fl (TyConApp tc tys)
                                                      , cc_depth  = d }
                                            -- Update the flat cache: just an optimisation!
                                ; updateFlatCache eqv fl' tc xi_args rhs_xi_var WhileFlattening
-                               ; return (mkEqVarLCo eqv, rhs_xi_var, [ct]) }
+                               ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
                         | otherwise ->
                     -- Derived or Wanted: make a new /unification/ flatten variable
                             do { rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
@@ -673,7 +672,7 @@ flatten d fl (TyConApp tc tys)
                                                     , cc_depth  = d }
                                           -- Update the flat cache: just an optimisation!
                                ; updateFlatCache eqv fl tc xi_args rhs_xi_var WhileFlattening
-                               ; return (mkEqVarLCo eqv, rhs_xi_var, [ct]) } }
+                               ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) } }
 
            -- Emit the flat constraints
          ; updWorkListTcS $ appendWorkListEqs ct
@@ -681,8 +680,8 @@ flatten d fl (TyConApp tc tys)
          ; let (cos_args, cos_rest) = splitAt (tyConArity tc) cos
          ; return ( mkAppTys rhs_xi xi_rest    -- NB mkAppTys: rhs_xi might not be a type variable
                                               --    cf Trac #5655
-                  , foldl AppCo (mkSymCo ret_co `mkTransCo` mkTyConAppCo tc cos_args)
-                                cos_rest
+                  , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo tc cos_args)
+                               cos_rest
                   ) }
 
 
@@ -692,7 +691,7 @@ flatten d ctxt ty@(ForAllTy {})
   = do { let (tvs, rho) = splitForAllTys ty
        ; when (under_families tvs rho) $ flattenForAllErrorTcS ctxt ty
        ; (rho', co) <- flatten d ctxt rho
-       ; return (mkForAllTys tvs rho', foldr mkForAllCo co tvs) }
+       ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
 
   where under_families tvs rho 
             = go (mkVarSet tvs) rho 
@@ -709,7 +708,7 @@ flatten d ctxt ty@(ForAllTy {})
 
 getCachedFlatEq :: TyCon -> [Xi] -> CtFlavor 
                 -> FlatEqOrigin
-                -> TcS (Maybe (Xi,Coercion))
+                -> TcS (Maybe (Xi, TcCoercion))
 -- Returns a coercion between (TyConApp tc xi_args ~ xi) if such an inert item exists
 -- But also applies the substitution to the item via calling flatten recursively
 getCachedFlatEq tc xi_args fl feq_origin
@@ -731,7 +730,7 @@ getCachedFlatEq tc xi_args fl feq_origin
                                     -- The only purpose of this flattening is to apply the
                                     -- inert substitution (since everything in the flat cache
                                     -- by construction will have a family-free RHS.
-                     ; return $ Just (xi'', co' `mkTransCo` (mkSymCo co)) }
+                     ; return $ Just (xi'', co' `mkTcTransCo` (mkTcSymCo co)) }
               _ -> do { traceTcS "getCachedFlatEq" $ text "failure!" <+> pprEvVarCache flat_cache
                       ; return Nothing }
 
@@ -769,7 +768,7 @@ canEq _d fl eqv ty1 ty2
   | eqType ty1 ty2     -- Dealing with equality here avoids
                        -- later spurious occurs checks for a~a
   = do { when (isWanted fl) $ 
-              do { _ <- setEqBind eqv (mkReflCo ty1) fl; return () }
+              do { _ <- setEqBind eqv (mkTcReflCo ty1) fl; return () }
        ; return Stop }
 
 -- Split up an equality between function types into two equalities.
@@ -780,11 +779,11 @@ canEq d fl eqv (FunTy s1 t1) (FunTy s2 t2)
              reseqv_v = evc_the_evvar reseqv
        ; (fl1,fl2) <- case fl of
            Wanted {} ->
-               do { _ <- setEqBind eqv (mkFunCo (mkEqVarLCo argeqv_v) (mkEqVarLCo reseqv_v)) fl
+               do { _ <- setEqBind eqv (mkTcFunCo (mkTcCoVarCo argeqv_v) (mkTcCoVarCo reseqv_v)) fl
                   ; return (fl,fl) }
            Given {} ->
-               do { fl1 <- setEqBind argeqv_v (mkNthCo 0 (mkEqVarLCo eqv)) fl
-                  ; fl2 <- setEqBind reseqv_v (mkNthCo 1 (mkEqVarLCo eqv)) fl 
+               do { fl1 <- setEqBind argeqv_v (mkTcNthCo 0 (mkTcCoVarCo eqv)) fl
+                  ; fl2 <- setEqBind reseqv_v (mkTcNthCo 1 (mkTcCoVarCo eqv)) fl 
                   ; return (fl1,fl2)
                   }
            Derived {} ->
@@ -814,17 +813,17 @@ canEq d fl eqv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
   = -- Generate equalities for each of the corresponding arguments
     do { let (kis1,  tys1') = span isKind tys1
              (_kis2, tys2') = span isKind tys2
-       ; let kicos = map mkReflCo kis1
+       ; let kicos = map mkTcReflCo kis1
 
        ; argeqvs <- zipWithM (newEqVar fl) tys1' tys2'
        ; fls <- case fl of 
            Wanted {} -> 
              do { _ <- setEqBind eqv
-                         (mkTyConAppCo tc1 (kicos ++ map (mkEqVarLCo . evc_the_evvar) argeqvs)) fl
+                         (mkTcTyConAppCo tc1 (kicos ++ map (mkTcCoVarCo . evc_the_evvar) argeqvs)) fl
                 ; return (map (\_ -> fl) argeqvs) }
            Given {} ->
              let do_one argeqv n = setEqBind (evc_the_evvar argeqv) 
-                                             (mkNthCo n (mkEqVarLCo eqv)) fl
+                                             (mkTcNthCo n (mkTcCoVarCo eqv)) fl
              in zipWithM do_one argeqvs [(length kicos)..]
            Derived {} -> return (map (\_ -> fl) argeqvs)
 
@@ -852,7 +851,7 @@ canEq d fl eqv ty1 ty2
                  eqv2 = evc_the_evvar evc2
  
            ; when (isWanted fl) $
-                  do { _ <- setEqBind eqv (mkAppCo (mkEqVarLCo eqv1) (mkEqVarLCo eqv2)) fl
+                  do { _ <- setEqBind eqv (mkTcAppCo (mkTcCoVarCo eqv1) (mkTcCoVarCo eqv2)) fl
                      ; return () }
            
            ; canEqEvVarsCreated d [fl,fl] [evc1,evc2] [s1,t1] [s2,t2] }
@@ -1087,8 +1086,8 @@ canEqLeaf d fl eqv s1 s2
        ; evc <- newEqVar fl s2 s1
        ; let eqv' = evc_the_evvar evc
        ; fl' <- case fl of 
-           Wanted {}  -> setEqBind eqv (mkSymCo (mkEqVarLCo eqv')) fl 
-           Given {}   -> setEqBind eqv' (mkSymCo (mkEqVarLCo eqv)) fl 
+           Wanted {}  -> setEqBind eqv (mkTcSymCo (mkTcCoVarCo eqv')) fl 
+           Given {}   -> setEqBind eqv' (mkTcSymCo (mkTcCoVarCo eqv)) fl 
            Derived {} -> return fl 
        ; if isNewEvVar evc then 
              do { canEqLeafOriented d fl' eqv' s2 s1 }
@@ -1151,7 +1150,7 @@ canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2  -- eqv :: F tys1 ~ ty2
        ; let is_cached = {-# SCC "lookupFunEq" #-} 
                          lookupFunEq flat_ty fl fam_eqs
 -}
-       ; let no_flattening = all isReflCo cos1
+       ; let no_flattening = all isTcReflCo cos1
                       
        ; if no_flattening && isNothing is_cached then 
              canEqLeafFunEqLeft d fl eqv (fn,xis1) ty2
@@ -1159,19 +1158,19 @@ canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2  -- eqv :: F tys1 ~ ty2
        { let (final_co, final_ty)
                  | no_flattening        -- Just in inerts
                  , Just (rhs_ty, ret_eq) <- is_cached
-                 = (mkSymCo ret_eq, rhs_ty)
+                 = (mkTcSymCo ret_eq, rhs_ty)
                  | Nothing <- is_cached -- Just flattening
-                 = (mkTyConAppCo fn cos1, flat_ty)
+                 = (mkTcTyConAppCo fn cos1, flat_ty)
                  | Just (rhs_ty, ret_eq) <- is_cached  -- Both
-                 = (mkSymCo ret_eq `mkTransCo` mkTyConAppCo fn cos1, rhs_ty)
+                 = (mkTcSymCo ret_eq `mkTcTransCo` mkTcTyConAppCo fn cos1, rhs_ty)
                  | otherwise = panic "No flattening and not cached!"
        ; delCachedEvVar eqv fl
        ; evc <- newEqVar fl final_ty ty2
        ; let new_eqv = evc_the_evvar evc
        ; fl' <- case fl of
            Wanted {}  -> setEqBind eqv 
-                           (mkSymCo final_co `mkTransCo` (mkEqVarLCo new_eqv)) fl
-           Given {}   -> setEqBind new_eqv (final_co `mkTransCo` (mkEqVarLCo eqv)) fl
+                           (mkTcSymCo final_co `mkTcTransCo` (mkTcCoVarCo new_eqv)) fl
+           Given {}   -> setEqBind new_eqv (final_co `mkTcTransCo` (mkTcCoVarCo eqv)) fl
            Derived {} -> return fl
        ; if isNewEvVar evc then
              if isNothing is_cached then
@@ -1183,12 +1182,12 @@ canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2  -- eqv :: F tys1 ~ ty2
        }
        }
 
-lookupFunEq :: PredType -> CtFlavor -> TypeMap Ct -> Maybe (TcType,Coercion)
+lookupFunEq :: PredType -> CtFlavor -> TypeMap Ct -> Maybe (TcType, TcCoercion)
 lookupFunEq pty fl fam_eqs = lookup_funeq pty fam_eqs
   where lookup_funeq pty fam_eqs
           | Just ct <- lookupTM pty fam_eqs
           , cc_flavor ct `canRewrite` fl 
-          = Just (cc_rhs ct, mkEqVarLCo (cc_id ct))
+          = Just (cc_rhs ct, mkTcCoVarCo (cc_id ct))
           | otherwise 
           = Nothing
 
@@ -1202,7 +1201,7 @@ canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
       ; (xi2,co2) <- 
           {-# SCC "flatten" #-} 
           flatten d fl s2 -- co2 :: xi2 ~ s2
-      ; let no_flattening_happened = isReflCo co2
+      ; let no_flattening_happened = isTcReflCo co2
       ; if no_flattening_happened then 
             continueWith $ CFunEqCan { cc_id     = eqv
                                      , cc_flavor = fl
@@ -1215,11 +1214,11 @@ canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
                     {-# SCC "newEqVar" #-}
                     newEqVar fl (mkTyConApp fn xis1) xi2
                 ; let new_eqv = evc_the_evvar evc -- F xis1 ~ xi2 
-                      new_cv  = mkEqVarLCo new_eqv
-                      cv      = mkEqVarLCo eqv    -- F xis1 ~ s2
+                      new_cv  = mkTcCoVarCo new_eqv
+                      cv      = mkTcCoVarCo eqv    -- F xis1 ~ s2
                 ; fl' <- case fl of
-                    Wanted {} -> setEqBind eqv (new_cv `mkTransCo` co2) fl 
-                    Given {}  -> setEqBind new_eqv (cv `mkTransCo` mkSymCo co2) fl
+                    Wanted {} -> setEqBind eqv (new_cv `mkTcTransCo` co2) fl 
+                    Given {}  -> setEqBind new_eqv (cv `mkTcTransCo` mkTcSymCo co2) fl
                     Derived {} -> return fl
                 ; if isNewEvVar evc then 
                       do { continueWith $
@@ -1238,7 +1237,7 @@ canEqLeafTyVarLeftRec :: SubGoalDepth
 canEqLeafTyVarLeftRec d fl eqv tv s2              -- eqv :: tv ~ s2
   = do {  traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2
        ; (xi1,co1) <- flatten d fl (mkTyVarTy tv) -- co1 :: xi1 ~ tv
-       ; case isReflCo co1 of 
+       ; case isTcReflCo co1 of 
              True -- If reflco and variable, just go on
                | Just tv' <- getTyVar_maybe xi1 
                  -> canEqLeafTyVarLeft d fl eqv tv' s2
@@ -1248,9 +1247,9 @@ canEqLeafTyVarLeftRec d fl eqv tv s2              -- eqv :: tv ~ s2
                   ; let new_ev = evc_the_evvar evc
                   ; fl' <- case fl of 
                     Wanted  {} -> setEqBind eqv 
-                                    (mkSymCo co1 `mkTransCo` mkEqVarLCo new_ev) fl
+                                    (mkTcSymCo co1 `mkTcTransCo` mkTcCoVarCo new_ev) fl
                     Given   {} -> setEqBind new_ev
-                                    (co1 `mkTransCo` mkEqVarLCo eqv) fl
+                                    (co1 `mkTcTransCo` mkTcCoVarCo eqv) fl
                     Derived {} -> return fl
                   ; if isNewEvVar evc then
                       do { canEq d fl' new_ev xi1 s2 }
@@ -1266,7 +1265,7 @@ canEqLeafTyVarLeft d fl eqv tv s2       -- eqv : tv ~ s2
   = do { traceTcS "canEqLeafTyVarLeft" (pprEq (mkTyVarTy tv) s2)
        ; (xi2, co) <- flatten d fl s2   -- Flatten RHS   co : xi2 ~ s2
                                                
-       ; let no_flattening_happened = isReflCo co
+       ; let no_flattening_happened = isTcReflCo co
              
        ; traceTcS "canEqLeafTyVarLeft" (nest 2 (vcat [ text "tv  =" <+> ppr tv
                                                      , text "s2  =" <+> ppr s2
@@ -1309,11 +1308,11 @@ canEqLeafTyVarLeft d fl eqv tv s2       -- eqv : tv ~ s2
              do { delCachedEvVar eqv fl
                 ; evc <- newEqVar fl (mkTyVarTy tv) xi2' 
                 ; let eqv' = evc_the_evvar evc -- eqv' : tv ~ xi2'
-                      cv   = mkEqVarLCo eqv    -- cv : tv ~ s2
-                      cv'  = mkEqVarLCo eqv'   -- cv': tv ~ xi2'
+                      cv   = mkTcCoVarCo eqv    -- cv : tv ~ s2
+                      cv'  = mkTcCoVarCo eqv'   -- cv': tv ~ xi2'
                  ; fl' <- case fl of 
-                     Wanted {}  -> setEqBind eqv (cv' `mkTransCo` co) fl         -- tv ~ xi2' ~ s2
-                     Given {}   -> setEqBind eqv' (cv `mkTransCo` mkSymCo co) fl -- tv ~ s2 ~ xi2'
+                     Wanted {}  -> setEqBind eqv (cv' `mkTcTransCo` co) fl         -- tv ~ xi2' ~ s2
+                     Given {}   -> setEqBind eqv' (cv `mkTcTransCo` mkTcSymCo co) fl -- tv ~ s2 ~ xi2'
                      Derived {} -> return fl
 
                  ; if isNewEvVar evc then 
@@ -1499,7 +1498,7 @@ now!).
 rewriteWithFunDeps :: [Equation]
                    -> [Xi] 
                    -> WantedLoc 
-                   -> TcS (Maybe ([Xi], [LCoercion], [(EvVar,WantedLoc)])) 
+                   -> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)])) 
                                            -- Not quite a WantedEvVar unfortunately
                                            -- Because our intention could be to make 
                                            -- it derived at the end of the day
@@ -1552,14 +1551,14 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
 
 rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
                   -> [Type]                    -- A sequence of types: tys
-                  -> [(Type,LCoercion)]      -- Returns: [(ty', co : ty' ~ ty)]
+                  -> [(Type, TcCoercion)]      -- Returns: [(ty', co : ty' ~ ty)]
 rewriteDictParams param_eqs tys
   = zipWith do_one tys [0..]
   where
-    do_one :: Type -> Int -> (Type,LCoercion)
+    do_one :: Type -> Int -> (Type, TcCoercion)
     do_one ty n = case lookup n param_eqs of
-                    Just wev -> (get_fst_ty wev, mkEqVarLCo (fst wev))
-                    Nothing  -> (ty,             mkReflCo ty)  -- Identity
+                    Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev))
+                    Nothing  -> (ty,             mkTcReflCo ty)        -- Identity
 
     get_fst_ty (wev,_wloc) 
       | Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev )
index 68f2714..77f1c42 100644 (file)
@@ -24,6 +24,7 @@ module TcClassDcl ( tcClassSigs, tcClassDecl2,
 import HsSyn
 import TcEnv
 import TcPat( addInlinePrags )
+import TcEvidence( idHsWrapper )
 import TcBinds
 import TcUnify
 import TcHsType
index 4fdb92f..fc5787c 100644 (file)
@@ -32,6 +32,7 @@ import FamInstEnv
 import TcHsType
 import TcMType
 import TcSimplify
+import TcEvidence
 
 import RnBinds
 import RnEnv  
@@ -40,7 +41,6 @@ import HscTypes
 
 import Class
 import Type
-import Coercion
 import ErrUtils
 import MkId
 import DataCon
@@ -1443,7 +1443,7 @@ genInst :: Bool             -- True <=> standalone deriving
         -> OverlapFlag
         -> DerivSpec -> TcM (InstInfo RdrName, BagDerivStuff)
 genInst standalone_deriv oflag
-        spec@(DS { ds_tc = rep_tycon, ds_tc_args = rep_tc_args
+        spec@(DS { ds_tvs = tvs, ds_tc = rep_tycon, ds_tc_args = rep_tc_args
                  , ds_theta = theta, ds_newtype = is_newtype
                  , ds_name = name, ds_cls = clas })
   | is_newtype
@@ -1462,12 +1462,12 @@ genInst standalone_deriv oflag
 
     inst_spec = mkInstance oflag theta spec
     co1 = case tyConFamilyCoercion_maybe rep_tycon of
-              Just co_con -> mkAxInstCo co_con rep_tc_args
+              Just co_con -> mkTcAxInstCo co_con rep_tc_args
               Nothing     -> id_co
               -- Not a family => rep_tycon = main tycon
-    co2 = mkAxInstCo (newTyConCo rep_tycon) rep_tc_args
-    co  = co1 `mkTransCo` co2
-    id_co = mkReflCo (mkTyConApp rep_tycon rep_tc_args)
+    co2 = mkTcAxInstCo (newTyConCo rep_tycon) rep_tc_args
+    co  = mkTcForAllCos tvs (co1 `mkTcTransCo` co2)
+    id_co = mkTcReflCo (mkTyConApp rep_tycon rep_tc_args)
 
 -- Example: newtype instance N [a] = N1 (Tree a)
 --          deriving instance Eq b => Eq (N [(b,b)])
index 4fe7ee1..5c2c895 100644 (file)
@@ -60,7 +60,7 @@ import TcIface
 import PrelNames
 import TysWiredIn
 import Id
-import Coercion
+import TcEvidence
 import Var
 import VarSet
 import RdrName
@@ -629,10 +629,10 @@ data InstBindings a
                         -- witness dictionary is identical to the argument 
                         -- dictionary.  Hence no bindings, no pragmas.
 
-        Coercion        -- The coercion maps from newtype to the representation type
-                        -- (mentioning type variables bound by the forall'd iSpec variables)
+        TcCoercion      -- The coercion maps from newtype to the representation type
+                        -- (quantified over type variables bound by the forall'd iSpec variables)
                         -- E.g.   newtype instance N [a] = N1 (Tree a)
-                        --        co : N [a] ~ Tree a
+                        --        co : forall a. N [a] ~ Tree a
 
         TyCon           -- The TyCon is the newtype N.  If it's indexed, then it's the 
                         -- representation TyCon, so that tyConDataCons returns [N1], 
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
new file mode 100644 (file)
index 0000000..0511aa1
--- /dev/null
@@ -0,0 +1,570 @@
+%\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,\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
+    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
+  | 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
+\r
+  deriving( Data.Data, Data.Typeable)\r
+\end{code}\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
+\begin{code}\r
+mkEvCast :: EvVar -> TcCoercion -> EvTerm\r
+mkEvCast ev lco\r
+  | isTcReflCo lco = EvId ev\r
+  | otherwise      = EvCast 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
+\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 (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
+\end{code}\r
+\r
index 5217756..340b33c 100644 (file)
@@ -46,7 +46,7 @@ import Name
 import TyCon
 import Type
 import Kind( splitKiTyVars )
-import Coercion
+import TcEvidence
 import Var
 import VarSet
 import VarEnv
@@ -680,7 +680,7 @@ tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
 
        -- Step 7: make a cast for the scrutinee, in the case that it's from a type family
        ; let scrut_co | Just co_con <- tyConFamilyCoercion_maybe tycon 
-                      = WpCast (mkAxInstCo co_con scrut_inst_tys)
+                      = WpCast (mkTcAxInstCo co_con scrut_inst_tys)
                       | otherwise
                       = idHsWrapper
        -- Phew!
@@ -922,7 +922,7 @@ tcTupArgs args tys
 
 ----------------
 unifyOpFunTysWrap :: LHsExpr Name -> Arity -> TcRhoType
-                  -> TcM (LCoercion, [TcSigmaType], TcRhoType)                 
+                  -> TcM (TcCoercion, [TcSigmaType], TcRhoType)                        
 -- A wrapper for matchExpectedFunTys
 unifyOpFunTysWrap op arity ty = matchExpectedFunTys herald arity ty
   where
@@ -1149,18 +1149,18 @@ tcTagToEnum loc fun_name arg res_ty
     doc3 = ptext (sLit "No family instance for this type")
 
     get_rep_ty :: TcType -> TyCon -> [TcType]
-               -> TcM (LCoercion, TyCon, [TcType])
+               -> TcM (TcCoercion, TyCon, [TcType])
        -- Converts a family type (eg F [a]) to its rep type (eg FList a)
        -- and returns a coercion between the two
     get_rep_ty ty tc tc_args
       | not (isFamilyTyCon tc) 
-      = return (mkReflCo ty, tc, tc_args)
+      = return (mkTcReflCo ty, tc, tc_args)
       | otherwise 
       = do { mb_fam <- tcLookupFamInst tc tc_args
            ; case mb_fam of 
               Nothing -> failWithTc (tagToEnumError ty doc3)
                Just (rep_tc, rep_args) 
-                   -> return ( mkSymCo (mkAxInstCo co_tc rep_args)
+                   -> return ( mkTcSymCo (mkTcAxInstCo co_tc rep_args)
                              , rep_tc, rep_args )
                  where
                    co_tc = expectJust "tcTagToEnum" $
index 6bc5a4f..bd9f1a9 100644 (file)
@@ -30,6 +30,7 @@ import RnEnv
 
 import FamInst
 import FamInstEnv
+import Coercion      
 import Type
 import TypeRep
 import ForeignCall
@@ -40,7 +41,6 @@ import RdrName
 import DataCon
 import TyCon
 import TcType
-import Coercion
 import PrelNames
 import DynFlags
 import Outputable
index 72f64dd..c1f425b 100644 (file)
@@ -42,7 +42,7 @@ import TcRnMonad
 import PrelNames
 import TcType
 import TcMType
-import Coercion
+import TcEvidence
 import TysPrim
 import TysWiredIn
 import Type
@@ -1081,8 +1081,8 @@ zonkVect _ (HsVectInstIn _) = panic "TcHsSyn.zonkVect: HsVectInstIn"
 zonkEvTerm :: ZonkEnv -> EvTerm -> TcM EvTerm
 zonkEvTerm env (EvId v)           = ASSERT2( isId v, ppr v ) 
                                     return (EvId (zonkIdOcc env v))
-zonkEvTerm env (EvCoercionBox co) = do { co' <- zonkTcLCoToLCo env co
-                                       ; return (EvCoercionBox co') }
+zonkEvTerm env (EvCoercion co)    = do { co' <- zonkTcLCoToLCo env co
+                                       ; return (EvCoercion co') }
 zonkEvTerm env (EvCast v co)      = ASSERT( isId v) 
                                     do { co' <- zonkTcLCoToLCo env co
                                        ; return (mkEvCast (zonkIdOcc env v) co') }
@@ -1122,18 +1122,18 @@ zonkEvBind env (EvBind var term)
   -- same types many types. See Note [Optimized Evidence Binding Zonking]
   = case term of 
       -- Fast path for reflexivity coercions:
-      EvCoercionBox co 
-        | Just ty <- isReflCo_maybe co
+      EvCoercion co 
+        | Just ty <- isTcReflCo_maybe co
         ->
           do { zty  <- zonkTcTypeToType env ty
              ; let var' = setVarType var (mkEqPred (zty,zty))
-             ; return (EvBind var' (EvCoercionBox (mkReflCo zty))) }
+             ; return (EvBind var' (EvCoercion (mkTcReflCo zty))) }
 
       -- Fast path for variable-variable bindings 
       -- NB: could be optimized further! (e.g. SymCo cv)
-        | Just cv <- getCoVar_maybe co 
+        | Just cv <- getTcCoVar_maybe co 
         -> do { let cv' = zonkIdOcc env cv -- Just lazily look up
-                    term' = EvCoercionBox (CoVarCo cv')
+                    term' = EvCoercion (TcCoVarCo cv')
                     var'  = setVarType var (varType cv')
               ; return (EvBind var' term') }
       -- Ugly safe and slow path
@@ -1282,7 +1282,7 @@ zonkTypeZapping tv
        ; return ty }
 
 
-zonkTcLCoToLCo :: ZonkEnv -> LCoercion -> TcM LCoercion
+zonkTcLCoToLCo :: ZonkEnv -> TcCoercion -> TcM TcCoercion
 -- NB: zonking often reveals that the coercion is an identity
 --     in which case the Refl-ness can propagate up to the top
 --     which in turn gives more efficient desugaring.  So it's
@@ -1290,22 +1290,21 @@ zonkTcLCoToLCo :: ZonkEnv -> LCoercion -> TcM LCoercion
 zonkTcLCoToLCo env co
   = go co
   where
-    go (CoVarCo cv)         = return (mkEqVarLCo (zonkEvVarOcc env cv))
-    go (Refl ty)            = do { ty' <- zonkTcTypeToType env ty
-                                 ; return (Refl ty') }
-    go (TyConAppCo tc cos)  = do { cos' <- mapM go cos; return (mkTyConAppCo tc cos') }
-    go (AxiomInstCo ax cos) = do { cos' <- mapM go cos; return (AxiomInstCo ax cos') }
-    go (AppCo co1 co2)      = do { co1' <- go co1; co2' <- go co2
-                                 ; return (mkAppCo co1' co2') }
-    go (UnsafeCo t1 t2)     = do { t1' <- zonkTcTypeToType env t1
-                                 ; t2' <- zonkTcTypeToType env t2
-                                 ; return (mkUnsafeCo t1' t2') }
-    go (SymCo co)           = do { co' <- go co; return (mkSymCo co')  }
-    go (NthCo n co)         = do { co' <- go co; return (mkNthCo n co')  }
-    go (TransCo co1 co2)    = do { co1' <- go co1; co2' <- go co2
-                                 ; return (mkTransCo co1' co2')  }
-    go (InstCo co ty)       = do { co' <- go co; ty' <- zonkTcTypeToType env ty
-                                 ; return (mkInstCo co' ty')  }
-    go (ForAllCo tv co)     = ASSERT( isImmutableTyVar tv )
-                              do { co' <- go co; return (mkForAllCo tv co') }
+    go (TcLetCo bs co)        = do { (env', bs') <- zonkTcEvBinds env bs
+                                   ; co' <- zonkTcLCoToLCo env' co
+                                   ; return (TcLetCo bs' co') }
+    go (TcCoVarCo cv)         = return (mkTcCoVarCo (zonkEvVarOcc env cv))
+    go (TcRefl ty)            = do { ty' <- zonkTcTypeToType env ty
+                                   ; return (TcRefl ty') }
+    go (TcTyConAppCo tc cos)  = do { cos' <- mapM go cos; return (mkTcTyConAppCo tc cos') }
+    go (TcAxiomInstCo ax tys) = do { tys' <- zonkTcTypeToTypes env tys; return (TcAxiomInstCo ax tys') }
+    go (TcAppCo co1 co2)      = do { co1' <- go co1; co2' <- go co2
+                                   ; return (mkTcAppCo co1' co2') }
+    go (TcSymCo co)           = do { co' <- go co; return (mkTcSymCo co')  }
+    go (TcNthCo n co)         = do { co' <- go co; return (mkTcNthCo n co')  }
+    go (TcTransCo co1 co2)    = do { co1' <- go co1; co2' <- go co2
+                                   ; return (mkTcTransCo co1' co2')  }
+    go (TcForAllCo tv co)     = ASSERT( isImmutableTyVar tv )
+                                do { co' <- go co; return (mkTcForAllCo tv co') }
+    go (TcInstCo co ty)       = do { co' <- go co; ty' <- zonkTcTypeToType env ty; return (TcInstCo co' ty') }
 \end{code}
index b86321e..33ba9cf 100644 (file)
@@ -48,6 +48,7 @@ import RnHsSyn
 import TcRnMonad
 import RnEnv   ( polyKindsErr )
 import TcHsSyn ( mkZonkTcTyVar )
+import TcEvidence( HsWrapper )
 import TcEnv
 import TcMType
 import TcUnify
index afcab3b..7ec86fc 100644 (file)
@@ -36,7 +36,7 @@ import TcHsType
 import TcUnify
 import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
 import Type
-import Coercion hiding (substTy)
+import TcEvidence
 import TyCon
 import DataCon
 import Class
@@ -1090,16 +1090,12 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
        ; mapAndUnzipM (tc_item rep_d_stuff) op_items }
   where
      loc = getSrcSpan dfun_id
-
-     inst_tvs = fst (tcSplitForAllTys (idType dfun_id))
      Just (init_inst_tys, _) = snocView inst_tys
-     rep_ty   = pFst (coercionKind co)  -- [p]
+     rep_ty   = pFst (tcCoercionKind co)  -- [p]
      rep_pred = mkClassPred clas (init_inst_tys ++ [rep_ty])
 
      -- co : [p] ~ T p
-     co = substCoWithTys (mkInScopeSet (mkVarSet tyvars))
-                         inst_tvs (mkTyVarTys tyvars) $
-          mkSymCo coi
+     co = mkTcSymCo (mkTcInstCos coi (mkTyVarTys tyvars))
 
      ----------------
      tc_item :: (TcEvBinds, EvVar) -> (Id, DefMeth) -> TcM (TcId, LHsBind TcId)
@@ -1121,8 +1117,8 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
      ----------------
      mk_op_wrapper :: Id -> EvVar -> HsWrapper
      mk_op_wrapper sel_id rep_d
-       = WpCast (liftCoSubstWith sel_tvs (map mkReflCo init_inst_tys ++ [co])
-                                 local_meth_ty)
+       = WpCast (liftTcCoSubstWith sel_tvs (map mkTcReflCo init_inst_tys ++ [co])
+                                   local_meth_ty)
          <.> WpEvApp (EvId rep_d)
          <.> mkWpTyApps (init_inst_tys ++ [rep_ty])
        where
index db90559..93f499a 100644 (file)
@@ -26,7 +26,6 @@ import Var
 import VarEnv ( ) -- unitVarEnv, mkInScopeSet
 
 import TcType
-import HsBinds
 
 import Class
 import TyCon
@@ -35,7 +34,7 @@ import IParam
 
 import FunDeps
 
-import Coercion
+import TcEvidence
 import Outputable
 
 import TcRnTypes
@@ -332,10 +331,10 @@ kickOutRewritableInerts ct
        ; traceTcS "Kick out" (ppr ct $$ ppr wl)
        ; updWorkListTcS (unionWorkList wl) }
 
-rewriteInertEqsFromInertEq :: (TcTyVar,Coercion, CtFlavor) -- A new substitution
-                           -> TyVarEnv (Ct,Coercion)       -- All inert equalities
-                           -> TcS (TyVarEnv (Ct,Coercion)) -- The new inert equalities
-rewriteInertEqsFromInertEq (subst_tv,subst_co, subst_fl) ieqs
+rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtFlavor) -- A new substitution
+                           -> TyVarEnv (Ct, TcCoercion)       -- All inert equalities
+                           -> TcS (TyVarEnv (Ct,TcCoercion)) -- The new inert equalities
+rewriteInertEqsFromInertEq (subst_tv, subst_co, subst_fl) ieqs
 -- The goal: traverse the inert equalities and rewrite some of them, dropping some others
 -- back to the worklist. This is delicate, see Note [Delicate equality kick-out]
  = do { mieqs <- Traversable.mapM do_one ieqs 
@@ -362,23 +361,29 @@ rewriteInertEqsFromInertEq (subst_tv,subst_co, subst_fl) ieqs
          | otherwise -- Just keep it there
          = return $ Just (ct,inert_co)
          where 
+          -- We have new guy         co : tv ~ something
+          -- and old inert  {wanted} cv : tv' ~ rhs[tv]
+          -- We want to rewrite to
+          --                {wanted} cv' : tv' ~ rhs[something] 
+           --                cv = cv' ; rhs[Sym co]
+          --                  
            rewrite_on_the_spot (ct,_inert_co)
-             = do { let rhs' = pSnd (liftedCoercionKind co)
+             = do { let rhs' = pSnd (tcCoercionKind co)
                   ; delCachedEvVar ev fl
                   ; evc <- newEqVar fl (mkTyVarTy tv) rhs'
-                  ; let ev' = evc_the_evvar evc
-                  ; let evco' = mkEqVarLCo ev' 
+                  ; let ev'   = evc_the_evvar evc
+                  ; let evco' = mkTcCoVarCo ev' 
                   ; fl' <- if isNewEvVar evc then
                                do { case fl of 
                                       Wanted {} 
-                                        -> setEqBind ev (evco' `mkTransCo` mkSymCo co) fl
+                                        -> setEqBind ev (evco' `mkTcTransCo` mkTcSymCo co) fl
                                       Given {} 
-                                        -> setEqBind ev' (mkEqVarLCo ev `mkTransCo` co) fl
+                                        -> setEqBind ev' (mkTcCoVarCo ev `mkTcTransCo` co) fl
                                       Derived {}
                                         -> return fl }
                            else
                                if isWanted fl then 
-                                   setEqBind ev (evco' `mkTransCo` mkSymCo co) fl
+                                   setEqBind ev (evco' `mkTcTransCo` mkTcSymCo co) fl
                                else return fl
                   ; let ct' = ct { cc_id = ev', cc_flavor = fl', cc_rhs = rhs' }
                   ; return (ct',evco') }
@@ -386,9 +391,9 @@ rewriteInertEqsFromInertEq (subst_tv,subst_co, subst_fl) ieqs
            fl  = cc_flavor ct
            tv  = cc_tyvar ct
            rhs = cc_rhs ct
-           co  = liftCoSubstWith [subst_tv] [subst_co] rhs
+           co  = liftTcCoSubstWith [subst_tv] [subst_co] rhs
 
-kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,Coercion)), InertSet)
+kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,TcCoercion)), InertSet)
 -- Returns ALL equalities, to be dealt with later
 kick_out_rewritable ct (IS { inert_eqs    = eqmap
                            , inert_eq_tvs = inscope
@@ -617,9 +622,9 @@ solveWithIdentity d eqv wd tv xi
                             ]
 
        ; setWantedTyBind tv xi
-       ; let refl_xi = mkReflCo xi
+       ; let refl_xi = mkTcReflCo xi
 
-       ; let solved_fl = mkSolvedFlavor wd UnkSkol (EvCoercionBox refl_xi) 
+       ; let solved_fl = mkSolvedFlavor wd UnkSkol (EvCoercion refl_xi) 
        ; (_,eqv_given) <- newGivenEqVar solved_fl (mkTyVarTy tv) xi refl_xi
 
        ; when (isWanted wd) $ do { _ <- setEqBind eqv refl_xi wd; return () }
@@ -805,7 +810,7 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i
            Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
            Wanted  {} ->
                do { _ <- setEvBind (cc_id workItem) 
-                            (mkEvCast id1 (mkSymCo (mkTyConAppCo (ipTyCon nm1) [mkEqVarLCo (evc_the_evvar eqv)]))) wfl
+                            (mkEvCast id1 (mkTcSymCo (mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo (evc_the_evvar eqv)]))) wfl
                   ; irWorkItemConsumed "IP/IP (solved by rewriting)" } }
 
 doInteractWithInert (CFunEqCan { cc_id = eqv1, cc_flavor = fl1, cc_fun = tc1
@@ -850,10 +855,10 @@ rewriteEqLHS LeftComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2)
        ; gw' <- case gw of 
            Wanted {} 
                -> setEqBind eqv2 
-                    (mkEqVarLCo eqv1 `mkTransCo` mkSymCo (mkEqVarLCo eqv2')) gw
+                    (mkTcCoVarCo eqv1 `mkTcTransCo` mkTcSymCo (mkTcCoVarCo eqv2')) gw
            Given {}
                -> setEqBind eqv2'
-                    (mkSymCo (mkEqVarLCo eqv2) `mkTransCo` mkEqVarLCo eqv1) gw
+                    (mkTcSymCo (mkTcCoVarCo eqv2) `mkTcTransCo` mkTcCoVarCo eqv1) gw
            Derived {} 
                -> return gw
        ; when (isNewEvVar evc) $ 
@@ -868,10 +873,10 @@ rewriteEqLHS RightComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2)
        ; gw' <- case gw of
            Wanted {} 
                -> setEqBind eqv2
-                    (mkEqVarLCo eqv1 `mkTransCo` mkEqVarLCo eqv2') gw
+                    (mkTcCoVarCo eqv1 `mkTcTransCo` mkTcCoVarCo eqv2') gw
            Given {}  
                -> setEqBind eqv2'
-                    (mkSymCo (mkEqVarLCo eqv1) `mkTransCo` mkEqVarLCo eqv2) gw
+                    (mkTcSymCo (mkTcCoVarCo eqv1) `mkTcTransCo` mkTcCoVarCo eqv2) gw
            Derived {} 
                -> return gw
 
@@ -1397,11 +1402,11 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl
                            -- RHS of a type function, so that it never
                            -- appears in an error message
                             -- See Note [Type synonym families] in TyCon
-                         coe = mkAxInstCo coe_tc rep_tys 
+                         coe = mkTcAxInstCo coe_tc rep_tys 
                    ; case fl of
                        Wanted {} -> do { evc <- newEqVar fl rhs_ty xi -- Wanted version
                                        ; let eqv' = evc_the_evvar evc
-                                       ; let coercion = coe `mkTransCo` mkEqVarLCo eqv'
+                                       ; let coercion = coe `mkTcTransCo` mkTcCoVarCo eqv'
                                        ; _ <- setEqBind eqv coercion fl
                                        ; when (isNewEvVar evc) $ 
                                             (let ct = CNonCanonical { cc_id = eqv'
@@ -1410,7 +1415,7 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl
                                              in updWorkListTcS (extendWorkListEq ct))
 
                                        ; let _solved   = workItem { cc_flavor = solved_fl }
-                                             solved_fl = mkSolvedFlavor fl UnkSkol (EvCoercionBox coercion)
+                                             solved_fl = mkSolvedFlavor fl UnkSkol (EvCoercion coercion)
 
                                        ; updateFlatCache eqv solved_fl tc args xi WhenSolved
 
@@ -1421,7 +1426,7 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl
                                                      -- Cache in inerts the Solved item
 
                        Given {} -> do { (fl',eqv') <- newGivenEqVar fl xi rhs_ty $ 
-                                                         mkSymCo (mkEqVarLCo eqv) `mkTransCo` coe
+                                                         mkTcSymCo (mkTcCoVarCo eqv) `mkTcTransCo` coe
                                       ; let ct = CNonCanonical { cc_id = eqv'
                                                                , cc_flavor = fl'
                                                                , cc_depth = cc_depth workItem + 1}  
index 4aa19ae..d09e384 100644 (file)
@@ -36,7 +36,7 @@ import TysWiredIn
 import Id
 import TyCon
 import TysPrim
-import Coercion         ( isReflCo, mkSymCo )
+import TcEvidence
 import Outputable
 import Util
 import SrcLoc
@@ -153,7 +153,7 @@ matchFunTys
 matchFunTys herald arity res_ty thing_inside
   = do { (co, pat_tys, res_ty) <- matchExpectedFunTys herald arity res_ty
        ; res <- thing_inside pat_tys res_ty
-        ; return (coToHsWrapper (mkSymCo co), res) }
+        ; return (coToHsWrapper (mkTcSymCo co), res) }
 \end{code}
 
 %************************************************************************
@@ -734,7 +734,7 @@ tcMcStmt ctxt (ParStmt bndr_stmts_s mzip_op bind_op return_op) res_ty thing_insi
        -- so for now we just check that it's the identity
     check_same actual expected
       = do { co <- unifyType actual expected
-          ; unless (isReflCo co) $
+          ; unless (isTcReflCo co) $
              failWithMisMatch [UnifyOrigin { uo_expected = expected
                                            , uo_actual = actual }] }
 
index fccde2b..f898f3d 100644 (file)
@@ -7,7 +7,8 @@
 -- for details
 
 module TcMatches where
-import HsSyn   ( GRHSs, MatchGroup, HsWrapper )
+import HsSyn   ( GRHSs, MatchGroup )
+import TcEvidence( HsWrapper )
 import Name    ( Name )
 import TcType  ( TcRhoType )
 import TcRnTypes( TcM, TcId )
index c9a67aa..137df8a 100644 (file)
@@ -35,7 +35,7 @@ import TcType
 import TcUnify
 import TcHsType
 import TysWiredIn
-import Coercion
+import TcEvidence
 import StaticFlags
 import TyCon
 import DataCon
@@ -199,7 +199,7 @@ res_ty free vars.
 %************************************************************************
 
 \begin{code}
-tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (LCoercion, TcId)
+tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (TcCoercion, TcId)
 -- (coi, xp) = tcPatBndr penv x pat_ty
 -- Then coi : pat_ty ~ typeof(xp)
 --
@@ -211,11 +211,11 @@ tcPatBndr (PE { pe_ctxt = LetPat lookup_sig no_gen}) bndr_name pat_ty
       
   | otherwise
   = do { bndr_id <- newNoSigLetBndr no_gen bndr_name pat_ty
-       ; return (mkReflCo pat_ty, bndr_id) }
+       ; return (mkTcReflCo pat_ty, bndr_id) }
 
 tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
   = do { bndr <- mkLocalBinder bndr_name pat_ty
-       ; return (mkReflCo pat_ty, bndr) }
+       ; return (mkTcReflCo pat_ty, bndr) }
 
 ------------
 newSigLetBndr :: LetBndrSpec -> Name -> TcSigInfo -> TcM TcId
@@ -554,14 +554,14 @@ tc_pat penv (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
 tc_pat _ _other_pat _ _ = panic "tc_pat"       -- ConPatOut, SigPatOut
 
 ----------------
-unifyPatType :: TcType -> TcType -> TcM LCoercion
+unifyPatType :: TcType -> TcType -> TcM TcCoercion
 -- In patterns we want a coercion from the
 -- context type (expected) to the actual pattern type
 -- But we don't want to reverse the args to unifyType because
 -- that controls the actual/expected stuff in error messages
 unifyPatType actual_ty expected_ty
   = do { coi <- unifyType actual_ty expected_ty
-       ; return (mkSymCo coi) }
+       ; return (mkTcSymCo coi) }
 \end{code}
 
 Note [Hopping the LIE in lazy patterns]
@@ -726,14 +726,14 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
        } }
 
 ----------------------------
-matchExpectedPatTy :: (TcRhoType -> TcM (LCoercion, a))
+matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercion, a))
                     -> TcRhoType -> TcM (HsWrapper, a) 
 -- See Note [Matching polytyped patterns]
 -- Returns a wrapper : pat_ty ~ inner_ty
 matchExpectedPatTy inner_match pat_ty
   | null tvs && null theta
   = do { (co, res) <- inner_match pat_ty
-       ; return (coToHsWrapper (mkSymCo co), res) }
+       ; return (coToHsWrapper (mkTcSymCo co), res) }
                 -- The Sym is because the inner_match returns a coercion
         -- that is the other way round to matchExpectedPatTy
 
@@ -749,7 +749,7 @@ matchExpectedPatTy inner_match pat_ty
 matchExpectedConTy :: TyCon     -- The TyCon that this data 
                                 -- constructor actually returns
                   -> TcRhoType  -- The type of the pattern
-                  -> TcM (LCoercion, [TcSigmaType])
+                  -> TcM (TcCoercion, [TcSigmaType])
 -- See Note [Matching constructor patterns]
 -- Returns a coercion : T ty1 ... tyn ~ pat_ty
 -- This is the same way round as matchExpectedListTy etc
@@ -764,10 +764,10 @@ matchExpectedConTy data_tc pat_ty
        ; co1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
                     -- co1 : T (ty1,ty2) ~ pat_ty
 
-       ; let co2 = mkAxInstCo co_tc tys
+       ; let co2 = mkTcAxInstCo co_tc tys
                     -- co2 : T (ty1,ty2) ~ T7 ty1 ty2
 
-       ; return (mkSymCo co2 `mkTransCo` co1, tys) }
+       ; return (mkTcSymCo co2 `mkTcTransCo` co1, tys) }
 
   | otherwise
   = matchExpectedTyConApp data_tc pat_ty
index fbdfa1b..4879974 100644 (file)
@@ -39,7 +39,8 @@ import RdrName
 import TcHsSyn
 import TcExpr
 import TcRnMonad
-import Coercion
+import TcEvidence
+import Coercion( pprCoAxiom )
 import FamInst
 import InstEnv
 import FamInstEnv
index c0a8817..381d535 100644 (file)
@@ -15,8 +15,8 @@ module TcRnMonad(
 
 import TcRnTypes        -- Re-export all
 import IOEnv            -- Re-export all
+import TcEvidence
 
-import Coercion
 import HsSyn hiding (LIE)
 import HscTypes
 import Module
@@ -382,11 +382,6 @@ newSysLocalIds fs tys
   = do  { us <- newUniqueSupply
         ; return (zipWith (mkSysLocal fs) (uniqsFromSupply us) tys) }
 
-newCoVar :: TcType -> TcType -> TcRnIf gbl lcl EvVar
-newCoVar ty1 ty2
-  = do { uniq <- newUnique
-       ; return (mkLocalId (mkInternalName uniq (mkVarOccFS (fsLit "co")) noSrcSpan) (mkCoercionType ty1 ty2)) }
-
 newName :: OccName -> TcM Name
 newName occ
   = do { uniq <- newUnique
index 2b53e17..ab26fa1 100644 (file)
@@ -88,6 +88,7 @@ module TcRnTypes(
 
 import HsSyn
 import HscTypes
+import TcEvidence( EvBind, EvBindsVar, EvTerm )
 import Type
 import Class    ( Class )
 import TyCon    ( TyCon )
@@ -1348,6 +1349,9 @@ data SkolemInfo
 
   | BracketSkol         -- Template Haskell bracket
 
+  | UnifyForAllSkol     -- We are unifying two for-all types
+       TcType
+
   | UnkSkol             -- Unhelpful info (until I improve it)
 
 instance Outputable SkolemInfo where
@@ -1376,6 +1380,7 @@ pprSkolInfo (PatSkol dc mc)  = sep [ ptext (sLit "a pattern with constructor")
 pprSkolInfo (InferSkol ids) = sep [ ptext (sLit "the inferred type of")
                                   , vcat [ ppr name <+> dcolon <+> ppr ty
                                          | (name,ty) <- ids ]]
+pprSkolInfo (UnifyForAllSkol ty) = ptext (sLit "the type") <+> ppr ty
 
 -- UnkSkol
 -- For type variables the others are dealt with by pprSkolTvBinding.  
index 2503197..4cdc28b 100644 (file)
@@ -1,5 +1,5 @@
 \begin{code}
-{-# OPTIONS -Wwarn -fno-warn-tabs #-}
+{-# OPTIONS -fno-warn-tabs #-}
 -- The above warning supression flag is a temporary kludge.
 -- While working on this module you are encouraged to remove it and
 -- detab the module (please do the detabbing in a separate patch). See
@@ -110,7 +110,7 @@ import TcType
 import DynFlags
 import Type
 
-import Coercion
+import TcEvidence
 import Class
 import TyCon
 import TypeRep 
@@ -123,11 +123,8 @@ import Bag
 import MonadUtils
 import VarSet
 
--- import Pair ( pSnd )
 import FastString
 import Util
-
-import HsBinds               -- for TcEvBinds stuff 
 import Id 
 import TcRnTypes
 
@@ -230,7 +227,7 @@ extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
 extendWorkListCt :: Ct -> WorkList -> WorkList
 -- Agnostic
 extendWorkListCt ct wl
- | isLCoVar (cc_id ct) = extendWorkListEq ct wl
+ | isEqVar (cc_id ct) = extendWorkListEq ct wl
  | otherwise = extendWorkListNonEq ct wl
 
 appendWorkListCt :: [Ct] -> WorkList -> WorkList
@@ -256,8 +253,8 @@ workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
 
 workListFromCt :: Ct -> WorkList
 -- Agnostic 
-workListFromCt ct | isLCoVar (cc_id ct) = workListFromEq ct 
-                  | otherwise           = workListFromNonEq ct
+workListFromCt ct | isEqVar (cc_id ct) = workListFromEq ct 
+                  | otherwise          = workListFromNonEq ct
 
 
 selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
@@ -394,7 +391,7 @@ partitionCCanMap pred cmap
                                           new_acc_cts = acc_cts `andCts` cts_out
                                           (cts_out, cts_keep) = partitionBag pred this_cts
 
-partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,Coercion) -> ([Ct], TyVarEnv (Ct,Coercion))
+partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion))
 partitionEqMap pred isubst 
   = let eqs_out = foldVarEnv extend_if_pred [] isubst
         eqs_in  = filterVarEnv_Directly (\_ (ct,_) -> not (pred ct)) isubst
@@ -413,7 +410,7 @@ extractUnsolvedCMap cmap =
 
 -- See Note [InertSet invariants]
 data InertSet 
-  = IS { inert_eqs     :: TyVarEnv (Ct,Coercion) 
+  = IS { inert_eqs     :: TyVarEnv (Ct,TcCoercion) 
          -- Must all be CTyEqCans! If an entry exists of the form: 
          --   a |-> ct,co
          -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } 
@@ -740,7 +737,7 @@ data EvVarCache
   = EvVarCache { evc_cache     :: TypeMap (EvVar,CtFlavor)    
                      -- Map from PredTys to Evidence variables
                      -- used to avoid creating new goals
-               , evc_flat_cache :: TypeMap (Coercion,(Xi,CtFlavor,FlatEqOrigin))
+               , evc_flat_cache :: TypeMap (TcCoercion,(Xi,CtFlavor,FlatEqOrigin))
                      -- Map from family-free heads (F xi) to family-free types.
                      -- Useful during flattening to share flatten skolem generation
                      -- The boolean flag:
@@ -1037,7 +1034,7 @@ getTcSEvVarCacheMap = do { cache_var <- getTcSEvVarCache
                          ; the_cache <- wrapTcS $ TcM.readTcRef cache_var 
                          ; return (evc_cache the_cache) }
 
-getTcSEvVarFlatCache :: TcS (TypeMap (Coercion,(Type,CtFlavor,FlatEqOrigin)))
+getTcSEvVarFlatCache :: TcS (TypeMap (TcCoercion,(Type,CtFlavor,FlatEqOrigin)))
 getTcSEvVarFlatCache = do { cache_var <- getTcSEvVarCache 
                           ; the_cache <- wrapTcS $ TcM.readTcRef cache_var 
                           ; return (evc_flat_cache the_cache) }
@@ -1064,8 +1061,8 @@ getTcEvBindsMap
        ; wrapTcS $ TcM.readTcRef ev_ref }
 
 
-setEqBind :: EqVar -> LCoercion -> CtFlavor -> TcS CtFlavor
-setEqBind eqv co fl = setEvBind eqv (EvCoercionBox co) fl
+setEqBind :: EqVar -> TcCoercion -> CtFlavor -> TcS CtFlavor
+setEqBind eqv co fl = setEvBind eqv (EvCoercion co) fl
 
 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
 -- Add a type binding
@@ -1091,7 +1088,7 @@ setEvBind ev t fl
 
 #ifdef DEBUG
        ; binds <- getTcEvBindsMap
-       ; let cycle = any (reaches binds) (evterm_evs t)
+       ; let cycle = any (reaches binds) (evVarsOfTerm t)
        ; when cycle (fail_if_co_loop binds)
 #endif
        ; return $ 
@@ -1105,7 +1102,7 @@ setEvBind ev t fl
   where fail_if_co_loop binds
           = pprTrace "setEvBind" (vcat [ text "Cycle in evidence binds, evvar =" <+> ppr ev
                                        , ppr (evBindMapBinds binds) ]) $
-            when (isLCoVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!"))
+            when (isEqVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!"))
 
         reaches :: EvBindMap -> Var -> Bool 
         -- Does this evvar reach ev? 
@@ -1113,16 +1110,8 @@ setEvBind ev t fl
           where go ev0
                   | ev0 == ev = True
                   | Just (EvBind _ evtrm) <- lookupEvBind ebm ev0
-                  = any go (evterm_evs evtrm)
+                  = any go (evVarsOfTerm evtrm)
                   | otherwise = False
-
-        evterm_evs (EvId v) = [v]
-        evterm_evs (EvCoercionBox lco) = varSetElems $ coVarsOfCo lco
-        evterm_evs (EvDFunApp _ _ evs) = evs
-        evterm_evs (EvTupleSel v _)    = [v]
-        evterm_evs (EvSuperClass v _)  = [v]
-        evterm_evs (EvCast v co)       = v : varSetElems (coVarsOfCo co)
-        evterm_evs (EvTupleMk evs)     = evs
 #endif
 
 \end{code}
@@ -1357,7 +1346,8 @@ newEvVar fl pty
                                            --            but they don't come with guarantees
                                            --            that they can be solved and we don't 
                                            --            quantify over them.
-             -> do { traceTcS "newEvVar"  $  text "already cached, doing nothing"
+             -> do { traceTcS "newEvVar: already cached, doing nothing" 
+                              (ppr (evc_cache ecache))
                    ; return (EvVarCreated False cached_evvar) }
            _   -- Not cached or cached with worse flavor
              -> do { new <- force_new_ev_var eref ecache fl pty
@@ -1425,21 +1415,21 @@ updateFlatCache ev fl fn xis rhs_ty feq_origin
              new_flat_cache = alterTM fun_ty x_flat_cache flat_cache
              new_evc = ecache { evc_flat_cache = new_flat_cache }
        ; wrapTcS $ TcM.writeTcRef eref new_evc }
-  where x_flat_cache _ = Just (mkEqVarLCo ev,(rhs_ty,fl,feq_origin))
+  where x_flat_cache _ = Just (mkTcCoVarCo ev,(rhs_ty,fl,feq_origin))
         fun_ty = mkTyConApp fn xis
 
 
-pprEvVarCache :: TypeMap (Coercion,a) -> SDoc
+pprEvVarCache :: TypeMap (TcCoercion,a) -> SDoc
 pprEvVarCache tm = ppr (foldTM mk_pair tm [])
- where mk_pair (co,_) cos = (co, liftedCoercionKind co) : cos
+ where mk_pair (co,_) cos = (co, tcCoercionKind co) : cos
 
 
-newGivenEqVar :: CtFlavor -> TcType -> TcType -> Coercion -> TcS (CtFlavor,EvVar)
+newGivenEqVar :: CtFlavor -> TcType -> TcType -> TcCoercion -> TcS (CtFlavor,EvVar)
 -- Pre: fl is Given
 newGivenEqVar fl ty1 ty2 co 
   = do { ecv <- newEqVar fl ty1 ty2
        ; let v = evc_the_evvar ecv -- Will be a new EvVar by post of newEvVar
-       ; fl' <- setEvBind v (EvCoercionBox co) fl
+       ; fl' <- setEvBind v (EvCoercion co) fl
        ; return (fl',v) }
 
 newEqVar :: CtFlavor -> TcType -> TcType -> TcS EvVarCreated
@@ -1500,47 +1490,47 @@ matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 \begin{code}
 
-getInertEqs :: TcS (TyVarEnv (Ct,Coercion), InScopeSet)
+getInertEqs :: TcS (TyVarEnv (Ct,TcCoercion), InScopeSet)
 getInertEqs = do { inert <- getTcSInerts
                  ; return (inert_eqs inert, inert_eq_tvs inert) }
 
-getCtCoercion :: Ct -> Coercion
+getCtCoercion :: Ct -> TcCoercion
 -- Precondition: A CTyEqCan.
 getCtCoercion ct 
-  | Just (GivenSolved (Just (EvCoercionBox co))) <- maybe_given
+  | Just (GivenSolved (Just (EvCoercion co))) <- maybe_given
   = co
   | otherwise
-  = mkEqVarLCo (setVarType (cc_id ct) (ctPred ct))
+  = mkTcCoVarCo (setVarType (cc_id ct) (ctPred ct))
                 -- NB: The variable could be rewritten by a spontaneously
-                -- solved, so it is not safe to simply do a mkEqVarLCo (cc_id ct)
+                -- solved, so it is not safe to simply do a mkTcCoVarCo (cc_id ct)
                 -- Instead we use the most accurate type, given by ctPred c
   where maybe_given = isGiven_maybe (cc_flavor ct)
 
 -- See Note [LiftInertEqs]
-liftInertEqsTy :: (TyVarEnv (Ct,Coercion),InScopeSet)
+liftInertEqsTy :: (TyVarEnv (Ct, TcCoercion),InScopeSet)
                  -> CtFlavor
-                 -> PredType -> Coercion
+                 -> PredType -> TcCoercion
 liftInertEqsTy (subst,inscope) fl pty
   = ty_cts_subst subst inscope fl pty
 
 
-ty_cts_subst :: TyVarEnv (Ct,Coercion)
-             -> InScopeSet -> CtFlavor -> Type -> Coercion
+ty_cts_subst :: TyVarEnv (Ct, TcCoercion)
+             -> InScopeSet -> CtFlavor -> Type -> TcCoercion
 ty_cts_subst subst inscope fl ty 
   = go ty 
   where 
         go ty = go' ty
 
-        go' (TyVarTy tv)      = tyvar_cts_subst tv `orElse` Refl (TyVarTy tv)
-        go' (AppTy ty1 ty2)   = mkAppCo (go ty1) (go ty2) 
-        go' (TyConApp tc tys) = mkTyConAppCo tc (map go tys)  
+        go' (TyVarTy tv)      = tyvar_cts_subst tv `orElse` mkTcReflCo (TyVarTy tv)
+        go' (AppTy ty1 ty2)   = mkTcAppCo (go ty1) (go ty2) 
+        go' (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)  
 
-        go' (ForAllTy v ty)   = mkForAllCo v' $! co
+        go' (ForAllTy v ty)   = mkTcForAllCo v' $! co
                              where 
                                (subst',inscope',v') = upd_tyvar_bndr subst inscope v
                                co = ty_cts_subst subst' inscope' fl ty 
 
-        go' (FunTy ty1 ty2)   = mkFunCo (go ty1) (go ty2)
+        go' (FunTy ty1 ty2)   = mkTcFunCo (go ty1) (go ty2)
 
 
         tyvar_cts_subst tv  
@@ -1556,7 +1546,7 @@ ty_cts_subst subst inscope fl ty
                         -- But we do not want to monadically create a new EvVar. So, we
                         -- create an 'unused_ct' but we cache reflexivity as the 
                         -- associated coercion. 
-                    | otherwise = extendVarEnv subst v (unused_ct, Refl (TyVarTy new_v))
+                    | otherwise = extendVarEnv subst v (unused_ct, mkTcReflCo (TyVarTy new_v))
 
                 no_change = new_v == v 
                 new_v     = uniqAway inscope v 
index 07875b1..a36be65 100644 (file)
@@ -14,7 +14,6 @@ module TcSimplify(
 
 #include "HsVersions.h"
 
-import HsSyn          
 import TcRnMonad
 import TcErrors
 import TcMType
@@ -26,7 +25,7 @@ import Unify  ( niFixTvSubst, niSubstTvSet )
 import Var
 import VarSet
 import VarEnv 
-import Coercion
+import TcEvidence
 import TypeRep
 import Name
 import NameEnv ( emptyNameEnv )
@@ -1046,7 +1045,7 @@ solveCTyFunEqs cts
       ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
   where
     solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
-                              ; _ <- setEqBind cv (mkReflCo ty) $
+                              ; _ <- setEqBind cv (mkTcReflCo ty) $
                                        (Wanted $ panic "Met an already solved function equality!")
                               ; return () -- Don't care about flavors etc this is
                                           -- the last thing happening
index 54bc0cd..7c37fc0 100644 (file)
@@ -55,6 +55,7 @@ import Class
 import Inst
 import TyCon
 import DataCon
+import TcEvidence( TcEvBinds(..) )
 import Id
 import IdInfo
 import DsMeta
index 018655b..d4d2642 100644 (file)
@@ -26,7 +26,7 @@ module TcType (
   --------------------------------
   -- Types 
   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
-  TcCoercion, TcTyVar, TcTyVarSet, TcKind, TcCoVar,
+  TcTyVar, TcTyVarSet, TcKind, TcCoVar,
 
   --------------------------------
   -- MetaDetails
@@ -166,8 +166,8 @@ import Class
 import Var
 import ForeignCall
 import VarSet
-import Type
 import Coercion
+import Type
 import TyCon
 
 -- others:
@@ -232,8 +232,6 @@ type TcType = Type  -- A TcType can have mutable type variables
        -- a cannot occur inside a MutTyVar in T; that is,
        -- T is "flattened" before quantifying over a
 
-type TcCoercion = Coercion  -- A TcCoercion can contain TcTypes.
-
 -- These types do not have boxy type variables in them
 type TcPredType     = PredType
 type TcThetaType    = ThetaType
@@ -445,6 +443,8 @@ pprUserTypeCtxt (DataTyCtxt tc)   = ptext (sLit "the context of the data type de
 %*                                                                     *
 %************************************************************************
 
+Tidying is here becuase it has a special case for FlatSkol
+
 \begin{code}
 -- | This tidies up a type for printing in an error message, or in
 -- an interface file.
@@ -550,7 +550,6 @@ tidyKind = tidyType
 %************************************************************************
 
 \begin{code}
-
 tidyCo :: TidyEnv -> Coercion -> Coercion
 tidyCo env@(_, subst) co
   = go co
@@ -575,7 +574,6 @@ tidyCo env@(_, subst) co
 
 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
 tidyCos env = map (tidyCo env)
-
 \end{code}
 
 %************************************************************************
index ca34ff7..23de50a 100644 (file)
@@ -49,7 +49,7 @@ import TcIface
 import TcRnMonad
 import TcType
 import Type
-import Coercion
+import TcEvidence
 import Name ( isSystemName )
 import Inst
 import Kind
@@ -119,7 +119,7 @@ expected type, becuase it expects that to have been done already
 matchExpectedFunTys :: SDoc    -- See Note [Herald for matchExpectedFunTys]
                    -> Arity
                    -> TcRhoType 
-                    -> TcM (LCoercion, [TcSigmaType], TcRhoType)
+                    -> TcM (TcCoercion, [TcSigmaType], TcRhoType)
 
 -- If    matchExpectFunTys n ty = (co, [t1,..,tn], ty_r)
 -- then  co : ty ~ (t1 -> ... -> tn -> ty_r)
@@ -138,7 +138,7 @@ matchExpectedFunTys herald arity orig_ty
     -- then   co : ty ~ t1 -> .. -> tn -> ty_r
 
     go n_req ty
-      | n_req == 0 = return (mkReflCo ty, [], ty)
+      | n_req == 0 = return (mkTcReflCo ty, [], ty)
 
     go n_req ty
       | Just ty' <- tcView ty = go n_req ty'
@@ -146,7 +146,7 @@ matchExpectedFunTys herald arity orig_ty
     go n_req (FunTy arg_ty res_ty)
       | not (isPredTy arg_ty)
       = do { (co, tys, ty_r) <- go (n_req-1) res_ty
-           ; return (mkFunCo (mkReflCo arg_ty) co, arg_ty:tys, ty_r) }
+           ; return (mkTcFunCo (mkTcReflCo arg_ty) co, arg_ty:tys, ty_r) }
 
     go _ (TyConApp tc _)             -- A common case
       | not (isSynFamilyTyCon tc)
@@ -189,14 +189,14 @@ matchExpectedFunTys herald arity orig_ty
 
 \begin{code}
 ----------------------
-matchExpectedListTy :: TcRhoType -> TcM (LCoercion, TcRhoType)
+matchExpectedListTy :: TcRhoType -> TcM (TcCoercion, TcRhoType)
 -- Special case for lists
 matchExpectedListTy exp_ty
  = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
       ; return (co, elt_ty) }
 
 ----------------------
-matchExpectedPArrTy :: TcRhoType -> TcM (LCoercion, TcRhoType)
+matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercion, TcRhoType)
 -- Special case for parrs
 matchExpectedPArrTy exp_ty
   = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
@@ -205,7 +205,7 @@ matchExpectedPArrTy exp_ty
 ----------------------
 matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
                       -> TcRhoType           -- orig_ty
-                      -> TcM (LCoercion,      -- T k1 k2 k3 a b c ~ orig_ty
+                      -> TcM (TcCoercion,      -- T k1 k2 k3 a b c ~ orig_ty
                               [TcSigmaType])  -- Element types, k1 k2 k3 a b c
                               
 -- It's used for wired-in tycons, so we call checkWiredInTyCon
@@ -216,7 +216,7 @@ matchExpectedTyConApp tc orig_ty
   = do  { checkWiredInTyCon tc
         ; go (tyConArity tc) orig_ty [] }
   where
-    go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (LCoercion, [TcSigmaType])
+    go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (TcCoercion, [TcSigmaType])
     -- If     go n ty tys = (co, [t1..tn] ++ tys)
     -- then   co : T t1..tn ~ ty
 
@@ -233,12 +233,12 @@ matchExpectedTyConApp tc orig_ty
     go n_req ty@(TyConApp tycon args) tys
       | tc == tycon
       = ASSERT( n_req == length args)   -- ty::*
-        return (mkReflCo ty, args ++ tys)
+        return (mkTcReflCo ty, args ++ tys)
 
     go n_req (AppTy fun arg) tys
       | n_req > 0
       = do { (co, args) <- go (n_req - 1) fun (arg : tys) 
-           ; return (mkAppCo co (mkReflCo arg), args) }
+           ; return (mkTcAppCo co (mkTcReflCo arg), args) }
 
     go n_req ty tys = defer n_req ty tys
 
@@ -255,7 +255,7 @@ matchExpectedTyConApp tc orig_ty
 
 ----------------------
 matchExpectedAppTy :: TcRhoType                         -- orig_ty
-                   -> TcM (LCoercion,                   -- m a ~ orig_ty
+                   -> TcM (TcCoercion,                   -- m a ~ orig_ty
                            (TcSigmaType, TcSigmaType))  -- Returns m, a
 -- If the incoming type is a mutable type variable of kind k, then
 -- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
@@ -267,7 +267,7 @@ matchExpectedAppTy orig_ty
       | Just ty' <- tcView ty = go ty'
 
       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
-      = return (mkReflCo orig_ty, (fun_ty, arg_ty))
+      = return (mkTcReflCo orig_ty, (fun_ty, arg_ty))
 
     go (TyVarTy tv)
       | ASSERT( isTcTyVar tv) isMetaTyVar tv
@@ -469,18 +469,18 @@ The exported functions are all defined as versions of some
 non-exported generic functions.
 
 \begin{code}
-unifyType :: TcTauType -> TcTauType -> TcM LCoercion
+unifyType :: TcTauType -> TcTauType -> TcM TcCoercion
 -- Actual and expected types
 -- Returns a coercion : ty1 ~ ty2
 unifyType ty1 ty2 = uType [] ty1 ty2
 
 ---------------
-unifyPred :: PredType -> PredType -> TcM LCoercion
+unifyPred :: PredType -> PredType -> TcM TcCoercion
 -- Actual and expected types
 unifyPred = unifyType
 
 ---------------
-unifyTheta :: TcThetaType -> TcThetaType -> TcM [LCoercion]
+unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercion]
 -- Actual and expected types
 unifyTheta theta1 theta2
   = do  { checkTc (equalLength theta1 theta2)
@@ -531,7 +531,7 @@ uType, uType_np, uType_defer
   :: [EqOrigin]
   -> TcType    -- ty1 is the *actual* type
   -> TcType    -- ty2 is the *expected* type
-  -> TcM LCoercion
+  -> TcM TcCoercion
 
 --------------
 -- It is always safe to defer unification to the main constraint solver
@@ -551,7 +551,7 @@ uType_defer (item : origin) ty1 ty2
             ; traceTc "utype_defer" (vcat [ppr eqv, ppr ty1,
                                            ppr ty2, ppr origin, doc])
             }
-       ; return (mkEqVarLCo eqv) }
+       ; return (mkTcCoVarCo eqv) }
 uType_defer [] _ _
   = panic "uType_defer"
 
@@ -567,7 +567,7 @@ uType_np origin orig_ty1 orig_ty2
               [ sep [ ppr orig_ty1, text "~", ppr orig_ty2]
               , ppr origin]
        ; co <- go orig_ty1 orig_ty2
-       ; if isReflCo co
+       ; if isTcReflCo co
             then traceTc "u_tys yields no coercion" empty
             else traceTc "u_tys yields coercion:" (ppr co)
        ; return co }
@@ -575,7 +575,7 @@ uType_np origin orig_ty1 orig_ty2
     bale_out :: [EqOrigin] -> TcM a
     bale_out origin = failWithMisMatch origin
 
-    go :: TcType -> TcType -> TcM LCoercion
+    go :: TcType -> TcType -> TcM TcCoercion
        -- The arguments to 'go' are always semantically identical 
        -- to orig_ty{1,2} except for looking through type synonyms
 
@@ -602,7 +602,7 @@ uType_np origin orig_ty1 orig_ty2
     go (FunTy fun1 arg1) (FunTy fun2 arg2)
       = do { co_l <- uType origin fun1 fun2
            ; co_r <- uType origin arg1 arg2
-           ; return $ mkFunCo co_l co_r }
+           ; return $ mkTcFunCo co_l co_r }
 
         -- Always defer if a type synonym family (type function)
        -- is involved.  (Data families behave rigidly.)
@@ -614,20 +614,20 @@ uType_np origin orig_ty1 orig_ty2
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       | tc1 == tc2        -- See Note [TyCon app]
       = do { cos <- uList origin uType tys1 tys2
-           ; return $ mkTyConAppCo tc1 cos }
+           ; return $ mkTcTyConAppCo tc1 cos }
      
        -- See Note [Care with type applications]
     go (AppTy s1 t1) ty2
       | Just (s2,t2) <- tcSplitAppTy_maybe ty2
       = do { co_s <- uType_np origin s1 s2  -- See Note [Unifying AppTy]
            ; co_t <- uType origin t1 t2        
-           ; return $ mkAppCo co_s co_t }
+           ; return $ mkTcAppCo co_s co_t }
 
     go ty1 (AppTy s2 t2)
       | Just (s1,t1) <- tcSplitAppTy_maybe ty1
       = do { co_s <- uType_np origin s1 s2
            ; co_t <- uType origin t1 t2
-           ; return $ mkAppCo co_s co_t }
+           ; return $ mkTcAppCo co_s co_t }
 
     go ty1 ty2
       | tcIsForAllTy ty1 || tcIsForAllTy ty2 
@@ -636,7 +636,7 @@ uType_np origin orig_ty1 orig_ty2
         -- Anything else fails
     go _ _ = bale_out origin
 
-unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM LCoercion
+unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM TcCoercion
 unifySigmaTy origin ty1 ty2
   = do { let (tvs1, body1) = tcSplitForAllTys ty1
              (tvs2, body2) = tcSplitForAllTys ty2
@@ -647,21 +647,12 @@ unifySigmaTy origin ty1 ty2
              in_scope = mkInScopeSet (mkVarSet skol_tvs)
              phi1     = Type.substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
              phi2     = Type.substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
+            skol_info = UnifyForAllSkol ty1
 
-       ; ((coi, _untch), lie) <- captureConstraints $ 
-                                 captureUntouchables $ 
-                                 uType origin phi1 phi2
-          -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
-          -- VERY UNSATISFACTORY; the constraint might be fine, but
-         -- we fail eagerly because we don't have any place to put 
-         -- the bindings from an implication constraint
-         -- This only works because most constraints get solved on the fly
-         -- See Note [Avoid deferring]
-         ; when (any (`elemVarSet` tyVarsOfWC lie) skol_tvs)
-              (failWithMisMatch origin)        -- ToDo: give details from bad_lie
-
-       ; emitConstraints lie
-       ; return (foldr mkForAllCo coi skol_tvs) }
+       ; (ev_binds, co) <- checkConstraints skol_info skol_tvs [] $
+                           uType origin phi1 phi2
+
+       ; return (foldr mkTcForAllCo (TcLetCo ev_binds co) skol_tvs) }
 
 ---------------
 uList :: [EqOrigin] 
@@ -774,7 +765,7 @@ of the substitution; rather, notice that @uVar@ (defined below) nips
 back into @uTys@ if it turns out that the variable is already bound.
 
 \begin{code}
-uVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTauType -> TcM LCoercion
+uVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTauType -> TcM TcCoercion
 uVar origin swapped tv1 ty2
   = do  { traceTc "uVar" (vcat [ ppr origin
                                 , ppr swapped
@@ -792,13 +783,13 @@ uUnfilledVar :: [EqOrigin]
              -> SwapFlag
              -> TcTyVar -> TcTyVarDetails       -- Tyvar 1
              -> TcTauType                      -- Type 2
-             -> TcM LCoercion
+             -> TcM TcCoercion
 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
 --            It might be a skolem, or untouchable, or meta
 
 uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
   | tv1 == tv2  -- Same type variable => no-op
-  = return (mkReflCo (mkTyVarTy tv1))
+  = return (mkTcReflCo (mkTyVarTy tv1))
 
   | otherwise  -- Distinct type variables
   = do  { lookup2 <- lookupTcTyVar tv2
@@ -832,7 +823,7 @@ uUnfilledVars :: [EqOrigin]
               -> SwapFlag
               -> TcTyVar -> TcTyVarDetails      -- Tyvar 1
               -> TcTyVar -> TcTyVarDetails      -- Tyvar 2
-              -> TcM LCoercion
+              -> TcM TcCoercion
 -- Invarant: The type variables are distinct,
 --           Neither is filled in yet
 
@@ -1018,10 +1009,10 @@ lookupTcTyVar tyvar
     details = ASSERT2( isTcTyVar tyvar, ppr tyvar )
               tcTyVarDetails tyvar
 
-updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM LCoercion
+updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM TcCoercion
 updateMeta tv1 ref1 ty2
   = do { writeMetaTyVarRef tv1 ref1 ty2
-       ; return (mkReflCo ty2) }
+       ; return (mkTcReflCo ty2) }
 \end{code}
 
 Note [Unifying untouchables]
index ac4d5dd..f53b658 100644 (file)
@@ -10,13 +10,13 @@ module TcUnify where
 import TcType     ( TcTauType, TcKind, Type, Kind )
 import VarEnv     ( TidyEnv )
 import TcRnTypes  ( TcM )
-import Coercion   ( LCoercion )
+import TcEvidence ( TcCoercion )
 import Outputable ( SDoc )
 
 -- This boot file exists only to tie the knot between
 --              TcUnify and Inst
 
-unifyType :: TcTauType -> TcTauType -> TcM LCoercion
+unifyType :: TcTauType -> TcTauType -> TcM TcCoercion
 unifyKindEq :: TcKind -> TcKind -> TcM ()
 mkKindErrorCtxt :: Type -> Type -> Kind -> Kind -> TidyEnv -> TcM (TidyEnv, SDoc)
 \end{code}
index 17179fd..840365e 100644 (file)
 module Coercion (
         -- * Main data type
         Coercion(..), Var, CoVar,
-        LCoercion,
 
         -- ** Functions over coercions
         coVarKind,
-        coercionType, coercionKind, coercionKinds, isReflCo, liftedCoercionKind,
+        coercionType, coercionKind, coercionKinds, isReflCo,
         isReflCo_maybe,
         mkCoercionType,
 
        -- ** Constructing coercions
-        mkReflCo, mkCoVarCo, mkEqVarLCo,
+        mkReflCo, mkCoVarCo, 
         mkAxInstCo, mkPiCo, mkPiCos,
         mkSymCo, mkTransCo, mkNthCo,
        mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
@@ -42,7 +41,7 @@ module Coercion (
         splitForAllCo_maybe,
 
        -- ** Coercion variables
-       mkCoVar, isCoVar, isCoVarType, isLCoVar, coVarName, setCoVarName, setCoVarUnique,
+       mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
 
         -- ** Free variables
         tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize,
@@ -53,8 +52,8 @@ module Coercion (
        isEmptyCvSubst, zapCvSubstEnv, getCvInScope,
         substCo, substCos, substCoVar, substCoVars,
         substCoWithTy, substCoWithTys, 
-       cvTvSubst, tvCvSubst, zipOpenCvSubst,
-        substTy, extendTvSubst,
+       cvTvSubst, tvCvSubst, mkCvSubst, zipOpenCvSubst,
+        substTy, extendTvSubst, extendCvSubstAndInScope,
        substTyVarBndr, substCoVarBndr,
 
        -- ** Lifting
@@ -67,7 +66,7 @@ module Coercion (
         seqCo,
         
         -- * Pretty-printing
-        pprCo, pprParendCo, pprCoAxiom,
+        pprCo, pprParendCo, pprCoAxiom, 
 
         -- * Other
         applyCo
@@ -91,7 +90,7 @@ import BasicTypes
 import Outputable
 import Unique
 import Pair
-import PrelNames       ( funTyConKey, eqPrimTyConKey, eqTyConKey )
+import PrelNames       ( funTyConKey, eqPrimTyConKey )
 import Control.Applicative
 import Data.Traversable (traverse, sequenceA)
 import Control.Arrow (second)
@@ -150,24 +149,6 @@ data Coercion
   deriving (Data.Data, Data.Typeable)
 \end{code}
 
-Note [LCoercions]
-~~~~~~~~~~~~~~~~~
-| 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 mkEqVarLCo.
-
-\begin{code}
-type LCoercion = Coercion
-\end{code}
 
 Note [Refl invariant]
 ~~~~~~~~~~~~~~~~~~~~~
@@ -314,14 +295,6 @@ setCoVarName   = setVarName
 isCoVar :: Var -> Bool
 isCoVar v = isCoVarType (varType v)
 
-isLCoVar :: Var -> Bool 
--- Is lifted coercion variable (only!)
-isLCoVar v 
-  | Just tc <- tyConAppTyCon_maybe (varType v) 
-  , tc `hasKey` eqTyConKey
-  = True
-  | otherwise = False 
-
 isCoVarType :: Type -> Bool
 isCoVarType ty             -- Tests for t1 ~# t2, the unboxed equality
   | Just tc <- tyConAppTyCon_maybe ty = tc `hasKey` eqPrimTyConKey
@@ -399,7 +372,7 @@ pprCo       co = ppr_co TopPrec   co
 pprParendCo co = ppr_co TyConPrec co
 
 ppr_co :: Prec -> Coercion -> SDoc
-ppr_co _ (Refl ty) = angles (ppr ty)
+ppr_co _ (Refl ty) = angleBrackets (ppr ty)
 
 ppr_co p co@(TyConAppCo tc [_,_])
   | tc `hasKey` funTyConKey = ppr_fun_co p co
@@ -424,9 +397,6 @@ ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo c
 ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendCo co]
 
 
-angles :: SDoc -> SDoc
-angles p = char '<' <> p <> char '>'
-
 ppr_fun_co :: Prec -> Coercion -> SDoc
 ppr_fun_co p co = pprArrowChain p (split co)
   where
@@ -508,14 +478,6 @@ coVarKind cv
    (ty1,ty2)
  | otherwise = panic "coVarKind, non coercion variable"
 
-liftedCoVarKind :: EqVar -> (Type,Type)
-liftedCoVarKind cv
- | Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
- = ASSERT (tc `hasKey` eqTyConKey)
-   (ty1,ty2)
- | otherwise = panic "liftedCoVarKind, non coercion variable"
-
-
 -- | Makes a coercion type from two types: the types whose equality 
 -- is proven by the relevant 'Coercion'
 mkCoercionType :: Type -> Type -> Type
@@ -545,16 +507,6 @@ mkCoVarCo cv
   where
     (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
 
-mkEqVarLCo :: EqVar -> LCoercion
--- ipv :: s ~ t  (the boxed equality type)
-mkEqVarLCo ipv
-  | ty1 `eqType` ty2 = Refl ty1
-  | otherwise        = CoVarCo ipv
-  where
-    (ty1, ty2) = case getEqPredTys_maybe (varType ipv) of
-        Nothing  -> pprPanic "mkCoVarLCo" (ppr ipv)
-        Just tys -> tys
-
 mkReflCo :: Type -> Coercion
 mkReflCo = Refl
 
@@ -627,7 +579,7 @@ mkTransCo co (Refl _) = co
 mkTransCo co1 co2     = TransCo co1 co2
 
 mkNthCo :: Int -> Coercion -> Coercion
-mkNthCo n (Refl ty) = Refl (getNth n ty)
+mkNthCo n (Refl ty) = Refl (tyConAppArgN n ty)
 mkNthCo n co        = NthCo n co
 
 -- | Instantiates a 'Coercion' with a 'Type' argument. 
@@ -818,6 +770,13 @@ extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
 extendTvSubst (CvSubst in_scope tenv cenv) tv ty
   = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
 
+extendCvSubstAndInScope :: CvSubst -> CoVar -> Coercion -> CvSubst
+-- Also extends the in-scope set
+extendCvSubstAndInScope (CvSubst in_scope tenv cenv) cv co
+  = CvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfCo co)
+            tenv
+            (extendVarEnv cenv cv co)
+
 substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
 substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
   = ASSERT( isCoVar old_var )
@@ -835,13 +794,16 @@ substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
     new_var = uniqAway in_scope subst_old_var
     subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
                  -- It's important to do the substitution for coercions,
-                 -- because only they can have free type variables
+                 -- because they can have free type variables
 
 substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
 substTyVarBndr (CvSubst in_scope tenv cenv) old_var
   = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
       (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
 
+mkCvSubst :: InScopeSet -> [(Var,Coercion)] -> CvSubst
+mkCvSubst in_scope prs = CvSubst in_scope Type.emptyTvSubstEnv (mkVarEnv prs)
+
 zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
 zipOpenCvSubst vs cos
   | debugIsOn && (length vs /= length cos)
@@ -1092,29 +1054,21 @@ coercionType co = case coercionKind co of
 --
 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
 
-liftedCoercionKind :: LCoercion -> Pair Type
-liftedCoercionKind = coercion_kind liftedCoVarKind 
-
 coercionKind :: Coercion -> Pair Type 
-coercionKind = coercion_kind coVarKind
-                                
-coercion_kind :: (CoVar -> (Type,Type)) -> Coercion -> Pair Type
--- Works for Coercions and LCoercions but you have to pass in what to do 
--- at the (unlifted or lifted) coercion variable. 
-coercion_kind f co = go co 
+coercionKind co = go co
   where 
     go (Refl ty)            = Pair ty ty
     go (TyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
     go (AppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
     go (ForAllCo tv co)     = mkForAllTy tv <$> go co
-    go (CoVarCo cv)         = toPair $ f cv
+    go (CoVarCo cv)         = toPair $ coVarKind cv
     go (AxiomInstCo ax cos) = let Pair tys1 tys2 = sequenceA $ map go cos 
                               in  Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax)) 
                                        (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax))
     go (UnsafeCo ty1 ty2)   = Pair ty1 ty2
     go (SymCo co)           = swap $ go co
     go (TransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)
-    go (NthCo d co)         = getNth d <$> go co
+    go (NthCo d co)         = tyConAppArgN d <$> go co
     go (InstCo aco ty)      = go_app aco [ty]
 
     go_app :: Coercion -> [Type] -> Pair Type
@@ -1126,12 +1080,6 @@ coercion_kind f co = go co
 -- | Apply 'coercionKind' to multiple 'Coercion's
 coercionKinds :: [Coercion] -> Pair [Type]
 coercionKinds tys = sequenceA $ map coercionKind tys
-
-getNth :: Int -> Type -> Type
--- Executing Nth
-getNth n ty | Just tys <- tyConAppArgs_maybe ty
-            = ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n
-getNth n ty = pprPanic "getNth" (ppr n <+> ppr ty)
 \end{code}
 
 Note [Nested InstCos]
index 579ae75..ebf542a 100644 (file)
@@ -36,7 +36,7 @@ module Type (
 
        mkTyConApp, mkTyConTy,
        tyConAppTyCon_maybe, tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs, 
-       splitTyConApp_maybe, splitTyConApp, 
+       splitTyConApp_maybe, splitTyConApp, tyConAppArgN,
 
         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, 
         mkPiKinds, mkPiType, mkPiTypes,
@@ -503,6 +503,13 @@ tyConAppArgs_maybe _                = Nothing
 tyConAppArgs :: Type -> [Type]
 tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
 
+tyConAppArgN :: Int -> Type -> Type
+-- Executing Nth
+tyConAppArgN n ty 
+  = case tyConAppArgs_maybe ty of
+      Just tys -> ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n
+      Nothing  -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty)
+
 -- | Attempts to tease a type apart into a type constructor and the application
 -- of a number of arguments to that constructor. Panics if that is not possible.
 -- See also 'splitTyConApp_maybe'
index fdadf7f..0b8a1bf 100644 (file)
@@ -31,7 +31,7 @@ module TypeRep (
        pprEqPred, pprTheta, pprForAll, pprThetaArrowTy, pprClassPred,
         pprKind, pprParendKind,
        Prec(..), maybeParen, pprTcApp, pprTypeNameApp, 
-        pprPrefixApp, pprArrowChain,
+        pprPrefixApp, pprArrowChain, ppr_type,
 
         -- Free variables
         tyVarsOfType, tyVarsOfTypes,