[Agda] Instance search and type variables

[Pavel Perikov]

Hi everybody. 

I think my previous message did not get to the list. If it did please excuse the duplicate.


 record A  : Set₁ where
    field
      T : Set
      S : Set
      VarRelated : Set → Set → Set
      instance
        inst₁ : Related T S -- this works
        inst₂ : VarRelated T S -- but this fails with a bit misleading message "Terms marked as eligible for instance search should end with a name"

I failed to find any references for this behaviour. Can anyone explain while declaring inst₂ is prohibited? 


Any input is appreciated.

Best regards, Pavel