[m-rev.] for post-commit review: check for terms containing distinct vars in one place

[Peter Wang]

On Sun, 21 Apr 2024 19:44:31 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> For review by anyone. I am particularly seeking feedback
> on the issue noted by a new XXX in the reference manual.
> 
> Zoltan.

> diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> index e436183cf..552f5c0ff 100644
> --- a/doc/reference_manual.texi
> +++ b/doc/reference_manual.texi
> @@ -7747,7 +7747,7 @@ Type class constraints may include any number of functional dependencies.
>  A @dfn{functional dependency} constraint
>  takes the form @code{(@var{Domain} -> @var{Range})}.
>  The @var{Domain} and @var{Range} arguments are either single type variables,
> -or conjunctions of type variables separated by commas.
> +or conjunctions of distinct type variables separated by commas.
>  
>  @example
>  	:- typeclass @var{Typeclass}(@var{Var}, @dots{})@
> @@ -7828,6 +7828,12 @@ However, variables which are in the range of a functional dependency
>  need not appear in the signature,
>  since it is known that their bindings will be determined
>  from the bindings of the variables in the domain.
> + at c XXX What about a class with two fundeps: A -> B, and B -> A.
> + at c Both A and B are in the range of a fundep.
> + at c The above text seems to imply that it is ok for *neither* to appear
> + at c in the signature.
> + at c Should we replace "since it is known that their bindings will be determined"
> + at c with "provided that their bindings are determined"?
>  

How about:

    Without any functional dependencies, all variables in constraints
    must appear in the signature of the predicate or function being
    declared.
    However, a variable [that appears] in the range of a functional
    dependency does not need appear in the signature *if* the variables
    in the domain of that functional dependency do appear in the
    signature.

Peter