sc optimizer fails to simplify (-> flat-recursive-contract)

[bennn]

Similar to #625 , I just found an error in some gradually-typed versions of the zordoz benchmark.

What version of Racket are you using?

6.10.1

What program did you run?

#lang racket/base

(module t typed/racket/base
  (provide f)

  (define-type Spec
    (-> (U Spec String)))

  (: f (-> Spec))
  (define (f)
    (λ () "hello")))

(require 't)

f

What should have happened?

No error

If you got an error message, please include it here.

recursive-contract: contract violation
  expected: flat-contract?
  given: (-> (or/c String g5))

Probable Cause

It's an issue instantiating recursive contracts, the type above makes a (recursive-contract .... #:flat). In this case it shouldn't be flat. Probably a bug with or/sc.

[bennn]

Small update: there's no problem if either:

• the contract contains a function with mandatory arguments
• the contract contains a function that returns a non-flat value

I still don't really understand the problem.
Somehow the static-contracts code thinks its making a flat recursive contract, but puts an -> inside.

I guess the optimizer needs to do whatever static-contracts/combinators/function.rkt is doing to tell when a function doesn't need a contract.

#lang racket/base

(module t typed/racket/base
  (provide f)

  (define-type Spec
    (-> Symbol (U Spec String))) ;; Now with non-zero arity

  (: f (-> Spec))
  (define (f)
    (λ (s) "hello")))

(require 't)

f
;; No error

[bennn]

Just posted 2 ideas for resolving this.

1. Improve the optimizer, so it can see that (Rec Spec (-> (U String Spec))) is a flat contract (need to solve recursive contract constraints in the optimizer)
2. Change the constraints on function/sc, because it's not currently true that a 0-arity function coming from the typed side that returns flat values will get a flat contract from the static contract instantiator

I'd rather merge Option 1 (#631). It'll do a little more work at compile-time, but can safely turn more contracts into any/cs

[bennn]

Note this is not really a "new error". The example program fails on 6.10.1.

[samth]

The example program fails on 6.10.1, but zordoz does not fail on 6.10.1, right?

[bennn]

Right

[samth]

Is there a smaller program that shows the zordoz issue?

[bennn]

Here's a smaller program that "shows the zordoz issue" --- this program runs on 6.10.1 and errors on the current master (after the changes to or/sc)

#lang racket/base

(module t typed/racket/base
  (provide f)

  (define-type Spec
    (-> (U Spec String)))

  (: f (U Spec String))
  (define (f)
    (λ () "hello")))

(require 't)

f

The difference between this & the program at the top is that the type for f uses Spec in a union with a flat contract. TR doesn't generate any contract for that union type, so it doesn't generate a contract for Spec.

(The problem with Spec is that one part of TR says Spec will produce a flat contract, but the part that actually makes the contract produces a chaperone.)

[bennn]

Closed by #631