## Stream: general

### Topic: help with typeclass timeout

#### Scott Morrison (Mar 11 2020 at 23:09):

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 (Mar 11 2020 at 23:10):

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 (Mar 11 2020 at 23:10):

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

#### Gabriel Ebner (Mar 12 2020 at 08:31):

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 ?,