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
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