Dafny crash on a recursive definition

[codyroux]

When evaluating this code

datatype Either<+L, +R> = Left(l: L) | Right(r: R)

datatype Lang<!A> = Lang(mem: (string, A) -> bool, repr: iset<A>)

function Atom<A>(s: string, value: A): Lang<A> {
  Lang((input, a) => s == input && a == value, iset{})
}

function Char(c: char): Lang<char> {
  Atom([c], c)
}

function EitherL<A, B>(l: Lang<A>, r: Lang<B>): Lang<Either<A, B>> {
  Lang((input, ab: Either<A, B>) =>
    || (exists a | a in l.repr :: ab == Left(a) && l.mem(input, a))
    || (exists b | b in r.repr :: ab == Right(b) && r.mem(input, b)),
    (iset a | a in l.repr :: Left(a)) + (iset b | b in r.repr :: Right(b))
  )
}

// Nondeterministic in general
function ConcatL<A, B> (l: Lang<A>, r: Lang<B>): Lang<(A, B)> {
  Lang((input, p) =>
    exists s1, s2, a, b | a in l.repr && b in r.repr::
      input == s1 + s2 && p == (a, b),
    iset a, b | a in l.repr && b in r.repr :: (a,b)
  )
}

function Empty<A>(): Lang<A> { Lang((_, _) => false, iset{}) }

function MapL<A, B> (l: Lang<A>, f: A -> B): Lang<B> {
  Lang((input, b) =>
    exists a: A | a in l.repr :: b == f(a) && l.mem(input, a),
    iset a | a in l.repr :: f(a)
  )
}

function Ignore<A>(l: Lang<A>): Lang<()> { MapL(l, (_) => ()) }

function Epsilon(): Lang<()> {
  Lang((input, _) => input == "", iset{})
}

function RepeatAux<A>(pred : (string, A) -> bool, repr: iset<A>, input: string, output: seq<A>): bool
  decreases |output|
{
  || (input == "" && output == [])
  || (exists init, tail, a, alist | a in repr ::
      && input == init + tail
      && output == [a] + alist
      && pred(a, init)
      && RepeatAux(pred, repr, tail, alist))
}

With this command:
/home/codyroux/dotnet/dotnet Dafny.dll myfile.dfy /verifyAllModules /compile:0

gives the following error:

Unhandled exception. System.AggregateException: One or more errors occurred. (Index was out of range. Must be non-negative and less than the size of the collection. (Parameter 'index'))
 ---> System.ArgumentOutOfRangeException: Index was out of range. Must be non-negative and less than the size of the collection. (Parameter 'index')
   at Microsoft.Dafny.Resolver.ImposeSubtypingConstraint(Type super, Type sub, ErrorMsg errorMsg)
   at Microsoft.Dafny.Resolver.AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, Boolean keepConstraints)
   at Microsoft.Dafny.Resolver.AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, Boolean keepConstraints)
   at Microsoft.Dafny.Resolver.AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, Boolean keepConstraints)
   at Microsoft.Dafny.Resolver.AssignKnownEndsFullstrength_SuperDirection(TypeProxy proxy)
   at Microsoft.Dafny.Resolver.ProcessFullStrength_SuperDirection(Type t, ISet`1 processed, Boolean& anyNewConstraints)
   at Microsoft.Dafny.Resolver.PartiallySolveTypeConstraints(Boolean allowDecisions)
   at Microsoft.Dafny.Resolver.SolveAllTypeConstraints()
   at Microsoft.Dafny.Resolver.ResolveFunction(Function f)
   at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl)
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport)
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport)
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog)
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter)
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass9_0.<Main>b__0()
   at System.Threading.Thread.StartCallback()

With /version giving ng.ide-vscode-2.8.2/out/resources/nightly-2022-09-28-4b97862/dafny/Dafny.dll.

Apologies for the lack of example minimization.

[cpitclaudel]

Short repro:

method RepeatAux()
{
  var a;
  var b := [a];
  var s: string := a;
}

Another short repro:

method RepeatAux<A>()
{
  var s;
  var s': string := s;
  var s'' := s + s;
}

[cpitclaudel]

The fix in both cases is to use additional type annotations. This reveals that pred(a, init) should have been pred(init, a) in the original example (and also that unbounded quantification on alist is not valid because it may contain references.