> Вопрос, что мы знаем в compile time. В случае с атд знаем про сам тип, а так же тип функций-конструкторов. В случае с динамикой, такой информации нет.
Почему же нет? Можно представить, что в динамике у нас в компайл-тайме достоверно известно: все термы одного и того же типа - одного из таких вот Т, которые мы можем объявлять в хаскеле показанным выше образом. А типы конструкторов можно вывести из стандарта данного динамического языка (они там будут называться "элементарные типы" и "определённые пользователем типы" и прочее в таком духе).

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

> это принципиально разные вещи, на мой взгляд
Наверное, соответствия Карри-Говарда тебе тоже не понравятся.