Normalize-by-evaluation gets stuck underneath a pattern-match

[amosr]

I ran into an issue where normalization got stuck evaluating a mostly-concrete term. After talking on Slack, @nikswamy was surprised that normalization-by-evaluation stops under pattern matches. @mtzguido also suggested zeta_full to force unfolding recursive functions, though that risks non-termination / stack overflow.

Here is a small-ish example.

NormGetsStuck.fst:

(* Test case: nbe seems to get stuck inside matches *)
module NormGetsStuck

module Tac = FStar.Tactics

module List = FStar.List.Tot

(* Helper definitions: heterogeneous lists *)
let rec row (l: list eqtype): Type =
  match l with
  | [] -> unit
  | t :: ts -> t * row ts

let rec index (l: list eqtype) (r: row l) (i: nat { i < List.length l}): List.index l i =
  match l with
  | t :: ts ->
    let r': t * row (List.tl l) = r in
    match r' with
    | (r0, rs) ->
      if i = 0
      then r0
      else (
        let res: List.index ts (i - 1) = index ts rs (i - 1) in
        coerce_eq #_ #(List.index l i) () res)

(* This is what we want to normalize. *)
let xxx (estop level_low: bool) =
  match estop with
  (* This index doesn't reduce: it seems to be blocked because it's inside the match *)
  | true -> index [Prims.bool; Prims.bool] (estop, (level_low, ())) 1
  | _    -> false

  (* It also fails to normalise when the arguments are all totally concrete values, eg: *)
  // | true -> index [Prims.bool; Prims.bool] (true, (false, ())) 1

let tac_extract () =
  (* I get the same result with or without nbe. Changing zeta to zeta_full does allow it to reduce. *)
  Tac.norm [nbe; primops; iota; zeta; delta];
  Tac.dump "tac_extract";
  Tac.trefl ()


// #push-options "--debug NormGetsStuck --debug_level NBE"
(*
 This reduces the above to give:
  Goal 1/1:
  |- _ : Prims.squash ((fun estop level_low ->
          match estop with
          | true ->
            NormGetsStuck.index [Prims.bool; Prims.bool]
              (estop, FStar.Pervasives.Native.Mktuple2 level_low ())
              1
          | _ -> false) ==
      (*?u16*)
      _)
 But I expected the NormGetsStuck.index to normalize to estop.
*)
[@@(Tac.postprocess_with tac_extract)]
let test (estop level_low: bool) = xxx estop level_low