Support projection-like definitions

[flupe]

As always, Agda's projection-like optimization is a pain in the.

Consider the following file:

record Pair (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

myfst : {A B : Set} → Pair A B → A
myfst = Pair.fst

Without projection-like, so with the --no-projection-like flag enabled, we get the following typed Lambox environment:

Pair:
  mutual inductive(s):
    Pair
    type variables:  [A, B]
      constructors:
        _,_ (2 arg(s))
          fst : @0
          snd : @1

fst:
  constant declaration:
    type variables: [A, B]
    type: Pair @0 @1 → @0
    body: λ _ → case<Pair{0},0> @0 of λ<[_, _]> @1

snd:
  constant declaration:
    type variables: [A, B]
    type: Pair @0 @1 → @1
    body: λ _ → case<Pair{0},0> @0 of λ<[_, _]> @0

myfst:
  constant declaration:
    type variables: [A, B]
    type: □ → □ → Pair @0 @1 → @0
    body: λ _ _ _ → fst @0

As expected, myfst gest two Box arguments that come from its type arguments A and B, but the rest of the signature refers to the type variables.

However, when the optimization is enabled, Agda detects that it is a projection, and drops the parameters in the function definition, and every time it is used.

myfst:
  constant declaration:
    type variables: [A, B]
    type: □ → □ → Pair @0 @1 → @0
    body: λ _ → fst @0

So its generated type no longer matches its actual body.

The question is: does it suffice to drop the first arguments of a projection-like function? How does it work with type variables generated from the record it operates on? Does it always operate on a record?

[flupe]

Another solution would be to eta-expand the body of the definition to account for the dropped parameters. But then, we shouldn't forget to also insert Boxes every time this projection-like function is used.