Создание структуры уровня типа, которая содержит TypeLit с синглетонами - PullRequest
Новая
       79

Создание структуры уровня типа, которая содержит TypeLit с синглетонами

2 голосов
/ 08 ноября 2019

Предположим, я определил некоторые структуры уровня типа, например, так: 

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 вручную?

...