Misleading error when using a macro from `typed/racket` in `typed/racket/shallow`

[NoahStoryM]

What version of Racket are you using?
8.18 [cs]

What program did you run?

#lang typed/racket/shallow

(module m typed/racket
  (provide (all-defined-out))
  (define-syntax-rule (1+ n) (add1 n)))
(require 'm)

(displayln (1+ 0))

What should have happened?
I think the program should run successfully and print 1, similar to this one:

#lang typed/racket/optional

(module m typed/racket/shallow
  (provide (all-defined-out))
  (define-syntax-rule (1+ n) (add1 n)))
(require 'm)

(displayln (1+ 0))

If this usage is intentionally disallowed, the error message should be more precise about the interaction between typed/racket and typed/racket/shallow.

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

Type Checker: Macro 1+ from typed module used in untyped code
  in: (1+ 0)

[mfelleisen]

If you remove "shallow", the program will produce 1. But, the two typing disciples are distinct and the Racket promise is that distinct typing disciplines are mitigated. The only mitigation here is to disallow this import of a macro.

Exercise: change the macro so that something bad would happen if the program ran.

[NoahStoryM]

I'm not very familiar with shallow typing, so I may have misunderstood some fundamental concepts—please bear with me.

If I understand correctly, deep, shallow, and optional all use the same static type checking. This is why I initially expected that shallow modules should be able to use macros from deep modules. The difference between them lies in the contracts generated at runtime, correct? But then why can't shallow use macros from deep, while optional can use macros from shallow?

Since TR prohibits using deep macros in shallow contexts, I can't actually run code to see what kind of problems this would cause in practice. I suspect that problematic macros might be those that involve contracts automatically generated by deep typing—for example, macros that expand to use cast or similar things?

[mfelleisen]

The "shallow" discipline (aka "transient") generates contracts that fail to detect certain failures of values to live up to the type guarantees as they cross the boundary from typed to untyped code or vice versa. The technical word for this is "unsafe" but as Ben's dissertation shows, "safe" isn't a black and white property. One consequence is that a "deep" module needs to protect itself imports from "shallow" modules in basically the same manner as against imports from optionally typed checked or untyped modules, including a prohibition against macros (which can hide unsafe code inside).