`l_to_r` fails when there is subtyping?

[TWal]

l_to_r do not work in this case:

open FStar.Tactics

assume val length_cons: #a:Type -> x:a -> l:list a -> Lemma (List.Tot.Base.length (x::l) == (List.Tot.Base.length l) + 1)

[@@ expect_failure]
let test (h:int) (t:list int) =
  assert (List.Tot.Base.length (h::t) == List.Tot.Base.length t + 1) by (
    l_to_r [(`length_cons)];
    trefl()
  )

// Workaround, note the additional `<: nat`
assume val length_cons_weird: #a:Type -> x:a -> l:list a -> Lemma (List.Tot.Base.length (x::l) == ((List.Tot.Base.length l) + 1 <: nat))

let test2 (h:int) (t:list int) =
  assert (List.Tot.Base.length (h::t) == List.Tot.Base.length t + 1) by (
    l_to_r [(`length_cons_weird)];
    trefl()
  )

A workaround works by adding an explicit <: nat in the lemma.

[W95Psp]

As we were discussing with @TWal and @R1kM, the bug really seems to come (1) from how type inference happens with eq2 and (2) from unification.

Consider the following two top-levels foo and bar: every time, we try to unify x == ?u with x == 3, but foo fails to unify, while bar works flawlessly.

[@@expect_failure]  
let foo (x: nat) = assert True by (
    let t = quote (x == 3) in
    if not (unify (`(`@x == (`#(fresh_uvar None)))) t) 
    then fail "unification failed"
  )

let bar (x: nat) = assert True by (
    let t = quote (eq2 #nat x 3) in
    if not (unify (`(`@x == (`#(fresh_uvar None)))) t) 
    then fail "unification failed"
  )

The thing is that x == ?u is actually typed as eq2 #nat x ?u, while (in foo) x == 3 is actually eq2 #int x 3. Thus, unification fails when trying to unify nat with int: foo (leaving the == typing implicit) fails, while bar works, forcing == to compare nats. This is also confirmed by turning the flag --debug_level TacUnify on:

[F*] %%%%%%%%do_unify x == (*?u137*) _ =? x == 3
[F*] try_teq of x == (*?u137*) _ and x == 3 {
[F*] solve:
[F*] 	
[F*] 6783:	x == (*?u137*) _ 
[F*] 		=
[F*] 	x == 3
[F*] Attempting 6783 (Tm_app::x == (*?u137*) _ vs Tm_app::x == 3); rel = (=)
[F*] >> (6783) (smtok=false)
[F*] >>> head1 = Prims.eq2 [interpreted=false; no_free_uvars=false]
[F*] >>> head2 = Prims.eq2 [interpreted=false;no_free_uvars=false]
[F*] Heads match: x == (*?u137*) _ (Tm_app) and x == 3 (Tm_app)
[F*] Solving 6783: with [[UNIV 64 <- U_unif ?65:125.194]]
[F*] Adding subproblems for arguments (smtok=false): [
[F*] 6786:	Prims.nat 
[F*] 		=
[F*] 	Prims.int
[F*] ; 
[F*] 6785:	x 
[F*] 		=
[F*] 	x
[F*] ; 
[F*] 6784:	(* uvar_env *)
[F*] ((x: Prims.nat) |- ?137 : Prims.nat)  
[F*] 		=
[F*] 	3
[F*] ]
[F*] Solving 6783: with []
[F*] Solving 6783 ((* new_problem: logical guard for Top-level:
[F*] x == (*?u137*) _
[F*] 	=
[F*] x == 3 *)
[F*] ((x: Prims.nat) |- ?151 : Type0)) with formula (*?u153*) _ /\ (*?u152*) _ /\ (*?u154*) _
[F*] solve:
[F*] 	
[F*] 6786:	Prims.nat 
[F*] 		=
[F*] 	Prims.int
[F*] 
[F*] 	
[F*] 6785:	x 
[F*] 		=
[F*] 	x
[F*] 
[F*] 	
[F*] 6784:	(* uvar_env *)
[F*] ((x: Prims.nat) |- ?137 : Prims.nat)  
[F*] 		=
[F*] 	3
[F*] Attempting 6786 (Tm_fvar: nat::Prims.nat vs Tm_fvar: int::Prims.int); rel = (=)
[F*] >> (6786) (smtok=false)
[F*] >>> head1 = Prims.nat [interpreted=false; no_free_uvars=true]
[F*] >>> head2 = Prims.int [interpreted=false;no_free_uvars=true]
[F*] Attempting 6786 (Tm_refine::i: Prims.int{i >= 0} vs Tm_fvar: int::Prims.int); rel = (=)
[F*] Attempting 6786 (Tm_refine::i: Prims.int{i >= 0} vs Tm_refine::_: Prims.int{Prims.l_True}); rel = (=)
[F*] ref1 = (i#10549):(Prims.int){i >= 0}
[F*] ref2 = (_#0):(Prims.int){Prims.l_True}
[F*] solve:
[F*] 	
[F*] 6788:	i >= 0 
[F*] 		=
[F*] 	Prims.l_True
[F*] Attempting 6788 (Tm_app::i >= 0 vs Tm_fvar: l_True::Prims.l_True); rel = (=)
[F*] >> (6788) (smtok=false)
[F*] >>> head1 = Prims.b2t [interpreted=false; no_free_uvars=true]
[F*] >>> head2 = Prims.l_True [interpreted=false;no_free_uvars=true]
[F*] Trying match heuristic for x: Prims.unit{Prims.equals (i >= 0) true} vs. Prims.l_True
[F*] Heuristic not applicable: tag lhs=Tm_refine, rhs=Tm_fvar: l_True
[F*] Failed head mismatch (Prims.b2t (Delta_constant_at_level 1) vs Prims.l_True (Delta_constant_at_level 0)):
[F*] 
[F*] 6788:	i >= 0 
[F*] 		=
[F*] 	Prims.l_True
[F*] Failed head mismatch (Prims.b2t (Delta_constant_at_level 1) vs Prims.l_True (Delta_constant_at_level 0)):
[F*] 
[F*] 6788:	i >= 0 
[F*] 		=
[F*] 	Prims.l_True
[F*] (<input>(19,19-23,3)) Failed to solve the sub-problem
[F*] 
[F*] 6788:	i >= 0 
[F*] 		=
[F*] 	Prims.l_True
[F*] 
[F*] Which arose because:
[F*] 	refinement formula
[F*] 	>index
[F*] 	>Top-level:
[F*] x == (*?u137*) _
[F*] 	=
[F*] x == 3
[F*] Failed because:head mismatch (Prims.b2t (Delta_constant_at_level 1) vs Prims.l_True (Delta_constant_at_level 0))
[F*] } res = None
[F*] %%%%%%%%do_unify (RESULT None) x == (*?u137*) _ =? x == 3

A (rather painful) workaround is to take care of retyping lemmas correctly before applying them, but it is not reliable and very slow.