[commit: ghc] type-holes-branch: Merge branch 'tc-untouchables' of http://darcs.haskell.org/ghc into tc-untouchables (cb72b66)

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : type-holes-branch

http://hackage.haskell.org/trac/ghc/changeset/cb72b66c9c006b280c10103b2b453cb492e9837e

>---------------------------------------------------------------

commit cb72b66c9c006b280c10103b2b453cb492e9837e
Merge: 2365822... 633dd55...
Author: Simon Peyton Jones <[email protected]>
Date:   Thu Sep 6 21:43:09 2012 +0100

    Merge branch 'tc-untouchables' of http://darcs.haskell.org/ghc into tc-untouchables

 compiler/typecheck/TcErrors.lhs   |   22 +++--
 compiler/typecheck/TcInteract.lhs |    6 +-
 compiler/typecheck/TcMType.lhs    |  106 ++++++++++++++++++++---
 compiler/typecheck/TcSimplify.lhs |  172 +++++++++++-------------------------
 4 files changed, 163 insertions(+), 143 deletions(-)

diff --cc compiler/typecheck/TcSimplify.lhs
index 7fd51a9,e112c19..66a9e89
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@@ -968,91 -975,41 +983,7 @@@ beta! Concrete example is in indexed_ty
              g2 z = case z of TEx y -> (h [[undefined]], op x [y])
          in (g1 '3', g2 undefined)
  
 -Note [Extra TcsTv untouchables]
 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -Whenever we are solving a bunch of flat constraints, they may contain 
 -the following sorts of 'touchable' unification variables:
 -   
 -   (i)   Born-touchables in that scope
 - 
 -   (ii)  Simplifier-generated unification variables, such as unification 
 -         flatten variables
 -
 -   (iii) Touchables that have been floated out from some nested 
 -         implications, see Note [Float Equalities out of Implications]. 
 -
 -Now, once we are done with solving these flats and have to move inwards to 
 -the nested implications (perhaps for a second time), we must consider all the
 -extra variables (categories (ii) and (iii) above) as untouchables for the 
 -implication. Otherwise we have the danger or double unifications, as well
 -as the danger of not ``seeing'' some unification. Example (from Trac #4494):
 -
 -   (F Int ~ uf)  /\  [untch=beta](forall a. C a => F Int ~ beta) 
 -
 -In this example, beta is touchable inside the implication. The 
 -first solveInteract step leaves 'uf' ununified. Then we move inside 
 -the implication where a new constraint
 -       uf  ~  beta  
 -emerges. We may spontaneously solve it to get uf := beta, so the whole
 -implication disappears but when we pop out again we are left with (F
 -Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
 -uf will get unified *once more* to (F Int).
 -
 -The solution is to record the unification variables of the flats, 
 -and make them untouchables for the nested implication. In the 
 -example above uf would become untouchable, so beta would be forced 
 -to be unified as beta := uf.
  
- \begin{code}
- unFlattenWC :: WantedConstraints -> TcS WantedConstraints
- unFlattenWC wc 
-   = do { (subst, remaining_unsolved_flats) <- solveCTyFunEqs (wc_flat wc)
-                 -- See Note [Solving Family Equations]
-                 -- NB: remaining_flats has already had subst applied
-        ; return $ 
-          WC { wc_flat  = mapBag (substCt subst) remaining_unsolved_flats
-             , wc_impl  = mapBag (substImplication subst) (wc_impl wc) 
-             , wc_insol = mapBag (substCt subst) (wc_insol wc) }
-        }
-   where 
-     solveCTyFunEqs :: Cts -> TcS (TvSubst, Cts)
-     -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
-     -- See Note [Solving Family Equations]
-     -- Returns: a bunch of unsolved constraints from the original Cts and implications
-     --          where the newly generated equalities (alpha := F xi) have been substituted through.
-     solveCTyFunEqs cts
-      = do { untch   <- TcSMonad.getUntouchables 
-           ; let (unsolved_can_cts, (ni_subst, cv_binds))
-                     = getSolvableCTyFunEqs untch cts
-           ; traceTcS "defaultCTyFunEqs" (vcat [ text "Trying to default family equations:"
-                                               , text "untch" <+> ppr untch 
-                                               , text "subst" <+> ppr ni_subst 
-                                               , text "binds" <+> ppr cv_binds
-                                               , ppr unsolved_can_cts
-                                               ])
-           ; mapM_ solve_one cv_binds
- 
-           ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
-       where
-         solve_one (CtWanted { ctev_evar = cv }, tv, ty) 
-           = setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
-         solve_one (CtDerived {}, tv, ty)
-           = setWantedTyBind tv ty
-         solve_one arg
-           = pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
- 
- ------------
- type FunEqBinds = (TvSubstEnv, [(CtEvidence, TcTyVar, TcType)])
-   -- The TvSubstEnv is not idempotent, but is loop-free
-   -- See Note [Non-idempotent substitution] in Unify
- emptyFunEqBinds :: FunEqBinds
- emptyFunEqBinds = (emptyVarEnv, [])
- 
- extendFunEqBinds :: FunEqBinds -> CtEvidence -> TcTyVar -> TcType -> FunEqBinds
- extendFunEqBinds (tv_subst, cv_binds) fl tv ty
-   = (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds)
- 
- ------------
- getSolvableCTyFunEqs :: Untouchables
-                      -> Cts                -- Precondition: all Wanteds or Derived!
-                      -> (Cts, FunEqBinds)  -- Postcondition: returns the unsolvables
- getSolvableCTyFunEqs untch cts
-   = Bag.foldlBag dflt_funeq (emptyCts, emptyFunEqBinds) cts
-   where
-     dflt_funeq :: (Cts, FunEqBinds) -> Ct
-                -> (Cts, FunEqBinds)
-     dflt_funeq (cts_in, feb@(tv_subst, _))
-                (CFunEqCan { cc_ev = fl
-                           , cc_fun = tc
-                           , cc_tyargs = xis
-                           , cc_rhs = xi })
-       | Just tv <- tcGetTyVar_maybe xi      -- RHS is a type variable
- 
-       , isTouchableMetaTyVar untch tv
-            -- And it's a *touchable* unification variable
- 
-       , typeKind xi `tcIsSubKind` tyVarKind tv
-          -- Must do a small kind check since TcCanonical invariants 
-          -- on family equations only impose compatibility, not subkinding
- 
-       , not (tv `elemVarEnv` tv_subst)
-            -- Check not in extra_binds
-            -- See Note [Solving Family Equations], Point 1
- 
-       , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
-            -- Occurs check: see Note [Solving Family Equations], Point 2
-       = ASSERT ( not (isGiven fl) )
-         (cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis))
- 
-     dflt_funeq (cts_in, fun_eq_binds) ct
-       = (cts_in `extendCts` ct, fun_eq_binds)
- \end{code}
  
  Note [Solving Family Equations] 
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~