Type checking of the eval parameter

[bodeveix]

We have noticed that eval does not perform type checking anymore on its parameter. For example, the test proof is accepted while the eval parameter is not correctly typed vs the #assume profile. We wonder if it is the expected behaviour?

require open tests.OK.Tactic;

//constant symbol #assume : String → Π [a:Set], (τ a → Tactic) → Tactic;
//builtin "assume" ≔ #assume;

constant symbol OK: Prop;

symbol test [a:Set] (x: τ a) : π OK → π OK ≔
begin
  assume a;
  eval (#assume "x" (λ (x: τ a), #assume "h" (λ (h: π OK), #apply h)));
end;

[fblanqui]

Hi JP. The argument of eval, here (#assume "x" (λ (x: τ a), (#assume "h" (λ (h: π OK), #apply h)))), is type-checked by LP. However, we do not check that it is of type Tactic. We should certainly do that. But we cannot do more.

[bodeveix]

The second #assume is not well typed vs the signature of #assume. π OK is not a τ _. The type error appears if we replace eval ... by set tac := ... In the previous version, such a term was (rightly) rejected.

By adding an embedding of Prop into Set (throw the function σ), we can use #assume on both Set and Prop in a typed way. In the following, the tactic is type-checked by the set command before being evaluated.

require open tests.OK.Tactic;
//constant symbol #assume : String → Π [a:Set], (τ a → Tactic) → Tactic;
//builtin "assume" ≔ #assume;

injective symbol σ: Prop → Set;
rule π $p ↪ τ (σ $p);

constant symbol OK: Prop;
symbol test [a:Set] (x: τ a) : π OK → π OK ≔
begin
  assume a;
  set tac ≔ (#assume "x" (λ (x: τ a),
                          (#assume "h" (λ (h: π OK), #apply h))));
  eval tac;
end;

[fblanqui]

So you say that this is normal that your first example is rejected because one needs an embedding of Prop into Set, either by adding σ or by declaring o:Set and τ o ↪ Prop as in Stdlib.Impred. So, what's the issue?

[bodeveix]

No, the first example is not rejected but it should be rejected as the argument of eval is not well typed. Putting the argument in an auxiliary variable using the set tactic behaves as expected: set is rejected.

The second example is well typed thanks to the sigma mapping and is accepted as it should do.

[fblanqui]

Which version of lambdapi do you use? Because, on master, the first example is rejected...

[tmp/1447.lp:11:2-69] 
Tactic
is not unifiable with
Π x0:(π OK → Tactic), ?7.
Cannot solve typing constraints for [#assume "x" (λ x, #assume "h" (λ h, #apply h))]

[bodeveix]

I have made the test on my current version which is the last dk/master with conditional rules. It is thus a side effect of my modifications. Sorry...

I have solved the problem on my version by adding the test !p.unsolved = [] in the management of P_tac_eval in tactic.ml:

      | Some(t,_) ->                                                            
        if Unif.solve_noexn p && !p.unsolved = [] then                          
          let ps, t = p_tactic ps g env pos t in handle ps t                    
        else fatal pos "Cannot solve typing constraints for [%a]" term t