Some scoping failures

[mtzguido]

Posting to get an issue number and making PR with fix soon. It's not like --defensive always works, but we really make it so. I'll add this file to regressions as a first step.

#set-options "--defensive error"

open FStar.Tactics.V2

val fa_cong : unit -> unit
let fa_cong (u1:unit) =
  let do1 (u2:unit) : Tac unit =
    let t = (`()) in
    let l = Cons #term t Nil in
    ()
  in
  ()

val ex_cong : unit -> unit
let ex_cong () =
  let t () : Tac unit =
    admit();
    let [ex] = l_intros () in
    ()
  in
  ()

val is_true : term -> Tac bool
let is_true t =
    begin match term_as_formula' t with
    | True_ -> true
    | x1 -> begin match inspect t with
           | Tv_App l r -> true
           | x2 -> false
           end
    end

$ ../master/bin/fstar.exe Bug.fst 
* Error 290 at Bug.fst(7,14-7,18):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u0*) _ _
  - FVs = [uu___#23]
  - Scope = []
  - Diff = [uu___#23]

* Error 290 at Bug.fst(7,14-7,18):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True /\ (Prims.hasEq _ ==> Prims.l_True)) _
  - FVs = [uu___#23]
  - Scope = []
  - Diff = [uu___#23]

* Error 290 at Bug.fst(7,14-7,26):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u4*) _ _
  - FVs = [uu___#29]
  - Scope = []
  - Diff = [uu___#29]

* Error 290 at Bug.fst(7,14-7,26):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True) _
  - FVs = [uu___#29]
  - Scope = []
  - Diff = [uu___#29]

* Error 290 at Bug.fst(7,14-7,18):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u5*) _ _
  - FVs = [uu___#33]
  - Scope = []
  - Diff = [uu___#33]

* Error 290 at Bug.fst(7,14-7,18):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True /\ (Prims.hasEq _ ==> Prims.l_True)) _
  - FVs = [uu___#33]
  - Scope = []
  - Diff = [uu___#33]

* Error 290 at Bug.fst(7,14-7,26):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u9*) _ _
  - FVs = [uu___#39]
  - Scope = []
  - Diff = [uu___#39]

* Error 290 at Bug.fst(7,14-7,26):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True) _
  - FVs = [uu___#39]
  - Scope = []
  - Diff = [uu___#39]

* Error 290 at Bug.fst(7,22-7,26):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u2*) _ _
  - FVs = [uu___#26]
  - Scope = [uu___#22]
  - Diff = [uu___#26]

* Error 290 at Bug.fst(7,22-7,26):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True /\ (Prims.hasEq _ ==> Prims.l_True)) _
  - FVs = [uu___#26]
  - Scope = [uu___#22]
  - Diff = [uu___#26]

* Error 290 at Bug.fst(7,22-7,26):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u7*) _ _
  - FVs = [uu___#36]
  - Scope = [uu___#32]
  - Diff = [uu___#36]

* Error 290 at Bug.fst(7,22-7,26):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True /\ (Prims.hasEq _ ==> Prims.l_True)) _
  - FVs = [uu___#36]
  - Scope = [uu___#32]
  - Diff = [uu___#36]

* Error 290 at Bug.fst(8,0-14,4):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u16*) _ _
  - FVs = [uu___#211]
  - Scope = [t#55; u2#45; u1#43]
  - Diff = [uu___#211]

* Error 290 at Bug.fst(8,0-14,4):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True) _
  - FVs = [uu___#211]
  - Scope = [t#55; u2#45; u1#43]
  - Diff = [uu___#211]

* Error 290 at Bug.fst(9,14-9,18):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u1*) _ _
  - FVs = [uu___#46]
  - Scope = [u1#43]
  - Diff = [uu___#46]

* Error 290 at Bug.fst(9,14-9,18):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True /\ (Prims.hasEq _ ==> Prims.l_True)) _
  - FVs = [uu___#46]
  - Scope = [u1#43]
  - Diff = [uu___#46]

* Error 290 at Bug.fst(9,26-9,30):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u3*) _ _
  - FVs = [uu___#50]
  - Scope = [u2#45; u1#43]
  - Diff = [uu___#50]

* Error 290 at Bug.fst(9,26-9,30):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True /\ (Prims.hasEq _ ==> Prims.l_True)) _
  - FVs = [uu___#50]
  - Scope = [u2#45; u1#43]
  - Diff = [uu___#50]

* Error 290 at Bug.fst(9,26-9,30):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u5*) _ _
  - FVs = [uu___#53]
  - Scope = [u2#45; u1#43]
  - Diff = [uu___#53]

* Error 290 at Bug.fst(9,26-9,30):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True) _
  - FVs = [uu___#53]
  - Scope = [u2#45; u1#43]
  - Diff = [uu___#53]

* Error 290 at Bug.fst(11,18-11,22):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u6*) _ _
  - FVs = [uu___#59]
  - Scope = [t#55; u2#45; u1#43]
  - Diff = [uu___#59]

* Error 290 at Bug.fst(11,18-11,22):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True) _
  - FVs = [uu___#59]
  - Scope = [t#55; u2#45; u1#43]
  - Diff = [uu___#59]

* Error 290 at Bug.fst(11,23-11,24):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u7*) _ _
  - FVs = [uu___#75]
  - Scope = [t#55; u2#45; u1#43]
  - Diff = [uu___#75]
  - See also Bug.fst(10,8-10,9)

* Error 290 at Bug.fst(11,23-11,24):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True) _
  - FVs = [uu___#75]
  - Scope = [t#55; u2#45; u1#43]
  - Diff = [uu___#75]
  - See also Bug.fst(10,8-10,9)

* Error 290 at Bug.fst(11,25-11,28):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = Prims.list a
  - FVs = [a#77]
  - Scope = [t#55; u2#45; u1#43]
  - Diff = [a#77]
  - See also prims.fst(594,10-594,16)

* Error 290 at Bug.fst(11,25-11,28):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u9*) _ _
  - FVs = [uu___#93]
  - Scope = [t#55; u2#45; u1#43]
  - Diff = [uu___#93]

* Error 290 at Bug.fst(11,25-11,28):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True) _
  - FVs = [uu___#93]
  - Scope = [t#55; u2#45; u1#43]
  - Diff = [uu___#93]

* Error 290 at Bug.fst(12,4-12,6):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u11*) _ _
  - FVs = [uu___#110]
  - Scope = [l#94; t#55; u2#45; u1#43]
  - Diff = [uu___#110]

* Error 290 at Bug.fst(12,4-12,6):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True) _
  - FVs = [uu___#110]
  - Scope = [l#94; t#55; u2#45; u1#43]
  - Diff = [uu___#110]

* Error 290 at Bug.fst(14,2-14,4):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (*?u14*) _ _
  - FVs = [uu___#204]
  - Scope = [do1#188; u1#43]
  - Diff = [uu___#204]

* Error 290 at Bug.fst(14,2-14,4):
  - Internal: term is not well-scoped (normalize_with_primitive_steps call)
  - t = (fun _ -> Prims.l_True) _
  - FVs = [uu___#204]
  - Scope = [do1#188; u1#43]
  - Diff = [uu___#204]

31 errors were reported (see above)