Coercion from a submodule to its underlying set

Stream: new members

[Joe]

A coercion from a submodule to its underlying set is defined in algebra/module:

instance : has_coe (submodule α β) (set β) := ⟨submodule.carrier⟩

However, the type inference system doesn't seem to use it. Instead, it is looking for has_coe_to_fun (submodule α β). This sometimes results in a timeout. See the following example.

import analysis.normed_space.basic

variables {α : Type*} {β : Type*}
  [add_comm_group α] [module ℝ α]
  (x : α) (K : submodule ℝ α)

#check (K : set α) -- (deterministic) timeout
-- [class_instances] (0) ?x_3 : has_coe_to_fun
  -- (@submodule ℝ α (@normed_ring.to_ring ℝ (@normed_field.to_normed_ring ℝ real.normed_field)) _inst_1
    -- (@vector_space.to_module ℝ α (@normed_field.to_discrete_field ℝ real.normed_field) _inst_1 _inst_2))
    -- ...

Does that mean we need to add the following instance?

instance : has_coe_to_fun (submodule ℝ α) := ⟨_, submodule.carrier⟩

[Mario Carneiro]

did you try writing (\u K : set A)?