-*- 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' ]);
The offending code is obviously not type correct, but should not make Beluga crash...