Проверка корректности программы с использованием фантомных типов в Haskell

Предположим, я работаю с кодом стековой машины, которая может выполнять некоторые простые операции (push constant, add, mul, dup, swap, pop, convert типов) на целые и двойные.

Теперь программа, которую я пишу, берет описание на каком-то другом языке и переводит его в код для этой стековой машины. Мне также нужно рассчитать максимальный размер стека.

Я подозреваю, что можно использовать средство проверки типов Haskell для устранения некоторых ошибок, например:

• извлечение из пустого стека
• умножение удвоения с использованием умножения int

Я подумал, что могу объявить, например:

dup :: Stack (a :%: b) -> Stack (a :%: b :%: b)
int2double :: Stack (a :%: SInt) -> Stack (a :%: SDouble)

и так далее. Но тогда я не знаю, как сгенерировать код и посчитать размер стека.

Можно ли это сделать вот так? И было бы это просто / удобно / стоило бы?