datatype list datasort list : odd < list; even < list datacon Nil : even datacon Cons : int * odd -> even && int * even -> odd val double_tail : (odd -> odd) && (even -> even) && (list -> list) fun double_tail xs = let in case xs of Nil => raise Match | Cons (h, t) => let val tail : (t : odd >:> even,, t : even >:> odd) val tail = case t of Nil => raise Match | Cons (_, inner_t) => inner_t in tail end end val print_list : list -> unit fun print_list xs = case xs of Nil => print "nil" | Cons (h, t) => let in print (Int.toString h); print "::"; print_list t end val loss : list val loss = (Cons (1, Cons (2, Cons (3, Nil)))) val q = double_tail loss val _ = print_list q val _ = print "\n\n"