normalize_term fragile wrt let-binding

[amosr-msft]

normalize_term isn't evaluating here, and I'm not sure why. when we let-bind the argument, it does evaluate.

(* discrepancy with normalize_term behaviour in assertions vs refinement types *)
module Error.NormalizeArguments

(* Refinement check, checks that all elements in list >= 0
  For this counterexample, seems to need a recursive function here *)
let imports_valid (imps: list int): bool =
  List.Tot.for_all (fun imp -> imp >= 0) imps

let check_config_bad (imps: list int { normalize_term (b2t (imports_valid imps)) }) =
  imps

let check_config_good (imps: list int): Pure (list int) (requires (normalize_term #bool (imports_valid imps))) (ensures (fun _ -> True)) =
  imps

// disable fuel to ensure the normalizer does the proof. this just helps with minimising the example.
// without these, we can still reproduce the issue, but the test case needs to be big enough to be too hard for SMT alone.
#set-options "--fuel 0 --ifuel 0"
#set-options "--no_smt"

// version with precondition works
let p_config_good0_ok =
  check_config_good [ 0 ]

// version with refinement works when let-bound
let p_config_bad0_ok =
  let ls = [ 0 ] in
  check_config_bad ls

// inlining `ls` in above fails
let p_config_bad0_fails =
  check_config_bad [ 0 ]

// I'd expect normalize_term here to let us prove this too - but it doesn't without the call to compute ()
let _ =
  assert (
    normalize_term #bool
    (imports_valid [ 0; ]))
    by (
      // Tactics.compute ();
      Tactics.dump "X")