Clarify laws of `TestCoercion`wip/clarify-test-coercion

- Add law to `TestCoercion` to match `TestEquality`

- Remove recommendation for singleton types because of uncertainty
  whether this is a good recommendation.

- Discuss the singleton type quandary under an [expandable
  heading](https://haskell-haddock.readthedocs.io/en/latest/markup.html?highlight=expandable#headings)
  for anyone that is curious, without cluttering the main documentation.

Follow up from a5ea78673eae7c837a5ccb7882e908a4df92e75d.

1 files changed, 58 insertions, 3 deletions

diff --git a/libraries/base/Data/Type/Coercion.hs b/libraries/base/Data/Type/Coercion.hs
index 618d506d64..c40ca5b3c9 100644
--- a/libraries/base/Data/Type/Coercion.hs
+++ b/libraries/base/Data/Type/Coercion.hs
@@ -97,9 +97,64 @@ instance Coercible a b => Enum (Coercion a b) where
 -- | @since 4.7.0.0
 deriving instance Coercible a b => Bounded (Coercion 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.
+-- | This class contains types where you can learn the coercibility of two
+-- types from information contained in /terms/.
+--
+-- The result should be @Just Coercion@ if and only if the types applied to @f@
+-- are coercible:
+--
+-- @testCoercion (x :: f a) (y :: f b) = Just Coercion@ ⟺ Coercible a b@
+--
+-- === __Guidance on use with singleton types__
+--
+-- It was previously recommend that only singleton types should inhabit this
+-- class. However, it is unclear what the singleton types should represent.
+--
+-- Normally, a singleton type has one value per *type*: types quotiented by
+-- nominal equivalence, i.e. just types.
+--
+-- An example of this would be:
+--
+-- @
+--     data Nom0 :: Type -> Type where
+--       Nom0Int  :: Nom0 Int
+--       Nom0Bool :: Nom0 Bool
+-- @
+--
+-- Which, to make relationship to the next part more clear, let's rewrite more
+-- verbosely as:
+--
+-- @
+--     data Nom1 :: Type -> Type where
+--       Nom1Int  :: forall a. a ~ Int  => Nom1 a
+--       Nom1Bool :: forall a. a ~ Bool => Nom1 a
+-- @
+--
+-- But arguably, given that we are testing for coercibility, it would be better
+-- to have one value per *representation*: types quotiented by representational
+-- equivalence, i.e. equivalence classes of types that are
+-- pairwise-'Coercible'.
+--
+-- An example of this would be:
+--
+-- @
+--     data Rep :: Type -> Type where
+--       RepInt  :: forall a. a `Coercible` Int  => Rep a
+--       RepBool :: forall a. a `Coercible` Bool => Rep a
+-- @
+--
+-- The goal of this would be to have laws similar to that for 'TestEquality'
+-- when used with singletons:
+--
+-- @testCoercion (x :: f a) (y :: f b) = Just Refl ⟺ a `Coercible` b ⟺ coerce x = coerce y@
+--
+-- @isJust (testCoercion x y) = coerce x == coerce y@
+--
+-- However, GHC today thinks the argument to 'Rep' must have a nominal role,
+-- and therefore the above doesn't work.
+--
+-- Regardless, singleton types are not required, however, and so the latter
+-- would-be laws are not in fact valid in general.
 class TestCoercion f where
   -- | Conditionally prove the representational equality of @a@ and @b@.
   testCoercion :: f a -> f b -> Maybe (Coercion a b)