RFE: A version of Inference[P, C] that fails for implicit chaining

[erikerlandson]

I could use a version of Inference that always fails to manifest. For example, the following inference "fails" but it doesn't fail to manifest, it just has a false value:

scala> implicitly[Inference[Greater[-1], Greater[0]]]
res7: eu.timepit.refined.api.Inference[eu.timepit.refined.numeric.Greater[-1],eu.timepit.refined.numeric.Greater[0]] = Inference(false,greaterInference(-1, 0))

This works for the casting in InferMacro and autoInfer but it's limited in how it can be used in chained implicits.

I could use an alternative that will fail like so:

scala> implicitly[ChainableInference[Greater[-1], Greater[0]]] 
   error: could not find implicit value ...

Given the current design, I think that another similar macro which returns a chainable inference type but only if inference.notValid is false, instead of just doing an implicit value conversion.

[fthomas]

Inference was designed before we had singleton-ops and the prospect of having them integrated into the compiler. The value-level Boolean field was an easy way to do something interesting in the autoInfer macro back then. Now that operations with singleton types are in Dotty, I agree that a better design would be if Inference only materializes if one predicate implies the other. Instead of checking the types at the value-level

  implicit def greaterInference[C, A, B](
      implicit
      wa: WitnessAs[A, C],
      wb: WitnessAs[B, C],
      nc: Numeric[C]
  ): Greater[A] ==> Greater[B] = Inference(nc.gt(wa.snd, wb.snd))

we could now just demand a check at the type-level

  implicit def greaterInference[A, B](
      implicit ev: A > B
  ): Greater[A] ==> Greater[B] = Inference()

With that change, autoInfer would not need to be a macro and could just be an implicit conversion.

#454 is a similar issue.

[erikerlandson]

I went through a similar transition with coulomb. Is migrating ==> to a non-macro implementation something you'd prefer to #756?

[erikerlandson]

singleton-ops doesn't seem to have the primitives to support StringInference rules

[erikerlandson]

overall, though, the number of places where ==> rules are currently punting to the isValid field isn't that large.