You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
-*- mode: compilation; default-directory: "/tmp/" -*-
Compilation started at Fri Jun 2 15:04:39
beluga /tmp/mwe.bel
## Type Reconstruction begin: /tmp/mwe.bel ##
Uncaught exception.
Please report this as a bug.
Failure("missing type information")
Compilation exited abnormally with code 1 at Fri Jun 2 15:04:39
on the following minimal working example:
LF cn : type =;
LF single : type =
| one : cn → single;
schema cns = block (c : cn);
rec crash : {g1 : cns} {g2 : cns} [ g1, a : cn ⊢ single ] → [ g1, g2, a : cn ⊢ single ] =
mlam g1 ⇒ mlam g2 ⇒ fn t1 => case t1 of
| [ a : cn ⊢ one a ] ⇒ [ a : cn ⊢ one a ];
The text was updated successfully, but these errors were encountered:
The exception is raised during abstraction because g2 is missing an LF type annotation in [g1, g2, a : cn |- single].
More importantly, Beluga does not support contexts having two context variables.
Beluga crashes with an uncaught exception,
on the following minimal working example:
The text was updated successfully, but these errors were encountered: