diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 29ede1a187c2..d6a1a41fb5f1 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -671,6 +671,8 @@ class Definitions {
   @tu lazy val QuotedMatchingSymClass: ClassSymbol = ctx.requiredClass("scala.quoted.matching.Sym")
   @tu lazy val TastyReflectionClass: ClassSymbol = ctx.requiredClass("scala.tasty.Reflection")
 
+  @tu lazy val TypeableClass = ctx.requiredClass("scala.Typeable")
+
   @tu lazy val Unpickler_unpickleExpr: Symbol = ctx.requiredMethod("scala.runtime.quoted.Unpickler.unpickleExpr")
   @tu lazy val Unpickler_unpickleType: Symbol = ctx.requiredMethod("scala.runtime.quoted.Unpickler.unpickleType")
 
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index fe2746e50987..2f97a2b46742 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -215,6 +215,8 @@ object StdNames {
     final val Type : N               = "Type"
     final val TypeTree: N            = "TypeTree"
 
+    final val Typeable: N             = "Typeable"
+
     // Annotation simple names, used in Namer
     final val BeanPropertyAnnot: N = "BeanProperty"
     final val BooleanBeanPropertyAnnot: N = "BooleanBeanProperty"
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 604a7c5055fb..9e36b53e7d45 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -678,17 +678,27 @@ class Typer extends Namer
    *  exists, rewrite to `ctag(e)`.
    *  @pre We are in pattern-matching mode (Mode.Pattern)
    */
-  def tryWithClassTag(tree: Typed, pt: Type)(implicit ctx: Context): Tree = tree.tpt.tpe.dealias match {
-    case tref: TypeRef if !tref.symbol.isClass && !ctx.isAfterTyper =>
-      require(ctx.mode.is(Mode.Pattern))
-      inferImplicit(defn.ClassTagClass.typeRef.appliedTo(tref),
-                    EmptyTree, tree.tpt.span)(ctx.retractMode(Mode.Pattern)) match {
-        case SearchSuccess(clsTag, _, _) =>
-          typed(untpd.Apply(untpd.TypedSplice(clsTag), untpd.TypedSplice(tree.expr)), pt)
-        case _ =>
-          tree
-      }
-    case _ => tree
+  def tryWithClassTag(tree: Typed, pt: Type)(implicit ctx: Context): Tree =  {
+    tree.tpt.tpe.dealias match {
+      case tref: TypeRef if !tref.symbol.isClass && !ctx.isAfterTyper =>
+        require(ctx.mode.is(Mode.Pattern))
+        inferImplicit(defn.TypeableClass.typeRef.appliedTo(pt, tref),
+        EmptyTree, tree.tpt.span)(ctx.retractMode(Mode.Pattern)) match {
+          case SearchSuccess(clsTag, _, _) =>
+            typed(untpd.Apply(untpd.TypedSplice(clsTag), untpd.TypedSplice(tree.expr)), pt)
+          case _ =>
+            inferImplicit(defn.ClassTagClass.typeRef.appliedTo(tref),
+              EmptyTree, tree.tpt.span)(ctx.retractMode(Mode.Pattern)) match {
+                case SearchSuccess(clsTag, _, _) =>
+                  typed(untpd.Apply(untpd.TypedSplice(clsTag), untpd.TypedSplice(tree.expr)), pt)
+                case _ =>
+
+                  tree
+              }
+        }
+
+      case _ => tree
+    }
   }
 
   def typedNamedArg(tree: untpd.NamedArg, pt: Type)(implicit ctx: Context): NamedArg = {
@@ -1467,7 +1477,7 @@ class Typer extends Namer
     val body1 = typed(tree.body, pt1)
     body1 match {
       case UnApply(fn, Nil, arg :: Nil)
-      if fn.symbol.exists && fn.symbol.owner == defn.ClassTagClass && !body1.tpe.isError =>
+      if fn.symbol.exists && (fn.symbol.owner == defn.ClassTagClass || fn.symbol.owner.derivesFrom(defn.TypeableClass)) && !body1.tpe.isError =>
         // A typed pattern `x @ (e: T)` with an implicit `ctag: ClassTag[T]`
         // was rewritten to `x @ ctag(e)` by `tryWithClassTag`.
         // Rewrite further to `ctag(x @ e)`
diff --git a/docs/docs/reference/other-new-features/typeable.md b/docs/docs/reference/other-new-features/typeable.md
new file mode 100644
index 000000000000..8d94365a8230
--- /dev/null
+++ b/docs/docs/reference/other-new-features/typeable.md
@@ -0,0 +1,85 @@
+---
+layout: doc-page
+title: "Typeable"
+---
+
+Typeable
+--------
+
+`Typeable` provides the a generalization of `ClassTag.unapply` where the type of the argument is generalized.
+`Typeable.unapply` will return `Some(x.asInstanceOf[Y])` if `x` conforms to `Y`, otherwise it returns `None`.
+
+```scala
+trait Typeable[S, T <: S] extends Serializable {
+  def unapply(x: S): Option[T]
+}
+```
+
+Just like `ClassTag` it can be used to perform type checks in patterns.
+
+```scala
+type X
+type Y <: X
+
+given Typeable[X, Y] = ...
+
+(x: X) match {
+  case y: Y => ... // safe checked downcast
+  case _ => ...
+}
+```
+
+
+Examples
+--------
+
+Given the following abstract definition of `Peano` numbers that provides `Typeable[Nat, Zero]` and `Typeable[Nat, Succ]`
+
+```scala
+trait Peano {
+  type Nat
+  type Zero <: Nat
+  type Succ <: Nat
+
+  def safeDiv(m: Nat, n: Succ): (Nat, Nat)
+
+  val Zero: Zero
+
+  val Succ: SuccExtractor
+  trait SuccExtractor {
+    def apply(nat: Nat): Succ
+    def unapply(nat: Succ): Option[Nat]
+  }
+
+  given Typeable[Nat, Zero] {
+    def unapply(x: Nat): Option[Zero] = matchZero(x)
+  }
+
+  given Typeable[Nat, Succ] {
+    def unapply(x: Nat): Option[Succ] = matchSucc(x)
+  }
+
+  protected def matchZero(x: Nat): Option[Zero]
+  protected def matchSucc(x: Nat): Option[Succ]
+}
+```
+
+it will be possible to write the following program
+
+```scala
+val peano: Peano = ...
+import peano.{_, given}
+
+def divOpt(m: Nat, n: Nat): Option[(Nat, Nat)] = {
+  n match {
+    case Zero => None
+    case s @ Succ(_) => Some(safeDiv(m, s))
+  }
+}
+
+val two = Succ(Succ(Zero))
+val five = Succ(Succ(Succ(two)))
+println(divOpt(five, two))
+```
+
+Note that without the `Typeable[Nat, Succ]` the pattern `Succ.unapply` would be unchecked.
diff --git a/library/src/scala/Typeable.scala b/library/src/scala/Typeable.scala
new file mode 100644
index 000000000000..355704930023
--- /dev/null
+++ b/library/src/scala/Typeable.scala
@@ -0,0 +1,10 @@
+package scala
+
+/** A `Typeable[S, T]` (where `T <: S`) contains the logic needed to know at runtime if a value of
+ *  type `S` can be downcased to `T`.
+ *
+ *  Unlike `ClassTag`, a `Typeable` must check the type arguments at runtime.
+ */
+trait Typeable[S, T <: S] extends Serializable {
+  def unapply(x: S): Option[T]
+}
diff --git a/library/src/scala/tasty/reflect/Core.scala b/library/src/scala/tasty/reflect/Core.scala
index b6c5717db2c9..1e29d1bebc3f 100644
--- a/library/src/scala/tasty/reflect/Core.scala
+++ b/library/src/scala/tasty/reflect/Core.scala
@@ -120,72 +120,95 @@ trait Core {
 
     /** Tree representing a pacakage clause in the source code */
     type PackageClause = internal.PackageClause
+    given (given ctx: Context): Typeable[Tree, PackageClause] = internal.matchPackageClause(_)
 
     /** Tree representing a statement in the source code */
     type Statement = internal.Statement
+    given (given ctx: Context): Typeable[Tree, Statement] = internal.matchStatement(_)
 
       /** Tree representing an import in the source code */
       type Import = internal.Import
+      given (given ctx: Context): Typeable[Tree, Import] = internal.matchImport(_)
 
       /** Tree representing a definition in the source code. It can be `PackageDef`, `ClassDef`, `TypeDef`, `DefDef` or `ValDef` */
       type Definition = internal.Definition
+      given (given ctx: Context): Typeable[Tree, Definition] = internal.matchDefinition(_)
 
         /** Tree representing a package definition. This includes definitions in all source files */
         type PackageDef = internal.PackageDef
+        given (given ctx: Context): Typeable[Tree, PackageDef] = internal.matchPackageDef(_)
 
         /** Tree representing a class definition. This includes annonymus class definitions and the class of a module object */
         type ClassDef = internal.ClassDef
+        given (given ctx: Context): Typeable[Tree, ClassDef] = internal.matchClassDef(_)
 
         /** Tree representing a type (paramter or member) definition in the source code */
         type TypeDef = internal.TypeDef
+        given (given ctx: Context): Typeable[Tree, TypeDef] = internal.matchTypeDef(_)
 
         /** Tree representing a method definition in the source code */
         type DefDef = internal.DefDef
+        given (given ctx: Context): Typeable[Tree, DefDef] = internal.matchDefDef(_)
 
         /** Tree representing a value definition in the source code This inclues `val`, `lazy val`, `var`, `object` and parameter defintions. */
         type ValDef = internal.ValDef
+        given (given ctx: Context): Typeable[Tree, ValDef] = internal.matchValDef(_)
 
       /** Tree representing an expression in the source code */
       type Term = internal.Term
+      given (given ctx: Context): Typeable[Tree, Term] = internal.matchTerm(_)
 
         /** Tree representing a reference to definition */
         type Ref = internal.Ref
+        given (given ctx: Context): Typeable[Tree, Ref] = internal.matchRef(_)
 
           /** Tree representing a reference to definition with a given name */
           type Ident = internal.Ident
+          given (given ctx: Context): Typeable[Tree, Ident] = internal.matchIdent(_)
 
           /** Tree representing a selection of definition with a given name on a given prefix */
           type Select = internal.Select
+          given (given ctx: Context): Typeable[Tree, Select] = internal.matchSelect(_)
 
         /** Tree representing a literal value in the source code */
         type Literal = internal.Literal
+        given (given ctx: Context): Typeable[Tree, Literal] = internal.matchLiteral(_)
 
         /** Tree representing `this` in the source code */
         type This = internal.This
+        given (given ctx: Context): Typeable[Tree, This] = internal.matchThis(_)
 
         /** Tree representing `new` in the source code */
         type New = internal.New
+        given (given ctx: Context): Typeable[Tree, New] = internal.matchNew(_)
 
         /** Tree representing an argument passed with an explicit name. Such as `arg1 = x` in `foo(arg1 = x)` */
         type NamedArg = internal.NamedArg
+        given (given ctx: Context): Typeable[Tree, NamedArg] = internal.matchNamedArg(_)
 
         /** Tree an application of arguments. It represents a single list of arguments, multiple argument lists will have nested `Apply`s  */
         type Apply = internal.Apply
+        given (given ctx: Context): Typeable[Tree, Apply] = internal.matchApply(_)
 
         /** Tree an application of type arguments */
         type TypeApply = internal.TypeApply
+        given (given ctx: Context): Typeable[Tree, TypeApply] = internal.matchTypeApply(_)
 
         /** Tree representing `super` in the source code */
         type Super = internal.Super
+        given (given ctx: Context): Typeable[Tree, Super] = internal.matchSuper(_)
 
         /** Tree representing a type ascription `x: T` in the source code */
         type Typed = internal.Typed
+        given (given ctx: Context): Typeable[Tree, Typed] = internal.matchTyped(_)
 
         /** Tree representing an assignment `x = y` in the source code */
         type Assign = internal.Assign
+        given (given ctx: Context): Typeable[Tree, Assign] = internal.matchAssign(_)
 
         /** Tree representing a block `{ ... }` in the source code */
         type Block = internal.Block
+        given (given ctx: Context): Typeable[Tree, Block] = internal.matchBlock(_)
 
         /** A lambda `(...) => ...` in the source code is represented as
          *  a local method and a closure:
@@ -197,87 +220,114 @@ trait Core {
          *
          */
         type Closure = internal.Closure
+        given (given ctx: Context): Typeable[Tree, Closure] = internal.matchClosure(_)
 
         /** Tree representing an if/then/else `if (...) ... else ...` in the source code */
         type If = internal.If
+        given (given ctx: Context): Typeable[Tree, If] = internal.matchIf(_)
 
         /** Tree representing a pattern match `x match  { ... }` in the source code */
         type Match = internal.Match
+        given (given ctx: Context): Typeable[Tree, Match] = internal.matchMatch(_)
 
         /** Tree representing a pattern match `delegate match { ... }` in the source code */  // TODO: drop
         type ImpliedMatch = internal.ImpliedMatch
+        given (given ctx: Context): Typeable[Tree, ImpliedMatch] = internal.matchImplicitMatch(_)
 
         /** Tree representing a try catch `try x catch { ... } finally { ... }` in the source code */
         type Try = internal.Try
+        given (given ctx: Context): Typeable[Tree, Try] = internal.matchTry(_)
 
         /** Tree representing a `return` in the source code */
         type Return = internal.Return
+        given (given ctx: Context): Typeable[Tree, Return] = internal.matchReturn(_)
 
         /** Tree representing a variable argument list in the source code */
         type Repeated = internal.Repeated
+        given (given ctx: Context): Typeable[Tree, Repeated] = internal.matchRepeated(_)
 
         /** Tree representing the scope of an inlined tree */
         type Inlined = internal.Inlined
+        given (given ctx: Context): Typeable[Tree, Inlined] = internal.matchInlined(_)
 
         /** Tree representing a selection of definition with a given name on a given prefix and number of nested scopes of inlined trees */
         type SelectOuter = internal.SelectOuter
+        given (given ctx: Context): Typeable[Tree, SelectOuter] = internal.matchSelectOuter(_)
 
         /** Tree representing a while loop */
         type While = internal.While
+        given (given ctx: Context): Typeable[Tree, While] = internal.matchWhile(_)
 
       /** Type tree representing a type written in the source */
       type TypeTree = internal.TypeTree
+      given (given ctx: Context): Typeable[Tree, TypeTree] = internal.matchTypeTree(_)
 
         /** Type tree representing an inferred type */
         type Inferred = internal.Inferred
+        given (given ctx: Context): Typeable[Tree, Inferred] = internal.matchInferred(_)
 
         /** Type tree representing a reference to definition with a given name */
         type TypeIdent = internal.TypeIdent
+        given (given ctx: Context): Typeable[Tree, TypeIdent] = internal.matchTypeIdent(_)
 
         /** Type tree representing a selection of definition with a given name on a given term prefix */
         type TypeSelect = internal.TypeSelect
+        given (given ctx: Context): Typeable[Tree, TypeSelect] = internal.matchTypeSelect(_)
 
         /** Type tree representing a selection of definition with a given name on a given type prefix */
         type Projection = internal.Projection
+        given (given ctx: Context): Typeable[Tree, Projection] = internal.matchProjection(_)
 
         /** Type tree representing a singleton type */
         type Singleton = internal.Singleton
+        given (given ctx: Context): Typeable[Tree, Singleton] = internal.matchSingleton(_)
 
         /** Type tree representing a type refinement */
         type Refined = internal.Refined
+        given (given ctx: Context): Typeable[Tree, Refined] = internal.matchRefined(_)
 
         /** Type tree representing a type application */
         type Applied = internal.Applied
+        given (given ctx: Context): Typeable[Tree, Applied] = internal.matchApplied(_)
 
         /** Type tree representing an annotated type */
         type Annotated = internal.Annotated
+        given (given ctx: Context): Typeable[Tree, Annotated] = internal.matchAnnotated(_)
 
         /** Type tree representing a type match */
         type MatchTypeTree = internal.MatchTypeTree
+        given (given ctx: Context): Typeable[Tree, MatchTypeTree] = internal.matchMatchTypeTree(_)
 
         /** Type tree representing a by name parameter */
         type ByName = internal.ByName
+        given (given ctx: Context): Typeable[Tree, ByName] = internal.matchByName(_)
 
         /** Type tree representing a lambda abstraction type */
         type LambdaTypeTree = internal.LambdaTypeTree
+        given (given ctx: Context): Typeable[Tree, LambdaTypeTree] = internal.matchLambdaTypeTree(_)
 
         /** Type tree representing a type binding */
         type TypeBind = internal.TypeBind
+        given (given ctx: Context): Typeable[Tree, TypeBind] = internal.matchTypeBind(_)
 
         /** Type tree within a block with aliases `{ type U1 = ... ; T[U1, U2] }` */
         type TypeBlock = internal.TypeBlock
+        given (given ctx: Context): Typeable[Tree, TypeBlock] = internal.matchTypeBlock(_)
 
       /** Type tree representing a type bound written in the source */
       type TypeBoundsTree = internal.TypeBoundsTree
+      given (given ctx: Context): Typeable[Tree, TypeBoundsTree] = internal.matchTypeBoundsTree(_)
 
       /** Type tree representing wildcard type bounds written in the source.
        *  The wildcard type `_` (for example in in `List[_]`) will be a type tree that
        *  represents a type but has `TypeBound`a inside.
        */
       type WildcardTypeTree = internal.WildcardTypeTree
+      given (given ctx: Context): Typeable[Tree, WildcardTypeTree] = internal.matchWildcardTypeTree(_)
 
   /** Branch of a pattern match or catch clause */
   type CaseDef = internal.CaseDef
+  given (given ctx: Context): Typeable[Tree, CaseDef] = internal.matchCaseDef(_)
 
   /** Branch of a type pattern match */
   type TypeCaseDef = internal.TypeCaseDef
diff --git a/tests/run-macros/i5715/Macro_1.scala b/tests/run-macros/i5715/Macro_1.scala
index 0eea998edf3b..a1205573b5a6 100644
--- a/tests/run-macros/i5715/Macro_1.scala
+++ b/tests/run-macros/i5715/Macro_1.scala
@@ -8,8 +8,7 @@ object scalatest {
     import qctx.tasty.{_, given}
 
     cond.unseal.underlyingArgument match {
-      case app @ Apply(sel @ Select(lhs, op), rhs :: Nil) =>
-        val IsSelect(select) = sel
+      case app @ Apply(select @ Select(lhs, op), rhs :: Nil) =>
         val cond = Apply(Select.copy(select)(lhs, "exists"), rhs :: Nil).seal.cast[Boolean]
         '{ scala.Predef.assert($cond) }
       case _ =>
diff --git a/tests/run-macros/reflect-select-copy/assert_1.scala b/tests/run-macros/reflect-select-copy/assert_1.scala
index 03a9e8ccede2..0a5ed60b5149 100644
--- a/tests/run-macros/reflect-select-copy/assert_1.scala
+++ b/tests/run-macros/reflect-select-copy/assert_1.scala
@@ -8,8 +8,7 @@ object scalatest {
     import qctx.tasty.{_, given}
 
     cond.unseal.underlyingArgument match {
-      case Apply(sel @ Select(lhs, op), rhs :: Nil) =>
-        val IsSelect(select) = sel
+      case Apply(select @ Select(lhs, op), rhs :: Nil) =>
         val cond = Apply(Select.copy(select)(lhs, ">"), rhs :: Nil).seal.cast[Boolean]
         '{ scala.Predef.assert($cond) }
       case _ =>
diff --git a/tests/run-macros/reflect-select-copy/reflect-select-copy/assert_1.scala b/tests/run-macros/reflect-select-copy/reflect-select-copy/assert_1.scala
index d428ede4c8cf..9b1fbd1840c9 100644
--- a/tests/run-macros/reflect-select-copy/reflect-select-copy/assert_1.scala
+++ b/tests/run-macros/reflect-select-copy/reflect-select-copy/assert_1.scala
@@ -24,7 +24,7 @@ object scalatest {
             }
           }
         }.seal.cast[Unit]
-      case Apply(f @ Apply(IsSelect(sel @ Select(Apply(qual, lhs :: Nil), op)), rhs :: Nil), implicits)
+      case Apply(f @ Apply(sel @ Select(Apply(qual, lhs :: Nil), op), rhs :: Nil), implicits)
       if isImplicitMethodType(f.tpe) =>
         let(lhs) { left =>
           let(rhs) { right =>
diff --git a/tests/run-macros/tasty-extractors-3/quoted_1.scala b/tests/run-macros/tasty-extractors-3/quoted_1.scala
index 8f3f4f414371..47f046ef8763 100644
--- a/tests/run-macros/tasty-extractors-3/quoted_1.scala
+++ b/tests/run-macros/tasty-extractors-3/quoted_1.scala
@@ -13,11 +13,11 @@ object Macros {
     val buff = new StringBuilder
     val traverser = new TreeTraverser {
       override def traverseTree(tree: Tree)(implicit ctx: Context): Unit = tree match {
-        case IsTypeBoundsTree(tree) =>
+        case tree: TypeBoundsTree =>
           buff.append(tree.tpe.showExtractors)
           buff.append("\n\n")
           traverseTreeChildren(tree)
-        case IsTypeTree(tree) =>
+        case tree: TypeTree =>
           buff.append(tree.tpe.showExtractors)
           buff.append("\n\n")
           traverseTreeChildren(tree)
diff --git a/tests/run/refined-binding-nat.check b/tests/run/refined-binding-nat.check
new file mode 100644
index 000000000000..5dc5e167eeae
--- /dev/null
+++ b/tests/run/refined-binding-nat.check
@@ -0,0 +1,6 @@
+Some((SuccClass(SuccClass(ZeroObject)),SuccClass(ZeroObject)))
+Some((ZeroObject,SuccClass(SuccClass(ZeroObject))))
+None
+Some((2,1))
+Some((0,2))
+None
diff --git a/tests/run/refined-binding-nat.scala b/tests/run/refined-binding-nat.scala
new file mode 100644
index 000000000000..0c6c12a257e9
--- /dev/null
+++ b/tests/run/refined-binding-nat.scala
@@ -0,0 +1,123 @@
+
+object Test {
+  def main(args: Array[String]): Unit = {
+    app(ClassNums)
+    app(IntNums)
+  }
+
+  def app(peano: Peano): Unit = {
+    import peano.{_, given}
+    def divOpt(m: Nat, n: Nat): Option[(Nat, Nat)] = {
+      n match {
+        case Zero => None
+        case s @ Succ(_) => Some(safeDiv(m, s))
+      }
+    }
+    val two = Succ(Succ(Zero))
+    val five = Succ(Succ(Succ(two)))
+    println(divOpt(five, two))
+    println(divOpt(two, five))
+    println(divOpt(two, Zero))
+  }
+}
+
+trait Peano {
+  type Nat
+  type Zero <: Nat
+  type Succ <: Nat
+
+  def safeDiv(m: Nat, n: Succ): (Nat, Nat)
+
+  given Typeable[Nat, Zero] {
+    def unapply(x: Nat): Option[Zero] = matchZero(x)
+  }
+
+  given Typeable[Nat, Succ] {
+    def unapply(x: Nat): Option[Succ] = matchSucc(x)
+  }
+
+  // given reflect.ClassTag[Succ] = ???
+
+  protected def matchZero(x: Nat): Option[Zero]
+  protected def matchSucc(x: Nat): Option[Succ]
+
+  implicit def succDeco(succ: Succ): SuccAPI
+  trait SuccAPI {
+    def pred: Nat
+  }
+
+  val Zero: Zero
+
+  val Succ: SuccExtractor
+  trait SuccExtractor {
+    def apply(nat: Nat): Succ
+    def unapply(nat: Succ): Option[Nat]
+  }
+}
+
+object IntNums extends Peano {
+  type Nat  = Int
+  type Zero = Int
+  type Succ = Int
+
+  protected def matchZero(x: Nat): Option[Zero] = if (x == 0) Some(0) else None
+  protected def matchSucc(x: Nat): Option[Succ] = if (x != 0) Some(x) else None
+
+  def safeDiv(m: Nat, n: Succ): (Nat, Nat) = (m / n, m % n)
+
+  val Zero: Zero = 0
+
+  object Succ extends SuccExtractor {
+    def apply(nat: Nat): Succ = nat + 1
+    def unapply(nat: Succ) = Some(nat - 1)
+  }
+  def succDeco(succ: Succ): SuccAPI = new SuccAPI {
+    def pred: Nat = succ - 1
+  }
+}
+
+object ClassNums extends Peano {
+  trait NatTrait
+  object ZeroObject extends NatTrait {
+    override def toString: String = "ZeroObject"
+  }
+  case class SuccClass(predecessor: NatTrait) extends NatTrait
+
+  type Nat  = NatTrait
+  type Zero = ZeroObject.type
+  type Succ = SuccClass
+
+  protected def matchZero(x: Nat): Option[Zero] = x match {
+    case Zero => Some(Zero)
+    case _ => None
+  }
+  protected def matchSucc(x: Nat): Option[Succ] = x match {
+    case nat: SuccClass => Some(nat)
+    case _ => None
+  }
+
+  def safeDiv(m: Nat, n: Succ): (Nat, Nat) = {
+    def intValue(x: Nat, acc: Int): Int = x match {
+      case nat: SuccClass => intValue(nat.predecessor, acc + 1)
+      case _ => acc
+    }
+    def natValue(x: Int): Nat =
+      if (x == 0) ZeroObject
+      else new SuccClass(natValue(x - 1))
+    val i = intValue(m, 0)
+    val j = intValue(n, 0)
+    (natValue(i / j), natValue(i % j))
+  }
+
+  val Zero: Zero = ZeroObject
+
+  object Succ extends SuccExtractor {
+    def apply(nat: Nat): Succ = new SuccClass(nat)
+    def unapply(nat: Succ) = Some(nat.predecessor)
+  }
+
+  def succDeco(succ: Succ): SuccAPI = new SuccAPI {
+    def pred: Nat = succ.predecessor
+  }
+
+}
diff --git a/tests/run/refined-binding.check b/tests/run/refined-binding.check
new file mode 100644
index 000000000000..14e859cfe54b
--- /dev/null
+++ b/tests/run/refined-binding.check
@@ -0,0 +1,2 @@
+ok
+9
diff --git a/tests/run/refined-binding.scala b/tests/run/refined-binding.scala
new file mode 100644
index 000000000000..9199f4e13d1e
--- /dev/null
+++ b/tests/run/refined-binding.scala
@@ -0,0 +1,33 @@
+
+sealed trait Foo {
+
+  type X
+  type Y <: X
+
+  def x: X
+
+  def f(y: Y) = println("ok")
+
+  given Typeable[X, Y] = new Typeable {
+    def unapply(x: X): Option[Y] = Some(x.asInstanceOf[Y])
+  }
+
+  object Z {
+    def unapply(arg: Y): Option[Int] = Some(9)
+  }
+}
+
+object Test {
+  def main(args: Array[String]): Unit = {
+    test(new Foo { type X = Int; type Y = Int; def x: X = 1 })
+  }
+
+  def test(foo: Foo): Unit = {
+    import foo.given
+    foo.x match {
+      case x @ foo.Z(i) => // `x` is refined to type `foo.Y`
+        foo.f(x)
+        println(i)
+    }
+  }
+}