stage-L3-tight-typings-and-split-bounds