Type system with subtyping on abstract data types?

Question

Consider this example on binary trees in some ML-like language:

type tree =
  | Null
  | Node of tree * tree

let rotate_left p =
  match p with
  | Null -> p
  | Node (a, q) ->
    match q with
    | Null -> p
    | Node (b, c) ->
      Node (Node (a, b), c)

In the definition of rotate_left above I only want to consider rotation on trees where the right subtree is also a node:

let rotate_left (Node (a, Node (b, c))) =
  Node (Node (a, b), c)

In relation to a ML-like type system, this second version of rotate_left is partial where as the first version is total.

Is there a type system expressive enough that such functions would be considered total?

Note; I use the term "subtyping" in the title of this question, since I think of the values of the type of the second version of rotate_left, to be a subset of the values of the type of the first version of rotate_left.