Hi !

I work with a small language which has a `literal`

type in its AST that’s similar to this (I removed most cases because they’re not relevant):

```
type literal =
| Null
| Bool of bool
| Num of float
| LList of literal list
```

I don’t think I need to spend too much time interpreting the different cases.

Because ASTs are the textbook example for GADTs, trying GADTs here has been in my todo list for quite a while.

So I did this:

```
type null
type llist (* not sure about those phantom types *)
type _ literal =
| Null : null literal
| Bool : bool -> bool literal
| Num : float -> float literal
| LList : ??? -> llist literal
```

The issue is that LLists are polymorphic. They can contain anything, so I don’t know how to express it.

One might think that adding ADTs has little meaning here but I think there are some nice things to do.

First of all, my language has expressions, and I would want to have a function with the following signature

```
val eval_expr : type a. a expr -> a literal
```

Which brings me to my second question, what’s the type of a variable in an AST ?

```
type _ expr =
| Lit : 'a literal -> 'a expr
| Plus : float expr -> float expr -> float expr
| ListCons : 'a expr -> llist expr -> llist expr
| Var : string -> 'a expr (* ??? *)
```

Moreover, my language also has (logic) formulae which are basically boolean expressions with quantifiers.

Right now, we have a function with the following signature:

```
val lift_expr : expr -> formula
```

Which has a lot of failing cases, and I would like to use GADTs to have something more like

```
val lift_expr : bool expr -> formula
```

And that would even allow me to rewrite the formula type as something similar to this:

```
type formula =
| QF of bool formula
| Forall of var list * formula
```

instead of having `formula`

being basically a duplicate of expr with less cases and quantifiers.

I don’t know how clear that is, but to summarise, here are my two questions:

- In that GADT literal type, what should be the type of the
`LList`

constructor to accept any kind of literal list ? - In an AST that has variables which are dynamically typed, what would be the definition for a nice GADT ?

And a more global question: are GADTs even interesting in my case ?

Thank you !