No—there are many properties that cannot be decided. For example, many programs can be proven to halt in finite time. For example, you can imagine a way to prove that the program
return 0
always halts. However, testing for this property is impossible (Halting Problem). More generally, it is not possible to test a general predicate for satisfaction. Even things that are decidable in principle may not be decidable quickly (SAT).
On the other hand, there is a lot of space for simple predicates like "str.length < 10" to be decided automatically, since the proofs for these can be constructed with only forward search.
Wouldn't the proposed function then just not compile for the instances were it would be impossible to test, as desired? It would still be useful for where it does work, like in the code you provided. Seems like a lack of meta programming to me if it's not currently possible.
Idris has type classes and it produces a polymorphic total function `decEq` for any type which instantiates the class DecEq.
decEq :: DecEq t => (x : t) -> y -> Dec (x = y)
where Dec denotes a decidable type, something like (but not actually)
data Dec t where
Yes : t -> Dec t
No : Not t -> Dec t
So now we have a proposition in our type-level prolog called `DecEq` and some types, the ones with decidable equality, can instantiate it
instance DecEq () where
decEq _ _ = Yes refl
-- Equality is symmetric, so is the negation of equality
total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
negEqSym p h = p (sym h)
-- Proof that zero isn't equal to any number greater than zero
total OnotS : Z = S n -> _|_
OnotS refl impossible
instance DecEq Nat where
decEq Z Z = Yes refl
decEq Z (S _) = No OnotS
decEq (S _) Z = No (negEqSym OnotS)
-- recurse on the arguments together and modify the eventual
-- decided proof so as to match the arguments actually passed.
--
-- I.e. we might find that Yes (n = m) but we need Yes (S n = S m)
--
decEq (S n) (S m) with (decEq n m)
| Yes p = Yes $ cong p
| No p = No $ \h : (S n = S m) => p $ succInjective n m h
Finally, at compile time Idris will try to infer the concrete types instantiating variables throughout the program. If any of the variables are bounded by `DecEq` then it must be able to solve the typeclass prolog to establish decidable equality for that type.
If it fails to fulfill that obligation then it'll fail at compile time.
-- this fails since functions on naturals are
-- far, far, far from decidable... Idris cannot achieve the
-- obligation to find `DecEq (Nat -> Nat)`.
decEq : (x : Nat -> Nat) -> y -> Dec (x = y)
On the other hand, there is a lot of space for simple predicates like "str.length < 10" to be decided automatically, since the proofs for these can be constructed with only forward search.