Impossible operation asserted in the SAWCore prelude

[robdockins]

The following polymorphic operation cannot exist in any meaningful capacity, but is nonetheless asserted to exist in the SAWCore prelude.

eq :: (a :: sort 0) -> a -> a -> Bool;

I would like to understand its purpose before deleting it.

[brianhuffman]

What do you mean, "cannot exist"? An operator with exactly this type is at the center of Higher Order Logic.

Anyway, operationally this is another one of those "magic" ad-hoc-polymorphic functions that does lots of non-parametric stuff with its arguments. Currently it's used to model == from Cryptol. We can't get rid of it until we switch to a nested representation of tuples and records (#6). Ad hoc polymorphism may be ugly, but right now it is the only way to have operations that work on arbitrary tuple and record types.

[robdockins]

I'd argue that the "Bool" of higher order logic is very different than the "Bool" in SAWCore. As I understand it, HOL's Bool is the type of classical logical propositions (for which no notion of effective computability is assumed), whereas SAWCore's Bool is a computable 2-element type (or, perhaps, the flat domain with two nonbottom elements). SAWCore's Eq :: (a::sort 0) -> a -> a -> sort 0 is closer to HOL's notion of equality, although it is not really the same either.

Anyway, my problems with this function are two-fold. First, it cannot be total and computable (there exist types with no computable equality). Second, it cannot be parametric (unless it is actually a constant function, which is useless).

RE ad-hoc polymorphsim: I think I understand how these pieces all fit together now, and more or less why they are this way. I think we can make this work more cleanly by using an explicit dictionary-passing translation. The ad-hoc polymorphism would then get compiled into type-directed explicit dictionary selection during the Cryptol->SAWCore translation.

[robdockins]

This operations is tied up into issues dealing with how we represent the type classes of Cryptol and the primitive operations that apply to all Cryptol types. Further discussion on this topic is better directed toward GaloisInc/cryptol-verifier#1

[robdockins]

In the intervening time since this ticket was opened, we reworked the translation of Cryptol's typeclasses to use explicit dictionary passing in SAWCore. The other dodgy parametric functions have since been removed, but the eq one has lingered around. According to offline discussion with @brianhuffman, it appears to no longer be used, so we should just remove it. Alternately if it is still being used somehow, we should determine why and find some better way to accomplish those ends.

[robdockins]

As far as I can tell, this (and the corresponding use on the JVM side) is the only remaining use of the eq primitive:
https://github.com/GaloisInc/saw-script/blob/476d6e8038b86e3954366d82dbe1c00ec298b5fe/src/SAWScript/Crucible/LLVM/Override.hs#L1269

Probably, we should just dispatch on the type and select the correct equality.

[robdockins]

Fixed via #176