[Haskell-cafe] restore type from existential

[Mikolaj Konarski]

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 <zoran.bosnjak at 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.