CC @griesemer

Relatedly, type A = interface { a1; a2 } should also be okay: #6977 (comment)

I think adding something like case t.Pkg != nil && t.Pkg != localpkg: return to the switch in addMethod in expandiface should work. That should suppress duplicate method errors for imported interface types.

[edited]

When compiling a Go 1.13 package, shouldn't we fail if we depend on a Go 1.14 feature via an import?

This is a corner-case because it can be "made to work" - but in general it's quite possible that a new language feature (contracts!) exposed via exports cannot be consumed by a package compiled for an older language version.

Summary: I agree with the argument in #6977 (comment): In this specific case, the combination of a1; a2 is done in package a and not "visible" in package b so this should be ok.

When compiling a Go 1.13 package, shouldn't we fail if we depend on a Go 1.14 feature via an import?

I'm not sure. We don't have much precedent for what it should do. For Go 1.9, we allowed a -lang=go1.9 package to export alias types, which could then be used by -lang=go1.8 packages. For Go 1.13, we didn't introduce any changes that could affect the type identity of exported identifiers.

I'm thinking the Go spec* needs to introduced the concept of Go language version, and it needs to be explained how differing language versions across packages should work. (* I'd also be fine with a separate document, like how the memory model is separately defined.)

Change https://golang.org/cl/205977 mentions this issue: cmd/compile: don't apply -lang=go1.X restrictions to imported packages