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

[Tom Ellis]

On Tue, Mar 02, 2021 at 03:16:23PM +0100, Paul Brauner wrote:
> 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?

What would you expect the type of 'g Foo' to be?