Can't produce a object file

[NotBad4U]

The file below can not produce a corresponding object file when I run the command:

lambdapi check -c Test.lp
Checking "/Users/alessiocoltellacci/Junk/foo/Test.lp" ...
Writing "/Users/alessiocoltellacci/Junk/foo/Test.lpo" ...
Uncaught [File "src/core/sign.ml", line 182, characters 16-22: Assertion failed].

Moreover, the proof goal is complete and I can have a lambda term.

File "src/core/sign.ml", line 182, characters 16-22: Assertion failed

The error comes from this assertion line. I do not understand which Meta term is blocking Lambdapi.

constant symbol Prop : TYPE;
builtin "Prop" ≔ Prop;
injective symbol π : Prop → TYPE; // `p
builtin "P" ≔ π;

constant symbol Set : TYPE;
injective symbol τ : Set → TYPE;
builtin "T" ≔ τ;

constant symbol ⊥ : Prop; // \bot

constant symbol ⇒ : Prop → Prop → Prop; notation ⇒ infix right 5; // =>
rule π ($p ⇒ $q) ↪ π $p → π $q;

symbol ¬ p ≔ p ⇒ ⊥; // ~~ or \neg
notation ¬ prefix 35;

constant symbol ∀ [a] : (τ a → Prop) → Prop; notation ∀ quantifier; // !! or \forall
rule π (∀ $f) ↪ Π x, π ($f x);

injective symbol πᶜ p ≔ π (¬ ¬ p);

symbol ∀ᶜ [a] p ≔ `∀ x : τ a, ¬ ¬ (p x); notation ∀ᶜ quantifier;

opaque symbol ∀ᶜᵢ p : (Π x, πᶜ (p x)) → πᶜ (∀ᶜ p) ≔
begin
  assume p Hnnpx Hnnnpx;
  apply Hnnnpx;
  assume x Hnnp;
  apply Hnnpx x;
  assume Hnp;
  apply Hnnp;
  apply Hnp;
end;

This issue is relative to my PR #13 for the Stdlib.
I am not sure if it is a bug or if I am doing something wrong. I would appreciate an explanation of how the gen-obj process works 😄 .

[fblanqui]

It looks like a bug: some meta is left uninstanciated. This should not happen.

[fblanqui]

In your definition of ∀ᶜᵢ, you forgot the type argument a. But lambdapi should reject this definition anyway.

[fblanqui]

There should be 2 goals after begin. One for the missing type a.

[NotBad4U]

In your definition of ∀ᶜᵢ, you forgot the type argument a. But lambdapi should reject this definition anyway.

You mean doing something like this?

opaque symbol ∀ᶜᵢ [a] p : (Π x : τ a, πᶜ (p x)) → πᶜ (∀ᶜ p) ≔

I still can not create the a.lpo but yeah a was missing.

But lambdapi should reject this definition anyway.

I agree...Should we also add more information on the error message?

Uncaught [File "src/core/sign.ml", line 182, characters 16-22: Assertion failed].

I had to deep into the source code to understand what was going on and I thought that was Π in my definition that created trouble.