I didn't say it was impossible. I said it was
nearly impossible, which is a synonym for "hard" for some value of hard.
Case in point: I looked into Agda and ended up in a deep rabbit hole that involved something I had never heard of called "Walther recursion." Whether this qualifies as "nearly impossible" or merely "hard" is quibbling over terminology, not substance.
