I've been playing with TypeLits recently, trying to create a vector with type-fixed size. I've hit a stumbling block trying to compile this (simplified) code: {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} import Control.Exception (assert) import GHC.TypeLits data Foo (n :: Nat) a = Foo a size :: SingI n => Foo n a -> Int size = fromInteger . fromSing . sizeSing where sizeSing :: Foo n a -> Sing n sizeSing _ = sing The error is: Could not deduce (SingI Nat n1) arising from a use of `sing' from the context (SingI Nat n) bound by the type signature for size :: SingI Nat n => Foo n a -> Int at /home/ben/test.hs:10:9-33 Possible fix: add an instance declaration for (SingI Nat n1) In the expression: sing In an equation for `sizeSing': sizeSing _ = sing In an equation for `size': size = fromInteger . fromSing . sizeSing where sizeSing :: Foo n a -> Sing n sizeSing _ = sing Can anybody shed light on this? It seems like the kind of thing that ScopedTypeVariables should solve, but it doesn't make a difference.