Move inferences to lower level of implicits, fixes fthomas#990

matwojcik · Jul 9, 2021 · f25f46e · f25f46e
1 parent 16d5a9d
commit f25f46e
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 20 deletions.
diff --git a/modules/core/shared/src/main/scala-3.0+/eu/timepit/refined/boolean.scala b/modules/core/shared/src/main/scala-3.0+/eu/timepit/refined/boolean.scala
@@ -245,15 +245,6 @@ private[refined] trait BooleanInference0 extends BooleanInference1 {
   implicit def conjunctionCommutativity[A, B]: (A And B) ==> (B And A) =
     Inference.alwaysValid("conjunctionCommutativity")
 
-  implicit def substitutionInConjunction[A, B, C](implicit p1: B ==> C): (A And B) ==> (A And C) =
-    p1.adapt("substitutionInConjunction(%s)")
-
-  implicit def disjunctionTautologyElimination[A, B, C](implicit
-      p1: A ==> C,
-      p2: B ==> C
-  ): (A Or B) ==> C =
-    Inference.combine(p1, p2, "disjunctionElimination")
-
   implicit def conjunctionEliminationR[A, B, C](implicit p1: B ==> C): (A And B) ==> C =
     p1.adapt("conjunctionEliminationR(%s)")
 
@@ -291,11 +282,23 @@ private[refined] trait BooleanInference1 extends BooleanInference2 {
     p1.adapt("modusTollens(%s)")
 }
 
-private[refined] trait BooleanInference2 {
+private[refined] trait BooleanInference2 extends BooleanInference3 {
 
   implicit def conjunctionEliminationL[A, B, C](implicit p1: A ==> C): (A And B) ==> C =
     p1.adapt("conjunctionEliminationL(%s)")
 
   implicit def hypotheticalSyllogism[A, B, C](implicit p1: A ==> B, p2: B ==> C): A ==> C =
     Inference.combine(p1, p2, "hypotheticalSyllogism(%s, %s)")
 }
+
+private[refined] trait BooleanInference3 {
+
+  implicit def substitutionInConjunction[A, B, C](implicit p1: B ==> C): (A And B) ==> (A And C) =
+    p1.adapt("substitutionInConjunction(%s)")
+
+  implicit def disjunctionTautologyElimination[A, B, C](implicit
+                                                        p1: A ==> C,
+                                                        p2: B ==> C
+                                                       ): (A Or B) ==> C =
+    Inference.combine(p1, p2, "disjunctionElimination")
+}
diff --git a/modules/core/shared/src/main/scala-3.0-/eu/timepit/refined/boolean.scala b/modules/core/shared/src/main/scala-3.0-/eu/timepit/refined/boolean.scala
@@ -273,15 +273,6 @@ private[refined] trait BooleanInference0 extends BooleanInference1 {
   implicit def conjunctionCommutativity[A, B]: (A And B) ==> (B And A) =
     Inference.alwaysValid("conjunctionCommutativity")
 
-  implicit def substitutionInConjunction[A, B, C](implicit p1: B ==> C): (A And B) ==> (A And C) =
-    p1.adapt("substitutionInConjunction(%s)")
-
-  implicit def disjunctionTautologyElimination[A, B, C](implicit
-      p1: A ==> C,
-      p2: B ==> C
-  ): (A Or B) ==> C =
-    Inference.combine(p1, p2, "disjunctionElimination")
-
   implicit def conjunctionEliminationR[A, B, C](implicit p1: B ==> C): (A And B) ==> C =
     p1.adapt("conjunctionEliminationR(%s)")
 
@@ -319,11 +310,22 @@ private[refined] trait BooleanInference1 extends BooleanInference2 {
     p1.adapt("modusTollens(%s)")
 }
 
-private[refined] trait BooleanInference2 {
+private[refined] trait BooleanInference2 extends BooleanInference3 {
 
   implicit def conjunctionEliminationL[A, B, C](implicit p1: A ==> C): (A And B) ==> C =
     p1.adapt("conjunctionEliminationL(%s)")
 
   implicit def hypotheticalSyllogism[A, B, C](implicit p1: A ==> B, p2: B ==> C): A ==> C =
     Inference.combine(p1, p2, "hypotheticalSyllogism(%s, %s)")
 }
+private[refined] trait BooleanInference3 {
+
+  implicit def substitutionInConjunction[A, B, C](implicit p1: B ==> C): (A And B) ==> (A And C) =
+    p1.adapt("substitutionInConjunction(%s)")
+
+  implicit def disjunctionTautologyElimination[A, B, C](implicit
+      p1: A ==> C,
+      p2: B ==> C
+  ): (A Or B) ==> C =
+    Inference.combine(p1, p2, "disjunctionElimination")
+}
diff --git a/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala b/modules/core/shared/src/test/scala-3.0-/eu/timepit/refined/BooleanInferenceSpec.scala
@@ -7,6 +7,7 @@ import eu.timepit.refined.char.{Digit, Letter, UpperCase, Whitespace}
 import eu.timepit.refined.numeric._
 import eu.timepit.refined.string._
 import eu.timepit.refined.collection._
+import eu.timepit.refined.predicates.all.{Equal, LetterOrDigit}
 import org.scalacheck.Prop._
 import org.scalacheck.Properties
 import shapeless.test.illTyped
@@ -72,6 +73,13 @@ class BooleanInferenceSpec extends Properties("BooleanInference") {
     Inference[Letter And UpperCase, UpperCase].isValid
   }
 
+  property("complex conjunction elimination") = secure {
+    type BaseRefinement = And[Size[Equal[10]], Forall[LetterOrDigit]]
+    type ConcreteRefinement = And[StartsWith[W.`"001"`.T], BaseRefinement]
+
+    Inference[ConcreteRefinement, BaseRefinement].isValid
+  }
+
   property("conjunction introduction") = wellTyped {
     illTyped("Inference[UpperCase, UpperCase And Digit]", "could not find.*Inference.*")
   }