Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Stange failure with unbound variable #3102

Closed
mtzguido opened this issue Nov 17, 2023 · 0 comments · Fixed by #3105
Closed

Stange failure with unbound variable #3102

mtzguido opened this issue Nov 17, 2023 · 0 comments · Fixed by #3105
Assignees
@mtzguido

Comments

@mtzguido
Copy link
Member 

open FStar.Tactics

let rtb_check_subtyping (g:env) (t1 t2:term) =
  let e2 = t2 in
  let res = Tactics.V2.Builtins.check_subtyping g t1 e2 in
  res

gives:

* Error 230 at Bug2.fst(7,53-7,55):
  - Variable "e2#11" not found
  - See also Bug2.fst(6,6-6,8)

1 error was reported (see above)
@mtzguido mtzguido self-assigned this Nov 17, 2023
mtzguido added a commit to mtzguido/FStar that referenced this issue Nov 18, 2023
@mtzguido
Tc: use extended environment for escape check
ae3e0cd 
Otherwise, the call to try_teq is wrong as one of the
terms cannot be typed in this environment. Also, wrap the whole
thing in a try/catch, and if something fails we can just report
that the variable escapes.

Fixes FStarLang#3102.
@mtzguido mtzguido mentioned this issue Nov 18, 2023
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@mtzguido mtzguido

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fixing the escape check to provide better errors mtzguido/FStar
1 participant
@mtzguido