adamc@191: datatype option a = None | Some of a
adamc@191: 
adamc@191: val none : option int = None
adamc@191: val some_1 : option int = Some 1
adamc@191: 
adamc@191: val f = fn t ::: Type => fn x : option t =>
adamc@191:         case x of None => None | Some x => Some (Some x)
adamc@191: 
adamc@191: val none_again = f none
adamc@191: val some_1_again = f some_1