Instance resolution bug with `Functor-Vec`

[WhatisRT]

This code fails to check:

module Test where

open import Class.Prelude
open import Class.Functor

private variable X Y : Type

test : ∀ {f : X} {x : Maybe (List Y)} → fmap (_++ []) x ≡ just []
test = {!!}

See agda/agda#8316 for full context. In this case, we get the following error:

  Resolve instance argument _r_13 : Functor _F_32
  Candidates
    Functor-Maybe : Functor Maybe
    Functor-Vec : ({n : ℕ} → Functor (flip Vec n))
    (stuck)

Note that there is absolutely no reason that Vec should show up here. So I'd suggest we mark Functor-Vec as INCOHERENT (or just not as an instance at all) for now. Thoughts @omelkonian?

[omelkonian]

To me, this seems like an Agda bug (caused by the unused {f : X} argument), so we shouldn't change anything on our side.

For now, setting fmap {F = Maybe} to help the type inference should suffice.

[WhatisRT]

Yeah, this is an Agda bug but it showed up in a real use case where f wasn't unused. I think it's better to have a temporary fix once here than on every use site.

[omelkonian]

Hmm don't know, this feels wrong to me. In the same vain, you would add workarounds like this for every Agda instance-related bug, and even worse you would have to revert them when the bugs are fixed.

Moreover, the Vec instance here is completely unrelated, so this could manifest from other instances (even user-written ones), hence this temporary fix is not even a fix.