在类型化模板中使用约束 Haskell

Question

我想在我的类型化模板 Haskell 片段中使用类型类约束，但无法使它们工作：实例似乎在拼接内丢失。

这是我的代码的独立最小化版本，用于演示该问题。第一个模块定义了一个 Typed Template Haskell 宏 memoryMap，它不对 tag 和 ram0 施加任何约束，它通过 [=20 约束 tag =]:

{-# LANGUAGE TemplateHaskell, QuasiQuotes #-}
{-# LANGUAGE DerivingStrategies, GeneralizedNewtypeDeriving #-}
module RetroClash.MemoryTH where

import Control.Monad.Identity
import Language.Haskell.TH

class C a where

newtype Signal tag a = Signal{ runSignal :: a }

newtype Addressing dom a = Addressing
    { runAddressing :: Identity a
    }
    deriving newtype (Functor, Applicative, Monad)

memoryMap :: Addressing tag () -> TExpQ (Signal tag (Maybe dat) -> Signal tag (Maybe dat))
memoryMap addressing = [|| \ wr -> wr ||]

ram0 :: (C tag) => Addressing tag ()
ram0 = pure ()

然后我尝试从另一个模块直接使用它：

{-# LANGUAGE TemplateHaskell #-}
module RetroClash.MemoryTHTest where

import RetroClash.MemoryTH

foo
    :: (C tag)
    => Signal tag (Maybe Int)
    -> Signal tag (Maybe Int)
foo = $$(memoryMap ram0)

但是，这会导致 GHC 8.10 出现以下类型错误：

src/RetroClash/MemoryTHTest.hs:11:20: error:
    • No instance for (C tag) arising from a use of ‘ram0’
    • In the first argument of ‘memoryMap’, namely ‘ram0’
      In the expression: memoryMap ram0
      In the Template Haskell splice $$(memoryMap ram0)
   |
11 | foo = $$(memoryMap ram0)
   |                    ^^^^

我尝试过的一件事就是直接将 C 约束添加到宏的 return 类型中：

memoryMap :: Addressing tag () -> TExpQ (C tag => Signal tag (Maybe dat) -> Signal tag (Maybe dat))
memoryMap addressing = [|| \ wr -> wr ||]

即使这有效，也无法解决我原来的问题，因为约束应该以开放世界的方式来自 Addressing tag () 论证中发生的任何事情；但无论如何这个版本失败了，因为它遇到了 GHC 的不确定性限制：

    • Illegal qualified type:
        C tag => Signal tag (Maybe dat) -> Signal tag (Maybe dat)
      GHC doesn't yet support impredicative polymorphism

Answer 1

不幸的是，这是当前类型化模板 Haskell 实施的一个根本缺陷，没有简单的解决方法。

约束没有得到正确处理。

我们在研究如何实现 generics-sop 的分阶段版本时遇到了同样的问题运行。您可能想查看 Staged Sums of Products paper. We also have a solution for the handling of constraints in Template Haskell, but this solution needs implementation in GHC, and that at the moment is only available in an experimental branch (see the staged-sop repo 的第 5 部分，了解有关如何尝试的一些说明）。目前，该分支处于不确定状态，因为由于所有线性类型的变化，它需要进行重大的重新设置。希望我们能尽快解决这个问题，因为我真的很想在 Typed Template Haskell.

中进行适当的约束处理

在类型化模板中使用约束 Haskell

Using constraints in Typed Template Haskell

haskell

metaprogramming

typeclass

template-haskell