I see the verification of the wellformedness of Absy.Foo is done twice. Is that required for soundness? I have trouble overseeing the implication of the import A : Absy and whether that could effect the wellformedness of Absy.Foo. In any case, suppose import A : Absy would cause a verification issue, then the error should be shown at the import, not at the original method definition.

Here is a variant of this same issue, which shows that it's not restricted to imports:

abstract module Absy {
  function f(): int { 0 / 0 }
}

abstract module StillAsby refines Absy {
}

This produces the following output:

test.dfy(2,22): Error: possible division by zero
  |
2 |   function f(): int { 0 / 0 }
  |                       ^^^^^

test.dfy[StillAsby](2,22): Error: possible division by zero
  |
2 | <nonexistent line>
  |                       ^


Dafny program verifier finished with 0 verified, 2 errors

For this variant, however, we did not use to print two errors until very recently; that bug was introduced in 3.7.2.

The problem in the original post:

abstract module Absy {
  function f(): int { 0 / 0 }
}

abstract module StillAsby {
  import A: Absy
}

reports two errors in every version of Dafny that can parse it.

I don't think it should: module verification is supposed to be modular, so I don't see why we're re-checking well-formedness :/

I agree that there should be no need to verify this twice. I don't know how come we do.

This is how these things are generally performed: There are two cases when we make a refinement clone of a module--when you say module B refines A and when you say import X: SomeModule. The refinement cloner wraps each IToken in a RefinementToken. This signals to the verifier that the AST node was created during refinement, which implies that the original AST node is verified elsewhere.

So, perhaps what's going wrong in the report bug is that the RefinementToken is either not created or not detected. It should have been created using a call to the virtually dispatched Tok method in Cloner. Maybe the detection doesn't handle multiply-wrapped tokens correctly--perhaps it only checks tok is RefinementToken, whereas it should keep unwrapping WrappedTokens to see if any of the wrappers is a RefinementToken.