<div dir="ltr">Hello,<div><br></div><div>the following program doesn't typecheck in GHC 9:</div><div><br></div><div><font face="monospace">data Tag = A | B<br>data Foo (a :: Tag) = Foo<br><br>class C a where<br>  f :: a -> Int<br><br>instance C (Foo A) where<br>  f x = 1<br><br>instance C (Foo B) where<br>  f x = 2<br><br>g :: Foo a -> Int<br>g = f</font><br></div><div><font face="monospace"><br></font></div><div>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?</div><div><br></div><div>Cheers,</div><div>Paul</div></div>