haskell - 使用 Tagless Final 方法时的类型变量不明确

Question

我正在使用模板 haskell 构造一个在类型级别用其值标记的整数：

{-# LANGUAGE TemplateHaskell TypeOperators, DataKinds, KindSignatures #-}

module TNat where

import GHC.TypeLits
import Language.Haskell.TH

data TNat (a::Nat) = TN Int deriving Show

zero = (TN 0 :: TNat 0)

inc :: TNat n -> TNat (n + 1)
inc (TN n) = TN (n + 1)

-- usage: fromNat @5
mkNat :: Int -> Q Exp
mkNat 0 = [| zero |]
mkNat n = [| inc ($(mkNat (n - 1))) |] 

我在我制作了一个示例版本的无标签最终样式 dsl 中使用它：

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, FlexibleContexts, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances, ExistentialQuantification, FlexibleInstances, GADTs #-}

{-# LANGUAGE TemplateHaskell #-}

module Test where

import TNat
import Text.Printf
import Language.Haskell.TH
import GHC.TypeLits

data IntList (ls :: [*])

class SYM repr where
    nat :: TNat a -> repr (TNat a)
    ret :: repr b -> repr (IntList '[b])
    comp :: repr a -> repr (IntList ls) -> repr (IntList (a ': ls))

newtype S a = S{unS :: String}
instance SYM S where
    nat (TN i) = S $ show i
    ret e1 = S $ unS e1
    comp e1 e2 = S $ (unS e1) ++ " " ++ (unS e2)

问题是以下语句因模棱两可的类型repr0而不是更一般的类型而失败repr：

t1 = ret $ nat $(mkNat 2) 

具体的错误信息是：

* Ambiguous type variable `repr0' arising from a use of `r et'
  prevents the constraint `(SYM repr0)' from being solved.
  Relevant bindings include
    t1 :: repr0 (IntList '[TNat 2]) (bound at test.hs:35:1 )
  Probable fix: use a type annotation to specify what `rep r0' should be.
  These potential instance exist:
    instance SYM S -- Defined at test.hs:29:10
* In the expression: ret $ nat (inc (inc zero))
  In an equation for `t1': t1 = ret $ nat (inc (inc zero))    | 35 | t1 = ret $ nat $(mkNat 2)    |      ^^^^^^^^^^^^^^^^^^^^

我觉得我遗漏了 DSL 声明的一些关键部分，或者这是 Template Haskell 和这种编写 DSL 的风格之间的奇怪交互（因为我在没有 TH 的以前版本中没有这个问题）。

标签： haskelltypes