Generalized variable blocks projection-likeness

[jespercockx]

Consider the following Agda file:

variable a : Set

data C (a : Set) : Set where

member : C a → a → a
member _ w = w

Running agda with -v tc.proj.like:50 reports the following:

checkDecl: checking projection-likeness of [RollbackWindow.C]
RollbackWindow.C is abstract or not a function, thus, not considered for projection-likeness
checkDecl: checking projection-likeness of [RollbackWindow.member, RollbackWindow..generalizedField-a,
 RollbackWindow.GeneralizeTel, RollbackWindow.mkGeneralizeTel]
mutual definitions are not considered for projection-likeness

and indeed the function is not considered to be projection-like. However, if one makes the {a : Set} -> explicit in the type of member then it is considered so:

checkDecl: checking projection-likeness of [RollbackWindow.C]
RollbackWindow.C is abstract or not a function, thus, not considered for projection-likeness
checkDecl: checking projection-likeness of [RollbackWindow.member]
Checking for projection likeness 
member  :  {a : Set} → C a → a → a
  candidates: [(RollbackWindow.C, 1)]
member  :  {a : Set} → C a → a → a
  is projection like in argument 1 for type C

[jespercockx]

Also, I do not understand why the function is considered projection-like when the type of the first visible argument is C a, but not when it is a. Why does the type of the unused argument matter for whether it is okay to drop?

[andreasabel]

Also, I do not understand why the function is considered projection-like when the type of the first visible argument is C a, but not when it is a. Why does the type of the unused argument matter for whether it is okay to drop?

Only functions of type (xs : As) (y : B xs) -> C can be projection-like, as far as I remember. The idea is that you should be able to infer the values of the dropped xs from the type of the first non-dropped argument y.

Projection-like or not does not matter for your example because there is never a stuck value of the form member foo bar.

[UlfNorell]

Here's where it actually matters:

{-# OPTIONS -v tc.proj.like:50 #-}

variable
  A B : Set

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

fst : A × B → A
fst (x , y) = x

checkDecl: checking projection-likeness of [Issue7530.fst, Issue7530..generalizedField-A,
 Issue7530..generalizedField-B, Issue7530.GeneralizeTel,
 Issue7530.mkGeneralizeTel]
mutual definitions are not considered for projection-likeness