Type class for sanity

[David Feuer]

Since type families can be stuck, it's sometimes useful to restrict
things to sane types. At present, the most convenient way I can see to
do this in general is with Typeable:

type family Foo x where
  Foo 'True = Int

class Typeable (Foo x) => Bar x where
  blah :: proxy x -> Foo x

This will prevent anyone from producing the bogus instance

instance Bar 'False where
  blah _ = undefined

Unfortunately, the Typeable constraint carries runtime overhead. One
possible way around this, I think, is with a class that does just
sanity checking and nothing more:

class Sane (a :: k)
instance Sane Int
instance Sane Char
instance Sane 'False
instance Sane 'True
instance Sane '[]
instance Sane '(:)
instance Sane (->)
instance Sane 'Just
instance Sane 'Nothing
instance (Sane f, Sane x) => Sane (f x)

To really do its job properly, Sane would need to have instances for
all sane types and no more. An example of an insane instance of Sane
would be

instance Sane (a :: MyKind)

which would include stuck types of kind MyKind.

Would it be useful to add such an automatic-only class to GHC?

David