Prohibiting invalid states with GADT - the airlock exercise

Community
10

Hm, anyone knows why this code doesn’t work?

module Airlock : sig
  type opened
  type closed
  type ('inner, 'outer) t

  val create : unit -> (closed, closed) t
  val print_inner_door : ('a, 'b) t -> unit
end = struct
  type opened = Opened
  type closed = Closed
  type ('inner, 'outer) t = State of 'inner * 'outer

  let create () = State (Closed, Closed)
  let print_inner_door : ('a, 'b) t -> unit = function
    | State (Closed, _) -> print_endline "Closed"
    | State (Opened, _) -> print_endline "Opened"
end

Error:

39 |     | State (Opened, _) -> print_endline "Opened"
                  ^^^^^^
Error: This variant pattern is expected to have type closed
       The constructor Opened does not belong to type closed

Also error when trying

  let print_inner_door : type a b. (a, b) t -> unit = function

fails with

38 |     | State (Closed, _) -> print_endline "Closed"
                  ^^^^^^
Error: This pattern matches values of type closed
       but a pattern was expected which matches values of type a

:thinking: Is this an inherit limit of polymorphism?

1 Like