structure declaration timeout

Stream: general

[Jireh Loreaux]

Can anyone explain what is going on with the interplay between continuous_linear_map and prod in these structure declarations? Some things seem fine, but as soon as a field in a structure includes a product of a continuous linear map with anything else, the declaration either times out, or almost does. It even does this if you pass all the arguments (including instances) to continuous_linear_map explicitly. Ideas appreciated. Remove the #exit to see what I mean.

import analysis.normed_space.basic

universes u v

variable (X : Type u)

section

variables (𝕜 : Type u) (A : Type v)
  [semiring 𝕜]
  [add_comm_monoid A]
  [module 𝕜 A]
  [topological_space A]

variables (f : (A →L[𝕜] A) × (A →L[𝕜] A))

example : (A →L[𝕜] A) × (A →L[𝕜] A) := f

structure okay₁ :=
(prod : (A →ₗ[𝕜] A) × (A →ₗ[𝕜] A))

structure okay₂ :=
(single : A →L[𝕜] A)

#exit

-- this is even slow with the minimal import `topology.algebra.module.basic`
-- moreover, it's slow even if you name all the instances and pass all arguments to
-- `continuous_linear_map` explicitly.
structure slow :=
(prod : (A →L[𝕜] A) × X)

end

-- with just a bit more type class inference, the structure above times out

variables (𝕜 : Type u) (A : Type v)
  [nondiscrete_normed_field 𝕜]
  [normed_group A]
  [normed_space 𝕜 A]

variables (f : (A →L[𝕜] A) × (A →L[𝕜] A))

example : (A →L[𝕜] A) × (A →L[𝕜] A) := f

structure okay₃ :=
(prod : (A →ₗ[𝕜] A) × (A →ₗ[𝕜] A))

structure okay₄ :=
(single : A →L[𝕜] A)

structure timeout :=
(prod : (A →L[𝕜] A) × X)

[Junyan Xu]

I'm unable to reproduce the timeout on current master; the declarations only takes a few seconds each. But in any case when you get such timeouts, noncomputable! should be a reasonable thing to try.