Skip to content

Avoid double-nested recursive-contract for Name types resolving to Mu #1496

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
samth merged 1 commit into from
Mar 5, 2026
Merged

Avoid double-nested recursive-contract for Name types resolving to Mu #1496

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 18 additions & 3 deletions typed-racket-lib/typed-racket/private/type-contract.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -461,10 +461,25 @@
(define rv recursive-values)
;; FIXME: need special treatment for type constructors
(define resolved-name (resolve-once type))
;; When the resolved type is a Mu, use the name-sc gen-names
;; for the Mu variable's self-reference instead of letting the
;; Mu case generate a separate recursive-sc. This avoids
;; double-nested recursive-contract in the output.
(define (loop-for-name-sc resolved side rv)
(match resolved
[(Mu: (list n) b)
(loop b
side
(hash-set rv
n
(triple (lookup-name-sc type 'untyped)
(lookup-name-sc type 'typed)
(lookup-name-sc type 'both))))]
[_ (loop resolved side rv)]))
(register-name-sc type
(λ () (loop resolved-name 'untyped rv))
(λ () (loop resolved-name 'typed rv))
(λ () (loop resolved-name 'both rv)))
(λ () (loop-for-name-sc resolved-name 'untyped rv))
(λ () (loop-for-name-sc resolved-name 'typed rv))
(λ () (loop-for-name-sc resolved-name 'both rv)))
(lookup-name-sc type typed-side)])]
;; Ordinary type applications or struct type names, just resolve
[(or (App: _ _) (Name/struct:)) (t->sc (resolve-once type))]
Expand Down
10 changes: 10 additions & 0 deletions typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
static-contract?
static-contract?)))]
[lookup-name-sc (-> Type? symbol? (or/c #f static-contract?))]
[lookup-name-def (-> Type? symbol? (or/c #f static-contract?))]
[register-name-sc (-> Type?
(-> static-contract?)
(-> static-contract?)
Expand Down Expand Up @@ -75,6 +76,15 @@
[(untyped) (caddr result)]
[else (raise-argument-error 'lookup-name-sc "side?" typed-side)])))

(define (lookup-name-def type typed-side)
(define result (hash-ref (name-defs-table) type #f))
(and result
(case typed-side
[(typed) (car result)]
[(untyped) (cadr result)]
[(both) (caddr result)]
[else (raise-argument-error 'lookup-name-def "side?" typed-side)])))

(define (register-name-sc type typed-thunk untyped-thunk both-thunk)
(define typed-name (generate-temporary))
(define untyped-name (generate-temporary))
Expand Down
78 changes: 78 additions & 0 deletions typed-racket-test/succeed/no-double-recursive-contract.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
#lang racket/base

;; Test that recursive Name types produce well-formed contracts.
;; Exercises Name->Mu, Name->Name->Mu, mutually recursive names,
;; and plain Mu types.

(require rackunit
racket/class)

;; ---------------------------------------------------------------
;; Case 1: Name type resolving to Mu (recursive class type alias)
(module typed1 typed/racket
(require typed/racket/class)
(define-type C% (Class [m (-> (Instance C%) Void)]))
(: obj (Instance C%))
(define obj
(new (class object%
(super-new)
(define/public (m x) (void)))))
(provide obj))

(require 'typed1)
(check-true (object? obj))
(send obj m obj)

;; ---------------------------------------------------------------
;; Case 2: Name type alias chain (Name->Name->Mu)
(module typed2 typed/racket
(require typed/racket/class)
(define-type Base% (Class [m (-> (Instance Base%) Void)]))
(define-type Alias% Base%)
(: obj2 (Instance Alias%))
(define obj2
(new (class object%
(super-new)
(define/public (m x) (void)))))
(provide obj2))

(require 'typed2)
(check-true (object? obj2))
(send obj2 m obj2)

;; ---------------------------------------------------------------
;; Case 3: Mutually recursive Name types
(module typed3 typed/racket
(require typed/racket/class)
(define-type A% (Class [get-b (-> (Instance B%))]))
(define-type B% (Class [get-a (-> (Instance A%))]))
(: a-obj (Instance A%))
(: b-obj (Instance B%))
(define b-obj
(new (class object%
(super-new)
(define/public (get-a) a-obj))))
(define a-obj
(new (class object%
(super-new)
(define/public (get-b) b-obj))))
(provide a-obj
b-obj))

(require 'typed3)
(check-true (object? a-obj))
(check-true (object? b-obj))
(check-true (object? (send a-obj get-b)))
(check-true (object? (send b-obj get-a)))

;; ---------------------------------------------------------------
;; Case 4: Recursive non-class Mu type (e.g., recursive list)
;; to make sure the fix doesn't break plain Mu types
(module typed4 typed/racket
(define-type Tree (U Null (Pairof Integer Tree)))
(: t Tree)
(define t (list 1 2 3))
(provide t))

(require 'typed4)
(check-equal? t '(1 2 3))
44 changes: 43 additions & 1 deletion typed-racket-test/unit-tests/static-contract-conversion-tests.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,11 @@
typed-racket/static-contracts/instantiate
typed-racket/static-contracts/structures
typed-racket/static-contracts/combinators
typed-racket/static-contracts/combinators/name
typed-racket/types/abbrev
typed-racket/types/numeric-tower))
typed-racket/types/numeric-tower
typed-racket/rep/type-rep
typed-racket/env/type-name-env))

(provide tests)
(gen-test-main)
Expand Down Expand Up @@ -209,4 +212,43 @@
(t/sc (-set Univ) #:ret any/sc #:optional)
(t/sc (-HT (-vec -Symbol) (-vec -Symbol)) #:ret any/sc #:optional)
(t/sc (-unit null null null ManyUniv) #:ret any/sc #:optional))

;; When a Name type resolves to a Mu, the name-def SC should be a
;; plain object/sc, not wrapped in recursive-sc. The single level of
;; recursive-contract comes from extra-defs in instantiate; verifying
;; that the name-def is not itself a recursive-sc ensures no doubling.
(test-suite "Name->Mu produces no double recursive-sc"
(test-case "recursive class type alias"
(phase1-phase0-eval (define name-id (datum->syntax #f 'TestC%))
(define the-type (make-Name name-id 0 #f))
(register-type-name name-id (-mu a (-object #:method [(m (-> a -Void))])))
(with-new-name-tables
(let ()
(define sc (type->static-contract the-type (lambda (#:reason _) #f)))
;; The top-level SC is just a name reference.
;; Default typed-side=#t maps to 'typed.
(define typed-name-sc (lookup-name-sc the-type 'typed))
(define both-name-sc (lookup-name-sc the-type 'both))
;; The name-def SC should be a plain object/sc.
;; Before the fix, this was a recursive-sc wrapping
;; the object/sc, which combined with the
;; recursive-contract from extra-defs produced
;; double nesting.
(define both-def (lookup-name-def the-type 'both))
(define expected-def
(object/sc #t
(list (member-spec 'method
'm
(function/sc #t
(list any/sc both-name-sc)
null
null
null
#f
(list (flat/sc #'void?)))))))
#`(begin
;; The top-level result is a name-sc reference
(check-equal? '#,sc '#,typed-name-sc)
;; The name-def is object/sc, not recursive-sc
(check-equal? '#,both-def '#,expected-def)))))))
))