We are using Z3 to prove properties of Haskell programs in our tool
. We would obviously like to use Z3 datatypes to model Haskell datatypes. The trouble is that Z3's datatypes are algebraic while Haskell's are coalgebraic. That is, in Haskell you can have an infinite value like n = Succ n, while with Z3 datatypes
As far as I can tell, the only thing stopping us from using Z3 datatypes is the "occurs check", which rules out cyclic terms like n = Succ n. Without the occurs check, I think Z3 datatypes would be agnostic about whether they are data or codata. So
I would like a way to switch off the occurs check for a particular datatype, or else somehow declare it as codata (which would have the same effect).