Variable not found?

[cpitclaudel]

The following snippet gives me a surprising error:

let rec f (x: option nat) : unit =
  match x with
  | Some s -> g s
  | _ -> ()
and g s = ()

$ fstar.exe bug933.fst
./bug933.fst(3,11-3,12): (Error) Variable "x#151053" not found
1 error was reported (see above)

Is this expected?

[kyoDralliam]

Minimizing just a tiny bit nore, the following still fails

let rec f x =
  match x with
  | Some s -> g s
  | _ -> ()
and g s = ()

but this verifies successfully

let rec f x =
  match x with
  | Some s -> g s
  | _ -> ()
and g s : unit = ()

It's a blind guess but I think we are generating a non-well formed decreasing clause in this case...

[nikswamy]

Looking at this with @mtzguido

It does seem to have something to do with the decreases clauses.

We minimized it to:

module Test
let rec f (x:int) : unit = g x
and g (y:int) = ()

When checking the body of f we add a termination check to the recursively bound g, giving it the type:

x:Prims.int |- y':Prims.int{Prims.precedes y' x} ->  ((?u @ (Prims.int -> Type)) y')

However, after type-checking f this variable ?u in type of g gets solved to (fun (z:Prims.int{Prims.precedes z x}) -> Prims.unit). This is actually a type-incorrect solution for ?u since the type of this lambda term has a smaller domain type.

Later, when type-checking the body of g. we again check the recursively bound type of g strengthened with a termination check, but this time in a different environment, i.e., only with the formal parameter of g.

y:Prims.int |- y':Prims.int{Prims.precedes y' y} -> ((fun (z:Prims.int{Prims.precedes z x}) -> Prims.unit) y')

And this fails because x is not in scope.

So much for the diagnosis. We don't yet know what a good fix would be.

For the record, the types actually printed out when debugging the compiler are:

Checking let rec annot: x#22:Prims.int |- (y#24:(y#24:Prims.int{(Prims.precedes y@0 x#22)}) -> Tot ((?26371 @ (y#14:Prims.int -> Type)) y@0))
Checking let rec annot: y#197:Prims.int |- (y#199:(y#199:Prims.int{(Prims.precedes y@0 y#197)}) -> Tot ((fun x#22:(y#27:Prims.int{(Prims.precedes y@0 x#22)}) -> Prims.unit) y@0))

[cpitclaudel]

Another, much smaller instance of this error (though I'm not sure whether it's the same problem:

let rec f #a =
  match f with

$ fstar.exe bug933b.fst
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Bound term variable not found (after unmangling): uu___#151164 in environment: _#0, a#151177, uu___#151176, uu___#151175, f, f, false_elim, ignore, __proj__Mkdtuple4__item___4, __proj__Mkdtuple4__item___3, __proj__Mkdtuple4__item___2, __proj__Mkdtuple4__item___1, uu___is_Mkdtuple4, Mkdtuple4, dtuple4, __proj__Mkdtuple3__item___3, __proj__Mkdtuple3__item___2, __proj__Mkdtuple3__item___1, uu___is_Mkdtuple3, Mkdtuple3, dtuple3, dsnd, dfst, __proj__Mktuple8__item___8, __proj__Mktuple8__item___7, __proj__Mktuple8__item___6, __proj__Mktuple8__item___5, __proj__Mktuple8__item___4, __proj__Mktuple8__item___3, __proj__Mktuple8__item___2, __proj__Mktuple8__item___1, uu___is_Mktuple8, Mktuple8, tuple8, __proj__Mktuple7__item___7, __proj__Mktuple7__item___6, __proj__Mktuple7__item___5, __proj__Mktuple7__item___4, __proj__Mktuple7__item___3, __proj__Mktuple7__item___2, __proj__Mktuple7__item___1, uu___is_Mktuple7, Mktuple7, tuple7, __proj__Mktuple6__item___6, __proj__Mktuple6__item___5, __proj__Mktuple6__item___4, __proj__Mktuple6__item___3, __proj__Mktuple6__item___2, __proj__Mktuple6__item___1, uu___is_Mktuple6, Mktuple6, tuple6, __proj__Mktuple5__item___5, __proj__Mktuple5__item___4, __proj__Mktuple5__item___3, __proj__Mktuple5__item___2, __proj__Mktuple5__item___1, uu___is_Mktuple5, Mktuple5, tuple5, __proj__Mktuple4__item___4, __proj__Mktuple4__item___3, __proj__Mktuple4__item___2, __proj__Mktuple4__item___1, uu___is_Mktuple4, Mktuple4, tuple4, __proj__Mktuple3__item___3, __proj__Mktuple3__item___2, __proj__Mktuple3__item___1, uu___is_Mktuple3, Mktuple3, tuple3, snd, fst, __proj__Mktuple2__item___2, __proj__Mktuple2__item___1, uu___is_Mktuple2, Mktuple2, tuple2, __proj__Inr__item__v, uu___is_Inr, __proj__Inl__item__v, uu___is_Inl, Inr, Inl, either, invertOption, __proj__Some__item__v, uu___is_Some, uu___is_None, Some, None, option, allow_inversion, inversion, all_trivial, all_null_wp, all_assume_p, all_assert_p, all_close_wp, all_stronger, all_if_then_else, all_bind_wp, all_return, all_ite_wp, all_wp_h, all_post_h, all_pre_h, raise, lift_div_exn, ex_trivial, ex_null_wp, ex_assume_p, ex_assert_p, ex_close_wp, ex_stronger, ex_if_then_else, ex_ite_wp, ex_bind_wp, ex_return, ex_wp, ex_post, ex_pre, ex_pre, __proj__Err__item__msg, uu___is_Err, __proj__E__item__e, uu___is_E, __proj__V__item__v, uu___is_V, Err, E, V, result, st_trivial, st_null_wp, st_assume_p, st_assert_p, st_close_wp, st_stronger, st_ite_wp, st_if_then_else, st_bind_wp, st_return, st_wp_h, st_post_h, st_pre_h, assert_norm, normalize, normalize_term, string_of_int, string_of_bool, abs, min, pow2, pow2, op_Division, op_Modulus, nonzero, nonzero, pos, pos, nat, nat, cut, _assert, admitP, unsafe_coerce, magic, admit, _assume, as_ensures, as_requires, LexTop, lex_t, lex_t, returnM, decreases, smt_pat_or, smt_pat, pattern, pattern, __proj__Cons__item__tl, __proj__Cons__item__hd, uu___is_Cons, uu___is_Nil, Cons, Nil, list, strcat, array, exn, exn, op_disEquality, op_Equality, op_LessThan, op_GreaterThanOrEqual, op_GreaterThan, op_LessThanOrEqual, op_Minus, op_Addition, op_Subtraction, op_Multiply, op_Negation, op_BarBar, op_AmpAmp, int, int, guard_free, pure_wp, pure_post, pure_pre, pure_pre, range_of, labeled, string, string, range_0, range_0, range, range, l_Exists, __proj__Mkdtuple2__item___2, __proj__Mkdtuple2__item___1, uu___is_Mkdtuple2, Mkdtuple2, dtuple2, prop, prop, l_Forall, has_type, precedes, l_not, l_iff, l_imp, l_or, __proj__Right__item___0, uu___is_Right, __proj__Left__item___0, uu___is_Left, Right, Left, c_or, l_and, __proj__And__item___1, __proj__And__item___0, uu___is_And, And, c_and, b2t, eq3, uu___is_HRefl, HRefl, h_equals, eq2, uu___is_Refl, Refl, equals, l_False, l_False, l_True, l_True, squash, unit, unit, uu___is_T, T, c_True, c_True, c_False, c_False, bool, bool, eqtype, eqtype, hasEq, cps, cps, attribute, attribute
./bug933b.fst(4,2-0,0): (Error) Patterns are incomplete
./bug933b.fst(4,8-4,9): (Error) Failed to resolve implicit argument of type '(a:uu___151164{ a << a })' introduced in uu___unification_ 26315 a
2 errors were reported (see above)```

[theolaurent]

Just ran into this bug. Trying to minimize it gave me Generalizing the types of these mutually recursive definitions requires an incompatible set of universes for f and g for

let rec f b = match b with
  | None -> ()
  | Some t -> ()
and g t = ()

Don't know whether or not the two are related. Maybe it deserves a separate issue?

EDIT: see https://github.com/FStarLang/FStar/issues/1480

[mtzguido]

Possibly related, and also to #1091. Annotating the return type of eq_int_list fixes it.

#set-options "--use_two_phase_tc false"

let rec eq_int_list (l m :list int) (* : bool *) =
  match l, m with
  | [], [] -> true
  | l::ls, m::ms -> l = m && eq_int_list ls ms
  | _ -> false

Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("Bound term variable not found  l#36 in environment: ...,CAbstractStruct, uu___#768, ls#766")

[mtzguido]

This issue seems mostly gone. Here's the current status. Everything succeeds or fails as expected, expected perhaps the universe errors:

module T

let rec f1 (x: option nat) : unit =
  match x with
  | Some s -> g1 s
  | _ -> ()
and g1 s = ()

// Universe failure:
// T.fst(9,0-13,13): (Error 189) Expected expression of type "Type u#(U_name uu___687)"; got expression "uu___#698" of type "Type u#(U_name uu___686)"
// T.fst(11,14-11,16): (Error 287) Failed while checking implicit ?158 set to uu___#698 of expected type Type u#(U_name uu___687)

[@(expect_failure [189;287])]
let rec f2 x =
  match x with
  | Some s -> g2 s
  | _ -> ()
and g2 s = ()

// Fails due to termination (OK)
[@(expect_failure [19])]
let rec f3 (x:nat) : unit = g3 x
and g3 (yyy:int) = ()

// Works fine
let rec f4 (x:nat) : unit = if x > 0 then g4 (x-1)
and g4 (y:int) = ()

// The scrutinee gets instantiated, we fail to resolve that implicit (expected)
[@(expect_failure [66])]
let rec f5 #a =
  match f5 with

// (Error 89) Generalizing the types of these mutually recursive definitions requires an incompatible set of universes for T.f6 and T.g6
[@(expect_failure [89])]
let rec f6 b = match b with
  | None -> ()
  | Some t -> ()
and g6 t = ()

#set-options "--use_two_phase_tc false"

(* OK *)
let rec eq_int_list (l m :list int) =
  match l, m with
  | [], [] -> true
  | l::ls, m::ms -> l = m && eq_int_list ls ms
  | _ -> false

[mtzguido]

Vincent found a fresh repro here: https://github.com/FStarLang/FStar/issues/2052#issuecomment-693575145

[mtzguido]

New repro

let rec all #a (pred : a -> bool) (l : list a) : bool =
  match l with
  | [] -> true
  | x::xs -> pred x && all pred xs

type pattern = | Pat_Cons of list pattern

let rec faithful_pattern (p : pattern) =
  match p with
  | Pat_Cons pats -> all faithful_pattern_arg pats

and faithful_pattern_arg (pb : pattern) =
  false