One of the original lambda proposals for Java - the one from Neal Gafter - also had checked exceptions.

The problem is that you then need a way to capture exception specifications as generic type parameters to properly propagate contracts, which complicates the type system quite a bit. Which is why Java ultimately went with the much simpler proposal that didn't even try to tackle this.

Yes I'm well aware, but that is uniquely a Java problem. With a sufficiently strong type system, like the one in Scala, you can easily make checked exceptions work across higher order functions.