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