Lack of qualified type names makes error messages unclear

[joscoh]

The program

module A {
  module C {
    datatype Option<T> = None | Some(x : T)
  }
}

module B {
  module C {
    datatype Option<T> = None | Some(x : T)

  }
}

module C {
  import A
  import B

  lemma Bad(x: int)
  ensures A.C.Some(x) == B.C.Some(x)
}

results in the error message (on the ensures clause)

Error: arguments must have comparable types (got Option<int> and Option<int>).

It would be helpful to print the qualified names of the types in these cases.

[tjhance]

To add on to this: I've noticed that even when Dafny does qualify type names in its error messages, it often uses import alias names in the qualifications, rather than using the canonical module name. I think having the canonical module names would be a lot more helpful to the user in determining the reason of the type error.