Bug in typechecking (inference generates ill-scoped terms)

[janmasrovira]

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