Matching of an imported ADT some times fails

[davidstreader]

This seems to be a bug But I am no expert.

module inner {
  export reveals Twee   
    datatype Twee = Node(value: int, left: Twee, right: Twee) | Leaf
}
module outer {
import TL = inner 
function working(t:TL.Twee) :TL.Twee
  {  match t 
       case Leaf => t  
       case Node(v,l,r) => TL.Node(v,r,l)
 }  
 function failing(t:TL.Twee) :TL.Twee
  {
    match t 
       case Leaf => t 
       case Node(v,Leaf,r) => TL.Node(v,TL.Leaf,r)
       case Node(v,Node(vl,ll,rl),r) => TL.Node(vl,ll,TL.Node(v,rl,r))       
  }
}

The function failing produces two parse errors. Yet moved to module inner and with TL. removed it can be verified.

[RustanLeino]

I don't get any parse errors on this example.

[RustanLeino]

Currently, Dafny looks up case-pattern constructor names in the type of the source expression (that is, the type of t in failing). It also does this for nested constructors in patterns. So, currently, case patterns do not support (or (usually) need) qualifications.

Enhancement: Dafny should support (but not insist on) qualifications in patterns. If a qualification (like TL.Leaf or TL.Twee.Leaf) is mentioned, then the qualification is the guide to where the constructor name is looked up. If no qualification is given, then the behavior is as today.

Another enhancement: For unqualified constructors in nested patterns, the Dafny implementation should partially solve type constraints before looking up the constructor name (just like it does at the outermost level).