I’m implementing an algorithm that translates the lambda calculus to combinators (from the paper “Lambda to ski semantically” by Oleg Kiselyov). I’m still a beginner at Coq, but I have a lot of experience with Haskell where I’ve already implemented the same algorithm with GADTs. Here is the code that is relevant for my issue:

```
Inductive ski : Type -> Type :=
si : forall {a}, ski (a -> a)
| sk : forall {b} {a}, ski (a -> b -> a)
| ss : forall {b} {c} {a}, ski ((a -> b -> c) -> (a -> b) -> a -> c)
| sapp : forall {b} {a}, ski (a -> b) -> ski a -> ski b.
Inductive conv : Type -> Type -> Type :=
cc : forall {ctx} {a}, ski a -> conv ctx a
| cn : forall {b} {ctx} {a}, conv ctx (b -> a) -> conv (ctx * b) a.
Definition amalg {ctx} {a} {b}
: conv ctx (a -> b) -> conv ctx a -> conv ctx b :=
fun x y =>
match x, y with
| cc d1, cc d2 => cc (sapp d1 d2) (* The error is here *)
| _, _ => _ (* TODO *)
end.
```

This gives the following error message:

```
In environment
ctx : Type
a : Type
b : Type
x : conv ctx (a -> b)
y : conv ctx a
T : Type
T0 : Type
d1 : ski T0
y0 : conv T a
T1 : Type
T2 : Type
d2 : ski T2
The term "d1" has type "ski T0" while it is expected to have type "ski (?a0@{y0:=y; y:=y0} -> ?b@{y0:=y; y:=y0})".
```

I would think `T0`

has to be equal to the function type `(a -> b)`

, because we know that `cc d1`

is a match of `x : conv ctx (a -> b)`

and `cc : ski a -> conv ctx a`

. Why does Coq give this error and how can I fix it?

General advice for improvement of this code is also appreciated.