inductive type mismatch

Stream: lean4

[Marcus Rossel]

The following produces an error:

#eval Lean.versionString -- "4.2.0-rc1"

inductive X where -- error: type mismatch
  | mk : (if True then X else X) → X

Is this expected?

---

This fails as well:

inductive X where
  | mk : (match decide True with | true => X | false => X) → X

But this doesn't:

inductive X where
  | mk : (match true with | true => X | false => X) → X

[Arthur Adjedj]

This error happens when Lean tries to generate the SizeOf instance. I'll go have a look.

[Arthur Adjedj]

Ah, it was a TC diamond all along ! Since if-then-else doesn't have a proper SizeOf instance, it would infer that its instance would be the default fun _ => 0, whereas X did have a non-zero instance ! Adding the following instance solves the issue:

instance [Decidable C] [SizeOf A] [SizeOf B] : SizeOf (if C then A else B) where
  sizeOf := iteInduction (motive := λ A => A → Nat) (λ _ x => sizeOf x) (λ _ x => sizeOf x)

inductive X :=
  | mk : (if True then X else X) → X --works