Uncaught exception, possibly due to missing annotations in context

[nad]

The following code triggers an internal error in Beluga f65d501160913a10f4b749c620711f0678c58c06:

LF term : type =
| lam : (term → term) → term
;

LF pred : (term → term) → type =
| pred_lam :
    ({y : term} pred (\x. T x y)) →
    pred (\x. lam (\y. T x y))
;

schema ctx = term;

rec foo :
  {γ : ctx}
  {T : [γ, x : term ⊢ term]}
  [γ ⊢ pred (\x. T)] → [⊢ term] =
mlam γ ⇒ mlam T ⇒ fn p ⇒ case p of
| [γ ⊢ pred_lam (\y. P)] ⇒ case [γ, x : term, y : term ⊢ T] of
  | [γ, x, y ⊢ #p1[..]] ⇒ ?
;

Error message:

Uncaught exception.
Please report this as a bug.

## Type Reconstruction: [...]/bug.bel ##
File "src/core/apxnorm.ml", line 458, characters 27-32: Pattern matching failed