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

[Henning Thielemann]

On Tue, 2 Mar 2021, Paul Brauner wrote:

> 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


You need a typecase on Tag's constructors. E.g.

class C a where switch :: f A -> f B -> f a
instance C A where switch h _ = h
instance C B where switch _ h = h

newtype G a = G {getG :: Foo a -> Int}

g :: (C a) => Foo a -> Int
g = getG $ switch (G f) (G f)



Or you define a helper GADT:

data Choice a where
   A :: Choice A
   B :: Choice B

class C a where choice :: Choice a
instance C A where choice = A
instance C B where choice = B

choiceFromFoo :: (C a) => Foo a -> Choice a
choiceFromFoo Foo = choice

g :: (C a) => Foo a -> Int
g foo =
   case choiceFromFoo foo of
     A -> f foo
     B -> f foo