Zulip Chat Archive

Stream: general

Topic: help with typeclass timeout


view this post on Zulip 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. :-(

view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip 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 ?,
_inst_1 : add_comm_group M
⊢ has_scalar ℤ M
-/

Last updated: May 10 2021 at 17:39 UTC