Bug in typechecking (inference generates ill-scoped terms)

The following

```
module Lambda;

type Box (A : Type) :=
  | box : A → Box A;

x : Box ((A : Type) → A → A);
x := box λ {A a := a};
```
gets typechecked into:

```
type Box (A : Type) =
  box : A → Box A

x : Box ((A : Type) → A → A)
x := box {Type → errorHere@A → A} λ : Type → A → A { A a := a}
```

The error is that that the `A` next to `errorHere` is out of scope
