Very interesting find here IMO. @jmw150 Have you seen this yet?
http://comonad.com/reader/2022/internalized-guarded-recursion-for-equational-reasoning/
Follow
So he found a decidable fragment. These are pretty common. But it is pretty neat that it is already part of Haskell's category flavored logic system. 
