Предположим, я определил некоторые структуры уровня типа, например, так:
import Data.Singletons.Prelude
import Data.Singletons.TH
singletons [d|
data Natural = Succ Natural | Zero deriving (Show, Ord, Eq)
data Coord = Coord Natural Natural deriving (Show, Eq)
|]
Однако вместо того, чтобы определять свой собственный тип Natural
, я хотел бы использовать вместо него GHC.TypeLit.Nat
(если не для другихпричина, по которой сообщения об ошибках компилятора приятнее). Пакет singletons
уже определил экземпляры для соответствующих классов в Data.Singletons.TypeLits
, поэтому это должно быть возможно.
Однако, попытка заменить Natural
на Nat
, как и
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.TypeLits
singletons [d| data Coord = Coord Nat Nat deriving (Show, Eq) |]
выдает следующую ошибку
• Couldn't match type ‘GHC.Natural.Natural’ with ‘Nat’
Expected type: Nat
Actual type: Demote Nat
• In the first argument of ‘Coord’, namely ‘(fromSing b_awjJ)’
In the expression: (Coord (fromSing b_awjJ)) (fromSing b_awjK)
In an equation for ‘fromSing’:
fromSing (SCoord b_awjJ b_awjK)
= (Coord (fromSing b_awjJ)) (fromSing b_awjK)
Я понимаю, почему эта ошибка появляется, но я не уверен, как действовать дальше. Можно ли создавать структуры уровня типа, содержащие TypeLits
, используя singletons
Template Haskell? А если нет, то есть ли какой-нибудь способ сделать это, не используя все необходимые механизмы синглтона для Coord
вручную?