[Haskell-cafe] restore type from existential

[zoran.bosnjak at via.si]

Dear haskellers,
if for example I have the following (simplified) situation:

import GHC.TypeLits

type MyTypes =
     '[ ()    -- index 0
      , Char  -- index 1
      , Int   -- index 2
      ]

data SNat (n :: Nat) where
     SZ :: SNat 0
     SS :: SNat n -> SNat (n+1)

data Wrap where
     WrapUnsafe :: SNat n -> t -> Wrap

t1 = WrapUnsafe SZ () :: Wrap
t2 = WrapUnsafe (SS SZ) 'x' :: Wrap
t3 = WrapUnsafe (SS (SS SZ)) (1::Int) :: Wrap

Is it possible to have an 'unwrap' function? That is: to combine MyType 
types table and the type index... to get the exact type back. Something 
in the form:

unwrapUnsafe :: Wrap -> t
unwrapUnsafe (WrapUnsafe (ix::SNat n) (val::t)) = undefined

x1 = unwrapUnsafe t1
x2 = unwrapUnsafe t2
x3 = unwrapUnsafe t3

GHC didn't like any of my attempt. Is it even possible?

regards,
Zoran