fix 4471

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -5066,8 +5066,7 @@ public record ResolveTypeReturn(Type ReplacementType, ExprDotName LastComponent)
  if (lax) {
  // we have to be careful about uses of the type being defined
  var cg = enclosingTypeDefinition.EnclosingModuleDefinition.CallGraph;
- var t0 = resolvedClass as ICallable;
- if (t0 != null && cg.GetSCCRepresentative(t0) == cg.GetSCCRepresentative((ICallable)enclosingTypeDefinition)) {
+ if (resolvedClass is ICallable t0 && enclosingTypeDefinition is ICallable t1 && cg.GetSCCRepresentative(t0) == cg.GetSCCRepresentative(t1)) {
  reporter.Error(MessageSource.Resolver, t.tok, "using the type being defined ('{0}') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)", resolvedClass.Name);
  }
  }

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

@@ -0,0 +1,8 @@
+// RUN: %exits-with 0 %verify "%s"
+
+trait YT<W> {
+ const f: W
+}
+
+class Y extends YT<Y -> nat> {
+}

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

@@ -0,0 +1,23 @@
+// RUN: %exits-with 2 %verify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait YT<W> {
+ const f: W
+}
+
+class Y extends YT<Y -> nat> {
+ constructor(f: Y -> nat)
+ ensures this.f == f
+ {
+ this.f := f;
+ }
+}
+
+method Main()
+ ensures false
+{
+ // error: knot.f calls itself without decreasing
+ var arrow := (x: Y) => 1 + x.f(x);
+ var knot := new Y(arrow);
+ var a := knot.f(knot);
+}

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

@@ -0,0 +1,2 @@
+git-issue-4471b.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 git-issue-4471b.dfy

docs/dev/news/4471.fix

@@ -0,0 +1 @@
+Fixed crash caused by cycle in type declaration