How would we convert this:

```
import Data.Leibniz (type (~))
data Expr a
= Add (Expr Int) (Expr Int) (a ~ Int)
| Eq (Expr Int) (Expr Int) (a ~ Boolean)
| Not (Expr Boolean) (a ~ Boolean)
| Val Int (a ~ Int)
```

to using `Type.Equality`

? The goal would be to approximate GADTs such as explained here https://hgiasac.github.io/posts/2018-12-18-PureScript-GADTs-Alternatives---Recap.html (which uses Leibniz).

To get something like `eval :: forall a. Expr a -> a`

that works. Is this even possible? I’m trying to wrap my head around this and tried a bunch of things none of which worked. This doesn’t seem to be a great idea:

```
data Expr a
= Add (TypeEquality a Int => Expr a) (TypeEquality a Int => Expr a)
| Eq (TypeEquality a Boolean => Expr a) (TypeEquality a Boolean => Expr a)
| Not (TypeEquality a Boolean => Expr a)
| Val (TypeEquality a Int => a)
```

And other similar forma all fail. Thanks