I'm not sure if anybody mentioned that, but if you have
data Wrap where
WrapUnsafe :: Typeable t => SNat n -> t -> Wrap
Then you can write something like
unwrapUnsafe :: Wrap -> t
unwrapUnsafe (WrapUnsafe @t0 (ix::SNat n) (val::t)) =
case testEquality (typeRep @t0) (typeRep @t) of
Just Refl -> val
Nothing -> error ""
No unsafeCoerce, but the error case can occur easily.
Cheers,
Mikolaj
On Wed, Jan 10, 2024 at 11:26 AM
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.