Dafny encountered an internal error

[sligocki]

I encountered the following error. Version v2.8.2 in Visual Studios.

[{
    "resource": "/Users/sl929/fun/dafny_projects/busy_beaver/tape.dfy",
    "owner": "dafny-vscode",
    "severity": 8,
    "message": "Dafny encountered an internal error. Please report it at <https://github.com/dafny-lang/dafny/issues>.\ncce+UnreachableException: Exception of type 'cce+UnreachableException' was thrown.\n   at Microsoft.Dafny.Resolver.SubstType(Type type, Dictionary`2 subst)\n   at Microsoft.Dafny.Substituter.Substitute(Expression expr)\n   at Microsoft.Dafny.Substituter.Substitute(Expression expr)\n   at Microsoft.Dafny.Translator.AddFunctionConsequenceAxiom(Function boogieFunction, Function f, List`1 ens)\n   at Microsoft.Dafny.Translator.AddClassMember_Function(Function f)\n   at Microsoft.Dafny.Translator.AddFunction_Top(Function f, Boolean includeAllMethods)\n   at Microsoft.Dafny.Translator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType)\n   at Microsoft.Dafny.Translator.AddTypeDecl(RevealableTypeDecl d)\n   at Microsoft.Dafny.Translator.DoTranslation(Program p, ModuleDefinition forModule)\n   at Microsoft.Dafny.Translator.Translate(Program p, ErrorReporter reporter, TranslatorFlags flags)+MoveNext()\n   at System.Collections.Generic.List`1..ctor(IEnumerable`1 collection)\n   at System.Linq.Enumerable.ToList[TSource](IEnumerable`1 source)\n   at System.Threading.Tasks.Task`1.InnerInvoke()\n   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)\n--- End of stack trace from previous location ---\n   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)\n--- End of stack trace from previous location ---\n   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(DocumentAfterResolution document, CancellationToken cancellationToken)\n   at Microsoft.Dafny.LanguageServer.Workspace.Compilation.PrepareVerificationTasksAsync(DocumentAfterResolution loaded, CancellationToken cancellationToken)\n   at Microsoft.Dafny.LanguageServer.Workspace.Compilation.TranslateAsync()",
    "startLineNumber": 1,
    "startColumn": 1,
    "endLineNumber": 1,
    "endColumn": 2
}]

File tape.dfy

include "turing_machine.dfy"

// Generic Tape interface with all necessary post-conditions listed.
abstract module TapeInterface {
  import TM : TuringMachineInterface

  type Symbol = TM.Symbol
  type Tape

  function Blank(init_symbol : Symbol) : Tape
    ensures forall pos :: Read(Blank(init_symbol), pos) == init_symbol

  function Read(tape : Tape, pos : int) : Symbol

  function Write(tape : Tape, pos : int, val : Symbol) : Tape
    ensures Read(Write(tape, pos, val), pos) == val
    ensures forall p2 :: p2 != pos ==>
      Read(Write(tape, pos, val), p2) == Read(tape, p2)
}

// Stack-allocated, non-mutable Tape representation convenient for
// specification
module Tape refines TapeInterface {
  datatype Tape = Tape(
    data : map<int, Symbol>,
    init_symbol : Symbol
  )

  function Blank(init_symbol : Symbol) : Tape {
    Tape(data := map[], init_symbol := init_symbol)
  }

  function Read(tape : Tape, pos : int) : Symbol {
    if pos in tape.data then tape.data[pos] else tape.init_symbol
  }

  // Return a new Tape with update written.
  function Write(tape : Tape, pos : int, val : Symbol) : Tape {
    Tape(data := tape.data[pos := val],
         init_symbol := tape.init_symbol)
  }
}

File turing_machine.dfy:

abstract module TuringMachineInterface {
  type State
  type Symbol
  type TM

  datatype StateOrHalt = State(state : State) | Halt

  datatype Dir = Right | Left
  datatype Transition =
    Transition(symbol : Symbol, state : StateOrHalt, dir : Dir)

  function LookupTrans(
    tm : TM, state : State, symbol : Symbol) : Transition
}

module TuringMachineNat refines TuringMachineInterface {
  type State = nat
  type Symbol = nat
}

[robin-aws]

By running your example through the dafny CLI I can see the underlying error:

tape.dfy[Tape](7,16): Error: a compiled module is not allowed to use an abstract module (TM)

That's because in TapeInterface you specify that TM must be a module that refines TuringMachineInterface, but the concrete Tape module doesn't specify which concrete module it uses. Adding import TM = TuringMachineNat to the top of that module resolves the error and is what I believe you intended.

This still exposes that there are incorrect assumptions about resolution that only the language server exposes for some reason though, so thank you for the bug report!

[sligocki]

Thanks, glad I could help.