Clarify laws of TestEqualitywip/clarify-TestEquality

It is unclear what `TestEquality` is for. There are 3 possible choices.

Assuming

```haskell
data Tag a where
    TagInt1 :: Tag Int
    TagInt2 :: Tag Int
```

Weakest -- type param equality semi-decidable
---------------------------------------------

`Just Refl` merely means the type params are equal, the values being compared might not be.
`Nothing` means the type params may or may not be not equal.

```haskell
instance TestEquality Tag where
    testEquality TagInt1 TagInt1 = Nothing -- oopsie is allowed
    testEquality TagInt1 TagInt2 = Just Refl
    testEquality TagInt2 TagInt1 = Just Refl
    testEquality TagInt2 TagInt2 = Just Refl
```

This option is better demonstrated with a different type:
```haskell
data Tag' a where
    TagInt1 :: Tag Int
    TagInt2 :: Tag a
```
```haskell
instance TestEquality Tag' where
    testEquality TagInt1 TagInt1 = Just Refl
    testEquality TagInt1 TagInt2 = Nothing -- can't be sure
    testEquality TagInt2 TagInt1 = Nothing -- can't be sure
    testEquality TagInt2 TagInt2 = Nothing -- can't be sure
```

Weaker -- type param equality decidable
---------------------------------------

`Just Refl` merely means the type params are equal, the values being compared might not be.
`Nothing` means the type params are not equal.

```haskell
instance TestEquality Tag where
    testEquality TagInt1 TagInt1 = Just Refl
    testEquality TagInt1 TagInt2 = Just Refl
    testEquality TagInt2 TagInt1 = Just Refl
    testEquality TagInt2 TagInt2 = Just Refl
```

Strong -- Like `Eq`
-------------------

`Just Refl` means the type params are equal, and the values are equal according to `Eq`.

```haskell
instance TestEquality Tag where
    testEquality TagInt1 TagInt1 = Just Refl
    testEquality TagInt2 TagInt2 = Just Refl
    testEquality _ _ = Nothing
```

Strongest -- unique value concrete type
---------------------------------------

`Just Refl` means the type params are equal, and the values are equal, and the class assume if the type params are equal the values must also be equal. In other words, the type is a singleton type when the type parameter is a closed term.

```haskell
-- instance TestEquality -- invalid instance because two variants for `Int`
```
------

The discussion in
https://github.com/haskell/core-libraries-committee/issues/21 has
decided on the "Weaker" option (confusingly formerly called the
"Weakest" option). So that is what is implemented.

1 files changed, 16 insertions, 2 deletions

diff --git a/libraries/base/Data/Type/Equality.hs b/libraries/base/Data/Type/Equality.hs
index de7deb3da2..36737ff5b7 100644
--- a/libraries/base/Data/Type/Equality.hs
+++ b/libraries/base/Data/Type/Equality.hs
@@ -145,8 +145,22 @@ instance a ~~ b => Enum (a :~~: b) where
 deriving instance a ~~ b => Bounded (a :~~: b)
 
 -- | This class contains types where you can learn the equality of two types
--- from information contained in /terms/. Typically, only singleton types should
--- inhabit this class.
+-- from information contained in /terms/.
+--
+-- The result should be @Just Refl@ if and only if the types applied to @f@ are
+-- equal:
+--
+-- @TestEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b@
+--
+-- Typically, only singleton types should inhabit this class. In that case type
+-- argument equality coincides with term equality:
+--
+-- @TestEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y@
+--
+-- @isJust (TestEquality x y) = x == y@
+--
+-- Singleton types are not required, however, and so the latter two would-be
+-- laws are not in fact valid in general.
 class TestEquality f where
   -- | Conditionally prove the equality of @a@ and @b@.
   testEquality :: f a -> f b -> Maybe (a :~: b)