## Eq documentation: substitutivity

## Summary

On the customary properties expected from `Eq`

, you can read:

Substitutivity: if x == y = True and f is a "public" function whose return type is an instance of Eq, then f x == f y = True

A "public" function is described as:

However, == is customarily expected to implement an equivalence relationship where two values comparing equal are indistinguishable by "public" functions, with a "public" function being one not allowing to see implementation details. For example, for a type representing non-normalised natural numbers modulo 100, a "public" function doesn't make the difference between 1 and 201.

Two things:

- I thought — but am not sure — this property is called «extensionality» (or maybe «function extensionality»)?
- I am not sure I understood what a public function is and moreover Haskell function are opaque, so the distinction seems not practically useful?

## Proposed improvements or changes

Reword the second paragraph as

The Haskell Report defines no laws for Eq. However, it is expected to have the following properties:

and "Substitutivity" as

Extensionality: if x == y = True and f is a function whose return type is an instance of Eq, then f x == f y = True

I can provide a patch if everyone agrees these changes are sensible.