Clarify laws of 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.

0 files changed, 0 insertions, 0 deletions