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