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