Stack overflow on rewrite

[mtzguido]

Isolated example. Adding the irreducible qualifier makes it work. Using the projector directly has the same problem (hence we believe this a problem in handling the match)

noeq
type vcode = {
    t : Type u#2;
    up : t -> v:vprop;
}

// irreducible // makes it work
let up_code (code:vcode) (c:code.t) : (v:vprop{v == code.up c}) = code.up c

```pulse
fn spawn' (code:vcode) (pre:code.t)
    requires up_code code pre
    ensures  emp
{
  let task_st = true;
  rewrite (up_code code pre)
  as
    (match task_st with
     | true -> up_code code pre
     | _ -> emp);
  admit();
}
```

The errors:

* Error 17 at share/pulse/examples/Bug24.fst(14,0-27,3):
  - Tactic logged issue:
  - Stack overflow
  - Raised within Tactics.refl_check_relation
  - > While running primitive Pulse.Main.check_pulse (plugin)
    > While normalizing a term
    > While running splice with a tactic
    > While typechecking the top-level declaration `%splice_t[Bug24.spawn'] (...)`

* Error <unknown> at share/pulse/examples/Bug24.fst(19,21-25,10):
  - Tactic logged issue:
  - rewrite: could not prove equality of
  - ((up_code code) pre)
  - (match task_st with
        | true  -> ((up_code code) pre)
        |uu___#1158  -> emp (residual_comp:vprop))
  - > check_rewrite @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > Tm_Rewrite @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > check_bind @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > Tm_Bind @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > check_assert @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > Tm_ProofHintWithBinders @ share/pulse/examples/Bug24.fst(19,21-25,10)
    > check_bind @ share/pulse/examples/Bug24.fst(19,2-25,10)
    > check_tot_bind @ share/pulse/examples/Bug24.fst(19,2-25,10)
    > Tm_TotBind @ share/pulse/examples/Bug24.fst(19,2-25,10)

proof-state: State dump @ depth 13 (at the time of failure):
Location: Pulse.Typing.Env.fst(405,2-405,31)
* Error 228 at share/pulse/examples/Bug24.fst(14,8-14,8):
  - Tactic failed
  - "Pulse checker failed"
  - Stack trace:
    Raised by primitive operation at FStar_Compiler_Util.stack_dump in file "fstar-lib/FStar_Compiler_Util.ml", line 129, characters 53-82
    Called from FStar_Errors_Msg.backtrace_doc in file "fstar-lib/generated/FStar_Errors_Msg.ml", line 43, characters 12-45
    Called from FStar_Errors.maybe_add_backtrace in file "fstar-lib/generated/FStar_Errors.ml", line 824, characters 32-65
    Called from FStar_Errors.raise_error_doc in file "fstar-lib/generated/FStar_Errors.ml", line 939, characters 27-50
    Called from FStar_Tactics_Hooks.splice.(fun) in file "fstar-lib/generated/FStar_Tactics_Hooks.ml", line 1821, characters 33-1023
    Called from FStar_Errors.with_ctx in file "fstar-lib/generated/FStar_Errors.ml", line 1013, characters 27-31
    Called from FStar_TypeChecker_Tc.tc_decl'.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 3448, characters 19-123
    Called from FStar_Errors.with_ctx in file "fstar-lib/generated/FStar_Errors.ml", line 1013, characters 27-31
    Called from FStar_TypeChecker_Tc.tc_decls.process_one_decl in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 4798, characters 20-102
    Called from FStar_TypeChecker_Tc.tc_decls.process_one_decl_timed in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 4889, characters 15-159
    Called from FStar_Compiler_Util.fold_flatten in file "fstar-lib/FStar_Compiler_Util.ml", line 770, characters 30-37
    Called from FStar_Syntax_Unionfind.with_uf_enabled in file "fstar-lib/generated/FStar_Syntax_Unionfind.ml", line 107, characters 12-16
    Called from FStar_TypeChecker_Tc.tc_decls in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 4907, characters 8-170
    Called from FStar_TypeChecker_Tc.tc_partial_modul.(fun) in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5095, characters 25-77
    Called from FStar_TypeChecker_Tc.tc_modul in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5175, characters 20-44
    Called from FStar_TypeChecker_Tc.check_module in file "fstar-lib/generated/FStar_TypeChecker_Tc.ml", line 5355, characters 22-39
    Called from FStar_Universal.tc_one_file.tc_source_file.check_mod.check.(fun) in file "fstar-lib/generated/FStar_Universal.ml", line 1086, characters 29-141
    Called from FStar_Universal.with_tcenv_of_env in file "fstar-lib/generated/FStar_Universal.ml", line 130, characters 65-73
    Called from FStar_Universal.tc_one_file.tc_source_file.check_mod in file "fstar-lib/generated/FStar_Universal.ml", line 1107, characters 21-134
    Called from FStar_Universal.tc_one_file in file "fstar-lib/generated/FStar_Universal.ml", line 1180, characters 32-49
    Called from FStar_Universal.tc_one_file_from_remaining in file "fstar-lib/generated/FStar_Universal.ml", line 1328, characters 16-98
    Called from FStar_Universal.tc_fold_interleave in file "fstar-lib/generated/FStar_Universal.ml", line 1360, characters 19-71
    Called from FStar_Universal.batch_mode_tc in file "fstar-lib/generated/FStar_Universal.ml", line 1405, characters 20-72
    Called from FStar_Main.go in file "fstar-lib/generated/FStar_Main.ml", line 230, characters 36-124
    Called from FStar_Compiler_Util.record_time in file "fstar-lib/FStar_Compiler_Util.ml", line 26, characters 14-18
    Called from FStar_Main.main.(fun) in file "fstar-lib/generated/FStar_Main.ml", line 348, characters 28-62
    Called from Dune__exe__Main.x in file "fstar/main.ml", line 19, characters 6-24
  - See also Pulse.Typing.Env.fst(405,2-405,31)
  - > While running splice with a tactic
    > While typechecking the top-level declaration `%splice_t[Bug24.spawn'] (...)`

Unexpected error
FStar_Errors.Error(_)
Raised at BatString.find_from.find in file "src/batString.ml", line 112, characters 31-46
Called from BatString.split_on_string_comp.loop in file "src/batString.ml", line 410, characters 19-43

This may be an F* bug.

[mtzguido]

This is just FStarLang/FStar#3224, to be fixed in a few minutes.