Но мы ведь можем в любой момент спрыгнуть до галимой динамики.
Сказать: "чёрт его знает, что там за точный тип, но, как минимум, forall a b . a-> b на самом верхнем уровне".
Или сам момент принятия решения "пора валить" не определён, и получается, как с шампунем: намылить-смыть-повторить?