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.

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

Assertion failure #1523

Closed
wintersteiger opened this Issue Aug 28, 2018 · 3 comments

Comments

Projects
None yet
2 participants
@wintersteiger
Contributor

wintersteiger commented Aug 28, 2018

I don't expect this to work as the implicit n can't be inferred:

module Bug
open FStar.UInt
let _ =  assert (forall i. add_mod (lognot i) 1 = sub_mod 0 i)

But, it currently triggers an assertion violation:

(Error) ASSERTION FAILURE: (<input>(3,36-3,42)) CheckNoUvars: Unexpected unification variable remains: (*?u4330*) _
F* may be in an inconsistent state.
@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Aug 28, 2018

Contributor

A smaller repro:

assume val f : #a:Type -> list a -> list a
let _ =  assert (l_Forall (fun i -> f i == f i)) // just what (forall i. f i == f i) desugars to
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("(A.fst(4,36-4,37)) CheckNoUvars: Unexpected unification variable remains: (*?u17*) _")

What I think is happening is that the typechecker is elaborating the assertion to:

l_Forall #?u1 (fun (i:?u2) -> eq2 #?u3 (f #?u4 i) (f #?u5 i))

and then solving each of them, via a new uvar

l_Forall #(list ?u17) (fun (i:list ?u17) -> eq2 #(list ?u17) (f #?u17 i) (f #?u17 i))

which is not being tracked in the internal guards.

Contributor

mtzguido commented Aug 28, 2018

A smaller repro:

assume val f : #a:Type -> list a -> list a
let _ =  assert (l_Forall (fun i -> f i == f i)) // just what (forall i. f i == f i) desugars to
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("(A.fst(4,36-4,37)) CheckNoUvars: Unexpected unification variable remains: (*?u17*) _")

What I think is happening is that the typechecker is elaborating the assertion to:

l_Forall #?u1 (fun (i:?u2) -> eq2 #?u3 (f #?u4 i) (f #?u5 i))

and then solving each of them, via a new uvar

l_Forall #(list ?u17) (fun (i:list ?u17) -> eq2 #(list ?u17) (f #?u17 i) (f #?u17 i))

which is not being tracked in the internal guards.

@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Aug 28, 2018

Contributor

I thought the culprit was here

let tx = UF.new_transaction () in
begin
match solve_t env eq_prob ({wl' with defer_ok=false; attempting=sub_probs}) with
| Success _ ->
let wl = {wl' with attempting=rest} in
let g = List.fold_left (fun g p -> U.mk_conj g (p_guard p))
eq_prob.logical_guard
sub_probs in
let wl = solve_prob' false (TProb tp) (Some g) [] wl in
let _ = List.fold_left (fun wl p -> solve_prob' true p None [] wl) wl bounds_probs in
UF.commit tx;
solve env wl
where its ignoring the implicits returned by the call to solve_t. Adding those implicits to the worklist gives saner errors for both programs above, but memory usage explodes wildly. Also, other places seem to ignore them, so it might be that I'm interpreting incorrectly. Anyway, that tip might help :)

Contributor

mtzguido commented Aug 28, 2018

I thought the culprit was here

let tx = UF.new_transaction () in
begin
match solve_t env eq_prob ({wl' with defer_ok=false; attempting=sub_probs}) with
| Success _ ->
let wl = {wl' with attempting=rest} in
let g = List.fold_left (fun g p -> U.mk_conj g (p_guard p))
eq_prob.logical_guard
sub_probs in
let wl = solve_prob' false (TProb tp) (Some g) [] wl in
let _ = List.fold_left (fun wl p -> solve_prob' true p None [] wl) wl bounds_probs in
UF.commit tx;
solve env wl
where its ignoring the implicits returned by the call to solve_t. Adding those implicits to the worklist gives saner errors for both programs above, but memory usage explodes wildly. Also, other places seem to ignore them, so it might be that I'm interpreting incorrectly. Anyway, that tip might help :)

mtzguido added a commit that referenced this issue Oct 8, 2018

mtzguido added a commit that referenced this issue Oct 8, 2018

tc: rel: tracking implicits that were being lost
Calling solve_t might return new implicits, which we must again keep
track of. To make sure we don't duplicate the implicits we're tracking,
we do the call with an empty list of implicits, and then we append the
result to the implicits we were already carrying.

c.f. #1443 and #1523
@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Oct 8, 2018

Contributor

I have a fix in that PR. The culprit was indeed there, and the memory explosion was because my previous change was stupidly duplicating the tracked implicits, leading to an exponential amount. Should be good now, and will merge after Nik reviews.

Contributor

mtzguido commented Oct 8, 2018

I have a fix in that PR. The culprit was indeed there, and the memory explosion was because my previous change was stupidly duplicating the tracked implicits, leading to an exponential amount. Should be good now, and will merge after Nik reviews.

mtzguido added a commit that referenced this issue Oct 9, 2018

tc: rel: tracking implicits that were being lost
Calling solve_t might return new implicits, which we must again keep
track of. To make sure we don't duplicate the implicits we're tracking,
we do the call with an empty list of implicits, and then we append the
result to the implicits we were already carrying.

c.f. #1443 and #1523

@mtzguido mtzguido closed this Oct 12, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment