Sharing types across modules and "as" keyword

Jul 18, 2014 at 12:06 PM
When I use module import with the "as" keyword, other modules no longer recognize that two references to the same type are the same.

For example, this works:

http://rise4fun.com/Dafny/ori95
module A
{
  type S
}

module B
{
  import A
  
  static function bar(s:A.S) : A.S
}

module C
{
    import A
    import BL as B
    
    function foo(s:A.S) : A.S
    {
      BL.bar(s)
    }
}
But this does not

http://rise4fun.com/Dafny/Hn8k
module A
{
  type S
}

module B
{
  import AL as A
  
  static function bar(s:AL.S) : AL.S
}

module C
{
    import AL as A 
    import BL as B
    
    function foo(s:AL.S) : AL.S
    {
      BL.bar(s)
    }
}
Jul 18, 2014 at 12:42 PM
I also expected to be able to do the following, and do not seem to be able to:

http://rise4fun.com/Dafny/hDhZ
module A
{
  type S
  static function bar(s:S) : S
}

module B refines A
{
  static function bar'(s:S) : S
}

module C
{
  import A 
  
  function foo(s:A.S) : A.S
  {
    A.bar(s)
  }
}

module D refines C
{
    import B
    
    function foo'(s:B.S) : B.S
    {
      foo(B.bar'(s))
    }
}