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