Repository navigation
Instance resolution bug with Functor-Vec #27
Description
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?
Activity
omelkonian commentedon Jan 12, 2026
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 commentedon Jan 13, 2026
Yeah, this is an Agda bug but it showed up in a real use case where
fwasn't unused. I think it's better to have a temporary fix once here than on every use site.omelkonian commentedon Jan 13, 2026
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
Vecinstance here is completely unrelated, so this could manifest from other instances (even user-written ones), hence this temporary fix is not even a fix.