Promoting Enum instance

[vladfi1]

I have a type for which Enum is not derivable, but I have instead written my own Enum instance. Is there a way to get singletons to promote this instance, giving me the PEnum, SEnum, and Apply instances I want?

[vagarenko]

@vladfi1 See http://hackage.haskell.org/package/singletons-2.0.1/docs/Data-Singletons-TH.html#g:5

[goldfirere]

@vagarenko, those functions are only for derivable instances.

But, @vladfi1, if you just wrap your instance definition in $(singletons [d| instance Enum ... |]), it should work. Singletons now supports full processing of class and instance declarations.

[goldfirere]

If this doesn't work, please reopen. Thanks!

[vladfi1]

Here's what I have:

{-# LANGUAGE DataKinds,
             PolyKinds,
             TypeOperators,
             TypeFamilies,
             GADTs,
             UndecidableInstances,
             KindSignatures,
             InstanceSigs,
             ScopedTypeVariables,
             TemplateHaskell
             #-}

module SingletonsTH where

import Data.Singletons.Prelude
import Data.Singletons.TH

$(singletons [d|
  data Nat = Z | S Nat
    deriving (Eq, Ord, Show)

  instance Enum Nat where
    succ = S

    pred Z = error "pred Z"
    pred (S n) = n

    toEnum 0 = Z
    toEnum n = S $ toEnum (n-1)

    fromEnum Z = 0
    fromEnum (S n) = 1 + (fromEnum n)

  |])

This fails with

SingletonsTH.hs:18:3: Cannot find type annotation for Succ

SingletonsTH.hs:18:3: Q monad failure

Now that I've manually implemented PEnum, SEnum, PNat, and SNat for this type I'm not sure if I should expect singletons to be able to do it. In particular, sToEnum/sFromInteger required some unsafeCoerce business, and I wasn't even able to write sFromEnum. At least Apply just works!

[goldfirere]

This worked for me:

{-# LANGUAGE DataKinds,
             PolyKinds,
             TypeOperators,
             TypeFamilies,
             GADTs,
             UndecidableInstances,
             KindSignatures,
             InstanceSigs,
             ScopedTypeVariables,
             TemplateHaskell
             #-}

module SingletonsTH where

import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.Prelude.Enum

$(singletons [d|
  data Nat = Z | S Nat
    deriving (Eq, Ord, Show)

  instance Enum Nat where
    succ n = S n

    pred Z = error "pred Z"
    pred (S n) = n

    toEnum n = if n == 0 then Z else S $ toEnum (n-1)

    fromEnum Z = 0
    fromEnum (S n) = 1 + (fromEnum n)

  |])

I identify three problems here:

1. Enum stuff should be exported from Data.Singletons.Prelude.
2. Literal patterns are not supported, so I had to change toEnum.
3. The eta-reduced succ (that is, declared in point-free style) wasn't accepted.

(1) and (3) are proper bugs. (2) is essentially a feature request. But, if I recall, (2) is trickier than you would think. (1) and (3) should be possible though. In the meantime, (1) and (3) are very easy to work around.

[vladfi1]

Cool, that works. I can now promote both Enum and Num instances! I'm curious how singletons is able to promote toEnum and fromEnum though (as I said, I had difficulty doing it manually).

[goldfirere]

You can always take a look at -ddump-splices to see how singletons does its magic. As for the fixes for the bugs we identified, don't hold your breath. Things are very busy over head, and I'm afraid singletons isn't at the top of the queue. I'd accept pull requests though!

[vladfi1]

I've run into more trouble, again with promoting Enum instances.

{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeFamilies, KindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
{-# LANGUAGE InstanceSigs, DefaultSignatures #-}

module Binary where

import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Singletons.Prelude.Enum
import Data.Singletons.Prelude.Num

type Bit = Bool
type BiNat = [Bit]

$(singletons [d|
  instance Enum BiNat where
    succ [] = [True]
    succ (False:as) = True : as
    succ (True:as) = False : succ as

    pred [] = error "pred 0"
    pred (False:as) = True : pred as
    pred (True:as) = False : as

    toEnum i | i < 0 = error "negative toEnum"
             | i == 0 = []
             | otherwise = succ (toEnum (pred i))

    fromEnum [] = 0
    fromEnum (False:as) = 2 * fromEnum as
    fromEnum (True:as) = 1 + 2 * fromEnum as
  |])

The toEnum definition causes problems such as

Could not deduce (SEnum 'KProxy) arising from a use of ‘sSucc’

The fromEnum [] case also causes an error:

Could not deduce (FromEnum '[] ~ FromEnum '[])
    from the context (t1 ~ '[])
      bound by the type signature for
                 lambda_aiF1 :: (t1 ~ '[]) => Sing (Apply FromEnumSym0 '[])
      at Binary.hs:(18,3)-(66,4)
    NB: ‘FromEnum’ is a type function, and may not be injective
    The kind variable ‘k0’ is ambiguous