search

Beluga-lang / Beluga

Contextual types meet mechanized metatheory!
http://complogic.cs.mcgill.ca/beluga/
GNU General Public License v3.0
184 stars 16 forks source link

Uncaught exception: "missing type information" #268

Open ryanakca opened 1 year ago

ryanakca commented 1 year ago

Beluga crashes with an uncaught exception,

-*- 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 ];
MartyO256 commented 1 year ago

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.