Hello,

I am trying for the (real) first time to solve a problem using a GADT.

I wan’t to represente a function specification using the type spec:

```
type _ spec =
| Elem : 'a Gen.t -> 'a spec
| Arrow : 'a spec * 'b spec -> ('a -> 'b) spec
let (^>) x y = Arrow (x, y)
let int = Term Gen.int
let foo : (int -> int -> int) spec = int ^> int ^> int
```

Then, from this function spec, I would like to transform it into an application through a

type expression:

```
type _ expr =
| Apply : ('a -> 'b) expr * 'a expr -> 'b expr
| Term : 'a -> 'a expr
| Fun : ('a -> 'b) -> ('a -> 'b) expr
let rec eval_expr : type a. a expr -> a = function
| Apply (f, x) -> (eval_expr f) (eval_expr x)
| Term x -> x
| Fun f -> f
```

The problem I currently have is typing of that transformation:

```
let rec spec_to_expr : type a b. a spec -> a expr -> b expr =
fun spec expr ->
match spec with
| Arrow (Elem x, y) ->
let x = Gen.sample x in
let expr = Apply (expr, Term x) in
spec_to_expr y expr
| Elem x ->
let x = Gen.sample x in
Apply (expr, Term x)
| _ -> assert false
(* Typing error: *)
| Elem x -> Apply (expr, Term x)
^^^^
Error: This expression has type a expr but an expression was expected of type
('a -> b) expr
Type a is not compatible with type 'a -> b
```

I get that I have defined expr as an `a expr`

, but in:

```
| Arrow (Elem x, y) ->
let x = Gen.sample x in
let expr = Apply (expr, Term x) in
spec_to_expr y expr
```

`expr`

has the same type but it does not appear to raise a typing error, and I don’t understand

why it is allowed in that case ?

I’m sorry if my question does not make any sens, but that’s really one of the first times I’m trying

to implement a GADT.