Access GADT contstraint from evaluation level

I am trying to make use of some of GADT parameter from runtime, assuming that I have used DataKinds extension to allow promoting data to types. i.e. having

data Num = Zero | Succ Num
data Something (len :: Num) where
  Some :: Something len

I would like to have function

toNum :: Something len -> Num

That for any Some :: Something n will return n:

toNum (s :: Something n) = n

Which is invalid in Haskell. Is it possible to do so?

Solution

In Haskell this is impossible, since types are erased at runtime. That is, when the program will run, there is no information in memory about the value of the index let in the type.

To overcome this issue, we need to force Haskell to keep in memory that value, at runtime. This is usually done using a singleton auxiliary type:

data Num = Zero | Succ Num

data SNum (n :: Num) where
   SZero :: SNum 'Zero
   SSucc :: SNum n -> SNum ('Succ n)

data Something (len :: Num) where
  Some :: SNum len -> Something len

Using this you can easily write

sToNum :: SNum n -> Num
sToNum SZero = Zero
sToNum (SSucc n) = Succ (sToNum n)

and then

toNum :: Something len -> Num
toNum (Some n) = sToNum n

If you look up "haskell singletons" you should find several examples. There's even a singletons library to partially automatize this.

If / when "dependent Haskell" will be released, we will have less cumbersome tools at our disposal. Currently, singletons work, but they are a hassle sometimes. Still, for the moment, we have to use them.