An interesting option would be to require that captured locals without explicit types are type-constant. That would allow intersecting all the bits of inferred info about their type instead of unioning, which is a pretty massive improvement in inferability.
For explicitly typed locals, one would of course respect the type annotation. So instead of jumping through Ref hoops to allow loosely typed captured locals, one would simply annotate them with the loose type one wants. This would, of course just be the type annotation of the local on the closure struct.