Typing rule for binding groups In "Typing Haskell in Haskell", by Mark P. Jones, is provided a sort of haskell-like specification for typing Haskell. As stated in this paper, binding groups is a area "neglected in most theoretical treatments of type inference". Jones provided inference and checking algorithms for this syntactic construct, but it's typing rule is not referenced.

As far I know, binding groups is quite differente from usual let bindings.
You can have mutual recursion, for example. Also, I don't know if is possible to simulate binding groups only using let expressions.

There is a typing rule for typing binding groups anywhere in the literature?
If there is, then maybe the rest of this question is pointless.

This paper also doesn't give us a (in)formal grammar for the syntax, because it's goal is type inference/checking from the data stucture itself. I don't think this is strictly necessary, but a syntactic definition of binding groups may help defining a typing rule. So, I decided to give a sugestion of what this informal grammar may look like. Brackets means finite sequence and curly bracket means no-empty finite sequence.



So, what I'm asking here is a rule for typing binding groups.

EDIT:

It seems that my question is not clear enough. I apologize for that. I'll try to make it more clear...

By typing rule (or type rule) I mean: en.wikipedia.org/wiki/Type_rule and by type checking algorithm I mean something easy to translate to code. I think the difference is more fundamental than just representation style. A rule is closer to a relation and an algorithm is closer to a function. What is missing is a rule, like in the wikipedia page, that could be used for certification of the algorithm.

Certification is the motivation behind my question. I want to certify the algorithms described in this paper.
I don't know what rule Jones intended to use, but I'd guess it's something like

$$
\dfrac{
\Gamma' = \Gamma,x_1:\tau_1,\ldots,x_n:\tau_n
\\
\Gamma' \vdash e_1 : \tau_1
\\
\cdots
\\
\Gamma' \vdash e_n : \tau_n
\\
\Gamma' \vdash e : \tau
}{
\Gamma \vdash {\sf let}\ x_1=e_1;\cdots;x_n=e_n\ {\sf in}\ e : \tau
}
$$

which handles mutual recursion in groups. The rule above does not consider patterns as in x [p] = e, but it could be amended to support those as well.

I think binding groups are usually neglected since mutual recursion can be translated into non-mutual one (e.g. exploiting Bekić's theorem). However, in a real-world language it's convenient to have mutual recursion, even if from a purely theoretical point it's redundant. Hence, having a typing rule for it and an inference algorithm is still quite useful.