What is the proper way to use Nat/Natural in a singletons data type?

5
votes

I am working on writing a prototype programming language in Haskell with polymorphic variants using the singletons library. I have a basic type of types that looks like this:

import Data.Singletons.TH
import Data.Singletons
import GHC.Natural
import Data.Singletons.TypeLits

$(singletons [d|
  data MyType = 
      PredT
    | ProcT [MyType]
    | IntT
    | FloatT
    | StringT
    | FuncT MyType MyType
    | VariantT Natural [MyType]
    | UnionT [MyType]
  |])

The Natural argument in VariantT is used to identity a particular variant, and it is important for this to actually be Natural (and not something like a Nat defined as an algebraic data type) for efficency reasons.

The issue is, with this definition, I get:

Couldn't match expected type ‘Natural’
     with actual type ‘Demote Natural’

Usually, in my experience with the singletons library, I get errors like this (to my understanding anyway), when trying to use a type as a singleton where SingKind is not supported for that type e.x. for Char, so I am at a loss as to why this is not working.

I have tried Demote Natural, Nat, as well as different imports (thinking maybe I'm not using the right "Nat" or "Natural" that singletons works with), all giving me similar errors. What's the issue here? Do I have to write the definitions that singletons generates manually for types for which Demote a != a, or is there something that I'm missing here?

1
haskellsingleton-type

1 Answers

4
votes

Apparently this is a still unfixed issue. If I understand correctly, currently the singletons TH script works by reusing the same type as both the promoted and demoted type, but Nat completely breaks this model. The long-term solution is to wait for GHC to merge Nat and Natural. Meanwhile, you will have to manually duplicate or generalize your type, or roll your own Nat.

https://github.com/goldfirere/singletons/issues/478

As a short-term fix, it seems possible to extend the TH script singletons to do something like that automatically. That would be a nice contribution for people who use singletons extensively.