The idea is that I can use (annotate 'MTYPE ...) only in the mytype_operation_definitions, but nowhere else.
def_opaque_type MYTYPE would also fail if (annote 'MYTYPE) has been called before.
Actually, you could probably do that (if you really want to) by overriding the 'annotate function and using a 'locked* list, so that you can only annotate an object with a type name that is not already in the locked* list :
(redef annotate (type obj)
(if (mem type locked*)
(err "This type is locked")
(old type obj)))
Here, 'old is a "keyword" of 'redef that calls the old version of 'annotate (the unprotected one, that cannot be accessed from outside anymore).
And how do you unlock it for the constructors that are supposed to do the proper locking?
Hmm.
(let real-annotate annotate
(def theorem (f)
(if (check-f-is-valid-theorem f)
(real-annotate 'theorem f)
(err "Not a valid theorem")))
(= annotate
(fn (type obj)
(if (is type 'theorem)
(err "Spank! Spank! Under the boots of your master!!")
(real-annotate tpye obj)))))
It does have the drawback that you can't, say, reload the file, but hey, you did say you didn't want anyone else to create theorems except by that method, so even redefining that method won't work!
It seems like you want to re-create an idiom from another programming language in arc. What is the language you come from and how would the standard solution to your problem look in it?