> type family Frozen t
> type family Thawed t
> class Immutable (Frozen t) => Mutable t where
>   thawedFrozen :: t -> Thawed (Frozen t)
>   unthawedFrozen :: Thawed (Frozen t) -> t
>
> class Mutable (Thawed t) => Immutable t where
>   frozenThawed :: t -> Frozen (Thawed t)
>   unfrozenThawed :: Frozen (Thawed t) -> t
>
> would enable you to explicitly program with the two isomorphisms, while
> avoiding superclass constraints.

Hmm, that's an interesting thought. If I'm guesstimating correctly,
defining instances would be more cumbersome than with the MPTC method,
but using them would be nicer, provided I write helper functions to
hide the use of the isomorphism witnesses. I'll give it a try. Thanks!

I seem to recall that in one of your packages, you had a typeclass
method returning a GADT wrapping the evidence for the equality of two
types, as a workaround for the lack of superclass equality constraints
-- what makes you prefer that workaround in one case and this one in
another?