>Можно представить, что в динамике у нас в компайл-тайме достоверно известно: все термы одного и того же типа
Согласен. (1)

>А типы конструкторов можно вывести из стандарта данного динамического языка
Можно. Статический анализ никто не отменял. Но по факту, динамика на то и динамика, что в компайл-тайм ничего подобного не известно.

>Не понял, о чём речь.
Я просто провел аналогию, что есть тип и его значения мы можем как-то различать. В одном случае (атд) говорят о динамической типизации, в другом (инт, бул) - просто про условный оператор.

>Наверное, соответствия Карри-Говарда тебе тоже не понравятся.
Я его не до конца понимаю, потому не могу говорить, нравится мне или нет, как не очень понимаю, какое отношение он имеет к обсуждаемому вопросу. Там что-то про типы и доказательство их существования. Если трактовать динамику описанным выше образом (см. 1), мы каждый раз будем доказывать (или не доказывать, что являет собой какие-то взаимоисключающие параграфы), что ентот единственный тип не пуст. Мне это не кажется хоть сколько-нибудь интересным. Хотя, опять же, у меня нет пониманию, потому, может, я бред несу.