diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/api/Inference.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/api/Inference.scala
index 6b9f44db0..194366967 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/api/Inference.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/api/Inference.scala
@@ -4,30 +4,57 @@ package eu.timepit.refined.api
  * Evidence that states if the conclusion `C` can be inferred from the
  * premise `P` or not.
  *
- * This type class is used to implement refinement subtyping. If a valid
- * `Inference[P, C]` exists, the type `F[T, P]` is considered a subtype
+ * This trait is used to implement refinement subtyping.
+ */
+trait Inference[P, C] {
+  type T[P2, C2] <: Inference[P2, C2]
+  def isValid: Boolean
+  final def notValid: Boolean = !isValid
+  def show: String
+  def adapt[P2, C2](adaptedShow: String): T[P2, C2]
+
+}
+
+/**
+ * This type class is used to implement compile-time refinement subtyping. If a
+ * `InferAlways[P, C]` exists, the type `F[T, P]` is considered a subtype
  * of `F[T, C]`.
  */
-case class Inference[P, C](isValid: Boolean, show: String) {
+final case class InferAlways[P, C] private (show: String) extends Inference[P, C] {
 
-  final def adapt[P2, C2](adaptedShow: String): Inference[P2, C2] =
-    copy(show = adaptedShow.format(show))
+  type T[P2, C2] = InferAlways[P2, C2]
+  override def isValid: Boolean = true
+  override def adapt[P2, C2](adaptedShow: String): T[P2, C2] = copy(show = adaptedShow.format(show))
+}
 
-  final def notValid: Boolean =
-    !isValid
+/**
+ * This type class is used to define a runtime refinement subtyping. If an inference
+ * `InferWhen[P, C]`  exists, and ''isValid'' is true, the type `F[T, P]` is considered a subtype of `F[T, C]`.
+ */
+final case class InferWhen[P, C] private (isValid: Boolean, show: String) extends Inference[P, C] {
+
+  type T[P2, C2] = InferWhen[P2, C2]
+  override def adapt[P2, C2](adaptedShow: String): T[P2, C2] = copy(show = adaptedShow.format(show))
 }
 
 object Inference {
 
-  type ==>[P, C] = Inference[P, C]
+  type ==>[P, C] = InferAlways[P, C]
+  type ?=>[P, C] = InferWhen[P, C]
 
   def apply[P, C](implicit i: Inference[P, C]): Inference[P, C] = i
 
-  def alwaysValid[P, C](show: String): Inference[P, C] =
-    Inference(isValid = true, show)
+  def alwaysValid[P, C](show: String): P ==> C =
+    InferAlways(show)
+
+  def apply[P, C](isValid: Boolean, show: String): P ?=> C =
+    InferWhen(isValid, show)
+
+  def combine[P1, P2, P, C1, C2, C](i1: P1 ==> C1, i2: P2 ==> C2, show: String): P ==> C =
+    alwaysValid(show)
 
   def combine[P1, P2, P, C1, C2, C](i1: Inference[P1, C1],
                                     i2: Inference[P2, C2],
-                                    show: String): Inference[P, C] =
+                                    show: String): P ?=> C =
     Inference(i1.isValid && i2.isValid, show.format(i1.show, i2.show))
 }
diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/auto.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/auto.scala
index c4a326071..b8a5de2c1 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/auto.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/auto.scala
@@ -1,7 +1,7 @@
 package eu.timepit.refined
 
 import eu.timepit.refined.api.{Refined, RefType, Validate}
-import eu.timepit.refined.api.Inference.==>
+import eu.timepit.refined.api.Inference.{==>, ?=>}
 import eu.timepit.refined.macros.{InferMacro, RefineMacro}
 import shapeless.tag.@@
 
