Clarify rules for default Apply vs Chain behavior and Explicit vs Implicit arguments about lambda-mountain HOT 4 OPEN

Apply Explicit is formally well-defined and sound atm.

f := λ(: x X)(: y Y). x y;

from lambda-mountain.

Apply Implicit is just a hidden variable.

f := λ(: x X)(: y Y)(implicit z Z). x y;

f x y

reduces to

f x y z

Implicit parameters are applied "after" specialization. A visible candidate a : B - > C could become a : (ImplicitX,B) -> C.

from lambda-mountain.

Chain Explicit is either Cons or Apply by default before specialization.

chain := λ(: f (->(X Y)))(: x X). apply f x;
chain := λ(: l L)(: r R). Cons l r;

from lambda-mountain.

Chain Implicit is responsible for both implicit parameters and calling apply. There is nothing complicated about this if it is entirely mechanical. Chain Implicit is the single most direct access to the application syntax: f x calls chain implicits f x after all the sugar gets taken off.

chain := λ(implicit ctx FunctionContext)(: x X)(: y Y). (
   chain (with (ctx ctx) x) (with (ctx ctx) y)
);

from lambda-mountain.