Another thing which I forgot to mention - if you absolutely need to have an existential, i.e. `MyTypes` should not be visible at the top level, you'll need to also include some existential wrapper for the versions of `Wrap` together with a singleton for the type level list, in order to be able to later at runtime recover what the original list of types was. On 1/10/24 12:25, zoran.bosnjak@via.si wrote:
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 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.