Make the expression type a GADT

[filipeom]

Mainly resistant due to operators types. Maybe we could type operators like this?

(* ty.ml *)
type _ t =
  | Ty_int : [ `Ty_int ] t
  | Ty_real : [ `Ty_real ] t
  | Ty_bool : [ `Ty_bool ] t
  | Ty_str : [ `Ty_str ] t
  | Ty_bitv : int -> [ `Ty_bitv ] t
  | Ty_fp : int -> [ `Ty_fp ] t

type _ unop =
  | Abs : [< `Ty_real | `Ty_fp ] unop
  | Ceil : [< `Ty_real | `Ty_fp ] unop
  | Clz : [ `Ty_bitv ] unop
  | Ctz : [ `Ty_bitv ] unop
  | Floor : [< `Ty_real | `Ty_fp ] unop
  | Is_nan : [ `Ty_fp ] unop
  | Len : [ `Ty_str ] unop
  | Neg : [< `Ty_int | `Ty_real | `Ty_bitv | `Ty_fp ] unop
  | Nearest : [< `Ty_real | `Ty_fp ] unop
  | Not : [< `Ty_bitv | `Ty_bool ] unop
  | Sqrt : [< `Ty_real | `Ty_fp ] unop
  | Trim : [ `Ty_str ] unop
  | Trunc : [< `Ty_real | `Ty_fp ] unop

...