"Unary transform" raises some typechecker problems

[mtzguido]

The following fails to check, since a call to instantiate_implicits on Cons 12345 Nil <: list nat elaborates it to Cons #int 12345 (Nil #int) <: list nat, instantiating the implicit with int instead of nat, even with the ascriptions. I think F* is to blame

fn test (_:unit)
  requires emp
  ensures emp
{
  let x : list nat = [12345] <: list nat;
  ()
}

[mtzguido]

Ah! It's not F*, this works fine"

module X

open FStar.Tactics.V2

let _ = assert True by begin
  let t = `([12345] <: list nat) in
  let res = instantiate_implicits (cur_env()) t in
  match res with
  | Some (t, ty), _ -> print (term_to_string t)
  | _ -> fail "None?"
end

TAC>> Prims.Cons #Prims.nat 12345 (Prims.Nil #Prims.nat) <: Prims.list Prims.nat
Verified module: X
All verification conditions discharged successfully

It's the deep_transform_to_unary_applications pass that "breaks" it by making the typechecker work differently

steel/lib/steel/pulse/Pulse.Checker.Pure.fst

Lines 59 to 65 in 0dae0f0

	let rtb_instantiate_implicits g f t =
	debug g (fun _ -> Printf.sprintf "Calling instantiate_implicits on %s"
	(T.term_to_string t));
	(* WARN: unary dependence, see comment in RU *)
	let t = RU.deep_transform_to_unary_applications t in
	let res, iss = RTB.instantiate_implicits f t in
	match res with

[mtzguido]

Another symptom (lucky coincidence to find it just after this)

This

open Pulse.Lib.Pervasives
module GR = Pulse.Lib.GhostReference

noeq
type finv (p:vprop) = {
  r : GR.ref bool;
  i : inv emp;
}

 ```pulse
fn crash (p:vprop)
   requires emp
   ensures emp
{
   let r = GR.alloc false;
   let i = new_invariant' emp;
   let fi : finv p = { r=r; i=i } <: finv p;
   admit()
}
``

Fails with

* Error 17 at Crash.fst(14,0-25,3):
  - Tactic logged issue:
  - Invalid_argument("List.combine: list lengths differ")
  - Raised within Tactics.refl_instantiate_implicits

But works fine if the pass is removed.

[aseemr]

https://github.com/FStarLang/FStar/blob/fe6dec16fc4f0234663da63de26d9d2e72fe14df/src/typechecker/FStar.TypeChecker.TcTerm.fst#L2466

Also, this is the code in F* that solves the constraints eagerly.

[nikswamy]

The trouble with record literal syntax and unary transform is addressed here:
7b877db