Stack overflow on reflection typing

[mtzguido]

module Unk

open FStar.Tactics.V2

let must_check (g:env) (e:term) (ty:term) : Tac (typing_token g e (E_Total, ty)) =
  match core_check_term g e ty E_Total with
  | Some tok, _ -> tok
  | None, issues -> 
    log_issues issues;
    fail "tc failed"

let l1 = [1]

let test () : Tac unit =
  let g = cur_env () in
  let t1 = (`l1) in
  let _ = must_check g t1 (`list int) in
  ()

let _ = assert True by test ()

$ ./bin/fstar.exe Unk.fst 
proof-state: State dump @ depth 1 (at the time of failure):
Location: Unk.fst(10,4-10,20)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

* Error 17 at Unk.fst(20,0-20,30):
  - Tactic logged issue:
  - Stack overflow

* Error 228 at Unk.fst(20,8-20,14):
  - Tactic failed
  - "tc failed"
  - See also Unk.fst(10,4-10,20)

2 errors were reported (see above)

[aseemr]

Without looking into why it loops : ), we should add typing hypotheses to the reflection tc APIs. This code would then fail to typecheck, and if we call must_check with list u#0 int, it succeeds.

[mtzguido]

Oh right! I forgot about that :).

I ran into this while trying to repro a weirdness I found in Pulse actually. I was trying to check some term i (which had type inv p for some p) at type inv _ (with a Tm_unknown), expecting it to fail... but it succeeded, seemingly returning a guard with an equality containing the Tm_unknown. I couldn't find a standalone repro though... this is as close as I got, not sure why.

But, if we add the preconditions that terms are elaborated, then it would automatically rule out terms with Tm_unknowns, so we'd be good, right?

[aseemr]

Yeah, that should rule it out. E.g., if we had:

val core_check_term #u (g:env) (e:term) (t:typ { universe_of g t u }) (eff:tot_or_ghost)
  : Tac (ret_t (typing_token g e (eff, t)))