<div dir="ltr">Thanks all, this all makes sense!</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Mar 2, 2021 at 4:34 PM Seph Shewell Brockway <seph@codex.scot> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Tue, Mar 02, 2021 at 03:00:55PM +0000, Richard Eisenberg wrote:<br>
> > Is there a way to somehow convince GHC of that fact so that g typechecks?<br>
> <br>
> No.<br>
> <br>
> 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: <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/14420" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/issues/14420</a> <<a href="https://gitlab.haskell.org/ghc/ghc/-/issues/14420" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/issues/14420</a>><br>
> <br>
> 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.<br>
> <br>
> 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.<br>
> <br>
> Hope this helps!<br>
> Richard<br>
<br>
To elaborate a little on Richard’s answer, this is the reason for<br>
GHC.TypeLits’ KnownNat class, so that we have<br>
<br>
natVal :: KnownNat n => proxy n -> Integer<br>
<br>
You’d have to supplement your program with a class KnownTag, like so:<br>
<br>
data Tag = A | B<br>
data Foo (a :: Tag) = Foo<br>
<br>
class KnownTag (a :: Tag) where<br>
  tagVal :: proxy a -> Tag<br>
<br>
instance KnownTag A where<br>
  tagVal _ = A<br>
<br>
instance KnownTag B where<br>
  tagVal _ = B<br>
<br>
class C a where<br>
  f :: a -> Int<br>
<br>
instance KnownTag a => C (Foo a) where<br>
  f _ = case tagVal (Proxy :: Proxy a) of A -> 1; B -> 2<br>
<br>
g :: KnownTag a => Foo a -> Int<br>
g = f<br>
<br>
                                             Regards,<br>
<br>
                                             Seph<br>
<br>
-- <br>
Seph Shewell Brockway, BSc MSc (Glas.)<br>
Pronouns: she/her<br>
</blockquote></div>