One would figure that the Agda compiler could figure out the type of not based on its simple definition, but nope. An algorithm that could figure it out would a

One would figure that the Agda compiler could figure out the type of not based on its simple definition, but nope. An algorithm that could figure it out would absolutely fall flat on a dependent type. Not totally correct – it's totally possible to infer (some) types in a dependently typed system. For example, in Coq: Coq < Definition not x := match x with true => false | false => true end. Coq < Check not. not : bool -> bool The trick is simply knowing when to stop – that's what turns an undecidable algorithm into a decidable, sound, but incomplete algorithm.