failed to synthesize type class instance

Stream: new members

[Winston Yin]

I can't understand why representation k A V is underlined with "fails to synthesize type class instance for module k (V →ₗ[k] V)" in :

structure subrepresentation
  {k : Type _} [field k]
  {A : Type _} [ring A] [assoc_algebra k A]
  {V : Type _} [add_comm_group V] [module k V]
  [ring (V →ₗ[k] V)] [module k (V →ₗ[k] V)]
  (ρ : representation k A V) := sorry

but it succeeds when I change structure to def. Lean also succeeds if I copy the same variables into a variables.

[Winston Yin]

For context, representation is defined with these variables:

  (k : Type _) [field k]
  (A : Type _) [ring A] [assoc_algebra k A]
  (V : Type _) [add_comm_group V] [module k V]
  [ring (V →ₗ[k] V)] [module k (V →ₗ[k] V)]

[Yakov Pechersky]

What are your imports?

[Winston Yin]

import algebra.module

[Yakov Pechersky]

Sorry, I guess I mean what is a #mwe? For example, where is assoc_algebra from?

[Winston Yin]

class assoc_algebra (k : Type _) [field k] (A : Type _) [ring A] extends module k A

[Yakov Pechersky]

And then finally, what's your representation definition?

[Winston Yin]

Sorry I should really be including everything, but the problem seems to be fixed when I import linear_algebra.basic

[Winston Yin]

Which is where the instance for the module in question is defined

[Winston Yin]

What's strange is that it succeeds when I write def instead of structure...

[Eric Wieser]

I assume you're deliberately avoiding docs#algebra as a learning exercise?

[Alex Zhang]

How can I fix this problem? :thinking:

import data.set.finite
def S:set ℕ:= {1, 2, 3}
def f : S → S := λ x, 1

failed to synthesize type class instance for
x : ↥S
⊢ has_one ↥S

[Anne Baanen]

f returns an element of S, i.e. an element y : ℕ along with a proof y ∈ S. So you need to return the proof as well:

def f : S → S := λ x, ⟨1, set.mem_insert 1 {2, 3}⟩

[Anne Baanen]

As @Eric Wieser noted, when you write 1 : S, it really means "lean can parse the syntax 1 into a term of type S". So there's an alternative way to make your original version of f work, namely by telling Lean how to interpret the syntax:

instance : has_one S := ⟨⟨1, set.mem_insert 1 {2, 3}⟩⟩

(This is the reason you got an error along the lines of "failed to synthesize type class instance for has_one S", rather than "expected type S, but 1 has type ℕ": Lean uses these typeclass instances to interpret numerals.)

[Anne Baanen]

Note that the 1 is purely a bit of syntax with no meaning. So you can also define that 1 : S actually corresponds to the natural number 2:

instance : has_one S := ⟨⟨2, set.mem_insert_of_mem 1 (set.mem_insert 2 {3})⟩⟩

[Alex Zhang]

instance fin.has_one' {n : nat} {i : fin n} : has_one (fin n) := sorry
#check fin.has_one'
example {n : ℕ} {i : fin n} : has_one (fin n) := @fin.has_one' n i
def f {n : nat} {i : fin n} := (1 : fin n)

Why does the definition of f report

failed to synthesize type class instance for
n : ℕ,
i : fin n
⊢ has_one (fin n)

[Reid Barton]

Since fin n is not a class, the argument i in the context is not available for your fin.has_one' instance to be selected, I think.

[Alex Zhang]

Is there a minor change that solves this problem?

[Floris van Doorn]

You could replace {i : fin n} by [inhabited (fin n)].
But the mathlib way is to use docs#fin.has_one, which only gives has_one (fin (succ n))

[Reid Barton]

There might be a better/more mathlib-approved way of doing whatever it is you want to do with 1 : fin n.

[Yakov Pechersky]

You can always construct the same value as ⟨1, your_proof_that (1 < n)⟩

[Yakov Pechersky]

Just because you somehow have a term of i : fin 0 doesn't mean that suddenly you should be able to write 1 for things of fin 0.

[Eloi Torrents]

Hi, the following code fails with this message:

import ring_theory.localization

variables {R : Type*} [integral_domain R]
variables {K : Type*} [field K] [comm_ring K] [algebra R K] [is_fraction_ring R K]

/-
failed to synthesize type class instance for
R : Type u_1,
_inst_1 : integral_domain R,
K : Type u_2,
_inst_2 : field K,
_inst_3 : comm_ring K,
_inst_4 : algebra R K
⊢ algebra R K
-/

I don't know why lean does not see the instance _inst_4...

[Alex J. Best]

Try adding set_option pp.all true after the imports, is there a difference then?

[Patrick Massot]

K is both a field and a comm ring

[Patrick Massot]

So it has two completely unrelated ring structures and Lean is completely confused

[Patrick Massot]

Try removing the [comm_ring K]