A deprecation function annotation.

[jfdm]

On the mailing list @david-christiansen suggested the creation of a deprecation annotation to aide in managing changes to Idris projects. Such an annotation could look like:

%deprecated PACKAGE VERSION COMMENT

where PACKAGE and VERSION are arbitrary strings with no spaces, or quoted strings, and COMMENT uses the same syntax as documentation (that is, Markdown as supported by Cheapskate).

Then, unless %deprecation off has been specified or Idris has been run with --no-deprecation-warnings, it would spit out a message like

<FILE>:<LINE NUM>:<COLUMN NUM>
When elaborating right hand side of <FNAME>:
  <DEPRECATED FNAME> is deprecated since version <VERSION> of <PACKAGE>. <COMMENT>

and each deprecation warning would be issued at most once per module to avoid having completely insane noise from something like the (Fin 10) 8.

For example, renaming an function fZ to FZ can be supported with the following annotation:

%deprecated Idris 0.9.15 Use `FZ` instead.
fZ : Fin n -> Fin (S n)
fZ = FZ

with the following error message if fZ is used in a function foo.

Foo.idr:30:15
When elaborating right hand side of foo:
  fZ is deprecated since version 0.9.15 of Idris. Use FZ instead.

[suhr]

Consider adding experimental/unstable/stable/frozen/locked annotations as well.

[Melvar]

A %deprecated annotation now exists, which does not take any details.