Detection of always True conditions

[treiher]

Show an error for always True conditions in message links and refinements.

Example

package Test is

   type Protocol is (PROTO_X) with Size => 8;

   type M is
      message
         Protocol : Protocol;
         Data : Opaque
            with Size => 0;
      end message;

   type X is null message;

   for M use (Data => X)
      if Protocol = PROTO_X;

end Test;

It should be detected that Protocol = PROTO_X is always True, as Protocol has only one value.

[jklmnn]

Clarification: Always true conditions should be detected in all cases (not just on refinements). If detected they should throw an error. If we notice at some point that an error is too restrictive, we may replace it with a warning.