Values provided by typed unit won't generate contract.

[NoahStoryM]

What version of Racket are you using?

v8.3

What program did you run?

#lang racket/base

(module typed typed/racket/base
  (require typed/racket/unit)
  (provide (all-defined-out))

  (define-type Non-Pair (Refine [t : Any] (! t (Pair Any Any))))
  (define-type Foo-List (Listof Foo))
  (define-type Foo      (U Non-Pair Foo-List))

  (: test [-> Foo True])
  (define (test x) #t))
(require 'typed)

(test 1)

What should have happened?

#t

And we can use the methods mentioned in https://github.com/racket/typed-racket/issues/1158#issuecomment-961706399 to circumvent this problem:

#lang racket/base

(module typed typed/racket/base
  (require typed/racket/unit)
  (provide (all-defined-out))

  (define-type Non-Pair (Refine [t : Any] (! t (Pair Any Any))))
  (define-type Foo-List (Listof Foo))
  (define-type Foo      (U Non-Pair Foo-List))

  (define-signature funcs^
    ([test : [-> Foo True]]))

  (define-unit funcs@
    (import)
    (export funcs^)

    (: test [-> Foo True])
    (define (test x) #t))

  (define-values/invoke-unit funcs@
    (import)
    (export funcs^)))
(require 'typed)

(test 1)

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

draft.rkt:15:0: Type Checker: could not convert type to a contract;
 proposition contract generation not supported for non-flat types
  identifier: test
  type: (-> Foo True)
  in: (test 1)
  location...:
   draft.rkt:15:0
  context...:
   /usr/share/racket/collects/syntax/wrap-modbeg.rkt:46:4

[NoahStoryM]

But the value provided in this way seems to lose its contract:

What program did you run?

#lang racket/base

(module typed typed/racket/base
  (require typed/racket/unit)
  (provide (all-defined-out))

  (define-type Non-Pair (Refine [t : Any] (! t (Pair Any Any))))
  (define-type Foo-List (Listof Foo))
  (define-type Foo      (U Non-Pair Foo-List))

  (define-signature funcs^
    ([test : [-> Foo True]]))

  (define-unit funcs@
    (import)
    (export funcs^)

    (: test [-> Foo True])
    (define (test x) #t))

  (define-values/invoke-unit funcs@
    (import)
    (export funcs^)))
(require 'typed)

(test '(1 . 2))

What should have happened?

Raise error like this:

Type Checker: type mismatch
  expected: Foo
  given: (Pairof One Positive-Byte)
  in: (quote (1 . 2))

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

It prints #t, which should not happen.

[samth]

Right, the problem here is that the version with the unit should have produced the same contract-generation error.