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.
TestCoercion documentation includes a similar caution about singleton types. But this is far too conservative! Length-indexed vectors can be made valid instances of
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.