> ([> `quit ] as 'a) screen = (module Screen with type message = 'a)
> but an expression was expected of type (module Screen)

Indeed, this is clearly wrong: these two module types are not equivalent.

Right, that one was obvious.

> New attempt:
>
> # let f (screen : 'a screen) =
> let module Screen = (val screen : Screen with type message = 'a) in
> match Screen.(emit init) with
> | Some `quit -> 1
> | _ -> 0
>
> ;;
> Error: Unbound type parameter 'a

Wrong again, as subtyping between module signatures does not
allow free type variables.

At some point, I remember having a message saying that indeed type variables are not allowed while unpacking the module, at least something closer to what you say and more specific than "unbound type parameter 'a". So I'd say it would be more convenient to have a specific message (just like there is for unbound type variables in class definitions for instance). If you don't consider it too futile, I can test it on the SVN head and file a bug report if appropriate.

> Though here I'm not sure the error is right. New attempt:
>
>
> # let f (type s) (screen : s screen) =
> let module Screen = (val screen : Screen with type message = s) in
> match Screen.(emit init) with
> | Some `quit -> 1
> | _ -> 0
>
> ;;
> Error: This type s should be an instance of type [> `quit ]
>
> Which makes sense. So here is my question: is there a way to impose a constraint on the "newtype" introduced in argument? Let me say that I'm aware I should write this more simply. For instance in the module type Screen, emit could have type state -> [`quit | `message of message]. So my question is only a matter of curiosity. Still, I'd be happy to know :o).

No, currently there is no way to do that.
One can only create locally abstract types, not locally private types.

Ok.

In theory I see no problem doing that, but with the current approach this would require new syntax,
and be rather heavy.

let f (type s = private [> `quit]) (screen : s screen) = ...

And to be fully general, recursion between those types should be allowed too...

Probably not worth the trouble. I'm just not used to writing a type and not being able to write a function using values of this type afterwards :o).

As a side note, writing
type message = private [> unit]
makes the problem clearer.
And solves it in some cases:

module type Screen =
sig
type state

type message = private [> `quit ]
val init : state

val emit : state -> message option
end

# let f (module Screen : Screen) =

match Screen.(emit init) with
| Some `quit -> 1
| _ -> 0
;;

val f : (module Screen) -> int = <fun>

Indeed that works! (with appropriate 3.12 syntax).

# module type Screen =
sig
   type state
   type message = private [> `quit ]
   val init : state
   val emit : state -> message option
end;;
module type Screen =
sig
    type state
    type message = private [> `quit ]
    val init : state
    val emit : state -> message option
end
# let f screen = let module Screen = (val screen : Screen) in match Screen.emit Screen.init with Some `quit -> 1 | _ -> 0;;
val f : (module Screen) -> int = <fun>
# module Screen1 : Screen = struct type state = unit type message = [`a | `quit] let init = () let emit () = Some `a end;;
module Screen1 : Screen
# module Screen2 : Screen = struct type state = int type message = [`a | `quit] let init = 0 let emit _ = Some `quit end;;
module Screen2 : Screen
# [ (module Screen1 : Screen) ; (module Screen2 : Screen) ];;
- : (module Screen) list = [<module>; <module>]

This nearly solves my problem: there will be several Screen modules, and those should share a common message type, so that they can communicate. That's why I introduced the 'a screen type. However, it seems that I can't define it anymore:

# type 'a screen = (module Screen with type message = 'a) constraint 'a = [> `quit];;
Error: In this `with' constraint, the new definition of message
       does not match its original definition in the constrained signature:
       Type declarations do not match:
         type message
       is not included in
         type message = private [> `quit ]

# type 'a screen = (module Screen with type message = 'a constraint 'a = [> `quit]);;
Error: Syntax error

It's only logical the first attempt fails. The second, however, seems more reasonable to me (but I guess if type constraints are only allowed in type definition there must be a good reason). Is there a workaround? In the end, I'd want to define a list of Screen modules that share a common message type containing the `quit tag. That said, I remember the work by Romain Bardou and yourself on unions of private polymorphic variants, and I guess we might face difficult problems here. In any case, I have a backup solution, so it's no big deal if it isn't possible.

(using 4.00, but you can also write with (val ...))