Fix retyping anomaly in rewrite

Fix #13045

Also make sure future anomalies won't be fed to tclzero.

Instead of retyping with lax:true we may question why we produce an
ill-typed term in decompose_app_rel: in the

    | App (f, [|arg|]) ->

case we produce `fun x y : T => bla x y` but we have no assurance that
the second argument of `bla` should have type `T`.

0 files changed, 0 insertions, 0 deletions