Commit 8dc6d645 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Re-engineer Given flatten-skolems

The big change here is to fix an outright bug in flattening of Givens,
albeit one that is very hard to exhibit.  Suppose we have the constraint
    forall a. (a ~ F b) => ..., (forall c. ....(F b)...) ...

Then
 - we'll flatten the (F) b to a fsk, say  (F b ~ fsk1)
 - we'll rewrite the (F b) inside the inner implication to 'fsk1'
 - when we leave the outer constraint we are suppose to unflatten;
   but that fsk1 will still be there
 - if we re-simplify the entire outer implication, we'll re-flatten
   the Given (F b) to, say, (F b ~ fsk2)
Now we have two fsks standing for the same thing, and that is very
wrong.

Solution: make fsks behave more like fmvs:
 - A flatten-skolem is now a MetaTyVar, whose MetaInfo is FlatSkolTv
 - We "fill in" that meta-tyvar when leaving the implication
 - The old FlatSkol form of TcTyVarDetails is gone completely
 - We track the flatten-skolems for the current implication in
   a new field of InertSet, inert_fsks.

See Note [The flattening story] in TcFlatten.

In doing this I found various other things to fix:

* I removed the zonkSimples from TcFlatten.unflattenWanteds; it wasn't
  needed.   But I added one in TcSimplify.floatEqualities, which does
  the zonk precisely when it is needed.

* Trac #13674 showed up a case where we had
     - an insoluble Given,   e.g.  a ~ [a]
     - the same insoluble Wanted   a ~ [a]
  We don't use the Given to rewwrite the Wanted (obviously), but
  we therefore ended up reporting
      Can't deduce (a ~ [a]) from (a ~ [a])
  which is silly.

  Conclusion: when reporting errors, make the occurs check "win"
  See Note [Occurs check wins] in TcErrors
