[design] notion of context entry for binder term constructors

[gares]

Context

When working at the ppx to synthesize the glue code, it felt natural to link a "context" data type to the one of a data type with binders. Eg

type ctx = Decl of string * ty
type t = Lam of string * ty * (t [@binder (fun s ty -> Decl(s,ty))])

In this way the APIs can read back not only a term but also the context of binders under which it occurs. This requires the user to
systematically add a decl clause when moving under a binder, that is p (lam S TY F) :- pi x\ decl x S TY => ..F x...

Wish

This piece of info (the link between Lam's arguments and Decl) would also be useful in the implementation of spilling, which turns out to be very useful in Coq-Elpi and Hierarchy Builder.
For example:

some-pred T R :- typecheck T TY, some-more TY R.
main :- T = lam "x" bool x\ {some-pred x}.

The code after spilling should look like

main :- (pi x\ decl x "x" bool => some-pred x (Spill1 x)), T = lam "x" bool x\ (Spill1 x).

so that some-pred can call typecheck correctly (which requires the context entry decl x ... to be present).

Mock up

The proposal (up to syntax) would be to equip a type declaration with the piece of info that is attached to the ML code above, eg

type lam string -> ty -> (term --(s\t\x\ decl x s t)--> term) -> term.

Alternative & discussion

A "cheap" but also not 100% satisfactory alternative proposed by Dale was to have one special term constructor called binder.
In this way the ADT for terms would be

type decl string -> ty -> t -> prop.

type app t -> t -> t.
type binder (t -> prop) -> (t -> t) -> t.

then lam "x" bool x\ .. would be represented as binder (decl "x" bool) x\ ... and the idiom to cross it would be
p (binder B F) :- pi x\ B x => .. F x. In this setting the spilling problem is solved, since when one spills across binder he can just collect its first argument in order to build the context for the spilled computation.

I'm not in love with this because there is a little encoding step that is visible. Eg. in Coq we have 4+ binders (fun, prod, let and fix) and all but let create the same context entry so one would need to pass to binder some extra info, like "lam", and then you really start to see the encoding. Still this proposal clarifies very well what I'd like, it's just that I'd like the encoding to be performed behind the scenes. Also, then .. --(..)--> .. function space constructor can be used by a linter/checker to tell the user "hey, you forgot to use => after pi (if F has type .. --(C)--> .. then F x needs x to be used in a context where C x => is there.

CC @CohenCyril