@leif something about lifts confused the macro stepper

Is there somewhere that describes how contracts for typed-untyped boundaries are generated. In particular, I’d like to know what Any means below, how the two different contracts are generated, and understand the four check-false results. #lang racket (module typed typed/racket (provide split split′) (: split : ∀ (α) (Listof α) (α → Any) → (Listof (Listof α))) (define (split a-list property) '(())) (: split′ : (Listof Any) (Any → Any) → (Listof (Listof Any))) (define split′ split)) (require 'typed rackunit) (define-values (split-contract split′-contract) (values (value-contract split) (value-contract split′))) (check-equal? (contract-name split-contract) '(-> (listof any/c) (-> any/c any/c) any)) (check-equal? (contract-name split′-contract) '(-> (listof any/c) (or/c struct-predicate-procedure?/c (-> Any any/c)) (listof (listof Any)))) (check-true (contract-stronger? (-> (listof any/c) (-> any/c any/c) any) (-> (listof any/c) (-> any/c any/c) any))) (check-true (contract-stronger? split-contract split-contract)) (check-true (contract-stronger? split′-contract split′-contract)) (check-false (contract-stronger? (value-contract split) (-> (listof any/c) (-> any/c any/c) any))) (check-false (contract-stronger? (-> (listof any/c) (-> any/c any/c) any) (value-contract split))) (check-false (contract-stronger? split-contract split′-contract)) (check-false (contract-stronger? split′-contract split-contract))

Any corresponds to the any-wrap/c contract

The latter two check-false results are probably because those are significantly different

the former two I don’t understand

Thanks, any-wrap/c is undocumented, but I found it in the source. Is looking at typed-racket/private/type-contract.rkt the best reference at the moment for how the contracts are generated?

@gfb for the details of how everything works, yes

@ryanc I see.

I can understand how it wouldn’t be able to step through that (possibly), but is that error expected?