Wrong order of quantifiers with type variables

[mezpusz]

Vampire sometimes produces output where type variables come after types that depend on them, such as the following line:

tff(f7336,plain,(
  ! [X0 : assn,X1 : list(X2),X2 : $tType, ...

Then, for example GDV complains about X2 not being quantified.
This can be reproduced with:

-p tptp --decode dis+1010_32:1_sil=2000:bsd=on:fd=off:slsq=on:random_seed=161430699:cts=off:i=1282:sd=1:av=off:gtg=position:ss=axioms_2877 $TPTP/Problems/ITP/ITP218_2.p

A couple of other occurrences:

• -p tptp --decode lrs+10_7_to=lpo:sil=64000:tgt=ground:drc=off:fde=none:sp=const_frequency:slsqc=4:slsq=on:random_seed=3561718340:i=10680:bd=all:gtg=exists_sym_2779 $TPTP/Problems/ITP/ITP220_4.p
• -p tptp --decode lrs+1002_1_to=lpo:sil=2000:sos=on:random_seed=1239504037:i=1674:sd=3:ss=axioms:sgt=16_2958 $TPTP/Problems/ITP/ITP222_4.p
• -p tptp --decode lrs+10_3_sil=8000:tgt=ground:fde=none:sp=reverse_arity:lcm=predicate:random_seed=3224555319:i=3317:sd=1:av=off:ss=axioms:sgt=50_2790 $TPTP/Problems/ITP/ITP223_4.p
• -p tptp --decode lrs+1002_1_to=lpo:sil=2000:sos=on:random_seed=2065495457:i=1674:sd=3:ss=axioms:sgt=16_2959 $TPTP/Problems/ITP/ITP225_4.p

[quickbeam123]

Yes, this is horrible!

We discussed this with Ahmed a few years ago. I wanted to propose we never merge type-forall and object-forall. We could even enforce it by having a different quantifier KIND. In any case, the fix is not small, as far as I remember, as all of parsing, preprocessing and printing need to be updated.

[mezpusz]

Then it's worse than I thought.. we can delay it until HOL/polymorphism becomes a more popular use case.

[MichaelRawson]

Couldn't we just move all the $tType variables to the front of the block (at least when printing, if not actually structurally)?

[quickbeam123]

For sure we could sort when printing.

I just thought we should maybe be more explicit about type quantification for our own future's sanity's sake ;)

(Not sure whether TPTP itselfs allows the mixing in a single block. I vaguely remember we do it to ourselves during Rectify, maybe.)