Allow default values to refer to previous arguments

[janmasrovira]

e- Currently default values can only refer to names available at the top scope (i.e. the scope where the function/constructor being defined is).
Sometimes it can be useful to refer to previos arguments. For instance consider the example given in #2427:

trait
type Ord A := mkOrd {
  cmp : A -> A -> Ordering
  < (x y : A) : Bool := case cmp x y of {
    | LT := true
    | _ := false
  };
  ..
};

In the default definition of < we need to refer to cmp.

Implementation

We briefly discussed online one possible way to implement this: If we have:

f {a : Nat := 0} {b : Nat := a + 1}  {c : Nat := a + b} := ...

Then if we find f we should generate the following:

let a := 0
     b := a + 1
     c := a + b
in f a b c;

Note that default arguments happens in FromConcrete.NamedArguments and in the aritychecker.
So if we have f {b := 1}, then the NamedArguments desugarer will generate

let a := _
     b := 1
in f {a} {b}

And the arity checker will introduce the final argument:

let a := _
     b := 1
in 
  let 
    c := a + b
   in  f {a} {b} {c}