GHC TypeLits 没有值

Question

尝试设计一个类型驱动的 API，我一直在尝试获得类似以下的工作（使用更复杂的代码/尝试，这被精简到澄清我在寻找什么所需的最低限度） ：

{-# 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

这个程序会打印 'foo'，但不会：

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

启用AllowAmbiguousTypes 并没有真正的帮助。有什么办法可以让它工作吗？

Answer 1

类型同义词（用type 定义）在类型检查期间被它们的定义替换。问题是Printer 在其定义中没有引用s，这导致了以下约束：

generic :: KnonwSymbol s => IO ()

此类型签名没有=> 右侧的s，因此无法通过歧义检查。它不能真正起作用，因为当你使用它时，没有地方可以指定s 应该是什么。

不幸的是，GHC 在错误消息中表示类型同义词的方式不一致。有时它们被扩展，有时它们被保留。具有讽刺意味的是，我认为错误消息的改进使这个特定错误更难追踪：通常，根据您定义的类型来表达错误更清楚，但在这里它隐藏了歧义的原因。

您需要某种方式来提供不依赖于类型同义词的相关类型级符号。但首先，您需要启用ScopedTypeVariables，并在generic 的签名中添加forall，以确保类型签名中的s 和Proxy :: Proxy s 中的s 相同。

有两种可能：

• 将Printer 更改为newtype 并在使用时打开它：

  newtype Printer (s :: Symbol) = Printer { runPrinter :: IO () }
  
  generic :: forall s. KnownSymbol s => Printer s
  generic = Printer $ putStrLn (symbolVal (Proxy :: Proxy s))
  
  main = runPrinter generic
  

• 向generic 传递一个额外的Proxy 参数，就像symbolVal：

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

  将proxy 作为类型变量是一个简洁的习惯用法，它可以让您不依赖Data.Proxy，并让调用者传递他们想要的任何东西。

Answer 2

这是错误的：

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

最后一个s与上面的s无关。它是局部隐式普遍量化的，就像在顶级类型注释中一样。代码实际上是什么意思

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

要解决上述问题，请启用ScopedTypeVariables 并使用

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

不过，正如 Tikhon Jelvis 在回答中指出的那样，还有其他问题。