Hi all!

I’m trying to write down a data type in PureScript for which I used GADTs in Idris. Roughly I had:

```
-- Idris
data Task : Type -> Type where
Edit : (val : Maybe a) -> Task a
And : Show a => Show b => (left : Task a) -> (right : Task b) -> Task (Pair a b)
...
```

I need three things:

- Equate types to pin down the return type
- Introduce new existential types
- Save dictionaries for class instances

For (1) I could use `Data.Leibniz`

or `Type.Equality`

. I prefer the later, because I don’t have to fiddle with `coerce`

, `symm`

, and friends. For (2) I could use `Data.Exists`

, but then I can’t access the existential type variable and use it for (1) and (3). How to specify I’d like to save a dictionary for `Show`

in that case?

I looked around and found this solution to use double negation to simulate existentials:

```
-- PureScript
data Task r
= Edit (Maybe r)
| And (forall p. (forall a b. Show a => Show b => TypeEquals r (Tuple a b) => Task a -> Task b -> p) -> p)
...
```

I’ve three questions regarding this encoding.

First, when I try to create a `Show`

instance in the following way:

```
instance showTask :: Show a => Show (Task a) where
...
show (And unpack) = unpack matcher
where
matcher x y = show x <> " <&> " <> show y
```

I get the error message

```
No type class instance was found for
Data.Show.Show a1
```

When I make a hole to check the context:

```
show (And unpack) = unpack matcher
where
matcher x y = ?hole
```

I get:

```
The type variable b, bound at
src/Data/Task/Minimal.purs line 24, column 30 - line 24, column 35
has escaped its scope (...)
```

What’s going on here?

Second, is this encoding trick still the way to go, or are there newer/better/more elegant solutions I could try?

And third, are there any plans to introduce language level support for existentials so we could write something like the code below and have support for it during pattern matching? Maybe it would be a stop-gap solution towards real GADTs, but useful nevertheless.

```
data Task r
= Edit (Maybe r)
| And (exist a b. Show a => Show b => TypeEquals r (Tuple a b) => Tuple (Task a) (Task b))
...
```