What is a correct way to prove the next propositional logic statement using Curry–Howard correspondence?

I am studying Curry–Howard correspondence.

Given propositional logic statement: (¬p -> q) -> ((¬p -> ¬q) -> p).

I need to define a type (as proposition) and a function (as a proof) in OCaml.

I came up with the next code and stuck:

type empty = | ;; 
let ex58: (('p->empty) -> 'q) -> (('p->empty) -> ('q->empty)) -> 'p = fun f g -> g(f)

Error:

This expression has type ('p -> empty) -> 'q but an expression was expected of type 'p -> empty.

When working on this exercise, it will probably easier to start with introducing a type constructor for not:

type empty = |
type 'a not = 'a -> empty

then use an explicit universal quantification to rewrite the exercise:

let proof_by_contradiction: type p q. (p not -> q) -> (p not -> q not) -> p =
   ...

which should improve slightly error messages

Error: This expression has type p not -> q but an expression was expected of type p not = p -> empty

Before diving into this exercise, it might be useful to try your hand at

let proof_by_negation:  type p q. (p -> q) -> (p -> q not) -> p not =
  ...

first.