Seemingly weird unification problem

Stream: new members

[Xuanrui Qi]

Hi, I'm pretty new to Lean (mainly a Coq user). Today I was formalizing some stuff using Lean4, and I run into a seemingly weird unification error:

variable {R : Type*} [CommRing R]
def Spec (A : Type*) [Semiring A] [Algebra R A] := A →ₐ[R] R
structure Z : Type where
  S : ∀ (A : Type*) [Semiring A] [Algebra R A] {FinitePresentation A},
    Spec A →+ R

Say I try to write this code. Then it tells me that it failed to synthesize instance Semiring A, but I have just given it in the forall!

[Xuanrui Qi]

I tried to pass it the instances explicitly, then it tells me:

application type mismatch
  @Spec R ?m.3666 A sr
argument
  sr
has type
  Semiring A✝ : Type u_2
but is expected to have type
  Semiring A : Type u_2

which is even weirder to me! Where did this dagger come from?

Likely, this is due to my misunderstanding of how type classes and instances work in Lean. Could anyone help me out?

[Damiano Testa]

I think that there are several issues at play here. First of all, what should Spec A →+ R means? It seems that Spec A is the type of algebra maps from A to R, while →+ expects to have an additive monoid on the left.

[Damiano Testa]

Also, imports and opens are missing in your code above.

[Damiano Testa]

Moreover, I think that R should be explicit in Spec, since I do not think that Spec A will find R, even with the Algebra R A assumption floating around.

[Damiano Testa]

Finally, the Type in Z is also messing Lean up, since the resulting structure will live in a higher universe.

[Sebastian Ullrich]

As for the specific error:

{FinitePresentation A}

This is a declaration of two variables FinitePresentation and A with inferred type

[Damiano Testa]

Maybe this is what you wanted?

import Mathlib

open Algebra

variable {R : Type*} [CommRing R]

def Spec (A : Type*) [Semiring A] [Algebra R A] := A →ₐ[R] R

structure Z : Type _ where  --  <--- `Type _`, so Lean figures out the right universe level
  S : ∀ (A : Type*) [Semiring A] [Algebra R A], FinitePresentation R A →
    Spec (R := R) A  --  <--- you have to tell Lean what `R` you are thinking of

#check Z

[Damiano Testa]

Sebastian Ullrich said:

As for the specific error:

{FinitePresentation A}

This is a declaration of two variables FinitePresentation and A with inferred type

Ah, I had forgotten that I added an R there as well!

[Xuanrui Qi]

Imports were omitted. All required modules have been imported.

[Xuanrui Qi]

Sebastian Ullrich said:

As for the specific error:

{FinitePresentation A}

This is a declaration of two variables FinitePresentation and A with inferred type

Thanks! This looks like the problem indeed

[Damiano Testa]

Xuanrui Qi said:

Imports were omitted. All required modules have been imported.

This does not help whoever is trying to help you, though! #mwe

[Ruben Van de Velde]

Xuanrui Qi said:

I tried to pass it the instances explicitly, then it tells me:

application type mismatch
  @Spec R ?m.3666 A sr
argument
  sr
has type
  Semiring A✝ : Type u_2
but is expected to have type
  Semiring A : Type u_2

which is even weirder to me! Where did this dagger come from?

Likely, this is due to my misunderstanding of how type classes and instances work in Lean. Could anyone help me out?

Note the dagger symbol after one of your A's in the error message. That means there are two things called A in your context