Auto implicit not solved, even though it should be straightforward function application on closed terms

Question

I have the following Agda code:

open import Data.Maybe
open import Data.Product

data Addressing : Set where
  PC++ SP++ SP-- : Addressing

combine : Maybe Addressing → Maybe Addressing → Maybe Addressing
combine nothing y = y
combine (just x) nothing = just x
combine (just PC++) (just PC++) = just PC++
combine (just SP++) (just SP++) = just SP++
combine (just SP--) (just SP--) = just SP--
combine (just _) (just _) = nothing

record Ends : Set where
  constructor _⇝_
  field
    before : Maybe Addressing
    after : Maybe Addressing
open Ends

Compatible : Ends → Maybe Ends → Set
Compatible this that = Is-just (combine (after this) (that >>= before))

open import Data.Maybe.Relation.Unary.Any

append : (this : Ends) → (that : Maybe Ends) → Compatible this that → Ends
append ends nothing _ = ends
append (start ⇝ _) (just (_ ⇝ end)) _ = start ⇝ end

data Transfer : Set where
  Load Store : Transfer

data Microcode (Step : Ends → Set) : Maybe Ends → Set where
  [] : Microcode Step nothing
  _∷_ : ∀ {this rest} → Step this → Microcode Step rest → {auto match : Compatible this rest} → Microcode Step (just (append this rest match))

infixr 20 _∷_

As you can see, combine is a total function with two datatype arguments. I would expect auto match : Compatible this rest to be easily resolved if this and rest are closed terms.

However, when I try to use it like this:

data Step : Ends → Set where
  Load : (addr : Addressing) → Step (just addr ⇝ nothing)
  Store : (addr : Addressing) → Step (nothing ⇝ just addr)
  ALU : Step (nothing ⇝ nothing)

microcode : Microcode Step (just (just PC++ ⇝ just SP++))
microcode = Load PC++ ∷ Store SP++ ∷ []

then I get unsolved metas at every cons step:

_auto_56 : Compatible (nothing ⇝ just SP++) nothing
_match_57 : Compatible (nothing ⇝ just SP++) nothing 
_auto_58 : Compatible (just PC++ ⇝ nothing) (just (nothing ⇝ just SP++))
_match_59 : Compatible (just PC++ ⇝ nothing) (just (nothing ⇝ just SP++))

What is going on here? If I put e.g. the first one in a hole and evaluate it, its normal form is:

Any (λ _ → Agda.Builtin.Unit.⊤) (just SP++)

which to me suggests Agda is able to compute it, so why is it not used to solve those auto implicits?

Answer 1

Agda doesn't have an auto keyword. {auto match : Compatible this rest} introduces two parameters, called auto and match.

For the desired behavior, one solution is to just use implicit arguments and predicates computing to ⊤ or ⊥. If the predicate computes to ⊤, its witness is inferred to be tt by the eta law.

Compatible : Ends → Maybe Ends → Set
Compatible this that = T (is-just (combine (after this) (that >>= before)))

_∷_ : ... {match : Compatible this rest} ...

The other solution, corresponding more closely to Idris auto, is instance arguments:

data Is-just' {A : Set} : Maybe A → Set where
  instance is-just' : ∀ {x} → Is-just' (just x)

Compatible this that = Is-just' (combine (after this) (that >>= before))

_∷_ : ... {{match : Compatible this rest}} ...