I have heard multiple authors and speakers (while watching various lectures and in papers) say emphatically that no one wants to deal with coinductiion in a typ

I have heard multiple authors and speakers (while watching various lectures and in papers) say emphatically that no one wants to deal with coinductiion in a type theory unless they ABSOLUTELY must. I'm not sure I've ever seen a concise explanation of the complications that arise by inserting coinductive types into a type theory, but I'll take it as an article of faith that the issues exist. But, the concept is certainly intriguing. Somehow, in my reading on type theory there has been a lack of exploration of instantiation of coinductive types, hopefully the paper by McBride you linked will give me some references to chase down.