Draft macroless ==>

[erikerlandson]

A candidate fix for #755 that refactors ==> to be macroless: if a valid inference cannot be proven, then P1 ==> P2 will fail to manifest. It no longer has a boolean field that is checked via macro.

Introduces a compile-time version of Refined called RefinedLT, which tests a literal type L's value against a corresponding predicate P. So the use of macros has been pushed from ==> to RefinedLT, where the macros are used to extract literal-type value and run the validator against it.

This PR is currently a bit rough - a few unit tests are failing, or failing to compile, which appear to work OK when I run them in the REPL. I also hacked around the old .isValid based unit-testing using a shim that made kittens cry.

[erikerlandson]

I have this passing[*] validateJVM locally, but it has to build against a version of singleton-ops with fthomas/singleton-ops#134, I'm using a publishLocal against head of master.

[*] a few things are disabled

[fthomas]

I applause the macroless ==>!

One quick question: Is RefinedLT only required to implement equalValidateInference or are there other reasons or instances it is required for?

[erikerlandson]

@fthomas that's right, I only implemented RefinedLT to solve equalValidateInference. It seemed possibly useful as an implicit tool in its own right. For example, expressing refined-like constraints on type variables. But that's purely speculative.

[erikerlandson]

Probably obvious from the PR diff, and my comments, but worth calling out that this does add singleton-ops as a new dependency.

[fthomas]

My thoughts with regards to equalValidateInference: If we accept that the Inference#isValid field was a mistake, then equalValidateInference was a mistake too. The instance was added without explanation in f1812d8 and is in the library since version 0.1.0. I guess my reasoning for adding it was something like this: if Inference requires a Boolean we can go from any value T Refined Equal[U] (which has the value U) to T Refined P by applying P to U to obtain that Boolean. So that instance either requires the questionable isValid field or another macro (RefinedLT). I think if we want to put refined in a better position for Scala 3 we should not trade one macro for another and remove equalValidateInference altogether.

WDYT, @erikerlandson?

[erikerlandson]

I think if we want to put refined in a better position for Scala 3 we should not trade one macro for another and remove equalValidateInference altogether.

@fthomas I have no use cases that would need the equalValidateInference rule. If you are OK with removing it, it seems like a good trade-off for truly reducing the number of macros.

The role of expressing predicate constraints on literal types is arguably the domain of singleton-ops, using forms like OpAuxBoolean[P[T], true]

[erikerlandson]

just as a use-case reference, here is how I'm applying ==> to constrain operations in type sound ways:
https://github.com/erikerlandson/coulomb/blob/refined/coulomb-refined/src/main/scala/coulomb/refined/package.scala#L154

[erikerlandson]

@fthomas I removed RefinedLT and equalValidateInference. There were two impacts.

1. this inference is no longer possible:

  property("Exists[A] ==> Exists[B]") = secure {
    Inference[Contains[W.`'5'`.T], Exists[Digit]].isValid
  }

2. this assignment no longer compiles

    val a: Char Refined Equal[W.`'0'`.T] = '0'
    val b: Char Refined Digit = a