+\begin{code}
+-----------------------------------------------------------
+-- tcSimplifyInferCheck is used when we know the constraints we are to simplify
+-- against, but we don't know the type variables over which we are going to quantify.
+-- This happens when we have a type signature for a mutually recursive group
+tcSimplifyInferCheck
+ :: InstLoc
+ -> TcTyVarSet -- fv(T)
+ -> [Inst] -- Given
+ -> [Inst] -- Wanted
+ -> TcM ([TyVar], -- Fully zonked, and quantified
+ TcDictBinds) -- Bindings
+
+tcSimplifyInferCheck loc tau_tvs givens wanteds
+ = do { (irreds, binds) <- innerCheckLoop loc givens wanteds
+
+ -- Figure out which type variables to quantify over
+ -- You might think it should just be the signature tyvars,
+ -- but in bizarre cases you can get extra ones
+ -- f :: forall a. Num a => a -> a
+ -- f x = fst (g (x, head [])) + 1
+ -- g a b = (b,a)
+ -- Here we infer g :: forall a b. a -> b -> (b,a)
+ -- We don't want g to be monomorphic in b just because
+ -- f isn't quantified over b.
+ ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
+ ; all_tvs <- zonkTcTyVarsAndFV all_tvs
+ ; gbl_tvs <- tcGetGlobalTyVars
+ ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs)
+ -- We could close gbl_tvs, but its not necessary for
+ -- soundness, and it'll only affect which tyvars, not which
+ -- dictionaries, we quantify over
+
+ ; qtvs' <- zonkQuantifiedTyVars qtvs
+
+ -- Now we are back to normal (c.f. tcSimplCheck)
+ ; implic_bind <- bindIrreds loc qtvs' givens irreds
+
+ ; return (qtvs', binds `unionBags` implic_bind) }
+\end{code}
+