[Haskell-cafe] TypeLits and ScopedTypeVariables

[Ben Foppa]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140111/46c5e5ae/attachment.html>