2
GADTとsingletonsライブラリを使用して、正規表現解析用のプログラムを作成しようとしています。私はこれを取得していますなぜ誰かが説明できHaskellでのデータの種類とシングルトンの問題
{-# LANGUAGE DataKinds, KindSignatures,
GADTs, TypeFamilies, TemplateHaskell,
QuasiQuotes, ScopedTypeVariables #-}
module Lib where
import Data.Proxy
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.TypeLits
$(singletons [d|
data RegExp = Sym Nat
| Eps
| Cat RegExp RegExp
| Choice RegExp RegExp|])
type family CHR :: Nat -> Symbol
data InRegExp (e :: RegExp) (n :: Symbol) where
InEps :: InRegExp Eps ""
InChr :: SNat n -> InRegExp (Sym n) (CHR n)
:私は、私は以下のコードをコンパイルするために必要なすべての拡張機能を使用していると信じている
Couldn't match type ‘Integer’ with ‘Nat’
Expected type: DemoteRep 'KProxy
Actual type: Nat
In the first argument of ‘toSing’, namely ‘b_a4Vr’
In the expression: toSing b_a4Vr :: SomeSing (KProxy :: KProxy Nat)
:私は奇妙なエラーメッセージが出ていエラーメッセージ?私はそれを解決する方法を知らない。
あなたは、[この問題](https://github.com/goldfirere/singletons/issues/76)に直面しています。 – crockeea
'データを変更するRegExp = Sym Nat | ... 'to 'data RegExp a = Sym a |あなたが '{to/from}}がこのタイプのために働くことを望むなら... ' – user2407038