Hi I don't know if it is theoretically sound or possible, but it would be helpful, if the typing of match-with statements with polymorphic variants was able to remove one or more variants from the "catch-all" cases In the following code, it would mean that three_is_a_lot would be typed like three_is_a_lot_2 without having to write all the cases. # let how_much = function | 1 -> `One | 2 -> `Two | 3 -> `Three | n -> `A_lot;; val how_much : int -> [> `A_lot | `One | `Three | `Two ] = # let three_is_a_lot x = match how_much x with | `Three -> `A_lot | any -> any;; val three_is_a_lot : int -> [> `A_lot | `One | `Three | `Two ] = # let three_is_a_lot_2 x = match how_much x with | `Three -> `A_lot | `One | `Two | `A_lot as any -> any;; val three_is_a_lot_2 : int -> [> `A_lot | `One | `Two ] = The practical use-case for us is that we use polymorphic variants to encode "semantic" errors in an Error/Result monad. What does the list think? Cheers, Sebastien