entering tactic mode causes stack overflow

Stream: lean4

[Kevin Buzzard]

import Mathlib.Algebra.Algebra.Subalgebra.Basic

variable {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] [Algebra R A]

open Subalgebra

def foo (S : Subalgebra R Aᵐᵒᵖ) : Subalgebra R A where
  __ := MulOpposite.unop (Submodule.equivOpposite (toSubmodule S))
  mul_mem' ha hb := sorry
  -- comment out the next line and uncomment the one after to cause a stack overflow
  algebraMap_mem' r := sorry
  -- algebraMap_mem' r := by sorry

Reported by @Jz Pan here. I haven't made any attempt to minimise, my first instinct was to raise the issue here as is, to see if anyone could guess what might be going on. The goal at the sorry is

⊢ (algebraMap R A) r ∈
  { toSubmonoid := { toSubsemigroup := { carrier := __spread✝⁻⁰.carrier, mul_mem' := ⋯ }, one_mem' := ⋯ },
      add_mem' := ⋯, zero_mem' := ⋯ }.carrier

[Jz Pan]

This also crashes:

import Mathlib.Algebra.Algebra.Subalgebra.Basic

variable {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] [Algebra R A]

open Subalgebra

-- just define an identity map
def foo (S : Subalgebra R A) : Subalgebra R A where
  __ := toSubmodule S
  mul_mem' ha hb := sorry
  -- comment out the next line and uncomment the one after to cause a stack overflow
  algebraMap_mem' r := sorry
  -- algebraMap_mem' r := by sorry

[Kim Morrison]

It would be great if someone could generate a Mathlib-free minimisation of this problem. Looks pretty buggy to me!

[Jz Pan]

The keyword __ does not work if import nothing.

[Jz Pan]

import Mathlib.Algebra.Algebra.Subalgebra.Basic

variable {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] [Algebra R A]

open Subalgebra

-- just define an identity map
def foo (S : Subalgebra R A) : Subalgebra R A := {
  toSubmodule S with
  mul_mem' := fun ha hb ↦ by sorry
  -- comment out the next line and uncomment the one after to cause a stack overflow
  algebraMap_mem' := fun r ↦ sorry
  -- algebraMap_mem' := fun r ↦ by sorry
}

[Jz Pan]

This does not crash:

class MyZero (T : Type) : Type where
  myZero' : T

def myZero {T : Type} [MyZero T] : T := MyZero.myZero'

class MyAlgebra (S T : Type) [MyZero S] [MyZero T] : Type where
  myAlgebraMap' : S → T
  map_zero' : myAlgebraMap' myZero = myZero

def myAlgebraMap (S T : Type) [MyZero S] [MyZero T] [MyAlgebra S T] :
    S → T := MyAlgebra.myAlgebraMap'

theorem my_map_zero (S T : Type) [MyZero S] [MyZero T] [MyAlgebra S T] :
    myAlgebraMap S T myZero = myZero := MyAlgebra.map_zero'

structure MySubmodule (S T : Type) [MyZero S] [MyZero T] where
  carrier : T → Prop
  zero_mem' : carrier myZero

structure MySubalgebra (S T : Type) [MyZero S] [MyZero T] [MyAlgebra S T] extends
  MySubmodule S T where
  algebraMap_mem' : ∀ r, carrier (myAlgebraMap S T r)
  zero_mem' := my_map_zero S T ▸ algebraMap_mem' myZero

def foo {S T : Type} [MyZero S] [MyZero T] [MyAlgebra S T] (M : MySubalgebra S T) : MySubalgebra S T := {
  M.toMySubmodule with
  algebraMap_mem' := fun r ↦ by sorry
}

I assume that it must get more complicated.

[Kevin Buzzard]

(deleted)

[Floris van Doorn]

Here is an import-free version:

structure SubInhabited (A : Type) [Inhabited A] : Type where
  carrier : A → Prop
  default_mem : carrier default

structure SubInhabited2 (A : Type) [Inhabited A] extends
  SubInhabited A : Type where
  new_default_mem : carrier default
  default_mem := new_default_mem

def foo {A : Type} [Inhabited A] (S : SubInhabited2 A) : SubInhabited2 A := {
  carrier := S.carrier
  new_default_mem := by sorry -- stack overflow
  -- uncomment the following to make the error go away
  -- default_mem := sorry
}

[Floris van Doorn]

lean4#3839