Мысли вслух.

[thesz]

Comments

[lomeo]

Лучше вместо зачёркнутого вопросительный знак в конце ставить, а то читать зачёркнутое неудобно.

rec - это обычный case (разбор АТД)?

Потом, где у тебя тут зависимые типы?

[thesz]

А вот, например: data Int32 = x :: Integer, length (integerBits x) == 32 => Int32 x

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