Ill-formed decreases clause with two phase

[mtzguido]

When using --use_two_phase_tc true, this tutorial example

module Ex04e
//find

type option 'a =  
   | None : option 'a
   | Some : v:'a -> option 'a

(* val find (f : 'a -> bool) (l : list 'a) : option 'a *)
let rec find f l = match l with
  | [] -> None
  | hd::tl -> if f hd then Some hd else find f tl

fails unless the val is provided. The output is:

From its type f:(uu___2303:uu___2300 -> Prims.Tot Prims.bool) ->
l:Prims.list uu___2300 -> Prims.Tot (Ex04e.option uu___2300), the definition of `let rec find` expects a function with 3 arguments, but 1 argument was found
./doc/tutorial/code/exercises/Ex04e.fst(11,47-11,49): (Error 19) Subtyping check failed; expected type (l:Prims.list uu___2304{ l << Prims.LexTop }); got type Prims.list uu___2304 (see also ./doc/tutorial/code/exercises/Ex04e.fst(9,19-11,49))
Verified module: Ex04e (370 milliseconds)
1 error was reported (see above)

I see this used to be a hard error but was changed to print this first message instead. I think we enforced that check after the discussion on #1017. But in any case, this example should not fail, and it seems the amount of actuals is being messed up.

The formals are OK, they are indeed 3 (the 2 visible ones and the implicit). But I guess for the actuals it is just counting the immediate binders on the Tm_abs without normalizing/canonizing it.

Following that, we get a bogus decreases clause, I guess since the code that generates it also makes the same mistake of taking the immediate binders.

[mtzguido]

I have a tentative fix for both issues, running CI on it.

[mtzguido]

For the record the reason was indeed two consecutive Tm_abs nodes and the compiler only considering the first one. The first problem (actuals vs formals) was easy enough, but I'm still a bit confused about the one for the decreases clause.

What's going on is that decreases_clause is called with a list of binders equal to 'a, and a body of fun f l -> ..., but these binders should be on the other argument. Then we try to make a decreases "list" or "value" for this (ending up with LexTop) and for the actuals f and l, obtaining just l (since f is a function). Hence the clause obtained is l << LexTop.

My change for this is making sure to collect all binders when typechecking a let rec, because trying to do it for all abstractions caused a bunch of regressions. Seems to work, but waiting on CI.

How these two Tm_abs node get stuck together, I'm not sure. Looking at the compiler there doesn't seem to be any spot where we just make a Tm_abs node, but we always call abs. Maybe there's some other node in between that later gets removed, or a uvar involved...

[mtzguido]

CI said green.. I'll merge it, but maybe @aseemr would be interested in reviewing (cff6349 and 5503162).

[aseemr]

Hi Guido, the changes look good to me. I also brought back the error about actuals and formals that I changed to a print message earlier. I was thinking of eta expansion cases, but reading #1017, I can see that it is supposed to fail (since finding other binders in an arbitrary lbdef is hard, that's how I understand it).

[mtzguido]

Great, thanks!