> Я совершенно не уверен, что могу делать допущение подобное a = pure a'

С точки зрения бананов и линз тип

pure :: (Functor f) => a -> f a

задаёт f-коалгебру (pure там - это psi в анаморфизме). Ну и для функторов есть изоморфизм между f a и a. Так что вроде можно, но я не настолько крут в бананах, чтобы поставить тут ЧТД :)