Weird warning for instance declarations of bad type

[felixwellen]

When writing something like this:

instance _ = Set

I get the following error message:

Terms marked as eligible for instance search should end with a
name, so `instance' is ignored here.
when checking the definition of _

It should be more helpful to write more or less, what the manual says:

Terms marked as eligible for instance search should be of type {Γ} → C vs, 
where C is a postulated name, a bound variable, or the name of a data or record type [...]

[andreasabel]

... where C is a postulated name, a bound variable,

More precise:

where C evaluates to a postulated name...

I think bound variable is no longer a valid form for instances. That should also be fixed in the docs.

[felixwellen]

I think bound variable is no longer a valid form for instances. That should also be fixed in the docs.

Yes:

addTypedInstance x t = do
  (tel , n) <- getOutputTypeName t
  case n of
    OutputTypeName n -> addNamedInstance x n
    OutputTypeNameNotYetKnown{} -> addUnknownInstance x
    NoOutputTypeName -> warning $ WrongInstanceDeclaration
    OutputTypeVar -> warning $ WrongInstanceDeclaration
    OutputTypeVisiblePi -> warning $ InstanceWithExplicitArg x

[felixwellen]

I'm a bit confused that the following checks without warning:

module _ (B : Set) where
  use : {{t : B}} → B
  use {{t}} = t

but when we declare an instance of the type, there is a warning:

module _ (B : Set) where
  postulate b : B
  instance _ = b
  use : {{t : B}} → B
  use {{t}} = t

produces:

Terms marked as eligible for instance search should be of type {Γ}
→ C vs, where C evaluates to a postulated name or the name of a
data or record type, so `instance' is ignored here.
when checking the definition of _

(That's already the new warning message from #6381)

[felixwellen]

Never mind everyone, I got it and have to update #6381 ...

[felixwellen]

For instance declarations, I would stick with the warning message above. For the types of instance arguments, I think the following makes sense (it is at least something I would have understood):

InstanceNoOutputTypeName b -> fsep $
      pwords "Instance arguments whose type is not {Γ} → C vs, where C evaluates to a variable or the name of a data or record type, are never considered by instance search," ++
      pwords "so having an instance argument" ++ [return b] ++ pwords "has no effect."