在另一模块的类中创建类对象的模块导入导出问题

问题场景 #

开发Dafny项目时遇到模块类型不兼容报错，代码结构如下：

Module1.dfy #

module Module1 {
    export Private
        provides test1
        reveals test1, T

    class test1{
        var a: nat
        var b: nat

        constructor()
        {
            a := 0;
            b := 0;
        }

        method add() returns (c: nat) 
            ensures c == a + b
        {
            c := a + b;
        }
    }

    trait T {
        var x: nat

        predicate valid()
            reads this
    }
}

Module2.dfy #

include "module1.dfy"

module Module2 refines Module1 {
    import opened Module1`Private

    class test2{
        var d: nat
        var module1Obj: test1

        constructor() {
            d := 0;
            module1Obj := new Module1.test1(); // ERROR: type Module1.test1 is not assignable to LHS (of type test1)
        }
    }

    class test3 extends T {
        predicate valid() {
            x == 0
        }

        constructor()
            ensures valid()
        {
            x := 0;
        }
    }
}

报错提示type Module1.test1 is not assignable to LHS (of type test1)，尝试将Module1改为抽象类未解决问题，需修正模块导入/导出逻辑。

解决方案 #

问题核心是精炼模块的类型作用域与父模块导出规则不匹配，调整如下：

1. 修正Module1的导出规则 #

将provides test1移除，仅保留reveals test1, T，让精炼模块能完整识别父模块的类型：

module Module1 {
    export Private
        reveals test1, T

    class test1{
        var a: nat
        var b: nat

        constructor()
        {
            a := 0;
            b := 0;
        }

        method add() returns (c: nat) 
            ensures c == a + b
        {
            c := a + b;
        }
    }

    trait T {
        var x: nat

        predicate valid()
            reads this
    }
}

说明：provides仅导出类的公共接口，不会建立精炼模块与父模块类型的直接兼容关系；reveals会完整暴露类型定义，确保精炼模块能正确解析父模块的类型。

2. 修正Module2的类型引用 #

在精炼模块中直接使用test1而非Module1.test1，因为精炼模块会继承父模块的类型作用域：

include "module1.dfy"

module Module2 refines Module1 {
    import opened Module1`Private

    class test2{
        var d: nat
        var module1Obj: test1

        constructor() {
            d := 0;
            module1Obj := new test1(); // 直接引用继承的test1类型
        }
    }

    class test3 extends T {
        predicate valid() {
            x == 0
        }

        constructor()
            ensures valid()
        {
            x := 0;
        }
    }
}

3. 可选：简化导入逻辑（若无需私有访问） #

如果Module2不需要访问Module1的私有导出块，可移除import opened Module1Private`，直接依赖精炼的公共接口：

include "module1.dfy"

module Module2 refines Module1 {
    class test2{
        var d: nat
        var module1Obj: test1

        constructor() {
            d := 0;
            module1Obj := new test1();
        }
    }

    class test3 extends T {
        predicate valid() {
            x == 0
        }

        constructor()
            ensures valid()
        {
            x := 0;
        }
    }
}

内容的提问来源于stack exchange，提问作者Drona Nagarajan