Non-recursiveResolutionForInstanceArguments

See the official user manual for the most up-to-date version of the information on this page.

TOC

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.