Crash on constrained subset of sequence type with explicit witness

[rod-chapman]

The following code crashes the Dafny compiler/verifier (version 3.9.0 I think from the output.) The final subset type declaration causes the crash. The one before (with the "witness *" clause) seems to be OK.

include "../libraries/src/BoundedInts.dfy"

module {:options "-functionSyntax:4"} DafnyNaCl
{
  import opened BoundedInts

  // M2256 = 2**256
  const M2256 := 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000

  // P = 2**255 - 19
  const P := 0x8000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000 - 19

  // Number of GF Digits. 15 digits of 16 bits each is 256 bits.
  const NGFD := 16
  const LM := 65536
  const LMM1 := 65535
  const R2256 := M2256 % P // 38 on a good day

  const MGFLC := (R2256 * 15) + 1

  const MGFLP := LMM1 * LMM1

  type Index_16 = x : nat | 0 <= x < NGFD

  type GF64_Any_Limb = i : int64 | -LM as int64 <= i <= (MGFLC * MGFLP) as int64
  type UGF64 = seq<GF64_Any_Limb>
  
  type GF64 = a : UGF64 | |a| == NGFD witness seq(NGFD, _ => 0)

  type Normal_GF64_OK      = a : GF64 | (forall i : Index_16 :: 0 <= a[i] <= LMM1 as GF64_Any_Limb) witness *
  type Normal_GF64_Crashes = a : GF64 | (forall i : Index_16 :: 0 <= a[i] <= LMM1 as GF64_Any_Limb) witness seq(NGFD, _ => 0)

}

The terminal output that I see in VSCode is:

rodchap@f4d4889dcf6d nacl % "/opt/homebrew/bin/dotnet" "/Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/dafny/Dafny.dll" "/Users/rodchap/Desktop/r
od/projects/dafny/nacl/issue2926.dfy" /verifyAllModules /spillTargetCode:1 /compile:3 /out:bin/issue2926
Unhandled exception. System.AggregateException: One or more errors occurred. (Unable to cast object of type 'Microsoft.Dafny.TypeSynonymDecl' to type 'Microsoft.Dafny.NewtypeDecl'.)
 ---> System.InvalidCastException: Unable to cast object of type 'Microsoft.Dafny.TypeSynonymDecl' to type 'Microsoft.Dafny.NewtypeDecl'.
   at Microsoft.Dafny.Translator.CheckResultToBeInType_Aux(IToken tok, Expression expr, Type toType, BoogieStmtListBuilder builder, ExpressionTranslator etran, String errorMsgPrefix) in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyCore/Verifier/Translator.cs:line 5551
   at Microsoft.Dafny.Translator.CheckResultToBeInType_Aux(IToken tok, Expression expr, Type toType, BoogieStmtListBuilder builder, ExpressionTranslator etran, String errorMsgPrefix) in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyCore/Verifier/Translator.cs:line 5555
   at Microsoft.Dafny.Translator.CheckResultToBeInType(IToken tok, Expression expr, Type toType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, String errorMsgPrefix) in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyCore/Verifier/Translator.cs:line 5531
   at Microsoft.Dafny.Translator.AddWellformednessCheck(RedirectingTypeDecl decl) in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyCore/Verifier/Translator.cs:line 4481
   at Microsoft.Dafny.Translator.AddTypeDecl(SubsetTypeDecl dd) in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyCore/Verifier/Translator.cs:line 1258
   at Microsoft.Dafny.Translator.AddTypeDecl(RevealableTypeDecl d) in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyCore/Verifier/Translator.cs:line 1217
   at Microsoft.Dafny.Translator.DoTranslation(Program p, ModuleDefinition forModule) in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyCore/Verifier/Translator.cs:line 789
   at Microsoft.Dafny.Translator.Translate(Program p, ErrorReporter reporter, TranslatorFlags flags)+MoveNext() in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyCore/Verifier/Translator.cs:line 861
   at Microsoft.Dafny.DafnyDriver.Translate(ExecutionEngineOptions options, Program dafnyProgram)+MoveNext() in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyDriver/DafnyDriver.cs:line 386
   at System.Collections.Generic.List`1..ctor(IEnumerable`1 collection)
   at System.Linq.Enumerable.ToList[TSource](IEnumerable`1 source)
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyDriver/DafnyDriver.cs:line 325
   --- 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) in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyDriver/DafnyDriver.cs:line 122
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0() in /Users/rodchap/.vscode/extensions/dafny-lang.ide-vscode-2.8.5/out/resources/3.9.0/custom/arm64/dafny/Source/DafnyDriver/DafnyDriver.cs:line 99
   at System.Threading.Thread.StartCallback()
zsh: abort      "/opt/homebrew/bin/dotnet"   /verifyAllModules /spillTargetCode:1 /compile:3 
rodchap@f4d4889dcf6d nacl %