Parse error: The level of the expression or operator substituted for 'Def' must be at most 0

Question

I have two specs: System and SystemMC. The System spec is the "nice" spec of the system I am specifying, useful for documentation. It defines a CONSTANT MessyAction(_) (in the actual specs I am writing, a hash function) that is messy to specify in an efficiently model-checkable way and so would reduce spec readability. I implement MessyAction(_) in the SystemMC spec, so I can model-check the System spec. However, the parser gives the following error in the SystemMC spec:

Level error in instantiating module 'System': The level of the expression or operator substituted for 'MessyAction' must be at most 0.

What does this error mean, and how can I accomplish my goal of model-checking the System spec without adding a bunch of stuff to it that is optimized for TLC? Here is the System spec:

------------------------------- MODULE System -------------------------------

EXTENDS
    Naturals

CONSTANTS
    MessyAction(_)

VARIABLES
    Counter

-----------------------------------------------------------------------------

TypeInvariant ==
    /\ Counter \in Nat

Init ==
    /\ Counter = 0

Increment ==
    /\ Counter' = Counter + 1
    /\ MessyAction(Counter)

Next ==
    \/ Increment

=============================================================================

Here is the SystemMC spec:

------------------------------ MODULE SystemMC ------------------------------

EXTENDS
    Naturals

CONSTANTS
    MaxCounterValue

VARIABLES
    Counter,
    PastValues

ASSUME MaxCounterValue \in Nat

-----------------------------------------------------------------------------

MessyAction(c) ==
    /\ PastValues' = PastValues \cup {c}

S == INSTANCE System

TypeInvariant ==
    /\ PastValues \subseteq Nat
    /\ S!TypeInvariant

Init ==
    /\ PastValues = {}
    /\ S!Init

Increment ==
    /\ Counter < MaxCounterValue
    /\ S!Increment

Next ==
    \/ Increment

=============================================================================

Answer 1

Per Leslie Lamport's reply here, when you instantiate a non-constant module (a module containing variables) like System, the CONSTANT entities can only be instantiated by other constants. So, in SystemMC you can rename MessyAction(_) to MessyActionImpl(_), define MessyAction(_) as a CONSTANT, then in the model define MessyAction(c) as MessyActionImpl(c). The System spec is unchanged, but here's the new SystemMC spec:

------------------------------ MODULE SystemMC ------------------------------

EXTENDS
    Naturals

CONSTANTS
    MessyAction(_),
    MaxCounterValue

VARIABLES
    Counter,
    PastValues

ASSUME MaxCounterValue \in Nat

-----------------------------------------------------------------------------

MessyActionImpl(c) ==
    /\ PastValues' = PastValues \cup {c}

S == INSTANCE System

TypeInvariant ==
    /\ PastValues \subseteq Nat
    /\ S!TypeInvariant

Init ==
    /\ PastValues = {}
    /\ S!Init

Increment ==
    /\ Counter < MaxCounterValue
    /\ S!Increment

Next ==
    \/ Increment

=============================================================================

When you create a model in the toolbox, define the value of the MessyAction(_) constant as MessyActionImpl(_):

End result:

Voila, dependency injection for TLA+!