timeout depending on variable location

Stream: general

[Winston Yin]

I'm getting "deterministic timeout" on a definition, but only when the variables are declared within the definition itself. When variables are declared under the variables keyword beforehand, all is good. Below is the best #mwe I could come up with:

import geometry.manifold.smooth_manifold_with_corners
import geometry.manifold.algebra.lie_group
import analysis.normed_space.units

noncomputable theory

open_locale manifold

namespace units

variables {R : Type*} [normed_ring R] [complete_space R]

instance : charted_space R Rˣ := open_embedding_coe.singleton_charted_space

lemma chart_at_apply {a : Rˣ} {b : Rˣ} : chart_at R a b = b := rfl
lemma chart_at_source {a : Rˣ} : (chart_at R a).source = set.univ := rfl

variables {𝕜 : Type*} [nontrivially_normed_field 𝕜] [normed_algebra 𝕜 R]

instance : smooth_manifold_with_corners 𝓘(𝕜, R) Rˣ :=
open_embedding_coe.singleton_smooth_manifold_with_corners 𝓘(𝕜, R)

instance : lie_group 𝓘(𝕜, R) Rˣ := sorry

end units

-- deterministic timeout:
-- example {𝕜 : Type*} [nontrivially_normed_field 𝕜]
--   {M : Type*} [normed_add_comm_group M] [complete_space M] [normed_space 𝕜 M]
--  : lie_group 𝓘(𝕜, M →L[𝕜] M) (M →L[𝕜] M)ˣ := sorry

variables
  {𝕜 : Type*} [nontrivially_normed_field 𝕜]
  {M : Type*} [normed_add_comm_group M] [complete_space M] [normed_space 𝕜 M]

example : lie_group 𝓘(𝕜, M →L[𝕜] M) (M →L[𝕜] M)ˣ := sorry

[Alex J. Best]

It seems the issue is something to do with universes, this works for me:

universes u v
example {𝕜 : Type u} [nontrivially_normed_field 𝕜]
  {M : Type v} [normed_add_comm_group M] [complete_space M] [normed_space 𝕜 M]
 : lie_group 𝓘(𝕜, M →L[𝕜] M) (M →L[𝕜] M)ˣ := sorry

[Winston Yin]

On a different note, would it be worth it to register an instance that can otherwise be synthesised, in order to speed up the synthesis?

[Alex J. Best]

I can't speak for this particular area, but yes there are instances of typeclass short circuits in mathlib already (normally with a comment saying so), so if its a decent speed up I'd say go for it