Make equality of Reference independent of the contents

[Lysxia]

We have an instance (Eq1 v, Eq a) => Eq (Reference v a) , which requires that the underlying reference type be comparable (Eq a). That happens to be fine with IORef but in general reference types such as mutable vectors do not have such an instance. A workaround is a wrapper that carries a unique identifier for each reference (see here for example), but could qc-state-machine integrate that somehow?

[stevana]

Perhaps it would make sense to move your trick into the library? That way we can also use Map (Reference ...)-like models...

[stevana]

I thought a bit more about this, and I'm beginning to wonder if post-conditions shouldn't have the type model Symbolic -> act Symbolic resp -> resp -> Bool?

Or perhaps the Var from Symbolic can be threaded through into Concrete and used for equality checks?

[stevana]

I played around a bit more with this in #209, see:

data Concrete a where
  Concrete :: Typeable a => a -> Unique -> Concrete a

instance Eq (Concrete a) where
  Concrete _ u1 == Concrete _ u2 = u1 == u2

instance Eq (r a) => Eq (Reference a r) where
  Reference r1 == Reference r2 = r1 == r2

reference :: Typeable a => a -> IO (Reference a Concrete)
reference x = Reference <$> (Concrete x <$> newUnique)

It seems to work, but I needed:

transition :: forall r. ForallF Ord r => model r -> cmd r -> resp r -> model r 

Which is terrible to work with, but maybe we can revisit this approach when GHC gets qualified contexts.