-- Simplify 'wanted' as much as possibles
-- Fail if not possible
simplifyDeriv orig tvs theta
- = do { tvs_skols <- tcInstSuperSkolTyVars tvs -- Skolemize
- -- One reason is that the constraint solving machinery
- -- expects *TcTyVars* not TyVars. Another is that
- -- when looking up instances we don't want overlap
- -- of type variables
+ = do { tvs_skols <- tcInstSkolTyVars tvs -- Skolemize
+ -- The constraint solving machinery
+ -- expects *TcTyVars* not TyVars.
+ -- We use *non-overlappable* (vanilla) skolems
+ -- See Note [Overlap and deriving]
; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
; return (substTheta subst_skol min_theta) }
\end{code}
+Note [Overlap and deriving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider some overlapping instances:
+ data Show a => Show [a] where ..
+ data Show [Char] where ...
+
+Now a data type with deriving:
+ data T a = MkT [a] deriving( Show )
+
+We want to get the derived instance
+ instance Show [a] => Show (T a) where...
+and NOT
+ instance Show a => Show (T a) where...
+so that the (Show (T Char)) instance does the Right Thing
+
+It's very like the situation when we're inferring the type
+of a function
+ f x = show [x]
+and we want to infer
+ f :: Show [a] => a -> String
+
+BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
+ the context for the derived instance.
+ Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
+
Note [Exotic derived instance contexts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a 'derived' instance declaration, we *infer* the context. It's a
; (lhs_results, lhs_binds)
<- runTcS SimplRuleLhs untch $
- solveWanteds emptyInert lhs_wanted
+ solveWanteds emptyInert zonked_lhs
; traceTc "simplifyRule" $
vcat [ text "zonked_lhs" <+> ppr zonked_lhs
= do { traceTcS "solveWanteds {" (ppr wanted)
-- Try the flat bit
+ -- Discard from insols all the derived/given constraints
+ -- because they will show up again when we try to solve
+ -- everything else. Solving them a second time is a bit
+ -- of a waste, but the code is simple, and the program is
+ -- wrong anyway!
; let all_flats = flats `unionBags` keepWanted insols
; inert1 <- solveInteractWanted inert (bagToList all_flats)
, text "inert =" <+> ppr inert ]
; let (just_given_inert, unsolved_cans) = extractUnsolved inert
- -- unsolved_ccans contains either Wanted or Derived!
+ -- unsolved_cans contains either Wanted or Derived!
- -- Go inside each implication
; (implic_eqs, unsolved_implics)
- <- solveNestedImplications just_given_inert implics
+ <- solveNestedImplications just_given_inert unsolved_cans implics
-- Apply defaulting rules if and only if there
-- no floated equalities. If there are, they may
unsolved_implics
}
-solveNestedImplications :: InertSet -> Bag Implication
+givensFromWanteds :: CanonicalCts -> Bag FlavoredEvVar
+-- Extract the *wanted* ones from CanonicalCts
+-- and make them into *givens*
+givensFromWanteds = foldrBag getWanted emptyBag
+ where
+ getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
+ getWanted cc givens
+ | not (isCFrozenErr cc)
+ , Wanted loc <- cc_flavor cc
+ , let given = mkEvVarX (cc_id cc) (Given (setCtLocOrigin loc UnkSkol))
+ = given `consBag` givens
+ | otherwise
+ = givens -- We are not helping anyone by pushing a Derived in!
+ -- Because if we could not solve it to start with
+ -- we are not going to do either inside the impl constraint
+
+solveNestedImplications :: InertSet -> CanonicalCts
+ -> Bag Implication
-> TcS (Bag FlavoredEvVar, Bag Implication)
-solveNestedImplications inerts implics
+solveNestedImplications just_given_inert unsolved_cans implics
| isEmptyBag implics
= return (emptyBag, emptyBag)
| otherwise
- = do { -- See Note [Preparing inert set for implications]
- traceTcS "solveWanteds: preparing inerts for implications {" empty
- ; let inert_for_implics = inerts
- -- DV: Used to be:
- -- inert_for_implics <- solveInteract inerts (makeGivens unsolved).
- -- But now the top-level simplifyInfer effectively converts the
- -- quantifiable wanteds to givens, and hence we don't need to add
- -- those unsolved as givens here; they will already be in the inert set.
-
- ; traceTcS "}" empty
-
- ; traceTcS "solveWanteds: doing nested implications {" $
+ = do { -- See Note [Preparing inert set for implications]
+ -- Push the unsolved wanteds inwards, but as givens
+ let pushed_givens = givensFromWanteds unsolved_cans
+ tcs_untouchables = filterVarSet isFlexiTcsTv $
+ tyVarsOfEvVarXs pushed_givens
+ -- See Note [Extra TcsTv untouchables]
+
+ ; traceTcS "solveWanteds: preparing inerts for implications {"
+ (vcat [ppr tcs_untouchables, ppr pushed_givens])
+
+ ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
+
+ ; traceTcS "solveWanteds: } now doing nested implications {" $
vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
, text "implics =" <+> ppr implics ]
- ; let tcs_untouchables = filterVarSet isFlexiTcsTv $
- tyVarsOfInert inert_for_implics
- -- See Note [Extra TcsTv untouchables]
-
; (implic_eqs, unsolved_implics)
<- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
\end{code}
-Note [Float Equalities out of Implications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We want to float equalities out of vanilla existentials, but *not* out
-of GADT pattern matches.
-
Note [Preparing inert set for implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before solving the nested implications, we convert any unsolved flat wanteds
a) In checking mode, suppresses unnecessary errors. We already have
on unsolved-wanted error; adding it to the givens prevents any
- consequential errors from showing uop
+ consequential errors from showing up
b) More importantly, in inference mode, we are going to quantify over this
constraint, and we *don't* want to quantify over any constraints that
are deducible from it.
+ c) Flattened type-family equalities must be exposed to the nested
+ constraints. Consider
+ F b ~ alpha, (forall c. F b ~ alpha)
+ Obviously this is soluble with [alpha := F b]. But the
+ unification is only done by solveCTyFunEqs, right at the end of
+ solveWanteds, and if we aren't careful we'll end up with an
+ unsolved goal inside the implication. We need to "push" the
+ as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
+ can be used to solve the inner (F b
+ ~ alpha). See Trac #4935.
+
+ d) There are other cases where interactions between wanteds that can help
+ to solve a constraint. For example
+
+ class C a b | a -> b
+
+ (C Int alpha), (forall d. C d blah => C Int a)
+
+ If we push the (C Int alpha) inwards, as a given, it can produce
+ a fundep (alpha~a) and this can float out again and be used to
+ fix alpha. (In general we can't float class constraints out just
+ in case (C d blah) might help to solve (C Int a).)
+
The unsolved wanteds are *canonical* but they may not be *inert*,
because when made into a given they might interact with other givens.
Hence the call to solveInteract. Example:
Note [Extra TcsTv untouchables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Furthemore, we record the inert set simplifier-generated unification variables of the TcsTv
-kind (such as variables from instance that have been applied, or unification flattens). These
-variables must be passed to the implications as extra untouchable variables. Otherwise
-we have the danger of double unifications. Example (from trac ticket #4494):
+Furthemore, we record the inert set simplifier-generated unification
+variables of the TcsTv kind (such as variables from instance that have
+been applied, or unification flattens). These variables must be passed
+to the implications as extra untouchable variables. Otherwise we have
+the danger of double unifications. Example (from trac ticket #4494):
(F Int ~ uf) /\ (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
+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 TcsTvs (i.e. the simplifier-generated unification variables)
-that are generated when solving 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.
+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 TcsTvs (i.e. the simplifier-generated
+unification variables) that are generated when solving 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.
+
+NB: A consequence is that every simplifier-generated TcsTv variable
+ that gets floated out of an implication becomes now untouchable
+ next time we go inside that implication to solve any residual
+ constraints. In effect, by floating an equality out of the
+ implication we are committing to have it solved in the outside.
-NB: A consequence is that every simplifier-generated TcsTv variable that gets floated out
- of an implication becomes now untouchable next time we go inside that implication to
- solve any residual constraints. In effect, by floating an equality out of the implication
- we are committing to have it solved in the outside.
+Note [Float Equalities out of Implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want to float equalities out of vanilla existentials, but *not* out
+of GADT pattern matches.
\begin{code}
; return (niFixTvSubst ni_subst, unsolved_can_cts) }
where
- solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setWantedCoBind cv ty
+ solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty
------------
type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])