chore: improve error message for seq type mismatch

Source/DafnyCore/Resolver.cs

@@ -17646,7 +17646,15 @@ void ResolveSeqSelectExpr(SeqSelectExpr e, ResolutionContext resolutionContext)
         AddXConstraint(e.E0.tok, "ContainerIndex", e.Seq.Type, e.E0.Type, "incorrect type for selection into {0} (got {1})");
         Contract.Assert(e.E1 == null);
         e.Type = new InferredTypeProxy() { KeepConstraints = true };
-        AddXConstraint(e.tok, "ContainerResult", e.Seq.Type, e.Type, "type does not agree with element type of {0} (got {1})");
+        AddXConstraint(e.tok, "ContainerResult",
+          e.Seq.Type, e.Type,
+          new TypeConstraint.ErrorMsgWithToken(
+            e.tok,
+            "selected element has type {0} which is incompatible with expected type {1} ({2} is incompatible with {3})",
+            new SeqTypeArgToBeResolved(e.Seq.Type),
+            new SeqTypeArgToBeResolved(e.Type),
+            e.Seq.Type,
+            e.Type));
       } else {
         AddXConstraint(e.tok, "MultiIndexable", e.Seq.Type, "multi-selection of elements requires a sequence or array (got {0})");
         if (e.E0 != null) {
@@ -17661,7 +17669,21 @@ void ResolveSeqSelectExpr(SeqSelectExpr e, ResolutionContext resolutionContext)
         }
         var resultType = new InferredTypeProxy() { KeepConstraints = true };
         e.Type = new SeqType(resultType);
-        AddXConstraint(e.tok, "ContainerResult", e.Seq.Type, resultType, "type does not agree with element type of {0} (got {1})");
+        AddXConstraint(e.tok, "ContainerResult", e.Seq.Type, resultType, "multi-selection has type {0} which is incompatible with expected type {1}");
+      }
+    }
+
+    /// <summary>
+    /// Allows to lazily call ToString on the given (sequence) type's element type.
+    /// 
+    /// When adding type constraints, a sequence type's element type (`AsSeqType.Arg`) may not be resolved,
+    /// so attempting to eagerly read it (for use in an error message) results in a null reference.
+    /// By wrapping the sequence type in this object, the error handling logic will only read `AsSeqType.Arg`
+    /// on the element type after it is resolved.
+    /// </summary>
+    private record SeqTypeArgToBeResolved(Type seqType) {
+      public override string ToString() {
+        return seqType.AsSeqType.Arg.ToString();
       }
     }
 

Test/git-issues/git-issue-1887.dfy

@@ -0,0 +1,12 @@
+// RUN: %dafny_0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function method selectOneConstraint<T>(s: seq<T>): seq<string> {
+  if |s| == 0 then []
+  else [s[0]] + selectOneConstraint(s[1..])
+}
+
+function method selectManyConstraint<T>(s: seq<T>): seq<string> {
+  if |s| <= 1 then []
+  else s[0..2] + selectManyConstraint(s[2..])
+}

Test/git-issues/git-issue-1887.dfy.expect

@@ -0,0 +1,3 @@
+git-issue-1887.dfy(6,9): Error: selected element has type T which is incompatible with expected type char (seq<T> is incompatible with seq<char>)
+git-issue-1887.dfy(11,8): Error: multi-selection has type seq<T> which is incompatible with expected type seq<char>
+2 resolution/type errors detected in git-issue-1887.dfy