#12421: TestEquality and TestCoercion documentation is confusing -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Core | Version: 8.0.1 Libraries | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Documentation Unknown/Multiple | bug Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12421 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler