Syntactic parametricity class search

[ecranceMERCE]

In order to constrain the various parametricity classes present in a type, the code must first find them. The procedure in charge of doing this seems to be very syntactic. It means that in the case of a term convertible to Type(α), such as the following constant, the class α would slip under the radar:

Definition T := Type.

Are there cases where this causes a problem in the translation?