Prevent SML type from becoming eqtype without hiding constructors

Question

In datatype declarations, Standard ML will produce an equality type if all of the type arguments to all of the variants are themselves eqtypes.

I've seen comments in a few places lamenting the inability of users to provide their own definition of equality and construct their own eqtypes and unexpected consequences of the SML rules (e.g. bare refs and arrays are eqtypes, but datatype Foo = Foo of (real ref) is not an eqtype).

Source: http://mlton.org/PolymorphicEquality

one might expect to be able to compare two values of type real t, because pointer comparison on a ref cell would suffice. Unfortunately, the type system can only express that a user-defined datatype admits equality or not.

I'm wondering whether it is possible to block eqtyping. Say, for instance, I am implementing a set as a binary tree (with an unnecessary variant) and I want to pledge away the ability to structurally compare sets with each other.

datatype 'a set = EmptySet | SetLeaf of 'a | SetNode of 'a * 'a set * 'a set;

Say I don't want people to be able to distinguish SetLeaf(5) and SetNode(5, EmptySet, EmptySet) with = since it's an abstraction-breaking operation.

I tried a simple example with datatype on = On | Off just to see if I could demote the type to a non-eqtype using signatures.

(* attempt to hide the "eq"-ness of eqtype *)
signature S = sig
  type on
  val foo : on
end

(* opaque transcription to kill eqtypeness *)
structure X :> S = struct
  datatype on = On | Off
  let foo = On
end

It seems that transparent ascription fails to prevent X.on from becoming an eqtype, but opaque ascription does prevent it. However, these solutions are not ideal because they introduce a new module and hide the data constructors. Is there a way to prevent a custom type or type constructor from becoming an eqtype or admitting equality without hiding its data constructors or introducing new modules?

Answer 1

Short answer is no. When a type's definition is visible, it's eq-ness is whatever the definition implies. The only way to prevent it being eq then is to tweak the definition such that it isn't, for example, by adding a dummy constructor with a real parameter.

Btw, small correction: your type foo should be an equality type. If your SML implementation disagrees then it has a bug. A different case is real bar when datatype 'a bar = Bar of 'a ref (which is what the MLton manual discusses). The reason that the first one works but the second doesn't is that ref is magic in SML: it has a form of polymorphic eq-ness that user types cannot have.