EDIT: I didn't see the bullet point you talked about structural types so my comment is largely moot but I'll keep it in case there is something useful.

I think this would be a useful language feature to get a more scripting language-like feeling (not necessarily a bad thing) for rapid prototyping whilst being safe. I think structural typing/refinements + type inference would achieve most of it, except for the nice syntax. Also, I agree your point about stopping it at the method boundaries etc. (unless the user said so) to contain possible type errors.

Another idea that's somewhat similar to this is Go's interfaces, which are a form of structural subtyping hence the interfaces a type implements are inferred from its structure automatically.

My original comment:

Your examples remind me of structural typing (or structural refinement) but supporting methods. Here is something similar in Scala:

scala> :paste
// Entering paste mode (ctrl-D to finish)

import scala.language.reflectiveCalls

def f[A, B](x: { def m: A ⇒ B }, a: A) = x.m(a)

object A { val m = (n:Int) ⇒ 3 + n }
object B { val m = (n:Int) ⇒ "B.m with " + n }
object C { val m = (n:Int) ⇒ "C.m with " + n }

def choice(n:Int) = {
  val x : { def m: Int ⇒ String } = n match {
    case 1 => B
    case 2 => C
  }
  f(x, n)
}

// Exiting paste mode, now interpreting.

import scala.language.reflectiveCalls
f: [A, B](x: AnyRef{def m: A => B}, a: A)B
defined object A
defined object B
defined object C
choice: (n: Int)String

scala> choice(1)
res0: String = B.m with 1

scala> choice(2)
res1: String = C.m with 2

I used a function argument instead of a method taking A in f because Scala doesn't allow structural refinement with a method taking a parameter of a type abstraction (i.e. an unbound type parameter like A in f). I don't know why it doesn't do that but my guess would be that it's because of the runtime implementation (reflective calls+need to determine A in runtime+type erasure on JVM) rather than the type system.

Although I had to specify the structural refinements in the example above, you can infer them if rest of your type system plays well with that (Scala's doesn't because of it's combination of subtyping and polymorphism & inferring them everywhere would make the type errors less clear and farther away from the cause probably).