+\begin{code}
+generalise_help doc tau_tvs lie_req sigs
+
+-----------------------
+ | null sigs
+ = -- INFERENCE CASE: Unrestricted group, no type signatures
+ tcSimplifyInfer doc
+ tau_tvs lie_req
+
+-----------------------
+ | otherwise
+ = -- CHECKING CASE: Unrestricted group, there are type signatures
+ -- Check signature contexts are empty
+ checkSigsCtxts sigs `thenTc` \ (sig_avails, sig_dicts) ->
+
+ -- Check that the needed dicts can be
+ -- expressed in terms of the signature ones
+ tcSimplifyInferCheck doc tau_tvs sig_avails lie_req `thenTc` \ (forall_tvs, lie_free, dict_binds) ->
+
+ -- Check that signature type variables are OK
+ checkSigsTyVars sigs `thenTc_`
+
+ returnTc (forall_tvs, lie_free, dict_binds, sig_dicts)
+
+generalise binder_names mbind tau_tvs lie_req sigs
+ | is_unrestricted -- UNRESTRICTED CASE
+ = generalise_help doc tau_tvs lie_req sigs
+
+ | otherwise -- RESTRICTED CASE
+ = -- Do a simplification to decide what type variables
+ -- are constrained. We can't just take the free vars
+ -- of lie_req because that'll have methods that may
+ -- incidentally mention entirely unconstrained variables
+ -- e.g. a call to f :: Eq a => a -> b -> b
+ -- Here, b is unconstrained. A good example would be
+ -- foo = f (3::Int)
+ -- We want to infer the polymorphic type
+ -- foo :: forall b. b -> b
+ generalise_help doc tau_tvs lie_req sigs `thenTc` \ (forall_tvs, lie_free, dict_binds, dict_ids) ->
+
+ -- Check signature contexts are empty
+ checkTc (null sigs || null dict_ids)
+ (restrictedBindCtxtErr binder_names) `thenTc_`
+
+ -- Identify constrained tyvars
+ let
+ constrained_tvs = varSetElems (tyVarsOfTypes (map idType dict_ids))
+ -- The dict_ids are fully zonked
+ final_forall_tvs = forall_tvs `minusList` constrained_tvs
+ in
+
+ -- Now simplify with exactly that set of tyvars
+ -- We have to squash those Methods
+ tcSimplifyRestricted doc final_forall_tvs [] lie_req `thenTc` \ (lie_free, binds) ->
+
+ returnTc (final_forall_tvs, lie_free, binds, [])
+
+ where
+ is_unrestricted | opt_NoMonomorphismRestriction = True
+ | otherwise = isUnRestrictedGroup tysig_names mbind
+
+ tysig_names = [name | (TySigInfo name _ _ _ _ _ _ _) <- sigs]
+
+ doc = ptext SLIT("type signature(s) for") <+> pprBinders binder_names
+
+-----------------------
+ -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE UNIFIABLE
+ -- The type signatures on a mutually-recursive group of definitions
+ -- must all have the same context (or none).
+ --
+ -- We unify them because, with polymorphic recursion, their types
+ -- might not otherwise be related. This is a rather subtle issue.
+ -- ToDo: amplify
+checkSigsCtxts sigs@(TySigInfo _ id1 sig_tvs theta1 _ _ _ _ : other_sigs)
+ = mapTc_ check_one other_sigs `thenTc_`
+ if null theta1 then
+ returnTc ([], []) -- Non-overloaded type signatures
+ else
+ newDicts SignatureOrigin theta1 `thenNF_Tc` \ sig_dicts ->
+ let
+ -- The "sig_avails" is the stuff available. We get that from
+ -- the context of the type signature, BUT ALSO the lie_avail
+ -- so that polymorphic recursion works right (see comments at end of fn)
+ sig_avails = sig_dicts ++ sig_meths
+ in
+ returnTc (sig_avails, map instToId sig_dicts)
+ where
+ sig1_dict_tys = map mkPredTy theta1
+ n_sig1_theta = length theta1
+ sig_meths = concat [insts | TySigInfo _ _ _ _ _ _ insts _ <- sigs]
+
+ check_one sig@(TySigInfo _ id _ theta _ _ _ src_loc)
+ = tcAddSrcLoc src_loc $
+ tcAddErrCtxt (sigContextsCtxt id1 id) $
+ checkTc (length theta == n_sig1_theta) sigContextsErr `thenTc_`
+ unifyTauTyLists sig1_dict_tys (map mkPredTy theta)
+
+checkSigsTyVars sigs = mapTc_ check_one sigs
+ where
+ check_one (TySigInfo _ id sig_tyvars sig_theta sig_tau _ _ src_loc)
+ = tcAddSrcLoc src_loc $
+ tcAddErrCtxtM (sigCtxt (sig_msg id) sig_tyvars sig_theta sig_tau) $
+ checkSigTyVars sig_tyvars (idFreeTyVars id)
+
+ sig_msg id = ptext SLIT("When checking the type signature for") <+> quotes (ppr id)
+\end{code}
+