predefined identifiers can be redefined

[tinelli]

This signature is legal:

(declare A type)
(define type A)
(declare a A)
(check (: type a ))

Being able to redefine type seems dangerous. It can lead to confusing error messages later. The same applies to mpz and mpq.