fix: Add CanCall’s for default-valued parameters of method calls (#6091)

Fixes #6090

<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>

Author: RustanLeino

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs

@@ -212,7 +212,10 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
         } else {
           actual = Args[i];
         }
-        if (!(actual is DefaultValueExpression)) {
+
+        if (actual is DefaultValueExpression) {
+          builder.Add(TrAssumeCmd(actual.Origin, etran.CanCallAssumption(actual)));
+        } else {
           TrStmt_CheckWellformed(actual, builder, locals, etran, true);
         }
         builder.Add(new CommentCmd("ProcessCallStmt: CheckSubrange"));

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

@@ -0,0 +1,66 @@
+// RUN: %testDafnyForEachResolver "%s"
+
+module Wrappers {
+  datatype Option<T> = Some(value: T) | None
+
+  class Box<T> {
+    var value: T
+
+    constructor(value: T) {
+      this.value := value;
+    }
+  }
+}
+
+module A {
+
+  import opened Wrappers
+
+  function DefaultFooArg(): Option<Box<int>>
+
+  method Foo(x: Option<Box<int>> := DefaultFooArg())
+    modifies if x.Some? then {x.value} else {}
+  {}
+}
+
+module B refines A {
+  function DefaultFooArg(): Option<Box<int>> {
+    None
+  }
+}
+
+module C {
+  import B
+
+  method Bar() {
+    B.Foo();
+  }
+}
+
+// ------------------------
+// Smaller repro, plus tests for function calls and datatype constructors with default-value parameters
+  
+module D {
+  function F(): int { 3 }
+
+  method Foo(u: int := F())
+    requires u < 10
+  {
+  }
+
+  function Bar(u: int := F()): int
+    requires u < 10
+  {
+    0
+  }
+
+  type Small = x: int | x < 10
+
+  datatype Cell = Cell(s: Small := F())
+
+  method Test() {
+    Foo();
+    var bar := Bar();
+    var cell := Cell();
+  }
+}

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

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 6 verified, 0 errors