Assertion failure in term.ml

[matijapretnar]

I encountered the following error in Abella 2.0.5 (and 2.0.4):

Error: File "src/term.ml", line 646, characters 10-16: Assertion failed

 Sorry for displaying a naked OCaml exception. An informative error message
 has not been designed for this situation.

 To help improve Abella's error messages, please file a bug report at
 <https://github.com/abella-prover/abella/issues>. Thanks!

I've tried to simplify my example and the best I could reduce it to can be found here.

Is there a workaround? Many thanks in advance!

[chaudhuri]

This is a weird bug that goes back to the pre 2.0.x days. I'll have to trace the type-checker to figure out what it's doing. Thanks for the report!

[chaudhuri]

A bit more tracing shows that this is being triggered by the logic programming engine. It is picking the wrong nominal to instantiate a nabla and then the type-checker complains.

Sorry, there doesn't appear to be a simple workaround. Thanks for the bug report. It's turning into a bit of a head-scratcher.

[matijapretnar]

Thanks for investigating! In the meantime, I have figured out how to simplify my formalization to avoid the bug (though it may reappear later), so there is no rush as far as I am concerned :) Good luck with finding a solution!

[yvting]

Here is what I found out.

The problem is that when deriving HH sequents from the hypotheses, Abella does not ensure that permutations of nominal constants respect types.

Coming back to Matija's example, the proof state is as follows when the assertion is made (where I annotated the nominal constant in H2 with its type for later explanation):

Variables: M Ty Ty' Knd
H2 : {of-knd (Ty' (n1:ty) Knd}
H3 : {of n1 Ty |- of n1 (Ty' Ty)}
============================
 true

When Abella searches for the derivability of {of (bar foo) Ty}, it will match it with the head of the second clause for of and create the (nomialized) subgoal {of (foo (n1:tm)) Ty}. This subgoal matches with the head of the first clause for of. Abella creates the following two subgoals after performing raising over n1:tm:

{pi ty\of-knd (Ty1' n1 ty) (Knd1 n1)}
{pi x\ of x Ty => of x (Ty1' n1 Ty)}

The first goal becomes of-knd (Ty1' (n1:tm) (n2:ty)) (Knd1 (n1:tm)) after normalization. When unifying it with H2, because Abella does not check compatibility of types for permutation of nominal constants, it will unify (n1:tm) in the goal with (n1:ty) in H2 and create the incorrect unifier Ty1' := n1 n2\Ty' n1. Under this substitution the subexpression (Ty1' n1 Ty) in the second subgoal becomes the ill-typed one Ty' (n1:tm). Hence the mentioned exception.

The fix is easy to implement. We only need to make ensure that permutation of nominal constants repsect types. I have pushed a fix to the branch norm_permute_fix. I have noticed the same problem when unifying metaterms and applied a similar fix.

[chaudhuri]

Thanks, yes, I had come to a similar conclusion earlier but had to put it aside because of other deadlines. I'll take a look at your branch at the end of the week. Sorry for dragging my feet on this.

Long term I am increasingly thinking that we need to move to explicit local contexts.

[matijapretnar]

Great, that also fixes my bigger original example. Thanks a lot!