[Haskell-cafe] Associated types, kind constraints & typelits

[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 ()