Missing TCC in Abbreviated Subtype

[marianomoscato]

Some TCCs for subtype abbreviated forms are not being generated.

See, for example, the following theory.

test: THEORY
BEGIN
  p(b: above(3))(c: nat): bool = 3 <= b + c
  f(m: nat): (p(m)) = 3
END test

The only TCC generated after typechecking is

% Subtype TCC generated (at line 4, column 22) for  3
    % expected type  (p(m))
  % unfinished
f_TCC1: OBLIGATION FORALL (m: nat): p(m)(3);

Nevertheless, a subtype tcc should be generated for the apparition of m in the expression p(m) (line 4, column 14).

In fact, the missing TCC is generated when typechecking the following version of the theory, in which the return type of f is defined using the expanded form instead of the abbreviation.

test: THEORY
BEGIN
  p(b: above(3))(c: nat): bool = 3 <= b + c
  f(m: nat): {c: nat | p(m)(c)} = 3
END test

In such case, the TCCs generated by the typechecker are shown below.

% Subtype TCC generated (at line 4, column 26) for  m
    % expected type  above(3)
  % unfinished
f_TCC1: OBLIGATION FORALL (m: nat): m > 3;

% Subtype TCC generated (at line 4, column 35) for  3
    % expected type  {c: nat | p(m)(c)}
  % unfinished
f_TCC2: OBLIGATION FORALL (m: nat): p(m)(3);

This problem occurs both in PVS 6.0 and PVS 7.0.