Using "@" in signatures makes type mismatch

[yoni206]

When using "@" inside a signature, there is a mismatch between the computed and expected types.

Example (the content of tmp.plf appears below):

$ lfscc sat.plf smt.plf tmp.plf
tmp.plf, line 11, column 10:
The type expected for an application does not match the computed type.

1. The expected type: (th_holds (= 0x22a7fb0 0x22a7f50 0x22a7f50))
2. The computed type: (th_holds (= 0x22a7fb0 0x2273880 0x2273880))

When replacing "(th_holds (= s tt tt))" with "(th_holds (= s t t))", the check is successful (no need to remove the "@" line).

tmp.plf

(declare tmp
(! s sort
(! t (term s)
(@ tt t
(th_holds (= s tt tt))))))

(check
(% s sort
(% t (term s)
(: (th_holds (= s t t))
(tmp s t))))))