agda
Data.List.Membership.Setoid should re-export Any's constructors
It's pretty annoying to have to import 2 modules every time we want to do anything with membership proofs.
This isn't quite as easy as it looks. If you implement the suggestion and then open Data.Any you get the error
Can't resolve overloaded constructors targeting the same datatype
(Data.List.Any.Any): Data.List.Any.Any.here
Data.List.Membership.Setoid._.here
Have you perhaps not passed the Setoid argument to Data.List.Membership.Setoid when opening it?
No, the problem seems to be that the here/there seem to be picking up an extra {A : Set a} parameter when they are exported in Membership.Propositional (from Membership.Setoid which in turn is from Any). Therefore the here from Any conflicts with the here from Membership.Propositional.
I can't seem to get it working. @gallais if you have the time, it'd be great if you'd have a look. Otherwise I'll drop it from v1.0 milestone as this is the last issue outstanding and it's not urgent.
Right, it seems to work on the LHS only. On the RHS Agda can't tell whether we mean
the Set-indexed or the Setoid-indexed version of here / there.
We can add it to Data.List.Membership.Propositional but it breaks again
when re-exported from Data.List.Membership.DecPropositional for the same reasons.
I guess this means this request is dead.
Whilst writing documentation, it has occurred to me we could redefine here and there locally instead of simply re-exporting. They wouldn't be compatible with here and there from ``Any`, but it would be better than nothing. Thoughts?