Internal error in unify.ml

[nad]

The following code triggers an internal error in Beluga f65d501160913a10f4b749c620711f0678c58c06:

LF empty : type =
;

schema ctx = empty;

LF t : type =
| c : t → t
;

LF p : t → type =
| d : p X
;

rec foo : {γ : ctx} {X : [γ ⊢ t]} [γ ⊢ p X] =
/ total m (foo x m) /
mlam γ, X ⇒ case [_ ⊢ X] of
| [_ ⊢ c Y] ⇒ case foo [_] [_ ⊢ Y] of
  | [_ ⊢ d] ⇒ [_ ⊢ d]
;

Error message:

Uncaught exception.
Please report this as a bug.

## Type Reconstruction: [...]/bug.bel ##
File "src/core/unify.ml", line 1143, characters 48-53: Pattern matching failed