- -- 1. Normalise the *given* *equality* constraints
- ; (given_eqs, eliminate_skolems) <- normaliseGivens given_eqs0
-
- -- 2. Normalise the *given* *dictionary* constraints
- -- wrt. the toplevel and given equations
- ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs
- given_dicts0
-
- -- 3. Solve the *wanted* *equation* constraints
- ; eq_irreds0 <- solveWanteds given_eqs wanted_eqs
-
- -- 4. Normalise the *wanted* equality constraints with respect to
- -- each other
- ; eq_irreds <- normaliseWanteds eq_irreds0
-
- -- 5. Build the Avail mapping from "given_dicts"
- ; init_state <- foldlM addGiven emptyAvails given_dicts
-
- -- 6. Solve the *wanted* *dictionary* constraints
- -- This may expose some further equational constraints...
- ; wanted_dicts' <- zonkInsts wanted_dicts
- ; avails <- reduceList env wanted_dicts' init_state
- ; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts'
- ; traceTc $ text "reduceContext extractresults" <+> vcat
- [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens]
-
- -- 7. Normalise the *wanted* *dictionary* constraints
- -- wrt. the toplevel and given equations
- ; (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
-
- -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
- ; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
-
- -- 9. eliminate the artificial skolem constants introduced in 1.
- ; eliminate_skolems
-
- -- If there was some FD improvement,
- -- or new wanted equations have been exposed,
- -- we should have another go at solving.
- ; let improved = availsImproved avails
- || (not $ isEmptyBag normalise_binds1)
- || (not $ isEmptyBag normalise_binds2)
- || (any isEqInst irreds)
+ -- Normalise and solve all equality constraints as far as possible
+ -- and normalise all dictionary constraints wrt to the reduced
+ -- equalities. The returned wanted constraints include the
+ -- irreducible wanted equalities.
+ ; let wanteds = wanteds0 ++ ancestor_eqs
+ givens = red_givens env
+ ; (givens',
+ wanteds',
+ tybinds,
+ normalise_binds) <- tcReduceEqs givens wanteds
+ ; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat
+ [ppr givens', ppr wanteds', ppr tybinds,
+ ppr normalise_binds]
+
+ -- Build the Avail mapping from "given_dicts"
+ ; (init_state, _) <- getLIE $ do
+ { init_state <- foldlM addGiven emptyAvails givens'
+ ; return init_state
+ }
+
+ -- Solve the *wanted* *dictionary* constraints (not implications)
+ -- 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
+ ; traceTc $ text "reduceContext: extractResults" <+> vcat
+ [ppr avails, ppr wanted_dicts, ppr dict_binds]
+
+ -- Solve the wanted *implications*. In doing so, we can provide
+ -- as "given" all the dicts that were originally given,
+ -- *or* for which we now have bindings,
+ -- *or* which are now irreds
+ -- NB: Equality irreds need to be converted, as the recursive
+ -- invocation of the solver will still treat them as wanteds
+ -- otherwise.
+ ; let implic_env = env { red_givens
+ = givens ++ bound_dicts ++
+ map wantedToLocalEqInst dict_irreds }
+ ; (implic_binds_s, implic_irreds_s)
+ <- mapAndUnzipM (reduceImplication implic_env) wanted_implics
+ ; let implic_binds = unionManyBags implic_binds_s
+ implic_irreds = concat implic_irreds_s
+
+ -- Collect all irreducible instances, and determine whether we should
+ -- go round again. We do so in either of two cases:
+ -- (1) If dictionary reduction or equality solving led to
+ -- improvement (i.e., bindings for type variables).
+ -- (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
+ eq_improved = anyBag (not . isCoVarBind) tybinds
+ improvedFlexible = avails_improved || eq_improved
+ reduced_dicts = not (isEmptyBag dict_binds)
+ improved = improvedFlexible || reduced_dicts
+ --
+ improvedHint = (if avails_improved then " [AVAILS]" else "") ++
+ (if eq_improved then " [EQ]" else "")