Suppose we have two seprate compilation units.

(declare f X1)
(define (f ...) ...)

and

(define (g ...) ... (f ...) ...)

Suppose now we redefine f leading to it having type X2 which is not equal to X1. Then g in general will now be unsound.

Warn when this happens so the user can go ahead and recompile g≥