> Is there a way to somehow convince GHC of that fact so that g typechecks?
No.
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
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-cafeOnly members subscribed via the mailman list are allowed to post.