I wonder if at some point LLM would "give up" when given a difficult to satisfy types and insert nonterminating code / bottoms instead.