2 Mar
2021
2 Mar
'21
2:41 p.m.
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?