+ ; -- 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
+
+-- -- Do the real work
+-- -- Process non-implication constraints first, so that they are
+-- -- available to help solving the implication constraints
+-- -- ToDo: seems a bit inefficient and ad-hoc
+-- ; let (implics, rest) = partition isImplicInst wanteds
+-- ; avails <- reduceList env (rest ++ implics) init_state
+
+ -- 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)
+ || (not $ null $ fst $ partitionGivenEqInsts irreds)