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

[Richard Eisenberg]

> Is there a way to somehow convince GHC of that fact so that g typechecks?

No.

First, it would actually be unsound to do so, because of the possibility of exotic types, built with pathological combinations of type and data families: https://gitlab.haskell.org/ghc/ghc/-/issues/14420 <https://gitlab.haskell.org/ghc/ghc/-/issues/14420>

But, actually, the bigger problem is that we need a class constraint in order to allow a function to compute at runtime. The function f actually takes two arguments at runtime: a representation of the instance which carries f's implementation (this is sometimes called a dictionary), and the normal argument of type a. `g`, on the other hand, has no access to the dictionary needed at runtime, and so it's unclear how it should compute.

Put another way: a value of type Foo carries no information (beyond the fact that it terminates), because Foo has only one data constructor. So there's no way that g :: Foo a -> Int could be anything but a constant function. You need the class constraint to change this fact.

Hope this helps!
Richard

> On Mar 2, 2021, at 9:16 AM, Paul Brauner <polux2001 at gmail.com> 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
> 
> 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?
> 
> Cheers,
> Paul
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210302/dae5d46e/attachment.html>