Hey there!

I’ve been following the 48h Scheme Haskell Tutorial to get more mileage and I’ve come across an impediment related to the existential types… again

In the tutorial they implement some weak typing check through heterogeneous lists.

They do this by creating this data type:

```
data Unpacker = forall a. Eq a => AnyUnpacker (LispVal -> ThrowsError a)
```

I tried a bunch of things, including `Exists`

& `TypeEquals`

, least of which:

```
newtype Unpacker = AnyUnpacker (∀ r. (∀ a. Eq a => a -> r) -> LispVal -> ThrowsError r)
```

Now… this almost works, but the problem is that he proof requires the result `r`

before applying the unpacker function (`LispVal -> ThrowsError r`

) if I understand right so that doesn’t work.

I mean it could work if we knew the type of `r`

and so we could do something like `unpacker (const 0) arg1`

or `unpacker (const "") arg1`

in:

```
unpackEquals :: LispVal -> LispVal -> Unpacker -> ThrowsError Boolean
unpackEquals arg1 arg2 (AnyUnpacker unpacker)
= do unpacked1 <- unpacker arg1
unpacked2 <- unpacker arg2
pure $ unpacked1 == unpacked2
pure false
`catchError` (const $ pure false)
```

Which is the direct translation of the original Haskell code.

Other relevant info might be that: `type ThrowsError = Either LispError`

. I’m getting closer to understanding these existential types, it’s just that I don’t know how to provide the proofs with these nested types.

The idea is to create a heterogeneous list like: `[AnyUnpacker unpackNum, AnyUnpacker unpackStr, AnyUnpacker unpackBool]`

where `unpackNum :: LispVal -> ThrowsError Int`

and so on for the rest, with appropriate return types. This is just copy/paste from the tutorial, this works in Haskell.

Any ideas much appreciated! Thanks