Warning when implicit arguments are not inferred in the definition of a synonym

[nad]

When I define a function I sometimes follow roughly the following procedure to avoid making too many arguments implicit:

• Use two names in the type signature and let one name be a synonym of the other:

  f g : Something
  f = …
  g = f
  

• Tweak the type signature until all meta-variables are solved in the body of the synonym.

This does not guarantee that all implicit arguments will always be inferred, but it does ensure that there is at least one invocation of the function for which all implicit arguments are inferred.

I would like Agda to do this work for me, or rather a variant where g is defined by g x1 … xn = f x1 … xn, where n is the number of explicit arguments in the type of f (as obtained by telView). This could be an optional warning: if there are unsolved meta-variables in the body of "g", then Agda could complain (by highlighting the name f in the type signature of f and presenting a suitable warning message). I think it would make sense to delay this test until there are no unsolved meta-variables in the type signature of f.

What do you think?

[JacquesCarette]

Surprised that no one's commented yet: yes, this does seem like a rather handy feature. I've certainly seen a lot of noise on social media from people who think that figuring out which arguments are reasonably safe to make implicit is a "black art" - I'd think this would help.