A project I’m working on has a peculiar construct. I created a module like so:

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
    }
}

I created another module with a different class like so:

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;
        }
    }
}

I’m not sure how to import/export modules in this construct. I tried redefining Module1 as abstract, but that does not work. If this is a wrong approach, a correct approach will be highly appreciated.