Hi Zoran, No, with your given Wrap data type, it would not be possible. The moment you only constraint `t` to be `forall` bound in `WrapUnsafe` and have not other properties, there's really no way to get it out without using `unsafeCoerce`. There are many approaches to achieve being able to "recover" what `t` is. One idea would be to add a list type parameter `ts` to `Wrap` and a constraint to `WrapUnsafe` which says "t is the type at index n in the list ts", i.e. something like ``` type family Index n ts where Index 0 (t ': _) = t -- might need your own definition of Nat for the next case Index (1 + n) (_ ': ts) = Index n ts data Wrap ts where MkWrap :: SNat n -> Index n ts -> Wrap ts ``` Another (which I personally think is cleaner) would be to entirely skip the `SNat`s and use an "membership proof" instead, i.e. something like ``` data Elem (x :: t) (xs :: [t]) where Here :: Elem x (x ': xs) There :: Elem x xs -> Elem x (y ': xs) ``` You could then have ``` data Wrap ts where MkWrap :: Elem t ts -> t -> Wrap ts t1, t2, t3 :: Wrap MyTypes t1 = MkWrap Here () t2 = MkWrap (There Here) 'x' t3 = MkWrap (There (There Here)) 1 ``` You could then also try to automate the membership proof generation via type classes. If you're going the unsafe approach and going to be `unsafeCoerce`ing, you could also just as well drop the `SNat` and use a raw `Int` instead, because you're the one who's going to be taking care not to `unsafeCoerce` the wrong thing anyways. Cheers, Georgi 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.