Spliced symbols end up with wrong attributes, leading to unification failures

[nikswamy]

Consider this program:

module Repro
open Proj

assume
val t : nat -> Type0
noeq
type test = {
    x:nat;
    y:t x;
}
%splice[x_of_test;
        y_of_test]
       (mk_projs (`%test)
                 ["x_of_test";
                   "y_of_test"])
let x_of_test_alt = x_of_test
#push-options "--debug Repro --debug_level Rel,ExplainRel"
let prob (i:test) (f:t (x_of_test_alt i))
  : t (x_of_test i)
  = f

On the command line, it fails with

(Repro.fst(18,19-18,20)) Failed to solve the sub-problem

224:    Repro.x_of_test_alt i
                =
        Repro.x_of_test i

Which arose because:
        index
        >Top-level:
Repro.t (Repro.x_of_test_alt i)
        <:
Repro.t (Repro.x_of_test i)
Failed because:head mismatch (Repro.x_of_test_alt (Delta_constant_at_level 2) vs
 Repro.x_of_test (Delta_constant_at_level 999))
Repro.fst(20,4-20,5): (Error 189) Expected expression of type "Repro.t (R
epro.x_of_test i)"; got expression "f" of type "Repro.t (Repro.x_of_test_alt i)"
 (see also Repro.fst(18,19-18,20))
1 error was reported (see above)

Interestingly, it succeeds in interactive mode in emacs. The delta_constant 999 is clearly suspicious and Reflection.Basic sets that in pack_fv. Not sure why that doesn't manifest with --ide.

A prerequisite for this example is the projector-generator tactic for records, shown below.

module Proj

open FStar.List.Tot
open FStar.Tactics

let mkproj (unf:list string) (np:nat) (i:nat) : Tac unit =
  let _ = ignore (repeatn (np+1) intro) in
  let b = nth_binder (-1) in
  let r = t_destruct b in
  // dump "GGG";
  // FIXME: if this is just t_destrcut (nth_binder (-1)), this tactic
  // fails when loaded from another file... ????
  match r with
  | [(cons, arity)] -> begin
    if (i >= arity) then
      fail "bad index";
    let bs = repeatn (arity+1) (fun () -> intro ()) in
    // dump "1";
    rewrite (nth_binder (-1));
    // dump "2";
    norm [iota; delta_only unf];
    // dump "3";
    match List.Tot.nth bs i with
    | None -> fail "impossible, but I should be able to prove it"
    | Some b -> exact b
    end
  | _ ->
    fail "no"

exception NotFound

let subst_map (ss : list (bv * fv)) (r:term) (t : term) : Tac term =
  // dump ("before = " ^ term_to_string t);
  let t = fold_left (fun t (x, fv) -> subst x (mk_e_app (Tv_FVar fv) [r]) t) t ss in
  // dump ("after  = " ^ term_to_string t);
  t

let rec embed_list_string (e : list string) : Tac term =
  match e with
  | [] -> `Nil
  | s::ss ->
    (`(`#(Tv_Const (C_String s))) :: (`#(embed_list_string ss)))

let mk_proj_decl proj_name (tyqn:name) ctorname univs indices (params:list binder) (idx:nat) (fieldty : typ)
                 (unfold_names : list string)
                 (smap : list (bv & fv))
: Tac (sigelt & fv)
=
  let np = List.Tot.length params in
  let ni = List.Tot.length indices in
  let tyfv = pack_fv tyqn in
  let fv = pack_fv (cur_module () @ [proj_name]) in
  let rty : binder = fresh_binder (mk_e_app (pack (Tv_FVar tyfv))
                                   (map binder_to_term (params @ indices)))
  in
  let projty = mk_tot_arr (List.Tot.map (binder_set_qual Q_Implicit) params
                           @ List.Tot.map (binder_set_qual Q_Implicit) indices
                           @ [rty])
                          (subst_map smap (binder_to_term rty) fieldty)
  in
  let lbdef =
    (`(_ by (mkproj (`#(embed_list_string unfold_names))
                        (`#(Tv_Const (C_Int (np+ni))))
                        (`#(Tv_Const (C_Int idx))))))
  in
  let lb = pack_lb ({ lb_fv = fv; lb_us= univs; lb_typ=projty; lb_def = lbdef}) in
  let sv
    : sigelt_view
    = Sg_Let false [lb]
  in
  // dump ("returning : " ^ term_to_string (quote sv));
  (pack_sigelt sv, fv)

#push-options "--fuel 2"
let rec zip #a #b (x:list a) (y:list b { length x == length y })
  : list (a & b)
  = match x, y with
    | [], [] -> []
    | x::xs, y::ys -> (x,y) :: zip xs ys

let mk_projs (tyname:string) (proj_names:list string) : Tac decls =
  let tyqn = explode_qn tyname in
  match lookup_typ (top_env ()) tyqn with
  | None ->
    raise NotFound
  | Some se ->
    match inspect_sigelt se with
    | Sg_Inductive ctorname univs params typ ctors ->
      if (List.Tot.length ctors <> 1) then
        fail "expected a record";
      let indices = fst (collect_arr_bs typ) in
      let [ctor] = ctors in
      let (fields, _) = collect_arr_bs (snd ctor) in
      if (List.Tot.length proj_names <> List.Tot.length fields)
      then fail "Not enough record names";
      let field_projectors = zip fields proj_names in
      let (decls, _, _, _) =
        fold_left (fun (decls, smap, unfold_names, idx) (field, proj_name) ->
                     let (d, fv) = mk_proj_decl proj_name tyqn ctorname univs indices params idx (type_of_binder field) unfold_names smap in
                     (d::decls,
                      (bv_of_binder field,fv)::smap,
                      (implode_qn (inspect_fv fv))::unfold_names,
                      idx+1))
                  ([], [], [], 0)
                  field_projectors
      in
      List.Tot.rev decls
    | _ ->
      fail "not an inductive"
#pop-options