Question

Dafny doesn’t like when a type and a module have the same name. How can I fix this?

module Result {
  datatype Result<T> = Success(x: T) | Failure(e: string)
}
module Test {
  import opened Result
  function method f(): Result<int>
  {
    Success(0)
  }
}

produces

FAQNameConflict.dfy(6,23): Error: Wrong number of type arguments (1 instead of 0) passed to module: Result
1 resolution/type errors detected in FAQNameConflict.dfy

Answer

The problem is that in the Test module, the name Result is both a module name and a datatype name. The module name takes precedence and so the resolution error happens. (Despite the error message, modules never have type arguments.)

This situation can be fixed two ways. First, write Result.Result to mean the datatype. Or second, import the module with a new name, such as import opened R = Result. Then inside module Test, there is the name R for a module and the name Result for the datatype. The following code shows both these options.

module Result {
  datatype Result<T> = Success(x: T) | Failure(e: string)
}
module Test {
  import opened Result
  function method f(): Result.Result<int>
  {
    Success(0)
  }
}
module Test1 {
  import opened R = Result
  function method f(): Result<int>
  {
    Success(0)
  }
}