tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
-- Zonk everything in sight
= do { traceTc (text "tcSimplifyRestricted")
- ; wanteds' <- zonkInsts wanteds
+ ; wanteds_z <- zonkInsts wanteds
-- 'ReduceMe': Reduce as far as we can. Don't stop at
-- dicts; the idea is to get rid of as many type
-- HOWEVER, some unification may take place, if we instantiate
-- a method Inst with an equality constraint
; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe)
- ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
+ ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds_z
-- Next, figure out the tyvars we will quantify over
; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
ppr _binds,
ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
+ -- Zonk wanteds again! The first call to reduceContext may have
+ -- instantiated some variables.
+ -- FIXME: If red_improve would work, we could propagate that into
+ -- the equality solver, too, to prevent instantating any
+ -- variables.
+ ; wanteds_zz <- zonkInsts wanteds_z
+
-- The first step may have squashed more methods than
-- necessary, so try again, this time more gently, knowing the exact
-- set of type variables to quantify over.
(is_nested_group || isDict inst) = Stop
| otherwise = ReduceMe
env = mkNoImproveRedEnv doc try_me
- ; (_imp, binds, irreds) <- reduceContext env wanteds'
+ ; (_imp, binds, irreds) <- reduceContext env wanteds_zz
-- See "Notes on implicit parameters, Question 4: top level"
; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
; let env = mkRedEnv doc try_me given_ips'
; (improved, binds, irreds) <- reduceContext env wanteds'
- ; if not improved then
+ ; if null irreds || not improved then
ASSERT( all is_free irreds )
do { extendLIEs irreds
; return binds }
- else
- tcSimplifyIPs given_ips wanteds }
+ else do
+ -- If improvement did some unification, we go round again.
+ -- We start again with irreds, not wanteds
+ -- Using an instance decl might have introduced a fresh type
+ -- variable which might have been unified, so we'd get an
+ -- infinite loop if we started again with wanteds!
+ -- See Note [LOOP]
+ { binds1 <- tcSimplifyIPs given_ips' irreds
+ ; return $ binds `unionBags` binds1
+ } }
where
doc = text "tcSimplifyIPs" <+> ppr given_ips
ip_set = mkNameSet (ipNamesOfInsts given_ips)
}
-- Solve the *wanted* *dictionary* constraints (not implications)
- -- This may expose some further equational constraints...
+ -- This may expose some further equational constraints in the course
+ -- of improvement due to functional dependencies if any of the
+ -- involved unifications gets deferred.
; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'
; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+ -- The getLIE is reqd because reduceList does improvement
+ -- (via extendAvails) which may in turn do unification
; (dict_binds,
bound_dicts,
dict_irreds) <- extractResults avails wanted_dicts
-- go round again. We do so in either of two cases:
-- (1) If dictionary reduction or equality solving led to
-- improvement (i.e., instantiated type variables).
- -- (2) If we uncovered extra equalities. We will try to solve them
- -- in the next iteration.
+ -- (2) If we reduced dictionaries (i.e., got dictionary bindings),
+ -- they may have exposed further opportunities to normalise
+ -- family applications. See Note [Dictionary Improvement]
+ --
+ -- NB: We do *not* go around for new extra_eqs. Morally, we should,
+ -- but we can't without risking non-termination (see #2688). By
+ -- not going around, we miss some legal programs mixing FDs and
+ -- TFs, but we never claimed to support such programs in the
+ -- current implementation anyway.
; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs
avails_improved = availsImproved avails
improvedFlexible = avails_improved || eq_improved
- extraEqs = (not . null) extra_eqs
- improved = improvedFlexible || extraEqs
+ reduced_dicts = not (isEmptyBag dict_binds)
+ improved = improvedFlexible || reduced_dicts
--
improvedHint = (if avails_improved then " [AVAILS]" else "") ++
- (if eq_improved then " [EQ]" else "") ++
- (if extraEqs then " [EXTRA EQS]" else "")
+ (if eq_improved then " [EQ]" else "")
; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
; return (tidy_env, msg) }
\end{code}
+Note [Dictionary Improvement]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In reduceContext, we first reduce equalities and then class constraints.
+However, the letter may expose further opportunities for the former. Hence,
+we need to go around again if dictionary reduction produced any dictionary
+bindings. The following example demonstrated the point:
+
+ data EX _x _y (p :: * -> *)
+ data ANY
+
+ class Base p
+
+ class Base (Def p) => Prop p where
+ type Def p
+
+ instance Base ()
+ instance Prop () where
+ type Def () = ()
+
+ instance (Base (Def (p ANY))) => Base (EX _x _y p)
+ instance (Prop (p ANY)) => Prop (EX _x _y p) where
+ type Def (EX _x _y p) = EX _x _y p
+
+ data FOO x
+ instance Prop (FOO x) where
+ type Def (FOO x) = ()
+
+ data BAR
+ instance Prop BAR where
+ type Def BAR = EX () () FOO
+
+During checking the last instance declaration, we need to check the superclass
+cosntraint Base (Def BAR), which family normalisation reduced to
+Base (EX () () FOO). Chasing the instance for Base (EX _x _y p), gives us
+Base (Def (FOO ANY)), which again requires family normalisation of Def to
+Base () before we can finish.
+
+
The main context-reduction function is @reduce@. Here's its game plan.
\begin{code}
projects / ghc-hetmet.git / blobdiff