typed-racket icon indicating copy to clipboard operation
typed-racket copied to clipboard

Unsoundness from require/typed struct not checking the parent

Open AlexKnauth opened this issue 3 years ago • 0 comments

What version of Racket are you using?

Racket version 8.1 with typed-racket-lib version 1.12.

What program did you run?

#lang typed/racket

(module untyped racket
  (provide (struct-out a) (struct-out b))
  (struct a ())
  (struct b a ()))

(require/typed 'untyped
               [#:struct a ()]
               [#:struct b ()])

(: true False)
(define true (a? (b)))
;=> #t : False

What should have happened?

There should have been an error... preferably a compile-time error, about not declaring the correct parent for b in the require/typed declaration.

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

This isn't an error message but it demonstrates the bug:

> true
- : False
#t

An equal and opposite error happens when declaring a parent it doesn't have:

#lang typed/racket

(module untyped racket
  (provide (struct-out a) (struct-out b))
  (struct a ())
  (struct b ()))

(require/typed 'untyped
               [#:struct a ()]
               [#:struct (b a) ()])

(: false True)
(define false (a? (b)))
;=> #f : True

This lack of checking the parent in require-typed-struct also allowed the exn:test inheritance errors caught by @bennn in https://github.com/racket/rackunit/pull/147

AlexKnauth avatar Jul 28 '21 01:07 AlexKnauth