-- The key_tys can contain skolem constants, and we can guarantee that those
-- are never going to be instantiated to anything, so we should not involve
-- them in the unification test. Example:
-- The key_tys can contain skolem constants, and we can guarantee that those
-- are never going to be instantiated to anything, so we should not involve
-- them in the unification test. Example: