Name resolution triggers typeclass resolution for EqDec instances

[skeuchel]

Using the machinery for name resolution currently triggers a recursive resolution for an EqDec instance the type of names, for every variable occurrence separately.

For instance the following statement

Definition foo : Stm [ "x" ∷ ty.int; "y" ∷ ty.int ] ty.int :=
  exp_var "x" + exp_var "y".

result in the following typeclass resolutions

Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false
Debug: 1: looking for ("x"∷ty.int ∈ ["x"∷ty.int; "y"∷ty.int])%type without backtracking
Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false
Debug: 1: looking for (EqDec string) without backtracking
Debug: 1.1: exact string_eqdec on (EqDec string), 0 subgoal(s)
Debug: 1.1: (*external*) (let xInΓ := eval compute in (ctx.resolve_mk_in Γ x ()) in
                          exact
                          xInΓ) on ("x"∷ty.int ∈ ["x"∷ty.int; "y"∷ty.int])%type, 0 subgoal(s)
Debug: 1: looking for ("y"∷ty.int ∈ ["x"∷ty.int; "y"∷ty.int])%type without backtracking
Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false
Debug: 1: looking for (EqDec string) without backtracking
Debug: 1.1: exact string_eqdec on (EqDec string), 0 subgoal(s)
Debug: 1.1: (*external*) (let xInΓ := eval compute in (ctx.resolve_mk_in Γ x ()) in
                          exact
                          xInΓ) on ("y"∷ty.int ∈ ["x"∷ty.int; "y"∷ty.int])%type, 0 subgoal(s)

which shows the looking for (EqDec string).

Instead of having a generic Hint for resolution we might want to add specific Hints that fix the EqDec instance upfront. Maybe through a module?