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

Paul Brauner polux2001 at gmail.com
Tue Mar 2 14:16:23 UTC 2021


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?

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

More information about the Haskell-Cafe mailing list