Trivial match match 0 = 0 not reducing in typechecker

[amosr]

I came across an example that gives a type error where the actual type should reduce to the expected type. The normalizer seems to be getting stuck.

The type error is:

* Error 114 at example/No.Norm.fst(32,8-32,12):
  - Type of pattern (Prims.bool) does not match type of scrutinee (match 0 = 0 with
    | true -> FStar.List.Tot.Base.hd [Prims.bool; Prims.bool]
    | _ -> FStar.List.Tot.Base.index (FStar.List.Tot.Base.tl [Prims.bool; Prims.bool]) (0 - 1))

However, I would expect 0=0 to reduce to true, and hd [bool;bool] to reduce to bool.

The program (No.Norm.fst) is:

module No.Norm

module List = FStar.List.Tot

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)


let stepx (b1 b2: bool): bool =
   let estop =
         (index [bool; bool]
         (b1, (b2, ()))
         0)
   in
      match estop with
      | true -> false
      | false -> true

@mtzguido