Capturing typeclass dictionaries

Question

Below is code that will happily compile (once adding the constraints package). Foo1 and Foo2 are two alternate definitions of Foo, which I can write f1 and f2 sensibly for.

However, I think Foo3 is reasonable as well. Yet I don't know how to write f3. It seems to me that Haskell should store a pointer to the typeclass dictionary inside the Foo3 constructor, for whatever a is passed when Foo3 is created, so then I should be able to just call silly. Since silly just returns String, it doesn't matter if a has been erased by now, I should be able to happily call the silly pointed to by the dictionary stored in the constructor Foo3.

Is my reasoning right? And if so, how can I write f3. Alternative, have I missed something and is there a good reason why I need either Dict or Proxy here because without them I haven't got enough information?

{-# LANGUAGE ScopedTypeVariables #-}

import Data.Constraint (Dict(Dict), withDict)
import Data.Proxy (Proxy)

data Alice

class C a where
    silly :: String

instance C Alice where
    silly = "Silly Alice"

data Foo1 where
    Foo1 :: Dict (C a) -> Foo1

f1 :: Foo1 -> String
f1 (Foo1 (dict :: Dict (C a))) = withDict dict $ silly @a

data Foo2 where
    Foo2 :: C a => Proxy a -> Foo2

f2 :: Foo2 -> String
f2 (Foo2 (_ :: Proxy a)) = silly @a

data Foo3 where 
    Foo3 :: C a => Foo3

mkFoo3 :: forall a. C a => Foo3
mkFoo3 = Foo3 @a 

f3 :: Foo3 -> String
f3 = undefined

Answer 1

With sufficient extensions turned on, and a sufficiently new GHC (9.2 seems to be new enough here, and maybe slightly older ones will work as well), the following works:

f3 (Foo3 @_ @a) = silly @a

What's that @_, you ask? There's an implicit kind argument, the kind of a, that we want to ignore. Alternately, you can use the NoPolyKinds extension and drop the @_.