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

【问题标题】：Using constraints in Typed Template Haskell在类型化模板 Haskell 中使用约束
【发布时间】：2020-12-22 03:38:08
【问题描述】：

我想在我的 Typed Template Haskell sn-ps 中使用 typeclass 约束，但无法让它们工作：拼接中的实例似乎丢失了。

这是我的代码的独立最小化版本，用于演示该问题。第一个模块定义了一个 Typed Template Haskell 宏 memoryMap，它不对 tag 施加任何约束，而 ram0 则通过 C 约束 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 约束添加到宏的返回类型：

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

【问题讨论】：

标签： haskell metaprogramming typeclass template-haskell

【解决方案1】：

不幸的是，这是当前 Typed Template Haskell 实现的一个根本缺陷，没有简单的解决方法。

约束没有正确处理。

在研究如何实现generics-sop 的分阶段版本时，我们遇到了同样的问题。您可能想查看Staged Sums of Products 论文的第 5 节。我们还有一个在 Template Haskell 中处理约束的解决方案，但是这个解决方案需要在 GHC 中实现，并且目前仅在实验分支中可用（有关如何尝试它的一些说明，请参阅the staged-sop repo）。目前，该分支处于不确定状态，因为由于所有线性类型的变化，它需要进行重大的变基。希望我们能尽快解决这个问题，因为我真的很想在 Typed Template Haskell 中进行适当的约束处理。

【讨论】：