infinite loop caused by (ann v t), where t uses polymorphic recursion

The typechecker goes into an infinite loop when checking if a value of a polymorphically recursive type t1 belongs to a type t2 with a identical declaration (except the recursive reference, which is renamed).

The types use polymorphic recursion, overwriting their argument with a ∀ X type parameter.

• If we change their definition to (define-type (t1 A) (∀ (X) (→ X (t1 String)))) (replacing X with String at the end, same thing for t2), the problem does not occur.
• If we change their definition to (define-type (t1 A) (∀ (X) (→ X (t1 A)))) (replacing X with A at the end, same thing for t2), the problem does not occur.

#lang typed/racket

(define-type (t1 A) (∀ (X) (→ X (t1 X))))
(define-type (t2 A) (∀ (X) (→ X (t2 X))))

;; Use the type in some way
(: f (∀ (A) (→ (t1 A) Any)))
(define (f a) 'dummy)
(define f-number (inst f Number))

(ann f-number (→ (t1 Number) Any)) ; This works
;(ann f-number (→ (t2 Number) Any)) ; This line makes the typechecker go in an infinite loop

Start by running the Typed Racket reproducer in the issue, especially the final annotation involving t2, and inspect the typechecker path for ann and polymorphic recursive types. Done means the example terminates without looping while the existing working cases remain valid.