Stack overflow on Core.check_equiv

[mtzguido]

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

let x = true
let tt : term = `(Mkvcode?.up)

let _ = assert True by (
  let g = cur_env () in
  let u = check_equiv g tt (`(match x with | true -> Mkvcode?.up)) in
  match u with
  | Some u, _ ->
    dump "ok"
  | _, [] ->
    dump "fail and no issue?"
  | _, i::is ->
    dump (FStar.Issue.render_issue i)
)

and

let _ = assert True by (
  let g = cur_env () in
  let u = tc_term g (`(fun projectee -> match projectee as proj_ret returns Mkvcode?.t proj_ret -> int with | Mkvcode t up -> up)) in
  match u with
  | Some u, _ ->
    dump "ok"
  | _, [] ->
    dump "fail and no issue?"
  | _, i::is ->
    dump (FStar.Issue.render_issue i)
)

both fail with a stack overflow. The bug is in the core typechecker, in the case for a matches with returns annotations. Posting a PR now.