# Zulip Chat Archive

## Stream: general

### Topic: simp canonize

#### Simon Hudon (Jan 22 2019 at 17:28):

I'm trying to get rid of some simp loops and I just realized that there is a part of it I don't understand and it seems to be getting into a loop. Here is the trace that Lean prints for it:

[simplify.canonize] category_theory.types ==> category_theory.types [simplify.canonize] category_theory.types ==> category_theory.types [simplify.canonize] _inst_2 ==> _inst_2 [simplify.canonize] category_theory.types ==> category_theory.types [simplify.canonize] category_theory.types ==> category_theory.types [simplify.canonize] _inst_2 ==> _inst_2

How do I prevent it from looping? I tried `simp [-category_theory.types]`

and it doesn't work.

#### Johan Commelin (Jan 22 2019 at 17:36):

But `category_theory.types`

isn't even marked as `[simp]`

. How come the simplifier is using it?

#### Simon Hudon (Jan 22 2019 at 18:36):

I am puzzled too. My tentative answer is that it comes from the `canonize`

phase of `simp`

which I did not know of. It seems like a phase where class instances are reduced but I can't say more. @Sebastian Ullrich, would you care to enlighten us?

#### Simon Hudon (Jan 22 2019 at 20:49):

Update: using `set_option trace.debug.dsimplify true`

and using `dsimp`

instead of `simp`

, I managed to find the offender which was unrelated to `canonize`

#### Mario Carneiro (Jan 22 2019 at 22:01):

MWE

#### Simon Hudon (Jan 22 2019 at 23:21):

import category_theory.category import category_theory.types universes u class comonad (w : Type u → Type u) extends functor w := (extract : Π {α}, w α → α) (extend : Π {α β}, (w α → β) → w α → w β) def Cokleisli (m) [comonad.{u} m] := Type u open category_theory comonad instance {m} [comonad.{u} m] : category.{u} (Cokleisli m) := sorry def copipe {w α β γ} [comonad w] (f : w α → β) (g : w β → γ) : (w α → γ) := g ∘ extend f infix ` =>= `:55 := copipe instance Cokleisli.category {m} [comonad m] : category (Cokleisli.{u} m) := { hom := λ α β, m α → β, id := λ α, extract, comp := λ X Y Z f g, f =>= g, id_comp' := sorry, comp_id' := sorry, assoc' := sorry } @[simp] lemma Cokleisli.comp_def {m : Type* → Type*} [comonad m] (α β γ : Cokleisli m) (xs : α ⟶ β) (ys : β ⟶ γ) : xs ≫ ys = xs =>= ys := sorry variables {α β : Type u} example {m} [comonad m] (f : α ⟶ m α) (g : m α ⟶ α) : f ≫ g = 𝟙 _ := by { simp, } -- deep recursion was detected at 'expression replacer' (potential -- solution: increase stack space in your system)

#### Simon Hudon (Jan 22 2019 at 23:22):

If you comment out `Cokleisli.comp_def`

, the error disappears

Last updated: May 13 2021 at 06:15 UTC