Typeclass resolution affects type inference of unrelated variables
The following code
From stdpp Require Import gmap.
Definition test γ (m : gset (nat * nat)) :=
γ = 0.shows this error
Error:
In environment
γ : finite.Finite (nat * nat)
m : gset (nat * nat)
The term "0" has type "nat" while it is expected to have type "finite.Finite (nat * nat)".This is due to TC resolution calling trivial which turns the type of γ into the goal:
Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false
Debug: 1: looking for (EqDecision (nat * nat)) with backtracking
Debug: 1.1: simple apply @trichotomyT_dec on (EqDecision (nat * nat)), 2 subgoal(s)
Debug: 1.1-1 : (TrichotomyT eq)
Debug: 1.1-1: looking for (TrichotomyT eq) with backtracking
Debug: 1.1-1: no match for (TrichotomyT eq), 0 possibilities
Debug: 1.2: simple apply @prod_eq_dec on (EqDecision (nat * nat)), 2 subgoal(s)
Debug: 1.2-1 : (EqDecision nat)
Debug: 1.2-1: looking for (EqDecision nat) with backtracking
Debug: 1.2-1.1: exact Nat.eq_dec on (EqDecision nat), 0 subgoal(s)
Debug: 1.2-2 : (EqDecision nat)
Debug: 1.2-2: looking for (EqDecision nat) with backtracking
Debug: 1.2-2.1: exact Nat.eq_dec on (EqDecision nat), 0 subgoal(s)
Debug: 2: looking for (Countable (nat * nat)) without backtracking
Debug: 2.1: simple apply @finite.finite_countable ; trivial on (Countable (nat * nat)), 0 subgoal(s)