Mutable strings are unsound with (make-predicate "abc")

What version of Racket are you using?

6.7.0.4

What program did you run?

#lang typed/racket
(define s (string #\a #\b #\c))
(if ((make-predicate "abc") s)
      (begin
        (string-set! s 1 #\x)
        (ann s "abc"))
      #f)

What should have happened?

make-predicate should refuse to generate the predicate, as it needs a non-flat contract.

I think it's best to wait until immutable data structures are implemented in TR before fixing this, as this may otherwise break programs which rely on make-predicate (and string mutations are exceedingly rare). Then it will be possible to write (make-predicate (∩ Immutable "abc")) or something similar.

The type of the generated predicate can also be changed to (-> Any Boolean : #:+ "abc" #:- (or (not "abc") Mutable)), although that goes against the general pattern for make-predicate which always generates (-> Any Boolean : T). Maybe it would be interesting in the future to have weaker versions (make-pos-predicate T) which returns a predicate with the type (-> Any Boolean : #:+ T) and (make-neg-predicate T) which returns a predicate with the type (-> Any Boolean : #:- T) ?

Start with the make-predicate entry point and run the Typed Racket reproducer shown in the issue. Resolve which proposed behavior is intended for mutable strings, then add coverage showing that the unsound (ann s "abc") path is no longer accepted; the issue names no source file or test.