[Haskell-cafe] data kinds and exhaustiveness of typeclass instances

[Paul Brauner]

Hello,

the following program doesn't typecheck in GHC 9:

data Tag = A | B
data Foo (a :: Tag) = Foo

class C a where
  f :: a -> Int

instance C (Foo A) where
  f x = 1

instance C (Foo B) where
  f x = 2

g :: Foo a -> Int
g = f

Yet one could argue that for all a :: Tag, C (Foo a) holds because a :: Tag
can only take two values: A or B, and C (Foo A) and C (Foo B) hold. Is
there a way to somehow convince GHC of that fact so that g typechecks?

Cheers,
Paul
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210302/a9fc50aa/attachment.html>