For example, let us think about the following example. Here, let us assume that + is only defined pertaining to Real.
reserve A,B for Real;
C,D for Nat;
L:C=A+B;
......
D=A by...;
then C=D+B by L;
Let us assume that C=A+B and D=A are demonstrated when A,B is Real and C is Nat. At this point, if we substitute D=A to a formula C=A+B and make C=D+B by L, it will be an error. It is because D and B have different modes. A calculation unit + is only defined to Real and it is not defined to Nat. Therefore, an error of unknown functor will appear.
This error can be taken care of by extending the mode of variable D. It will be fine if we can state that D is Nat as well as Real.