TestEquality and TestCoercion documentation is confusing

Currently, the documentation for the TestEquality class indicates

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.

The TestCoercion documentation includes a similar caution about singleton types. But this is far too conservative! Length-indexed vectors can be made valid instances of TestEquality and TestCoercion in exactly one way:

data Nat = Z | S Nat

data Vec a n where
  Nil :: Vec a 'Z
  Cons :: a -> Vec a n -> Vec a ('S n)

instance TestEquality (Vec a) where
  testEquality Nil Nil = Just Refl
  testEquality (Cons _ xs) (Cons _ ys) =
                           fmap (\Refl -> Refl) (testEquality xs ys)
  testEquality _ _ = Nothing

instance TestCoercion (Vec a) where
  testCoercion xs ys = fmap (\Refl -> Coercion) (testEquality xs ys)

Polykinded heterogeneous lists are another nice non-singleton example for which each class has a single "most reasonable" instance:

data HList (f :: k -> *) (xs :: [k]) where
  HNil :: HList f '[]
  HCons :: f a -> HList f as -> HList f (a ': as)

instance TestEquality f => TestEquality (HList f) where
  testEquality HNil HNil = Just Refl
  testEquality (HCons x xs) (HCons y ys) = do
    Refl <- testEquality x y
    Refl <- testEquality xs ys
    Just Refl
  testEquality _ _ = Nothing

instance TestCoercion f => TestCoercion (HList f) where
  testCoercion HNil HNil = Just Coercion
  testCoercion (HCons x xs) (HCons y ys) = do
    Coercion <- testCoercion x y
    Coercion <- testCoercion xs ys
    Just Coercion
  testCoercion _ _ = Nothing

I don't know just how far the warning should be weakened; it may make sense to go as far as saying the type should generally be a GADT.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Core Libraries
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	ekmett
Operating system
Architecture