On Tue, Mar 02, 2021 at 03:00:55PM +0000, Richard Eisenberg wrote:

...

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

To elaborate a little on Richard’s answer, this is the reason for GHC.TypeLits’ KnownNat class, so that we have natVal :: KnownNat n => proxy n -> Integer You’d have to supplement your program with a class KnownTag, like so: data Tag = A | B data Foo (a :: Tag) = Foo class KnownTag (a :: Tag) where tagVal :: proxy a -> Tag instance KnownTag A where tagVal _ = A instance KnownTag B where tagVal _ = B class C a where f :: a -> Int instance KnownTag a => C (Foo a) where f _ = case tagVal (Proxy :: Proxy a) of A -> 1; B -> 2 g :: KnownTag a => Foo a -> Int g = f Regards, Seph -- Seph Shewell Brockway, BSc MSc (Glas.) Pronouns: she/her

Another way of putting it, please correct me if I'm wrong. In coq we could prove forall a, C (Foo a) by case analysis on a. Then we could use that proof to recover the f by applying it to p inside g. It can't work in Haskell because p has no runtime representation. In Haskell the proxy plays the role of p, KnownTag plays the role of the proof that p can be eliminated, and "instance KnownTag a => C (Foo a)" plays the role of the theorem. On Tue, Mar 2, 2021 at 8:23 PM Paul Brauner wrote:

Thanks all, this all makes sense!

On Tue, Mar 2, 2021 at 4:34 PM Seph Shewell Brockway wrote:

...

...

...

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

On Tue, Mar 02, 2021 at 03:00:55PM +0000, Richard Eisenberg wrote: 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

To elaborate a little on Richard’s answer, this is the reason for GHC.TypeLits’ KnownNat class, so that we have

natVal :: KnownNat n => proxy n -> Integer

You’d have to supplement your program with a class KnownTag, like so:

data Tag = A | B data Foo (a :: Tag) = Foo

class KnownTag (a :: Tag) where tagVal :: proxy a -> Tag

instance KnownTag A where tagVal _ = A

instance KnownTag B where tagVal _ = B

class C a where f :: a -> Int

instance KnownTag a => C (Foo a) where f _ = case tagVal (Proxy :: Proxy a) of A -> 1; B -> 2

g :: KnownTag a => Foo a -> Int g = f

Regards,

Seph

-- Seph Shewell Brockway, BSc MSc (Glas.) Pronouns: she/her