It'd be more like decideValidity : (p : A -> Type) -> (a : A) -> Either (p a) (Not (p a)) and for some classes of propositions this is a really useful typ

It'd be more like decideValidity : (p : A -> Type) -> (a : A) -> Either (p a) (Not (p a)) and for some classes of propositions this is a really useful type, e.g. the notion of decidable equality[0]. For general propositions you're talking about unbounded proof search, however. Undecidable propositions will fail to terminate (thus causing problems in a total language). Decidable propositions may still be exponentially slow to decide. Some classes of propositions may be known to be decidable, but knowing generally whether or not a proposition is undecidable is undecidable (Halting). [0] https://github.com/agda/agda-stdlib/blob/master/src/Relation/Nullary/Core.agda https://github.com/agda/agda-stdlib/blob/master/src/Relation...