@@ -11,6 +11,16 @@ import shapeless.tag.@@
  */
 object auto {
 
+  /**
+   * Implicitly converts (at compile-time) a value of type `F[T, A]` to
+   * `F[T, B]`.
+   *
+   */
+  implicit def autoInferAlways[F[_, _], T, A, B](ta: F[T, A])(
+      implicit rt: RefType[F],
+      ir: A ==> B
+  ): F[T, B] = macro InferMacro.always[F, T, A, B]
+
   /**
    * Implicitly converts (at compile-time) a value of type `F[T, A]` to
    * `F[T, B]` if there is a valid inference `A ==> B`. If the
@@ -29,7 +39,7 @@ object auto {
    */
   implicit def autoInfer[F[_, _], T, A, B](ta: F[T, A])(
       implicit rt: RefType[F],
-      ir: A ==> B
+      ir: A ?=> B
   ): F[T, B] = macro InferMacro.impl[F, T, A, B]
 
   /**
diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/boolean.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/boolean.scala
index 587b779ed..59f1bccf1 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/boolean.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/boolean.scala
@@ -1,7 +1,7 @@
 package eu.timepit.refined
 
 import eu.timepit.refined.api._
-import eu.timepit.refined.api.Inference.==>
+import eu.timepit.refined.api.Inference.{==>, ?=>}
 import eu.timepit.refined.boolean._
 import eu.timepit.refined.internal.Resources
 import shapeless.{::, HList, HNil}
@@ -261,10 +261,10 @@ private[refined] trait BooleanInference0 extends BooleanInference1 {
   implicit def minimalTautology[A]: A ==> A =
     Inference.alwaysValid("minimalTautology")
 
-  implicit def doubleNegationElimination[A, B](implicit p1: A ==> B): Not[Not[A]] ==> B =
+  implicit def doubleNegationEliminationAlways[A, B](implicit p1: A ==> B): Not[Not[A]] ==> B =
     p1.adapt("doubleNegationElimination(%s)")
 
-  implicit def doubleNegationIntroduction[A, B](implicit p1: A ==> B): A ==> Not[Not[B]] =
+  implicit def doubleNegationIntroductionAlways[A, B](implicit p1: A ==> B): A ==> Not[Not[B]] =
     p1.adapt("doubleNegationIntroduction(%s)")
 
   implicit def conjunctionAssociativity[A, B, C]: ((A And B) And C) ==> (A And (B And C)) =
@@ -273,7 +273,7 @@ private[refined] trait BooleanInference0 extends BooleanInference1 {
   implicit def conjunctionCommutativity[A, B]: (A And B) ==> (B And A) =
     Inference.alwaysValid("conjunctionCommutativity")
 
-  implicit def conjunctionEliminationR[A, B, C](implicit p1: B ==> C): (A And B) ==> C =
+  implicit def conjunctionEliminationRAlways[A, B, C](implicit p1: B ==> C): (A And B) ==> C =
     p1.adapt("conjunctionEliminationR(%s)")
 
   implicit def disjunctionAssociativity[A, B, C]: ((A Or B) Or C) ==> (A Or (B Or C)) =
@@ -306,15 +306,39 @@ private[refined] trait BooleanInference0 extends BooleanInference1 {
 
 private[refined] trait BooleanInference1 extends BooleanInference2 {
 
-  implicit def modusTollens[A, B](implicit p1: A ==> B): Not[B] ==> Not[A] =
+  implicit def modusTollensAlways[A, B](implicit p1: A ==> B): Not[B] ==> Not[A] =
     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 =
+  implicit def conjunctionEliminationLAlways[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 =
+  implicit def hypotheticalSyllogismAlways[A, B, C](implicit p1: A ==> B, p2: B ==> C): A ==> C =
+    Inference.combine(p1, p2, "hypotheticalSyllogism(%s, %s)")
+}
+
+private[refined] trait BooleanInference3 extends BooleanInference4 {
+  implicit def doubleNegationElimination[A, B](implicit p1: A ?=> B): Not[Not[A]] ?=> B =
+    p1.adapt("doubleNegationElimination(%s)")
+
+  implicit def doubleNegationIntroduction[A, B](implicit p1: A ?=> B): A ?=> Not[Not[B]] =
+    p1.adapt("doubleNegationIntroduction(%s)")
+
+  implicit def conjunctionEliminationR[A, B, C](implicit p1: B ?=> C): (A And B) ?=> C =
+    p1.adapt("conjunctionEliminationR(%s)")
+}
+
+private[refined] trait BooleanInference4 {
+
+  implicit def conjunctionEliminationL[A, B, C](implicit p1: A ?=> C): (A And B) ?=> C =
+    p1.adapt("conjunctionEliminationL(%s)")
+
+  implicit def modusTollens[A, B](implicit p1: A ?=> B): Not[B] ?=> Not[A] =
+    p1.adapt("modusTollens(%s)")
+
+  implicit def hypotheticalSyllogism[A, B, C](implicit p1: Inference[A, B],
+                                              p2: Inference[B, C]): A ?=> C =
     Inference.combine(p1, p2, "hypotheticalSyllogism(%s, %s)")
 }
diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/collection.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/collection.scala
index ee86bdf9e..775d49b14 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/collection.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/collection.scala
@@ -1,7 +1,7 @@
 package eu.timepit.refined
 
 import eu.timepit.refined.api.{Inference, Result, Validate}
-import eu.timepit.refined.api.Inference.==>
+import eu.timepit.refined.api.Inference.{==>, ?=>}
 import eu.timepit.refined.boolean.Not
 import eu.timepit.refined.collection._
 import eu.timepit.refined.generic.Equal
@@ -309,32 +309,50 @@ object collection extends CollectionInference {
     }
 }
 
-private[refined] trait CollectionInference {
+private[refined] trait CollectionInference extends CollectionInference1 {
 
-  implicit def existsInference[A, B](implicit p1: A ==> B): Exists[A] ==> Exists[B] =
+  implicit def existsInferenceAlways[A, B](implicit p1: A ==> B): Exists[A] ==> Exists[B] =
     p1.adapt("existsInference(%s)")
 
   implicit def existsNonEmptyInference[P]: Exists[P] ==> NonEmpty =
     Inference.alwaysValid("existsNonEmptyInference")
 
-  implicit def headInference[A, B](implicit p1: A ==> B): Head[A] ==> Head[B] =
+  implicit def headInferenceAlways[A, B](implicit p1: A ==> B): Head[A] ==> Head[B] =
     p1.adapt("headInference(%s)")
 
   implicit def headExistsInference[P]: Head[P] ==> Exists[P] =
     Inference.alwaysValid("headExistsInference")
 
-  implicit def indexInference[N, A, B](implicit p1: A ==> B): Index[N, A] ==> Index[N, B] =
+  implicit def indexInferenceAlways[N, A, B](implicit p1: A ==> B): Index[N, A] ==> Index[N, B] =
     p1.adapt("indexInference(%s)")
 
   implicit def indexExistsInference[N, P]: Index[N, P] ==> Exists[P] =
     Inference.alwaysValid("indexExistsInference")
 
-  implicit def lastInference[A, B](implicit p1: A ==> B): Last[A] ==> Last[B] =
+  implicit def lastInferenceAlways[A, B](implicit p1: A ==> B): Last[A] ==> Last[B] =
     p1.adapt("lastInference(%s)")
 
   implicit def lastExistsInference[P]: Last[P] ==> Exists[P] =
     Inference.alwaysValid("lastExistsInference")
 
-  implicit def sizeInference[A, B](implicit p1: A ==> B): Size[A] ==> Size[B] =
+  implicit def sizeInferenceAlways[A, B](implicit p1: A ==> B): Size[A] ==> Size[B] =
+    p1.adapt("sizeInference(%s)")
+}
+
+private[refined] trait CollectionInference1 {
+
+  implicit def existsInference[A, B](implicit p1: A ?=> B): Exists[A] ?=> Exists[B] =
+    p1.adapt("existsInference(%s)")
+
+  implicit def headInference[A, B](implicit p1: A ?=> B): Head[A] ?=> Head[B] =
+    p1.adapt("headInference(%s)")
+
+  implicit def indexInference[N, A, B](implicit p1: A ?=> B): Index[N, A] ?=> Index[N, B] =
+    p1.adapt("indexInference(%s)")
+
+  implicit def lastInference[A, B](implicit p1: A ?=> B): Last[A] ?=> Last[B] =
+    p1.adapt("lastInference(%s)")
+
+  implicit def sizeInference[A, B](implicit p1: A ?=> B): Size[A] ?=> Size[B] =
     p1.adapt("sizeInference(%s)")
 }
diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/generic.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/generic.scala
index 598e39e2e..959cf483b 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/generic.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/generic.scala
@@ -1,7 +1,7 @@
 package eu.timepit.refined
 
 import eu.timepit.refined.api.{Inference, Validate}
-import eu.timepit.refined.api.Inference.==>
+import eu.timepit.refined.api.Inference.?=>
 import eu.timepit.refined.generic._
 import shapeless._
 import shapeless.ops.coproduct.ToHList
@@ -108,14 +108,14 @@ private[refined] trait GenericInference {
   implicit def equalValidateInferenceWit[T, U <: T, P](
       implicit v: Validate[T, P],
       wu: Witness.Aux[U]
-  ): Equal[U] ==> P =
+  ): Equal[U] ?=> P =
     Inference(v.isValid(wu.value), s"equalValidateInferenceWit(${v.showExpr(wu.value)})")
 
   implicit def equalValidateInferenceNat[T, N <: Nat, P](
       implicit v: Validate[T, P],
       nt: Numeric[T],
       tn: ToInt[N]
-  ): Equal[N] ==> P =
+  ): Equal[N] ?=> P =
     Inference(v.isValid(nt.fromInt(tn())),
               s"equalValidateInferenceNat(${v.showExpr(nt.fromInt(tn()))})")
 }
diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/macros/InferMacro.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/macros/InferMacro.scala
index a42f4322b..e5541da00 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/macros/InferMacro.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/macros/InferMacro.scala
@@ -1,6 +1,6 @@
 package eu.timepit.refined.macros
 
-import eu.timepit.refined.api.Inference.==>
+import eu.timepit.refined.api.Inference.{==>, ?=>}
 import eu.timepit.refined.api.RefType
 import eu.timepit.refined.internal.Resources
 import macrocompat.bundle
@@ -10,9 +10,15 @@ import scala.reflect.macros.blackbox
 class InferMacro(val c: blackbox.Context) extends MacroUtils {
   import c.universe._
 
-  def impl[F[_, _], T: c.WeakTypeTag, A: c.WeakTypeTag, B: c.WeakTypeTag](ta: c.Expr[F[T, A]])(
+  def always[F[_, _], T: c.WeakTypeTag, A: c.WeakTypeTag, B: c.WeakTypeTag](ta: c.Expr[F[T, A]])(
       rt: c.Expr[RefType[F]],
       ir: c.Expr[A ==> B]
+  ): c.Expr[F[T, B]] =
+    refTypeInstance(rt).unsafeRewrapM(c)(ta)
+
+  def impl[F[_, _], T: c.WeakTypeTag, A: c.WeakTypeTag, B: c.WeakTypeTag](ta: c.Expr[F[T, A]])(
+      rt: c.Expr[RefType[F]],
+      ir: c.Expr[A ?=> B]
   ): c.Expr[F[T, B]] = {
 
     val inference = eval(ir)
diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/numeric.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/numeric.scala
index dd25820b6..49e6e451f 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/numeric.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/numeric.scala
@@ -1,7 +1,7 @@
 package eu.timepit.refined
 
 import eu.timepit.refined.api.{Inference, Validate}
-import eu.timepit.refined.api.Inference.==>
+import eu.timepit.refined.api.Inference.?=>
 import eu.timepit.refined.boolean.{And, Not}
 import eu.timepit.refined.numeric._
 import shapeless.{Nat, Witness}
@@ -160,45 +160,45 @@ private[refined] trait NumericInference {
       implicit wa: Witness.Aux[A],
       wb: Witness.Aux[B],
       nc: Numeric[C]
-  ): Less[A] ==> Less[B] =
+  ): Less[A] ?=> Less[B] =
     Inference(nc.lt(wa.value, wb.value), s"lessInferenceWit(${wa.value}, ${wb.value})")
 
   implicit def greaterInferenceWit[C, A <: C, B <: C](
       implicit wa: Witness.Aux[A],
       wb: Witness.Aux[B],
       nc: Numeric[C]
-  ): Greater[A] ==> Greater[B] =
+  ): Greater[A] ?=> Greater[B] =
     Inference(nc.gt(wa.value, wb.value), s"greaterInferenceWit(${wa.value}, ${wb.value})")
 
   implicit def lessInferenceNat[A <: Nat, B <: Nat](
       implicit ta: ToInt[A],
       tb: ToInt[B]
-  ): Less[A] ==> Less[B] =
+  ): Less[A] ?=> Less[B] =
     Inference(ta() < tb(), s"lessInferenceNat(${ta()}, ${tb()})")
 
   implicit def greaterInferenceNat[A <: Nat, B <: Nat](
       implicit ta: ToInt[A],
       tb: ToInt[B]
-  ): Greater[A] ==> Greater[B] =
+  ): Greater[A] ?=> Greater[B] =
     Inference(ta() > tb(), s"greaterInferenceNat(${ta()}, ${tb()})")
 
   implicit def lessInferenceWitNat[C, A <: C, B <: Nat](
       implicit wa: Witness.Aux[A],
       tb: ToInt[B],
       nc: Numeric[C]
-  ): Less[A] ==> Less[B] =
+  ): Less[A] ?=> Less[B] =
     Inference(nc.lt(wa.value, nc.fromInt(tb())), s"lessInferenceWitNat(${wa.value}, ${tb()})")
 
   implicit def greaterInferenceWitNat[C, A <: C, B <: Nat](
       implicit wa: Witness.Aux[A],
       tb: ToInt[B],
       nc: Numeric[C]
-  ): Greater[A] ==> Greater[B] =
+  ): Greater[A] ?=> Greater[B] =
     Inference(nc.gt(wa.value, nc.fromInt(tb())), s"greaterInferenceWitNat(${wa.value}, ${tb()})")
 
-  implicit def greaterEqualInference[A]: Greater[A] ==> GreaterEqual[A] =
+  implicit def greaterEqualInference[A]: Greater[A] ?=> GreaterEqual[A] =
     Inference(true, "greaterEqualInference")
 
-  implicit def lessEqualInference[A]: Less[A] ==> LessEqual[A] =
+  implicit def lessEqualInference[A]: Less[A] ?=> LessEqual[A] =
     Inference(true, "lessEqualInference")
 }
diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/string.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/string.scala
index 621349dc5..3cedf4292 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/string.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/string.scala
@@ -1,7 +1,7 @@
 package eu.timepit.refined
 
 import eu.timepit.refined.api.{Inference, Validate}
-import eu.timepit.refined.api.Inference.==>
+import eu.timepit.refined.api.Inference.?=>
 import eu.timepit.refined.string._
 import shapeless.Witness
 
@@ -217,12 +217,12 @@ private[refined] trait StringInference {
   implicit def endsWithInference[A <: String, B <: String](
       implicit wa: Witness.Aux[A],
       wb: Witness.Aux[B]
-  ): EndsWith[A] ==> EndsWith[B] =
+  ): EndsWith[A] ?=> EndsWith[B] =
     Inference(wa.value.endsWith(wb.value), s"endsWithInference(${wa.value}, ${wb.value})")
 
   implicit def startsWithInference[A <: String, B <: String](
       implicit wa: Witness.Aux[A],
       wb: Witness.Aux[B]
-  ): StartsWith[A] ==> StartsWith[B] =
+  ): StartsWith[A] ?=> StartsWith[B] =
     Inference(wa.value.startsWith(wb.value), s"startsWithInference(${wa.value}, ${wb.value})")
 }
diff --git a/modules/core/shared/src/test/scala/eu/timepit/refined/ImplicitInferenceSpec.scala b/modules/core/shared/src/test/scala/eu/timepit/refined/ImplicitInferenceSpec.scala
new file mode 100644
index 000000000..6b0afbaa1
--- /dev/null
+++ b/modules/core/shared/src/test/scala/eu/timepit/refined/ImplicitInferenceSpec.scala
@@ -0,0 +1,33 @@
+package eu.timepit.refined
+
+import eu.timepit.refined.api._
+import eu.timepit.refined.api.Inference.==>
+import eu.timepit.refined.api.RefType.applyRef
+import eu.timepit.refined.auto._
+import eu.timepit.refined.boolean._
+import eu.timepit.refined.numeric.{Greater, Positive}
+import org.scalacheck.Prop._
+import org.scalacheck.Properties
+
+class ImplicitInferenceSpec extends Properties("ImplicitInference") {
+
+  private def convert[B, A]: PartiallyApplied[B, A] = new PartiallyApplied[B, A]
+
+  private class PartiallyApplied[B, A] {
+    final def apply[T](value: T)(implicit I: B ==> A,
+                                 V: Validate[T, B]): Either[String, T Refined A] = {
+      val res = applyRef[T Refined B](value)
+      res.map(v => v: T Refined A)
+    }
+  }
+
+  property("Convert with AlwaysValid Inference") = secure {
+    type RefT1 = Positive And Greater[W.`10`.T]
+    type RefT1Inverse = Greater[W.`10`.T] And Positive
+    type T1 = Int Refined RefT1
+    type T1Inverse = Int Refined RefT1Inverse
+    val expected: T1Inverse = 12
+
+    convert[RefT1, RefT1Inverse](12) == Right(expected)
+  }
+}