Provide good indication of all constants’ real names and types

[mn200]

show_types works tolerably well for indicating the types of variables and some constants. But when a constant is involved in a special syntactic form (typically an infix) or is overloaded polymorphically, the user gets nothing back at all. For example,

- load "integerTheory";
- show_types := true;
- ``x + y``;
> val it = ``(x: int) + (y:int)`` : term

No indication that + is really int$+, though it's easy enough (given knowledge about the theories) to see that this is so. With show_types on,

- ``LENGTH``;
> val it = ``(LENGTH : α list -> num)`` : term

(good). But also:

- Define`SUC (n:int) = n + 1`;
> val it = |- ∀(n :int). SUC n = n + (1 :int) : thm

(bad) and

- ``SUC``;
<<HOL message: more than one resolution of overloading was possible>>
> val it = ``SUC`` : term

(also bad).

For the last example, I'd like to see

``SUC : int -> int``

as this case isn't.

Worse, I'm not sure what the output should be in the following scenario. Just annotating the SUC with its type is not sufficient:

- Define`SUC (n:num) = n - 1`;
Definition has been stored under "SUC_def"
> val it =
   |- ∀(n :num). SUC n = n − (1 :num) : thm

- ``SUC x``;
<<HOL message: more than one resolution of overloading was possible>>
> val it = ``SUC (x :num)`` : term

- dest_term (rator it);
> val it =
   CONST
    {Ty = ``:num -> num``,
     Thy = "scratch", Name = "SUC"} : lambda

[mn200]

My feeling now is that it's impossible to get this information printed only when it's needed.

So, instead, my attitude is that the information can be provided for all constants through backend annotations. Unfortunately, this means that people using less capable backends (raw or vt100 as opposed to emacs) will not see this solution.