Underspecified subset-type type arguments causes crash

[RustanLeino]

Dafny version

4.0.0

Code to produce this issue

type SubsetType<X> = x: int | true

method M() {
  var s: SubsetType; // type parameter underspecified
  s := 3;
}

Command to run and resulting output

% dafny test.dfy
Unhandled exception. System.AggregateException: One or more errors occurred. (Exception of type 'cce+UnreachableException' was thrown.)
 ---> cce+UnreachableException: Exception of type 'cce+UnreachableException' was thrown.
   at Microsoft.Dafny.Translator.TypeToTy(Type type)
   at System.Collections.Generic.List`1.ConvertAll[TOutput](Converter`2 converter)
   at Microsoft.Dafny.Translator.TypeToTy(Type type)
   at Microsoft.Dafny.Translator.MkIs(Expr x, Type t)
   at Microsoft.Dafny.Translator.GetSubrangeCheck(Expr bSource, Type sourceType, Type targetType, ProofObligationDescription& desc, String errorMessagePrefix)
   at Microsoft.Dafny.Translator.TrAssignmentRhs(IToken tok, IdentifierExpr bGivenLhs, IVariable lhsVar, Type lhsType, AssignmentRhs rhs, Type rhsTypeConstraint, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)
...

What happened?

Instead of giving an error that the type of s is underspecified, Dafny (proceeds to the verifier and) crashes.

What type of operating system are you experiencing the problem on?

Mac

[RustanLeino]

Here's a similar test case that fails in the same way:

type SubsetType<X> = x: int | true
datatype Record<U> = Record(SubsetType<U>)

method P(r: Record<real>) {
  match r
  case Record(s: SubsetType) => // type argument underspecified
}