parent c2eea089
......@@ -1538,7 +1538,7 @@ Suppose we have [G] Num (F [a])
then we flatten to
[G] Num fsk
[G] F [a] ~ fsk
where fsk is a flatten-skolem (FlatSkol). Suppose we have
where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
type instance F [a] = a
then we'll reduce the second constraint to
[G] a ~ fsk
......
......@@ -1466,7 +1466,7 @@ mkEqErr1 ctxt ct -- Wanted or derived;
NomEq -> empty
ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
; dflags <- getDynFlags
; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct))
; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going)
; let report = mconcat [important wanted_msg, important coercible_msg,
relevant_bindings binds_msg]
; if keep_going
......@@ -1604,15 +1604,21 @@ reportEqErr ctxt report ct oriented ty1 ty2
where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2
eqInfo = important $ mkEqInfoMsg ct ty1 ty2
mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> Report -> Ct
mkTyVarEqErr, mkTyVarEqErr'
:: DynFlags -> ReportErrCtxt -> Report -> Ct
-> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
-- tv1 and ty2 are already tidied
mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
| isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
= do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr ty2)
; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 }
mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2
| not insoluble_occurs_check -- See Note [Occurs check wins]
, isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
-- be oriented the other way round;
-- see TcCanonical.canEqTyVarTyVar
|| isSigTyVar tv1 && not (isTyVarTy ty2)
|| ctEqRel ct == ReprEq && not insoluble_occurs_check
|| isSigTyVar tv1 && not (isTyVarTy ty2)
|| ctEqRel ct == ReprEq
-- the cases below don't really apply to ReprEq (except occurs check)
= mkErrorMsgFromCt ctxt ct $ mconcat
[ important $ misMatchOrCND ctxt ct oriented ty1 ty2
......@@ -1827,7 +1833,6 @@ extraTyVarInfo ctxt tv
= ASSERT2( isTyVar tv, ppr tv )
case tcTyVarDetails tv of
SkolemTv {} -> pprSkol implics tv
FlatSkol {} -> pp_tv <+> text "is a flattening type variable"
RuntimeUnk {} -> pp_tv <+> text "is an interactive-debugger skolem"
MetaTv {} -> empty
where
......@@ -2016,7 +2021,22 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg"
{-
{- Note [Insoluble occurs check wins]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider [G] a ~ [a], [W] a ~ [a] (Trac #13674). The Given is insoluble
so we don't use it for rewriting. The Wanted is also insoluble, and
we don't solve it from the Given. It's very confusing to say
Cannot solve a ~ [a] from given constraints a ~ [a]
And indeed even thinking about the Givens is silly; [W] a ~ [a] is
just as insoluble as Int ~ Bool.
Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck)
then report it first.
(NB: there are potentially-soluble ones, like (a ~ F a b), and we don't
wnat to be as draconian with them.)
Note [Expanding type synonyms to make types similar]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -4,7 +4,7 @@ module TcFlatten(
FlattenMode(..),
flatten, flattenManyNom,
unflatten,
unflattenWanteds
) where
#include "HsVersions.h"
......@@ -36,31 +36,50 @@ import Control.Arrow ( first )
Note [The flattening story]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* A CFunEqCan is either of form
[G] <F xis> : F xis ~ fsk -- fsk is a FlatSkol
[W] x : F xis ~ fmv -- fmv is a unification variable,
-- but untouchable,
-- with MetaInfo = FlatMetaTv
[G] <F xis> : F xis ~ fsk -- fsk is a FlatSkolTv
[W] x : F xis ~ fmv -- fmv is a FlatMetaTv
where
x is the witness variable
fsk/fmv is a flatten skolem
xis are function-free
CFunEqCans are always [Wanted], or [Given], never [Derived]
fsk/fmv is a flatten skolem;
it is always untouchable (level 0)
fmv untouchable just means that in a CTyVarEq, say,
fmv ~ Int
we do NOT unify fmv.
* CFunEqCans can have any flavour: [G], [W], [WD] or [D]
* KEY INSIGHTS:
- A given flatten-skolem, fsk, is known a-priori to be equal to
F xis (the LHS), with <F xis> evidence
F xis (the LHS), with <F xis> evidence. The fsk is still a
unification variable, but it is "owned" by its CFunEqCan, and
is filled in (unflattened) only by unflattenGivens.
- A unification flatten-skolem, fmv, stands for the as-yet-unknown
type to which (F xis) will eventually reduce
type to which (F xis) will eventually reduce. It is filled in
only by dischargeFmv.
* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
then xis1 /= xis2
i.e. at most one CFunEqCan with a particular LHS
- All fsk/fmv variables are "untouchable". To make it simple to test,
we simply give them TcLevel=0. This means that in a CTyVarEq, say,
fmv ~ Int
we NEVER unify fmv.
- A unification flatten-skolems, fmv, ONLY gets unified when either
a) The CFunEqCan takes a step, using an axiom
b) By unflattenWanteds
They are never unified in any other form of equality.
For example [W] ffmv ~ Int is stuck; it does not unify with fmv.
* We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan.
That would destroy the invariant about the shape of a CFunEqCan,
and it would risk wanted/wanted interactions. The only way we
learn information about fsk is when the CFunEqCan takes a step.
However we *do* substitute in the LHS of a CFunEqCan (else it
would never get to fire!)
* Unflattening:
- We unflatten Givens when leaving their scope (see unflattenGivens)
- We unflatten Wanteds at the end of each attempt to simplify the
wanteds; see unflattenWanteds, called from solveSimpleWanteds.
* Each canonical [G], [W], or [WD] CFunEqCan x : F xis ~ fsk/fmv
has its own distinct evidence variable x and flatten-skolem fsk/fmv.
......@@ -70,7 +89,11 @@ Note [The flattening story]
In contrast a [D] CFunEqCan shares its fmv with its partner [W],
but does not "own" it. If we reduce a [D] F Int ~ fmv, where
say type instance F Int = ty, then we don't discharge fmv := ty.
Rather we simply generate [D] fmv ~ ty
Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq)
* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
then xis1 /= xis2
i.e. at most one CFunEqCan with a particular LHS
* Function applications can occur in the RHS of a CTyEqCan. No reason
not allow this, and it reduces the amount of flattening that must occur.
......@@ -104,20 +127,6 @@ Note [The flattening story]
- Add new wanted to flat cache
- Discharge x = F cos ; x2
* Unification flatten-skolems, fmv, ONLY get unified when either
a) The CFunEqCan takes a step, using an axiom
b) During un-flattening
They are never unified in any other form of equality.
For example [W] ffmv ~ Int is stuck; it does not unify with fmv.
* We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan.
That would destroy the invariant about the shape of a CFunEqCan,
and it would risk wanted/wanted interactions. The only way we
learn information about fsk is when the CFunEqCan takes a step.
However we *do* substitute in the LHS of a CFunEqCan (else it
would never get to fire!)
* [Interacting rule]
(inert) [W] x1 : F tys ~ fmv1
(work item) [W] x2 : F tys ~ fmv2
......@@ -1476,8 +1485,8 @@ flattens to
We must solve both!
-}
unflatten :: Cts -> Cts -> TcS Cts
unflatten tv_eqs funeqs
unflattenWanteds :: Cts -> Cts -> TcS Cts
unflattenWanteds tv_eqs funeqs
= do { tclvl <- getTcLevel
; traceTcS "Unflattening" $ braces $
......@@ -1506,10 +1515,7 @@ unflatten tv_eqs funeqs
; let all_flat = tv_eqs `andCts` funeqs
; traceTcS "Unflattening done" $ braces (pprCts all_flat)
-- Step 5: zonk the result
-- Motivation: makes them nice and ready for the next step
-- (see TcInteract.solveSimpleWanteds)
; zonkSimples all_flat }
; return all_flat }
where
----------------
unflatten_funeq :: Ct -> Cts -> TcS Cts
......
......@@ -1557,7 +1557,6 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
= case tcTyVarDetails tv of
SkolemTv {} -> lookup_in_env
RuntimeUnk {} -> lookup_in_env
FlatSkol ty -> zonkTcTypeToType env ty
MetaTv { mtv_ref = ref }
-> do { cts <- readMutVar ref
; case cts of
......
......@@ -160,6 +160,7 @@ solveSimpleGivens givens
solveSimpleWanteds :: Cts -> TcS WantedConstraints
-- NB: 'simples' may contain /derived/ equalities, floated
-- out from a nested implication. So don't discard deriveds!
-- The result is not necessarily zonked
solveSimpleWanteds simples
= do { traceTcS "solveSimpleWanteds {" (ppr simples)
; dflags <- getDynFlags
......@@ -199,12 +200,13 @@ solveSimpleWanteds simples
solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
-- Try solving these constraints
-- Affects the unification state (of course) but not the inert set
-- The result is not necessarily zonked
solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
= nestTcS $
do { solveSimples simples1
; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
; (unif_count, unflattened_eqs) <- reportUnifications $
unflatten tv_eqs fun_eqs
unflattenWanteds tv_eqs fun_eqs
-- See Note [Unflatten after solving the simple wanteds]
; return ( unif_count
, WC { wc_simple = others `andCts` unflattened_eqs
......@@ -2241,6 +2243,13 @@ Other notes:
- natural numbers
- Typeable
* Flatten-skolems: we do not treat a flatten-skolem as unifiable
for this purpose.
E.g. f :: Eq (F a) => [a] -> [a]
f xs = ....(xs==xs).....
Here we get [W] Eq [a], and we don't want to refrain from solving
it because of the given (Eq (F a)) constraint!
* The given-overlap problem is arguably not easy to appear in practice
due to our aggressive prioritization of equality solving over other
constraints, but it is possible. I've added a test case in
......@@ -2274,7 +2283,7 @@ Other notes:
in point.
All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;#
simplifiable class givens, we warn about signatures that contain them;
see TcValidity Note [Simplifiable given constraints].
-}
......
......@@ -550,8 +550,13 @@ instSkolTyCoVarX mk_tcv subst tycovar
newFskTyVar :: TcType -> TcM TcTyVar
newFskTyVar fam_ty
= do { uniq <- newUnique
; let name = mkSysTvName uniq (fsLit "fsk")
; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
; ref <- newMutVar Flexi
; let details = MetaTv { mtv_info = FlatSkolTv
, mtv_ref = ref
, mtv_tclvl = fmvTcLevel }
name = mkMetaTyVarName uniq (fsLit "fsk")
; return (mkTcTyVar name (typeKind fam_ty) details) }
{-
Note [Kind substitution when instantiating]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -593,10 +598,9 @@ newFmvTyVar :: TcType -> TcM TcTyVar
newFmvTyVar fam_ty
= do { uniq <- newUnique
; ref <- newMutVar Flexi
; cur_lvl <- getTcLevel
; let details = MetaTv { mtv_info = FlatMetaTv
, mtv_ref = ref
, mtv_tclvl = fmvTcLevel cur_lvl }
, mtv_tclvl = fmvTcLevel }
name = mkMetaTyVarName uniq (fsLit "s")
; return (mkTcTyVar name (typeKind fam_ty) details) }
......@@ -707,7 +711,7 @@ writeMetaTyVarRef tyvar ref ty
tv_lvl = tcTyVarLevel tyvar
ty_lvl = tcTypeLevel ty
level_check_ok = isFmvTyVar tyvar
level_check_ok = isFlattenTyVar tyvar
|| not (ty_lvl `strictlyDeeperThan` tv_lvl)
level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
......@@ -768,6 +772,7 @@ newAnonMetaTyVar meta_info kind
s = case meta_info of
TauTv -> fsLit "t"
FlatMetaTv -> fsLit "fmv"
FlatSkolTv -> fsLit "fsk"
SigTv -> fsLit "a"
; details <- newMetaDetails meta_info
; return (mkTcTyVar name kind details) }
......@@ -998,7 +1003,7 @@ zonkQuantifiedTyVar tv
MetaTv {} -> skolemiseUnboundMetaTyVar tv
_other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
_other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- RuntimeUnk
defaultTyVar :: Bool -- True <=> please default this kind variable to *
-> TcTyVar -- If it's a MetaTyVar then it is unbound
......@@ -1490,7 +1495,6 @@ zonkTcTyVar tv
= case tcTyVarDetails tv of
SkolemTv {} -> zonk_kind_and_return
RuntimeUnk {} -> zonk_kind_and_return
FlatSkol ty -> zonkTcType ty
MetaTv { mtv_ref = ref }
-> do { cts <- readMutVar ref
; case cts of
......
......@@ -1589,8 +1589,8 @@ data Ct
-- *never* over-saturated (because if so
-- we should have decomposed)
cc_fsk :: TcTyVar -- [Given] always a FlatSkol skolem
-- [Wanted] always a FlatMetaTv unification variable
cc_fsk :: TcTyVar -- [Given] always a FlatSkolTv
-- [Wanted] always a FlatMetaTv
-- See Note [The flattening story] in TcFlatten
}
......
......@@ -52,7 +52,7 @@ module TcSMonad (
getNoGivenEqs, setInertCans,
getInertEqs, getInertCans, getInertGivens,
getInertInsols,
emptyInert, getTcSInerts, setTcSInerts,
getTcSInerts, setTcSInerts,
matchableGivens, prohibitedSuperClassSolve,
getUnsolvedInerts,
removeInertCts, getPendingScDicts,
......@@ -383,6 +383,16 @@ data InertSet
-- Canonical Given, Wanted, Derived
-- Sometimes called "the inert set"
, inert_fsks :: [(TcTyVar, TcType)]
-- A list of (fsk, ty) pairs; we add one element when we flatten
-- a function application in a Given constraint, creating
-- a new fsk in newFlattenSkolem. When leaving a nested scope,
-- unflattenGivens unifies fsk := ty
--
-- We could also get this info from inert_funeqs, filtered by
-- level, but it seems simpler and more direct to capture the
-- fsk as we generate them.
, inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
-- See Note [Type family equations]
-- If F tys :-> (co, rhs, flav),
......@@ -421,6 +431,7 @@ emptyInert
, inert_irreds = emptyCts
, inert_insols = emptyCts }
, inert_flat_cache = emptyExactFunEqs
, inert_fsks = []
, inert_solved_dicts = emptyDictMap }
......@@ -1814,24 +1825,21 @@ getNoGivenEqs :: TcLevel -- TcLevel of this implication
-- See Note [When does an implication have given equalities?]
getNoGivenEqs tclvl skol_tvs
= do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
, inert_funeqs = funeqs
, inert_insols = insols })
<- getInertCans
; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
; let has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
(iirreds `unionBags` insols)
|| anyDVarEnv (eqs_given_here local_fsks) ieqs
|| anyDVarEnv eqs_given_here ieqs
; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
, ppr insols])
; return (not has_given_eqs, insols) }
where
eqs_given_here :: VarSet -> EqualCtList -> Bool
eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
eqs_given_here :: EqualCtList -> Bool
eqs_given_here [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
-- Givens are always a sigleton
= not (skolem_bound_here local_fsks tv) && ev_given_here ev
eqs_given_here _ _ = False
= not (skolem_bound_here tv) && ev_given_here ev
eqs_given_here _ = False
ev_given_here :: CtEvidence -> Bool
-- True for a Given bound by the curent implication,
......@@ -1840,16 +1848,10 @@ getNoGivenEqs tclvl skol_tvs
= isGiven ev
&& tclvl == ctLocLevel (ctEvLoc ev)
add_fsk :: Ct -> VarSet -> VarSet
add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
, isGiven ev = extendVarSet fsks tv
| otherwise = fsks
skol_tv_set = mkVarSet skol_tvs
skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
skolem_bound_here tv -- See Note [Let-bound skolems]
= case tcTyVarDetails tv of
SkolemTv {} -> tv `elemVarSet` skol_tv_set
FlatSkol {} -> not (tv `elemVarSet` local_fsks)
_ -> False
-- | Returns Given constraints that might,
......@@ -1889,9 +1891,11 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans })
-- bindable when unifying with givens. That ensures that we
-- conservatively assume that a meta tyvar might get unified with
-- something that matches the 'given', until demonstrated
-- otherwise.
bind_meta_tv tv | isMetaTyVar tv = BindMe
| otherwise = Skolem
-- otherwise. More info in Note [Instance and Given overlap]
-- in TcInteract
bind_meta_tv tv | isMetaTyVar tv
, not (isFskTyVar tv) = BindMe
| otherwise = Skolem
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
-- See Note [Solving superclass constraints] in TcInstDcls
......@@ -2413,6 +2417,8 @@ runTcSWithEvBinds ev_binds_var tcs
; when (count > 0) $
csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
; unflattenGivens inert_var
#if defined(DEBUG)
; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
; checkForCyclicBinds ev_binds
......@@ -2420,6 +2426,7 @@ runTcSWithEvBinds ev_binds_var tcs
; return res }
----------------------------
#if defined(DEBUG)
checkForCyclicBinds :: EvBindMap -> TcM ()
checkForCyclicBinds ev_binds_map
......@@ -2447,6 +2454,7 @@ checkForCyclicBinds ev_binds_map
-- Note [Deterministic SCC] in Digraph.
#endif
----------------------------
setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
setEvBindsTcS ref (TcS thing_inside)
= TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
......@@ -2460,8 +2468,9 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
, tcs_count = count
} ->
do { inerts <- TcM.readTcRef old_inert_var
; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs }
-- See Note [Do not inherit the flat cache]
; let nest_inert = emptyInert { inert_cans = inert_cans inerts
, inert_solved_dicts = inert_solved_dicts inerts }
-- See Note [Do not inherit the flat cache]
; new_inert_var <- TcM.newTcRef nest_inert
; new_wl_var <- TcM.newTcRef emptyWorkList
; let nest_env = TcSEnv { tcs_ev_binds = ref
......@@ -2472,6 +2481,8 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
; res <- TcM.setTcLevel inner_tclvl $
thing_inside nest_env
; unflattenGivens new_inert_var
#if defined(DEBUG)
-- Perform a check that the thing_inside did not cause cycles
; ev_binds <- TcM.getTcEvBindsMap ref
......@@ -2627,15 +2638,6 @@ unifyTyVar tv ty
; TcM.writeMetaTyVar tv ty
; TcM.updTcRef (tcs_unified env) (+1) }
unflattenFmv :: TcTyVar -> TcType -> TcS ()
-- Fill a flatten-meta-var, simply by unifying it.
-- This does NOT count as a unification in tcs_unified.
unflattenFmv tv ty
= ASSERT2( isMetaTyVar tv, ppr tv )
TcS $ \ _ ->
do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
; TcM.writeMetaTyVar tv ty }
reportUnifications :: TcS a -> TcS (Int, a)
reportUnifications (TcS thing_inside)
= TcS $ \ env ->
......@@ -2790,8 +2792,12 @@ which will result in two Deriveds to end up in the insoluble set:
wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
-}
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
{- *********************************************************************
* *
* Flatten skolems *
* *
********************************************************************* -}
newFlattenSkolem :: CtFlavour -> CtLoc
-> TyCon -> [TcType] -- F xis
-> TcS (CtEvidence, Coercion, TcTyVar) -- [G/WD] x:: F xis ~ fsk
......@@ -2806,9 +2812,14 @@ newFlattenSkolem flav loc tc xis
new_skolem
| Given <- flav
= do { fsk <- wrapTcS (TcM.newFskTyVar fam_ty)
; let co = mkNomReflCo fam_ty
; ev <- newGivenEvVar loc (mkPrimEqPred fam_ty (mkTyVarTy fsk),
EvCoercion co)
-- Extend the inert_fsks list, for use by unflattenGivens
; updInertTcS $ \is -> is { inert_fsks = (fsk, fam_ty) : inert_fsks is }
-- Construct the Refl evidence
; let pred = mkPrimEqPred fam_ty (mkTyVarTy fsk)
co = mkNomReflCo fam_ty
; ev <- newGivenEvVar loc (pred, EvCoercion co)
; return (ev, co, fsk) }
| otherwise -- Generate a [WD] for both Wanted and Derived
......@@ -2817,6 +2828,25 @@ newFlattenSkolem flav loc tc xis
; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
; return (ev, hole_co, fmv) }
----------------------------
unflattenGivens :: IORef InertSet -> TcM ()
-- Unflatten all the fsks created by flattening types in Given
-- constraints We must be sure to do this, else we end up with
-- flatten-skolems buried in any residual Wanteds
--
-- NB: this is the /only/ way that a fsk (MetaDetails = FlatSkolTv)
-- is filled in. Nothing else does so.
--
-- It's here (rather than in TcFlatten) becuause the Right Places
-- to call it are in runTcSWithEvBinds/nestImplicTcS, where it
-- is nicely paired with the creation an empty inert_fsks list.
unflattenGivens inert_var
= do { inerts <- TcM.readTcRef inert_var
; mapM_ flatten_one (inert_fsks inerts) }
where
flatten_one (fsk, ty) = TcM.writeMetaTyVar fsk ty
----------------------------
extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
extendFlatCache tc xi_args stuff@(_, ty, fl)
| isGivenOrWDeriv fl -- Maintain the invariant that inert_flat_cache
......@@ -2832,6 +2862,33 @@ extendFlatCache tc xi_args stuff@(_, ty, fl)
| otherwise
= return ()
----------------------------
unflattenFmv :: TcTyVar -> TcType -> TcS ()
-- Fill a flatten-meta-var, simply by unifying it.
-- This does NOT count as a unification in tcs_unified.
unflattenFmv tv ty
= ASSERT2( isMetaTyVar tv, ppr tv )
TcS $ \ _ ->
do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
; TcM.writeMetaTyVar tv ty }
----------------------------
demoteUnfilledFmv :: TcTyVar -> TcS ()
-- If a flatten-meta-var is still un-filled,
-- turn it into an ordinary meta-var
demoteUnfilledFmv fmv
= wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
; unless is_filled $
do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
; TcM.writeMetaTyVar fmv tv_ty } }
{- *********************************************************************
* *
* Instantaiation etc
* *
********************************************************************* -}
-- Instantiations
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -2845,15 +2902,6 @@ newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
demoteUnfilledFmv :: TcTyVar -> TcS ()
-- If a flatten-meta-var is still un-filled,
-- turn it into an ordinary meta-var
demoteUnfilledFmv fmv
= wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
; unless is_filled $
do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
; TcM.writeMetaTyVar fmv tv_ty } }
instFlexi :: [TKVar] -> TcS TCvSubst
instFlexi = instFlexiX emptyTCvSubst
......
......@@ -615,8 +615,8 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
psig_givens = mkGivens loc psig_theta_vars
; _ <- solveSimpleGivens psig_givens
-- See Note [Add signature contexts as givens]
; solveWanteds wanteds }
; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
; wanteds' <- solveWanteds wanteds
; TcS.zonkWC wanteds' }
-- Find quant_pred_candidates, the predicates that
-- we'll consider quantifying over
......@@ -1953,20 +1953,29 @@ floatEqualities skols no_given_eqs
wanteds@(WC { wc_simple = simples })
| not no_given_eqs -- There are some given equalities, so don't float
= return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
| otherwise
= do { outer_tclvl <- TcS.getTcLevel
= do { -- First zonk: the inert set (from whence they came) are is fully
-- zonked, but unflattening may have filled in unification
-- variables, and we /must/ see them. Otherwise we may float
-- constraints that mention the skolems!
<