If you find an ornament between A and B, and then also find an ornament between C and D, where D depends on A, and try to forgetfully lift terms defined over packed D, you get a term that also tries to lift along the ornament from A at the same time. This is weird behavior.
An example is finding an ornament between nat and some other type, then forgetting from packed vectors. Forget will unfortunately try to promote nat at the same time.
If you find an ornament between A and B, and then also find an ornament between C and D, where D depends on A, and try to forgetfully lift terms defined over packed D, you get a term that also tries to lift along the ornament from A at the same time. This is weird behavior.
An example is finding an ornament between nat and some other type, then forgetting from packed vectors. Forget will unfortunately try to promote nat at the same time.