OCaml's GADT and many type variables

Question

I'm trying to model a card game in OCaml (let's assume that it is a solitaire game for the sake of simplicity). A given state of this game is represented by a value of type game. Then I will define a function moves : game -> move list that gives the list of valid moves for the given state of the game; and a function apply: game -> move -> game gives the state after making the given move. (The types presented here may actually be replaced by polymorphic ones, as explained below.)

It so happens that there are two qualitatively different kinds of moves in this game. At some points of the game, one needs to decide to bid or not to bid. At the other points of the game, one simply needs to play a card. It should be an error to apply apply g to m where g requires a (non-)bidding move and m is a card-playing move, for instance.

I would like this error to be a static one. So I thought of using a GADT. I started like this:

type card = int * int
type common = { cards : card list }
type play_phase = Play_phase
type bid_phase = Bid_phase
type _ game = Play_game :  common ->  play_phase game | Bid_game :  common ->  bid_phase game
type _ move =
  | Play : card -> play_phase move
  | Bid : bid_phase move
  | NoBid : bid_phase move

let moves : type a. a game -> a move list = function
  | Bid_game _ -> [Bid; NoBid]
  | Play_game _ ->  [Play (0,0)]

All of these type-check so far. The following, however, does not:

let apply : type a b. (a game * a move) -> b game = function
  | (Bid_game g, _) -> Play_game g
  | (Play_game ({ cards = [] } as g), _) -> Bid_game g
  | (Play_game g, _) -> Play_game g

The content of the function is a nonsense now, but the point is that it requires nontrivial (run-time) computation to determine whether the new game state requires a (non-)bidding move or a card-playing move. Here, I don't know the correct type declaration.

Also, the function apply, when defined correctly, has to have something like the following type-check:

(* ... *)
let rec loop g (* more parameters *) =
   let ms = moves g in
   let m = (* choose an element of ms somehow *) in
   loop (apply g m) (* more parameters *)
(* ... *)

Is this possible with a GADT? If not, can that be circumvented by encoding GADTs by using first-class modules? Or do I have to resort to the object system?

(In case this is relevant, I'm going to use these functions in the innermost loop in a code compiled by using js_of_ocaml.)

EDIT: in response to PatJ's answer:

module type Exist = sig type t val x : t game end

let apply' : type a. a game -> a move -> (module Exist)
  = fun { data = cs }  m ->
  match cs with
  | [] ->
     let module M =  struct
         type t = bid_phase 
         let x = { phase = Bid_phase; data = [] }
       end in
     (module M)
  | cs ->
     let module M = struct
         type t = play_phase
         let x = { phase = Play_phase; data = cs}
       end in
     (module M)

Answer 1

@PatJ's solution is to hide the types and try to move on like that. I think this is a bad solution because, in the end, it doesn't really give you anything and forces you to play hide-and-seek with the existentials.

Instead, you should embrace the fact that you are encoding a state-machine in the type system where games are the states and moves are the transition. If you do that the path seems clearer: transitions are always from one state to another:

type card = int * int
type common = { cards : card list }
type play = Play
type bid = Bid
type _ game = Play_game :  common ->  play game | Bid_game :  common ->  bid game
type (_,_) move =
  | Play : card -> (play, play) move
  | StartBid : (play, bid) move
  | Bid : (bid, play) move
  | NoBid : (bid, play) move

type 'a any_move = Ex : ('a, 'b) move -> 'a any_move

let moves : type a. a game -> a any_move list = function
  | Bid_game _ -> [Ex Bid; Ex NoBid]
  | Play_game _ ->  [Ex (Play (0,0))]

let apply : type a b. a game -> (a, b) move -> b game =
  fun g m -> match m, g with
    | Bid, Bid_game g -> Play_game g
    | NoBid, Bid_game g -> Play_game g
    | StartBid, Play_game g -> Bid_game g
    | Play _c, Play_game g -> Play_game g

let rec loop : type a . a game -> _ =
  function g ->
    let ms = moves g in
    let Ex m = List.hd ms (* choose an element of ms somehow *) in
    loop (apply g m) (* more parameters *)

Note here the explicit move to enter a bid. You can only decide the types based on other type information. In particular you can't say "the game is now bidding because the list of cards is empty" without lifting the fact that the card list is empty to the type level.

If you ask me, I think this is grossly overkill, but Eh. :p