[commit: ghc] type-holes-branch: Merge branch 'tc-untouchables' of http://darcs.haskell.org/ghc into tc-untouchables (cb72b66)
Simon Peyton Jones
simonpj at microsoft.com
Mon Sep 17 13:05:03 CEST 2012
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 <simonpj at microsoft.com>
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
More information about the Cvs-ghc
mailing list