bad_gadt.ml

module GADT = struct
  type 'a option = Some : 'a -> 'a option | None : 'a option

  let x = Some 1
  let y = None

  module Ty = struct
    type _ ty = Int : int ty | String : string ty

    let int = Int
    let string = String

    let f (type a) (ty : a ty) (x : a) =
      match ty with
      | Int ->
          let x : int = x in
          string_of_int x
      | String ->
          let x : string = x in
          x

    let _x = f int 1
    let _x = f string "a"
  end

  module Explicit_ty = struct
    module Eq = struct
      type (_, _) eq = Refl : ('a, 'a) eq

      let cast (type a b) (eq : (a, b) eq) (x : a) : b =
        match eq with Refl -> x

      let symm (type a b) (eq : (a, b) eq) : (b, a) eq =
        match eq with Refl -> eq
    end

    open Eq

    type 'a ty =
      | Int : ('a, int) eq -> 'a ty
      | String : ('a, string) eq -> 'a ty

    let int = Int Refl
    let string = String Refl

    let f (type a) (ty : a ty) (x : a) =
      match ty with
      | Int a_is_int ->
          let x : int = cast a_is_int x in
          string_of_int x
      | String a_is_string ->
          let x : string = cast a_is_string x in
          x

    let _x = f int 1
    let _x = f string "a"
  end

  module Univ = struct
    type _ ty = Int : int ty | String : string ty
    type dyn = Dyn : 'a. ('a * 'a ty) -> dyn

    (* forall a. a *)
    (* exists a. a *)

    let x = Dyn (1, Int)
    let x = Dyn ("a", String)

    let y =
      match x with
      | Dyn (type a) (content : a * a ty) -> (
          let x, ty = content in
          match ty with
          | Int ->
              let x : int = x in
              string_of_int x
          | String ->
              let x : string = x in
              x)

    let f (None : _ option) = ()

    let f (x : _ option) =
      let None = x in
      ()

    let f (x : _ option) = match x with None -> ()

    (* let <pat> = <expr> in <expr> 
       match <expr> with | <pat> -> <expr> 
       fun <pat> -> <expr>
       <expr> <expr>  *)
    let y =
      let (Dyn (type a) (content : a * a ty)) = x in
      let x, ty = content in
      match ty with
      | Int ->
          let x : int = x in
          string_of_int x
      | String ->
          let x : string = x in
          x
  end
end