assertion violation

[kbuzzard]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Sometimes when creating structures when there are a lot of _ in my code, I get an assertion violation. This is on 3.5.1 and 3.4.2

Steps to Reproduce

import ring_theory.algebra

open function

def quot.lift 
  {R : Type*} [comm_ring R]
  {A : Type*} [comm_ring A] [algebra R A]
  {B : Type*} [comm_ring B] [algebra R B]
  {C : Type*} [comm_ring C] [algebra R C]
  (f : A →ₐ[R] B) (hf : surjective f)
  (g : A →ₐ[R] C) (hfg : ∀ a : A, f a = 0 → g a = 0) :
  B →ₐ[R] C :=
{ to_fun := λ b, _,
  map_one' := _,
  map_mul' := _,
  map_zero' := _,
  map_add' := _,
  commutes' := _ }

Expected behavior: [What you expect to happen]

Perhaps some indication as to what the type of the _ I'm about to fill in is

Actual behavior: [What actually happens]

LEAN ASSERTION VIOLATION
File: /home/travis/build/leanprover-community/lean/src/frontends/lean/elaborator.cpp
Line: 3174
Task: /home/buzzard/lean-projects/M4P33/scratch/unreachable.lean: quot.lift
m_ctx.match(e, *val2)

Reproduces how often: [What percentage of the time does it reproduce?]

These are often hard to catch and can sometimes be fixed by restarting Lean, but this one seems to be reliably problematic.

Versions

3.5.1 on Ubuntu 18.04 at least.

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[semorrison]

Here's another instance of the same LEAN ASSERTION VIOLATION:

LEAN ASSERTION VIOLATION
File: /Users/travis/build/leanprover-community/lean/src/frontends/lean/elaborator.cpp
Line: 3174
Task: /Users/scott/projects/lean/mathlib-Rep/src/group_theory/Rep.lean: Rep.monoid_algebra_equivalence.distrib_mul_action_of_monoid_algebra_module
m_ctx.match(e, *val2)

$lean --version
Lean (version 3.8.0, commit e694f496aa08, Release)

Sorry it's far from minimised, but if anyone wants to play with it:

cd mathlib
git checkout origin/Rep
git checkout aaeb43eabda619b90e03d5197f864f6bc7e66770
lean --make src/group_theory/Rep.lean

[kbuzzard]

You can add leanproject get-cache after the second checkout if you want to see this happening more quickly. NB there's a typo in the imports in group_theory/Action.lean: category_Theory.eq_to_hom -> category_theory.eq_to_hom.

Scott's variant is particularly scary though, because he has filled in all the underscores. I have not seen this before. It will make working on the code basically impossible, I guess.

Here's a minimised version with no mathlib imports at all:

/-- notation typeclass not in core.  -/
class has_scalar (G : Type) (V : Type) := (smul : G → V → V)

infixr ` • `:73 := has_scalar.smul

structure Ring : Type.

instance : has_coe_to_sort Ring :=
{ 
  S := Type,
  coe := λ R, unit
}

variables {G : Type} [has_mul G] {R : Ring}

class distrib_mul_action' (G : Type) (V : Type) 
  [has_mul G]
  extends has_scalar G V :=
(foo : ∀ (x y : G) (b : V), x • b = x • y • b) -- note that changing x • y • b to y • b fixes the violation
                                               -- and instead we get a different error.

structure finsupp' (β : Type) : Type :=
(to_fun             : β → β)

def mas (r : R) : finsupp' ↥R  := 
{ 
  to_fun := id,
}

variables (V : Type)

instance foo : distrib_mul_action' G V :=
{ 
  smul := λ g v, (mas ()) • v, -- note that changing () to 37 also causes an assertion violation
  foo := λ g g' v, sorry
}

[kbuzzard]

NB I just edited the previous post; this is now a reliable mathlib-free example. Issue manifests itself with Lean 3.8.0.

[kbuzzard]

Mathlib-free version of first example:

open function

class has_scalar' (R : Type*) (A : Type*) := (smul : R → A → A)

infixr ` • `:73 := has_scalar'.smul

structure ring_hom' (M : Type*) (N : Type*) [semiring M] [semiring N] :=
(to_fun : M → N)
(map_one' : to_fun 1 = 1)
(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)
(map_zero' : to_fun 0 = 0)
(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)

instance (α : Type*) (β : Type*) [semiring α] [semiring β] : has_coe_to_fun (ring_hom' α β) :=
⟨_, λ f, ring_hom'.to_fun (f)⟩

class algebra' (R : Type*) (A : Type*) [comm_semiring R] [semiring A]
  extends has_scalar' R A, ring_hom' R A :=
(commutes' : ∀ r x, to_fun r * x = x * to_fun r)
(smul_def' : ∀ r x, r • x = to_fun r * x)

def algebra_map' (R : Type*) (A : Type*) [comm_semiring R] [semiring A] [algebra' R A] : ring_hom' R A :=
algebra'.to_ring_hom'

structure alg_hom' (R : Type*) (A : Type*) (B : Type*)
  [comm_semiring R] [semiring A] [semiring B] [algebra' R A] [algebra' R B] extends ring_hom' A B :=
(commutes' : ∀ r : R, to_fun (algebra_map' R A r) = algebra_map' R B r)

variables {R : Type*} {A : Type*} {B : Type*}
variables [comm_semiring R] [semiring A] [semiring B]
variables [algebra' R A] [algebra' R B]

instance : has_coe_to_fun (alg_hom' R A B) := ⟨_, λ f, f.to_fun⟩

def quot.lift
  {R : Type} [comm_ring R]
  {A : Type} [comm_ring A] [algebra' R A]
  {B : Type*} [comm_ring B] [algebra' R B]
  {C : Type} [comm_ring C] [algebra' R C]
  (f : alg_hom' R A B) (hf : surjective f)
  (g : alg_hom' R A C) (hfg : ∀ a : A, f a = 0 → g a = 0) :
  alg_hom' R B C :=
{ to_fun := λ b, _,
  map_one' := _,
  map_mul' := _,
  map_zero' := _,
  map_add' := _,
  commutes' := _ }

[kbuzzard]

This also shows up in 3.8.0. Note also conversation at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/cool.20assertion.20violation/near/194431048