fix: Clarify error location of inlined is predicates (#5587)

### Description

Changes error location of `x is T` predicates (especially, inlined `is`
predicates) from the `x` to the `is`.

Fixes #5586 

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -862,7 +862,7 @@ public Boogie.Expr TrExpr(Expression expr) {
             }
           case TypeTestExpr testExpr: {
               var e = testExpr;
-              return BoogieGenerator.GetSubrangeCheck(TrExpr(e.E), e.E.Type, e.ToType, e.E, null, out var _) ?? Boogie.Expr.True;
+              return BoogieGenerator.GetSubrangeCheck(e.tok, TrExpr(e.E), e.E.Type, e.ToType, e.E, null, out var _) ?? Boogie.Expr.True;
             }
           case BinaryExpr binaryExpr: {
               BinaryExpr e = binaryExpr;

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -1666,7 +1666,7 @@ private void CheckElementInit(IToken tok, bool forArray, List<Expression> dims,
       var apply = UnboxUnlessInherentlyBoxed(FunctionCall(tok, Apply(dims.Count), TrType(elementType), args), elementType);
 
       CheckElementInitReturnSubrangeCheck(dims, init, out var dafnySource, out var checkContext);
-      var cre = GetSubrangeCheck(apply, sourceType.Result, elementType, dafnySource, checkContext, out var subrangeDesc);
+      var cre = GetSubrangeCheck(apply.tok, apply, sourceType.Result, elementType, dafnySource, checkContext, out var subrangeDesc);
       if (cre != null) {
         // assert (forall i0,i1,i2,... ::
         //            0 <= i0 < ... && ... ==> init.requires(i0,i1,i2,...) is Subtype);

Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs

@@ -798,7 +798,7 @@ private void TrForLoop(ForLoopStmt stmt, BoogieStmtListBuilder builder, List<Var
         var sourceBoundVar = new BoundVar(Token.NoToken, "x", Type.Int);
         var checkContext = MakeNumericBoundsSubrangeCheckContext(sourceBoundVar, dLo, dHi);
         var cre = GetSubrangeCheck(
-          x, Type.Int, indexVar.Type,
+          x.tok, x, Type.Int, indexVar.Type,
           new IdentifierExpr(Token.NoToken, sourceBoundVar),
           checkContext, out var desc);
 

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -3804,15 +3804,15 @@ Bpl.Expr MkIsBox(Bpl.Expr x, Type t) {
     }
 
     // Boxes, if necessary
-    Bpl.Expr MkIs(Bpl.Expr x, Type t) {
-      return MkIs(x, TypeToTy(t), ModeledAsBoxType(t));
+    Bpl.Expr MkIs(Bpl.Expr x, Type t, Bpl.IToken tok = null) {
+      return MkIs(x, TypeToTy(t), ModeledAsBoxType(t), tok);
     }
 
-    Bpl.Expr MkIs(Bpl.Expr x, Bpl.Expr t, bool box = false) {
+    Bpl.Expr MkIs(Bpl.Expr x, Bpl.Expr t, bool box = false, Bpl.IToken tok = null) {
       if (box) {
-        return FunctionCall(x.tok, BuiltinFunction.IsBox, null, x, t);
+        return FunctionCall(tok ?? x.tok, BuiltinFunction.IsBox, null, x, t);
       } else {
-        return FunctionCall(x.tok, BuiltinFunction.Is, null, x, t);
+        return FunctionCall(tok ?? x.tok, BuiltinFunction.Is, null, x, t);
       }
     }
 
@@ -3983,6 +3983,7 @@ string SurrogateName(Field field) {
     public delegate Expression SubrangeCheckContext(Expression check);
 
     Bpl.Expr GetSubrangeCheck(
+      Bpl.IToken tok,
       Bpl.Expr bSource, Type sourceType, Type targetType,
       // allow null for checked expressions that cannot necessarily be named without side effects, such as method out-params
       [CanBeNull] Expression source,
@@ -4002,13 +4003,13 @@ Bpl.Expr GetSubrangeCheck(
       Bpl.Expr cre;
       if (udt?.ResolvedClass is RedirectingTypeDecl redirectingTypeDecl &&
           ModeledAsBoxType((redirectingTypeDecl as NewtypeDecl)?.BaseType ?? redirectingTypeDecl.Var.Type)) {
-        cre = MkIs(BoxIfNecessary(bSource.tok, bSource, sourceType), TypeToTy(targetType), true);
+        cre = MkIs(BoxIfNecessary(bSource.tok, bSource, sourceType), TypeToTy(targetType), true, tok);
       } else if (ModeledAsBoxType(sourceType)) {
-        cre = MkIs(bSource, TypeToTy(targetType), true);
+        cre = MkIs(bSource, TypeToTy(targetType), true, tok);
       } else if (targetType is UserDefinedType targetUdt) {
-        cre = MkIs(BoxifyForTraitParent(bSource.tok, bSource, udt.ResolvedClass, sourceType), targetType);
+        cre = MkIs(BoxifyForTraitParent(bSource.tok, bSource, udt.ResolvedClass, sourceType), targetType, tok);
       } else {
-        cre = MkIs(bSource, targetType);
+        cre = MkIs(bSource, targetType, tok);
       }
 
       Expression dafnyCheck = null;
@@ -4055,7 +4056,7 @@ void CheckSubrange(IToken tok, Bpl.Expr bSource, Type sourceType, Type targetTyp
       Contract.Requires(targetType != null);
       Contract.Requires(builder != null);
 
-      var cre = GetSubrangeCheck(bSource, sourceType, targetType, source, null, out var desc, errorMsgPrefix);
+      var cre = GetSubrangeCheck(tok, bSource, sourceType, targetType, source, null, out var desc, errorMsgPrefix);
       if (cre != null) {
         builder.Add(Assert(tok, cre, desc));
       }

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5586.dfy

@@ -0,0 +1,15 @@
+// RUN: %exits-with 4 %verify --type-system-refresh "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+trait Trait { }
+
+class Class extends Trait { }
+
+predicate P(t: Trait) {
+  t is Class // this is the related location of the error below
+}
+
+method M(u: Trait) {
+  assert P(u); // error
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5586.dfy.expect

@@ -0,0 +1,4 @@
+git-issue-5586.dfy(14,9): Error: assertion might not hold
+git-issue-5586.dfy(10,4): Related location: this proposition could not be proved
+
+Dafny program verifier finished with 0 verified, 1 error

docs/dev/news/5587.fix

@@ -0,0 +1 @@
+Clarify error location of inlined `is` predicates.