File "src/core/lfrecon.ml", line 1205, characters 9-14: Pattern matching failed

[ryanakca]

-*- mode: compilation; default-directory: "~/Documents/Note-CDST/" -*-
Compilation started at Mon Jun  5 22:17:28

beluga /home/rak/Documents/Note-CDST/traces.bel
## Type Reconstruction begin: /home/rak/Documents/Note-CDST/traces.bel ##
Uncaught exception.
Please report this as a bug.
File "src/core/lfrecon.ml", line 1205, characters 9-14: Pattern matching failed
Compilation exited abnormally with code 1 at Mon Jun  5 22:17:28

The offending code is obviously not type correct, but should not make Beluga crash...

LF cn : type =;
--name cn C c.

LF payload : type =
  | close : cn → payload;

LF trace : type =
  | msg  :  payload → trace;

LF tlist : type =
  | nil  : tlist
  | cons : trace → tlist;

schema ctx = cn;

rec merge : {g : ctx} [ g ⊢ trace ] → [ g ⊢ trace ] → [ g ⊢ tlist ] =
mlam g ⇒ fn t ⇒ fn t' ⇒
case t of
  | [ a ⊢ msg (close a) ] ⇒
	(case t' of
	  | [ a ⊢ msg (close a) t' ] ⇒ [ a ⊢ msg (close a) t' ]);