Why are flexible types not allowed in record type definitions?

Question

I'm trying this:

type TS1<'state, 'action> = {
    actions : 'state -> #seq<'action>
    move    : 'state -> 'action -> 'state
    state0  : 'state
}

But the type checker won't let me:

.../stdin(2,29):error FS0715: Anonymous type variables are not permitted in this declaration

However, if I unfold the definition of the flexible type, I'm good:

type TS2<'state, 'action, 'actions when 'actions :> seq<'action>> = {
    actions : 'state -> 'actions
    move    : 'state -> 'action -> 'state
    state0  : 'state
}

I'm unhappy with having to add the 'actions type variable—it makes the connection to deterministic transition systems as mathematical objects less obvious.

I don't see what could go wrong by allowing flexible types in record definitions. Is it somehow dangerous? Is there some other way I could get the clarity of definition I would like?

Update. I was hoping to be able to write functions on TS types that exploits known implementations; i.e., I want to be able to define a function

let has_action a ts s = Set.contains a <| ts.actions s

This obviously won't type if the type of the actions member is actions : 'state -> seq<'action>. I can do it with the second definition, in which case has_action has type

has_action : a:'a -> ts:TS2<'s,'a,Set<'a>> -> s:'s -> bool when 'a : comparison

The type of this example suggests that the flexible type in TS1 perhaps wouldn't help. There is no way I can avoid the messy third type parameter in TS2? It seems to me the exact implementation of the collection of actions for a state is an implementation detail that should not be exposed in the type.

Answer 1

You pretty much answered your own question here... The second option works, because you introduce another type argument, i.e. you abstract over 'actions. The point being, that you need cannot really define generic values in a record definition. Consider, that the second option is not generic with respect to types, as 'state and 'actions are defined.

Answer 2

This is just a limitation of the current compiler's implementation of the permitted kinds of record signatures. For instance, if you define your type in the same way conceptually, but using an interface or an abstract class instead of a record, it compiles fine:

type TS1<'state, 'action> = 
    abstract actions : 'state -> #seq<'action>
    abstract move    : 'state -> 'action -> 'state
    abstract state0  : 'state