GHC TypeLits without values

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 signature for ‘generic’:
  generic :: KnownSymbol s => Printer s

Enabling AllowAmbiguousTypes doesn't really help. Any way to get this working anyway?

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:

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

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

main = runPrinter generic

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

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

This is wrong:

generic :: KnownSymbol s => Printer s
generic = ...(Proxy :: Proxy s)

The last s has nothing to do with the s above it. It is locally implicitly universally quantified, as in top-level type annotations. The code actually means

generic :: KnownSymbol s => Printer s
generic = ...(Proxy :: forall z. Proxy z)

To fix the above, enable ScopedTypeVariables and use

-- the explicit forall makes s available below
generic :: forall s. KnownSymbol s => Printer s
generic = ...(Proxy :: Proxy s)

There are other issues, though, as Tikhon Jelvis points out in his answer.

上一篇: 国防部必须使用全名的类型？

下一篇: GHC TypeLits没有值