Zulip Chat Archive

Stream: new members

Topic: Coercion from a submodule to its underlying set

Joe (Jul 30 2019 at 14:13):

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 (Jul 30 2019 at 23:08):

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

Last updated: Dec 20 2023 at 11:08 UTC