Expressing a hierarchy within a type-system with ADT and (possibly) GADT

Question

In my type-system I want to support promotable types, where an Int would be promoted to a Double if used with division, and String to StringBuffer if used with concatenation. Can I express this with agebraic data-types, so the compiler would throw a type error if it tried to promote the wrong type?

E.g.:

type ty =
  | Int
  | Double
  | String
  | StringBuffer
  | Promotable of ref ty

But, Int can only be promoted to Double, not StringBuffer or String.

Using GADT:

type _ ty =
  | Int : arith ty
  | Double : arith ty
  | String : text ty
  | StringBuffer : text ty
  | Promotable of ref ty : ... ??

Where arith and text need to be a type "family" (kind, type class)? Can I express this in OCaml?

Thanks in advance!

Edit: Example usage based on answer below:

let promote : type a. a ty -> a ty = function
  | Promotable (Int, IntToDouble) ->Double (* StringBuffer here would not type-check *)
  | Promotable (String, StringToStringBuffer) -> StringBuffer
  | t -> t

Answer 1

You could have another GADT describing what the hierarchy is and then expect a proof to be handed to you when someone tries to promote a value. E.g.:

type arith
type text

type (_ , _) lessThan =
  | IntToDouble          : (arith, arith) lessThan
  | StringToStringBuffer : (text, text) lessThan

type _ ty =
  | Int          : arith ty
  | Double       : arith ty
  | String       : text ty
  | StringBuffer : text ty
  | Promotable   : 'ref ty * ('ref, 'promo) lessThan -> 'promo ty