The description of why strict posivity is needed is wrong

[david-christiansen]

Describe the bug This came up on Zulip:

at the explanation for the requirements for inductive types, the example claims that the defined Fix (fun a => a -> a) would be equivalent to Bad... i've given a shot, but i couldn't seem to prove that you can construct Bad.rec function from Fix.rec? Maybe it would be easier to say that Fix (. -> Empty) is an inconsistent type (as you're creating a fixpoint for negation)?

And later in the thread:

at the explanation for the requirements for inductive types, the example claims that the defined Fix (fun a => a -> a) would be equivalent to Bad... i've given a shot, but i couldn't seem to prove that you can construct Bad.rec function from Fix.rec? Maybe it would be easier to say that Fix (. -> False) is an inconsistent type (as you're creating a fixpoint for negation)?

I looked into this and indeed Lean generates a recursor without an induction hypothesis for Fix.rec:

unsafe inductive Fix (f : Type u → Type u) where
  | fix : f (Fix f) → Fix f

#check Fix.rec
-- Fix.rec.{u_1, u} {f : Type u → Type u} {motive : Fix f → Sort u_1}
--   (fix : (a : f (Fix f)) → motive (Fix.fix a))
--   (t : Fix f) : motive t

So I guess the Fix that comes out of the unsafe inductive declaration is an accidentally consistent but non-inductive type.

And the the answer:

it's still not consistent, using f := (. -> Empty)

my point is that the argument as to why it isn't consistent is wrong (or at least not clear)

This should be investigated and fixed.

[edegeltje]

for what it's worth, here is a proof that indeed Fix is inconsistent:

set_option autoImplicit false

universe u v

axiom Fix : (f:Type u → Type u) → Type u
axiom Fix.mk : {f:Type u → Type u} → f (Fix f) → Fix f

axiom Fix.rec : {f:Type u → Type u} → {motive : Fix f → Sort v} →
  (mk: (a:f (Fix f)) → motive (Fix.mk a)) → (a:Fix f) → motive a

noncomputable def Bad.toEmpty : Fix (· → Empty) → Empty := fun b => 
  Fix.rec (motive := fun _ => Empty) (fun v => v b) b

noncomputable instance : Inhabited (Fix (· → Empty)) := ⟨Fix.mk (Bad.toEmpty)⟩

example : False := (Bad.toEmpty.{u} default).elim