Types in the halting problem proof

If a machine H that can decide the halting problem is defined as
H = (P -> X -> Y) -> X -> Boolean
where P is the type of the program, X is the type of the input that the program accepts, and Y is the type of the output of the program, and then we define H' to be H but if the result is true we loop forever and if the result is false we return false, then feed H' into itself like so
H' H' H'
then the type signature would be
((P -> X -> Y) -> X -> Boolean) ((P -> X -> Y) -> X -> Boolean)
and so X must be of type
((P -> X -> Y) -> X -> Boolean)
but we are using X in its own definition and so there is infinite recursion.

Can someone explain this?

You made a small mistake. We need quote or eval to move between levels.

Halts : Prg -> Bool
"Halts" : Prg
Liar : Prg -> Bool
Liar x = If halts x rhen loop else halt
Para = liar "liar"