With inspectTVar it's possible to inspect a ModelTVar n in an Invariant n context. This is very useful, however, it's unclear to me how the types provided by concurrency built on top of TVars can be inspected in Invariant.
As an example, a TMVar stm a is, basically, a newtype around TVar stm (Maybe a). If the TMVar constructor were exported, it'd be possible to implement inspectTMVar (= \(TMVar ctvar) -> inspectTVar ctvar or something like that), but since it isn't, we're kinda stuck.
Other STM types like TChan, TSem,... also wrap something in a TVar, but can't be inspected.
Adding inspectTMVar etc. to concurrency would add a dependency on dejafu to concurrency which is likely undesired. At the same time, exposing the various constructors could be undesired as well, since giving direct access to the inner TVar could easily break invariants.
I couldn't think of a good way to tackle this yet, but it seems quite useful/important not to be restricted to only TVars when defining invariant checks.
With
inspectTVarit's possible to inspect aModelTVar nin anInvariant ncontext. This is very useful, however, it's unclear to me how the types provided byconcurrencybuilt on top ofTVars can be inspected inInvariant.As an example, a
TMVar stm ais, basically, anewtypearoundTVar stm (Maybe a). If theTMVarconstructor were exported, it'd be possible to implementinspectTMVar(= \(TMVar ctvar) -> inspectTVar ctvaror something like that), but since it isn't, we're kinda stuck.Other STM types like
TChan,TSem,... also wrap something in aTVar, but can't be inspected.Adding
inspectTMVaretc. toconcurrencywould add a dependency ondejafutoconcurrencywhich is likely undesired. At the same time, exposing the various constructors could be undesired as well, since giving direct access to the innerTVarcould easily break invariants.I couldn't think of a good way to tackle this yet, but it seems quite useful/important not to be restricted to only
TVars when defining invariant checks.