+ red_env = mkRedEnv doc try_me []
+ ; (irreds1, binds1) <- checkLoop red_env bound
+
+ -- Note [Inference and implication constraints]
+ -- By putting extra_dicts first, we make them available
+ -- to solve the implication constraints
+ ; let extra_dicts = getImplicWanteds qtvs irreds1
+ ; (irreds2, binds2) <- if null extra_dicts
+ then return (irreds1, emptyBag)
+ else do { extra_dicts' <- mapM cloneDict extra_dicts
+ ; checkLoop red_env (extra_dicts' ++ irreds1) }
+
+ -- By now improvment may have taken place, and we must *not*
+ -- quantify over any variable free in the environment
+ -- tc137 (function h inside g) is an example
+ ; gbl_tvs <- tcGetGlobalTyVars
+ ; qtvs1 <- zonkTcTyVarsAndFV (varSetElems qtvs)
+ ; qtvs2 <- zonkQuantifiedTyVars (varSetElems (qtvs1 `minusVarSet` gbl_tvs))
+
+ -- Do not quantify over constraints that *now* do not
+ -- mention quantified type variables, because they are
+ -- simply ambiguous (or might be bound further out). Example:
+ -- f :: Eq b => a -> (a, b)
+ -- g x = fst (f x)
+ -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
+ -- We decide to quantify over 'alpha' alone, but free1 does not include f77
+ -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
+ -- constraint (Eq beta), which we dump back into the free set
+ -- See test tcfail181
+ ; let (free3, irreds3) = partition (isFreeWhenInferring (mkVarSet qtvs2)) irreds2
+ ; extendLIEs free3
+
+ -- We can't abstract over any remaining unsolved
+ -- implications so instead just float them outwards. Ugh.
+ ; let (q_dicts, implics) = partition isDict irreds3