Annotations are part of types in Michelson

I understand this is by design, but it is a bit counter-intuitive that stacks which contain elements of the same type with different annotations have a different type (besides, this only applies for branches).

For instance,

return int;
parameter int;
storage unit;
code { DROP;
       PUSH @zero int 0; DUP;
       PUSH int 1;
       ADD @zero_plus_one;
       PUSH bool True ;
       IF @res { DUP } { DUUP } ;
       DIP { DROP; DROP; PUSH unit Unit } ;
       PAIR };

is ill typed.

Worse,

return unit;
parameter unit;
storage unit;
code { PUSH bool True ;
       IF { DUP; CAR } { DUP; CDR } ;
       DIP { DROP } ; PUSH unit Unit;
       PAIR };

is also ill-typed.

From line 6 character 9 to line 17 character 80,
  two branches don't end with the same stack type:
  - first stack type:
    [ unit @parameter : pair (unit @parameter) (unit @storage) ],
  - other stack type:
    [ unit @storage : pair (unit @parameter) (unit @storage) ].
The two annotations do not match:
  - @parameter
  - @storage

This can be reproduced on the zeronet branch.