Can a program decide whether an arbitrary program halts for SOME input?

Is there a program (may-halt? p) that can tell whether there exists an input so that (p input) halts?

I tried simple diagonalization, but it only tells me that (may-halt? diag-may-halt) must be true. It doesn't help proving whether the program exists or not.

Does such a program exist?

Nope, may-halt? doesn't exist.

(I don't think a direct proof by diagonalization would be less complex than the proof that the Halting problem is undecidable; otherwise that would be the standard example. Instead, let's reduce your problem to the Halting problem:)

Suppose there was a program may-halt? p, that decides if program p halts for some input. Then define:

halt? p x := may-halt? (\y -> if y==x then p x else ⊥)

where the thing in braces is a derived program. Lets break it down:

halt? p x := may-halt? p'

where p' is the program that (i) on input x computes p x, (ii) on any other input just loops around without terminating:

p' y := if y==x then p x else ⊥

Then may-halt? p' outputs true if and only if p x terminates.

Thus, for any program p and input x, halt? p x would decide if p x terminates. But we know that that isn't possible, so may-halt? doesn't exist.