GHC TypeLits without values

Question

Trying to design a type-driven API, I've been trying to get something like the following working (using much more complicated code/attempts, this is stripped down to the minimum required to clarify what I'm looking for): ``` {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} module Main where import Data.Proxy import GHC.TypeLits type Printer (s :: Symbol) = IO () concrete :: Printer "foo" concrete = generic generic :: KnownSymbol s => Printer s generic = putStrLn (symbolVal (Proxy :: Proxy s)) main :: IO () main = concrete ``` This program would print 'foo', but doesn't: ``` Could not deduce (KnownSymbol s0) arising from the ambiguity check for ‘generic’ from the context (KnownSymbol s) bound by the type signature for generic :: KnownSymbol s => Printer s at test5.hs:14:12-37 The type variable ‘s0’ is ambiguous In the ambiguity check for: forall (s :: Symbol). KnownSymbol s => Printer s To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signatur…

Accepted Answer

Type synonyms (defined with `type`) are replaced with their definition during typechecking. The problem is that `Printer` has no reference to `s` in its definition, which leads to the following constraint:

```
generic :: KnonwSymbol s => IO ()
```

This type signature does not have an `s` right of the `=>` and so fails the ambiguity check. It can't really work because there's nowhere to specify what `s` should be when you use it.

Unfortunately, GHC is inconsistent about how it represents type synonyms in error messages. Sometimes they are expanded and sometimes they are preserved. Ironically, I think improvements in the error messages have made this particular error harder to track down: normally, expressing the error in terms of the types you defined is clearer, but here it hides the cause of the ambiguity.

What you need is some way to supply the relevant type-level symbol that does not rely on type synonyms. But first, you need to enable `ScopedTypeVariables` and add a `forall` to the signature of `generic` to make sure the `s` in the type signature and the `s` in `Proxy :: Proxy s` are the same.

There are two possibilities:

change `Printer` to a `newtype` and unwrap it when you use it:

```
newtype Printer (s :: Symbol) = Printer { runPrinter :: IO () }

generic :: forall s. KnownSymbol s => Printer s
generic = Printer $ putStrLn (symbolVal (Proxy :: Proxy s))

main = runPrinter generic
```

pass in an extra `Proxy` argument to `generic`, just like `symbolVal`:

```
concrete :: Printer "foo"
concrete = generic (Proxy :: Proxy "foo")

generic :: forall proxy s. KnownSymbol s => proxy s -> IO ()
generic _ = putStrLn (symbolVal (Proxy :: Proxy s))
```

Having `proxy` as a type variable is a neat idiom that lets you not depend on `Data.Proxy` and lets callers pass in whatever they want in its stead.

GHC TypeLits without values

Solution

Problem