Reducible definition and TC problem

Stream: lean4

[Tomas Skrivan]

I'm having a trouble to synthesize an instance where one of the arguments is hidden behind a reducible definition. Such definition such be invisible to TC but it does not seems so in a specific case.

class Trait (X : Type u) where
  R : Type v

attribute [reducible] Trait.R

class SemiInner (X : Type u) (R : Type v) where
  semiInner : X → X → R

@[reducible] instance (X) (R : Type u) [SemiInner X R] : Trait X := ⟨R⟩

def norm {X} [Trait X] [inst : SemiInner X (Trait.R X)] (x : X) : Trait.R X := SemiInner.semiInner x x

section Real
  def ℝ := Float
  instance : SemiInner ℝ ℝ := ⟨λ x y : Float => x * y⟩

  variable (x : ℝ)

  set_option trace.Meta.synthInstance true in
  #check (norm x : ℝ) -- error

  -- These all work correctly
  example : Trait.R ℝ = ℝ := by rfl
  example : Trait ℝ := by infer_instance
  example : Trait (Trait.R ℝ) := by infer_instance
end Real


section Float
  instance : SemiInner Float Float := ⟨λ x y => x * y⟩

  variable (x : Float)

  #check (norm x : Float) -- this works
end Float

The problematic line is #check (norm x : ℝ)

The trace log ends with:

[Meta.synthInstance.newSubgoal] SemiInner ℝ (Trait.R ℝ)
[Meta.synthInstance.globalInstances] SemiInner ℝ (Trait.R ℝ), []
[Meta.synthInstance] failed

It looks like there is no instance for SemiInner ℝ (Trait.R ℝ) However, this example : SemiInner ℝ (Trait.R ℝ) := by infer_instance succeeds.

The example with Float instead of ℝ works fine. Which is even stranger. Do I misunderstand something or is this a bug?

[Tomas Skrivan]

One more thing to point out, it is important that the type ℝ is enforced.

#check norm x

works but type is Trait.R ℝ. This type should reduce to ℝ as Trait.R is marked reducible. However

#check (norm x  : ℝ)

fails

[Mario Carneiro]

I don't think you can (usefully) mark constructors/projections as reducible

[Leonardo de Moura]

To understand the issue, we have to display the implicit arguments. You can do that using set_option pp.explicit true. The trace now is

    [Meta.synthInstance.newSubgoal] SemiInner ℝ (@Trait.R ℝ (@Trait.mk ℝ Float))
    [Meta.synthInstance.globalInstances] SemiInner ℝ (@Trait.R ℝ (@Trait.mk ℝ Float)), []
    [Meta.synthInstance] failed

Note the Float in the trace above. You can fix this issue using

  abbrev ℝ := Float

[Mario Carneiro]

That is, I don't think Trait.R ℝ = ℝ is a reducible defeq

[Mario Carneiro]

Assuming you didn't want to make ℝ reducible, I think another option would be instance : SemiInner ℝ Float := ⟨λ x y : Float => x * y⟩

[Tomas Skrivan]

Yes I don't want to make ℝ reducible.

Great, I didn't know about the option set_option pp.explicit true, it will be super useful to debug this.

[Tomas Skrivan]

One thing I do not understand is how did Float sneaked in to:

main goal SemiInner ℝ (@Trait.R ℝ (@Trait.mk ℝ Float))

[Tomas Skrivan]

If I define ℝ as inductive ℝ it works, i.e. it is some arbitrary type with no connection to Float.

Making the definition as @[irreducible] def ℝ := Float, still produced the goal:

main goal SemiInner ℝ (@Trait.R ℝ (@Trait.mk ℝ Float))

I really do not understand where the Float comes in.

[Tomas Skrivan]

Mario Carneiro said:

I don't think you can (usefully) mark constructors/projections as reducible

What do you mean by that? If you comment it out, the code breaks even more.

[Tomas Skrivan]

Ohh is reducible transitive? So because Trait.R is marked as reducible and if Trait.R X happens to be ℝ does it get reduced all the way to Float? Is this really the intended behavior?

[Leonardo de Moura]

One thing I do not understand is how did Float sneaked in to:

The elaborator has to solve typing constraints, and one of them is

ℝ =?= @Trait.R.{?u.166, ?u.165} ?m.167 ?m.168

You can see how Lean solves it using

  set_option trace.Meta.isDefEq true in
  #check (norm x : ℝ) -- error

The trace contains

      [Meta.isDefEq.step] ℝ =?= @Trait.R.{?u.166, ?u.165} ?m.167 ?m.168
      [Meta.isDefEq.delta.unfoldLeft] ℝ
        [Meta.isDefEq.step] Float =?= @Trait.R.{?u.166, ?u.165} ?m.167 ?m.168
        [Meta.isDefEq.delta.unfoldRight] Trait.R
          [Meta.isDefEq.step] Float =?= ?m.168.1
          [Meta.isDefEq.assign]
              [Meta.isDefEq.assign] ?m.168 := @Trait.mk.{?u.166, ?u.165} ?m.167 Float
              [Meta.isDefEq.assign.beforeMkLambda] ?m.168 [] := @Trait.mk.{?u.166, ?u.165} ?m.167 Float
              [Meta.isDefEq.assign.checkTypes]
                [Meta.isDefEq.step] Trait.{?u.166, ?u.165} ?m.167 =?= Trait.{?u.166, ?u.165} ?m.167
                [Meta.isDefEq.assign.final] ?m.168 := @Trait.mk.{?u.166, ?u.165} ?m.167 Float
      [Meta.isDefEq] ℝ =?= @Trait.R.{?u.166, ?u.165} ?m.167 (@Trait.mk.{?u.166, ?u.165} ?m.167 Float) ... success

Making the definition as @[irreducible] def ℝ := Float, still produced the goal:

I will take a look at this issue.

If I define ℝ as inductive ℝ it works, i.e. it is some arbitrary type with no connection to Float.

Yes, structures (or inductives) are the way to go if you want to "seal" ℝ
Example:

section Real
  structure ℝ where
    val : Float

  instance : SemiInner ℝ ℝ := ⟨λ x y : ℝ => ℝ.mk (x.val * y.val) ⟩

  variable (x : ℝ)
  #check (norm x : ℝ) -- Works

[Leonardo de Moura]

Tomas Skrivan said:

Ohh is reducible transitive? So because Trait.R is marked as reducible and if Trait.R X happens to be ℝ does it get reduced all the way to Float? Is this really the intended behavior?

See comment above. The Float is not exposed by the TC procedure, but the elaborator while solving the typing constraints for norm x.

[Mario Carneiro]

      [Meta.isDefEq.step] ℝ =?= @Trait.R.{?u.166, ?u.165} ?m.167 ?m.168
      [Meta.isDefEq.delta.unfoldLeft] ℝ
        [Meta.isDefEq.step] Float =?= @Trait.R.{?u.166, ?u.165} ?m.167 ?m.168
        [Meta.isDefEq.delta.unfoldRight] Trait.R

Why did that happen? Trait.R is marked as reducible and ℝ is not, so it seems odd that it decided to unfold on the left first

[Leonardo de Moura]

@Mario Carneiro Trait.R is a projection, they have special treatment.

[Leonardo de Moura]

Making the definition as @[irreducible] def ℝ := Float, still produced the goal:

I will take a look at this issue.

https://github.com/leanprover/lean4/commit/2fff4c42b71fc1d451bf968a7f1a07d10993f2eb