Catching more knots (#4478)

Fixes #

<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->

<!-- Is this a bug fix? Remember to include a test in Test/git-issues/
-->

<!-- Is this a bug fix for an issue introduced in the latest release?
Mention this in the PR details and ensure a patch release is considered
-->

<!-- Does this PR need tests? Add them to `Test/` or to
`Source/*.Test/…` and run them with `dotnet test` -->

<!-- Are you moving a large amount of code? Read CONTRIBUTING.md to
learn how to do that while maintaining git history -->

<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/Resolver/HigherOrderHeapAllocationCheckerConstructor.cs

@@ -60,6 +60,9 @@ private bool Occurs(Type obj, Type rhs, bool left) {
       if (left && Type.Equal_Improved(obj, t)) {
         return true;
       }
+      if (left && t.IsTraitType) {
+        return true;
+      }
       var b = false;
       if (t.IsArrowType) {
         var arrow = type.AsArrowType;

Test/Landin/Knot16.dfy

@@ -0,0 +1,22 @@
+// RUN: %exits-with 2 %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait YT {
+  const f: Y -> nat
+}
+
+class Y extends YT {
+  constructor(f: YT -> nat)
+    ensures this.f == f
+  {
+    this.f := f;
+  }
+}
+
+method Main()
+  ensures false
+{
+  // error: knot.f calls itself without decreasing
+  var knot := new Y((x: YT) => if x is Y then 1 + x.f(x as Y) else 0);
+  var a := knot.f(knot);
+}

Test/Landin/Knot16.dfy.expect

@@ -0,0 +1,2 @@
+Knot16.dfy(12,11): Error: To prevent the creation of non-terminating functions, storing functions into an object's fields that reads the object is disallowed
+1 resolution/type errors detected in Knot16.dfy

Test/Landin/Knot17.dfy

@@ -0,0 +1,22 @@
+// RUN: %exits-with 2 %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait YT {
+  const f: YT -> nat
+}
+
+class Y extends YT {
+  constructor(f: YT -> nat)
+    ensures this.f == f
+  {
+    this.f := f;
+  }
+}
+
+method Main()
+  ensures false
+{
+  // error: knot.f calls itself without decreasing
+  var knot := new Y((x: YT) => if x is Y then 1 + x.f(x as Y) else 0);
+  var a := knot.f(knot);
+}

Test/Landin/Knot17.dfy.expect

@@ -0,0 +1,2 @@
+Knot17.dfy(12,11): Error: To prevent the creation of non-terminating functions, storing functions into an object's fields that reads the object is disallowed
+1 resolution/type errors detected in Knot17.dfy