"[...] we can prove any theorem using Haskell types because every type is inhabited. Therefore, Haskell's type system actually corresponds to an inconsistent logic system."
Thus Haskell programs in general don't correspond to a consistent axiomatic system, which provides counterexample to your statement. Rebuttal complete.
Inconsistent axiomatic systems can prove anything. Thus either Haskell programs can prove the limits (and prove the opposite statement, as they are inconsistent) or they aren't axiomatic system as you mean it. Both possibilities contradict your statement:
> Chaitin's incompleteness theorem mean AI cannot learn
If programs are not axiomatic systems, then they cannot learn, period. Only ones that have consistent axioms have a hope of learning, and even then it is severely limited.
