help with typeclass timeout

Stream: general

[Scott Morrison]

If you try

example {M : Type*} [add_comm_group M] : has_scalar ℤ M := infer_instance

in src/group_theory/group_action.lean, you get a timeout. :-(

[Scott Morrison]

Much later, we defined a instance {M : Type*} [add_comm_group M] module ℤ M := ... which makes this timeout go away by providing a short-circuit, but this problem has its own problems.

[Scott Morrison]

If anyone can suggest some instances we could remove to avoid this has_scalar problem, that would be wonderful. :-)

[Gabriel Ebner]

This will be fixed in 3.7:

example {M : Type*} [add_comm_group M] : has_scalar ℤ M :=
infer_instance
/-
group_action.lean:230:0: error
failed to synthesize type class instance for
M : Type ?,
_inst_1 : add_comm_group M
⊢ has_scalar ℤ M
-/