Improve constructors' type-annotations

Currently, to build an option value for example, we have to explicitly and extensively specify the variant's type.

n_opt = (Some : [ None : unit | Some : nat] ) n

For named type it would be better to be able to give the type name.