On Mon, 2014-01-06 at 09:15 -0800, Nathan Howell wrote:

This requires -XScopedTypeVariables and some constraints:

tOf :: forall a . (SingI (T a), C a) => a -> Integer tOf _ = fromSing $ (sing :: Sing (T a))

Wonderful, thanks. I tried using ScopedTypeVariables, but "SingI Nat (T a)" didn't work out, although the compiler error hinted in that direction. Thanks, Nicolas

natVal accepts any type witness now, not just sing. One such type in base is the polykinded Data.Proxy.Proxy, e.g. `natVal (Proxy :: Proxy 0`. For types of kind * you can use almost anything, including an empty list. On Mon, Jan 6, 2014 at 9:27 AM, Erik Hesselink wrote:

Small additions: the 'Nat' in the original argument is the kind argument to the class. It seems to be a bug that GHC provided this in the error, and the latest HEAD doesn't seem to do so anymore. Also, in the latest HEAD, I think you need to use the singletons library, as all the singletons stuff is gone from base. My working code:

{-# LANGUAGE TypeFamilies , DataKinds , FlexibleContexts , ScopedTypeVariables #-} module Main where

import GHC.TypeLits import Data.Singletons

class C a where type T a :: Nat

data D = D instance C D where type T D = 10

{- This is not allowed, as intended:

data E = E instance C E where type T E = Int -}

-- This works: tOfD :: D -> Integer tOfD D = fromSing $ (sing :: Sing (T D))

tOf :: forall a. (KnownNat (T a), C a) => a -> Integer tOf _ = fromSing $ (sing :: Sing (T a))

main :: IO () main = return ()

Erik

On Mon, Jan 6, 2014 at 6:15 PM, Nathan Howell wrote:

...

This requires -XScopedTypeVariables and some constraints:

tOf :: forall a . (SingI (T a), C a) => a -> Integer tOf _ = fromSing $ (sing :: Sing (T a))

On Mon, Jan 6, 2014 at 9:06 AM, Nicolas Trangez wrote:

...

All,

While toying with typelits I wanted to get the following to work, but failed to. Is it intended not to work at all, should I change something to get it to work, or is this something which needs some GHC support?

Note I obviously tried to add the constraint mentioned in the compiler error, but failed to: I seem to add too many type arguments to SingI, which somewhat puzzles me.

Thanks,

Nicolas

{-# LANGUAGE TypeFamilies, DataKinds #-} module Main where

import GHC.TypeLits

class C a where type T a :: Nat

data D = D instance C D where type T D = 10

{- This is not allowed, as intended:

data E = E instance C E where type T E = Int -}

-- This works: tOfD :: D -> Integer tOfD D = fromSing $ (sing :: Sing (T D))

{- This doesn't work: - Could not deduce (SingI Nat (T a1)) arising from a use of `sing' - from the context (C a)

tOf :: C a => a -> Integer tOf _ = fromSing $ (sing :: Sing (T a)) -}

main :: IO () main = return ()

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe