Add annotations to System F
Before this MR, the ML program (t : some a . ty) would elaborate into elab((t : some a. ty)) := elab(t).
This can hide issues with the inference engine; for example our inference engine could have just completely ignored annotations, and you would never notice the difference on well-typed programs. (We mostly test using well-typed programs, especially in the random generator.)
@omartino and myself are starting to work on rigid variables, and there the question of elaborating annotations becomes even more interesting: we want an elaboration for (fun x -> x : for a. a -> a) that enforces polymorphism in the elaborated System F term -- (Fun a. fun (x:a) -> x : forall a. a -> a) [tau] for tau the instantiation witness.
In preparation for these questions, the current MR introduces annotations in System F, and elaborates ML annotations into System F annotations. We now have elab(t : some a. ty) := (elab(t): elab(ty)[tau/a]), where tau is the witness of a. (One could add type-level lets and elaborate into (elab(t) : let a = tau in elab(ty)) to respect sharing, but I did not bother.)
