A type checker that derails:
“show :: a -> String”
“OK”
“x :: Int”
“OK”
“show x”
“but you can’t show functions”

A proof checker that derails:
“Birds fly. Tweety the Canary is a bird. So Tweety flies.”
“But Fido the Ostrich doesn’t fly.”

---

Another type checker that derails:
“main = putStrLn s”
“OK, how about s = show id”

Another proof checker that derails:
“Fido doesn’t fly.”
“But Fido is a bird, and birds fly.”

---

A helpful type checker:
“show id”
“but you can’t show functions”

A helpful proof checker:
“Birds fly. Fido is a bird. So Fido flies.”
“But Fido is an ostrich, and ostriches don’t fly.”

---

Another helpful type checker:
“main = putStrLn s”
“OK, how about s = show 42”

Another helpful proof checker:
“Tweety doesn’t fly.”
“But Tweety is a bird, and birds fly.”