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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
