# Non-recursive Resolution For Instance Arguments

**Note**: as of Agda 2.4.2, instance search is in fact recursive (see the changelog for more details: https://github.com/agda/agda/blob/maint-2.4.2/CHANGELOG#L128), and if `listEq`

and `boolEq`

are declared in an `instance`

block, then `test`

can be written as expected.

As discussed, Agda resolves not explicitly provided instance arguments using a resolution strategy that tries to select a unique type-correct value from the call-site scope. It is important to remark that this resolution strategy is less powerful than the equivalent instance search for Haskell type classes. Suppose we have the following definitions:

`record Eq (t : Set) : Set where`

`field _==_ : t → t → Bool`

And we bring in scope the record functions taking the record as an instance argument:

` ``open module EqWithImplicits {t : Set} {{eqT : Eq t}} = Eq EqT`

Then we could have the following equivalent of a Haskell parameterised class instance:

`listEq : {A : Set} → Eq A → Eq (List A)`

`listEq {A} eqA = record { _==_ = eq } where`

`eq : List A → List A → Bool`

`eq [] [] = true`

`eq (a ∷ as) (b ∷ bs) = and (Eq.eq eqA a b) (eq' as bs)`

`eq _ _ = false`

However, if we try to use this, Agda will not automatically try to
apply this parameterised instance to obtain a value of `Eq t`

. The
following will cause a type error, saying that no value of type
`Eq (List Bool)`

was found in scope:

`postulate boolEq : Eq Bool`

`test = (true ∷ false ∷ []) == []`

Unlike in Haskell, we need to help Agda to find a correct instance:

`test = (true ∷ false ∷ []) == []`

`where eqListBool = listEq boolEq`

This limitation of the power of the instance search power was introduced to prevent the instance search from being exploited as a computational primitive. However, as a consequence, Agda does require a bit more guidance than Haskell to find the correct instance in situations such as this one.