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

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 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.