Why is it not possible to formulate Haskell's Fix in Lean?

Stream: lean4

[nrs]

Am delving into type theory and am trying to come up with a formulation of catamorphisms in Lean. I'm wondering, what is the type-theoretical reason we can't formulate Haskell's Fix f = f (Fix f) in Lean? I know this has something to do with enforcing totality, but is there a way to formulate this more formally by comparing Lean and Haskell's type theories?

[Mario Carneiro]

It's inconsistent

[Mario Carneiro]

What is the type of Fix?

[Mario Carneiro]

The answer is presumably (A -> A) -> A, but if you substitute A := False then you can immediately prove false from it

[nrs]

Mario Carneiro said:

The answer is presumably (A -> A) -> A, but if you substitute A := False then you can immediately prove false from it

I see, I will be mulling this fact over, thank you very much for the answer!