I have a data structure
record IdentityPreservingMorphism domain codomain where
constructor MkMorphismOfMonoids
func : domain -> codomain
funcRespId : (Monoid domain, Monoid codomain) => func (Algebra.neutral) = Algebra.neutral
which just says that an IdentityPreservingMorphism is a morphism between monoids which needs to respect the identity.
I'm trying to prove that the identity morphisms is an IdentityPreservingMorphism
monoidIdentity : Monoid m => MorphismOfMonoids m m
monoidIdentity = MkMorphismOfMonoids
id
?respId
The easy shot for ?respId at Refl does not work because there are too many Monoid instances available. How can I tell the compiler that I would like to use only the instance coming from the monoidIdentity definition?
The "proper" solution to this requires (1) writing a proof of a form (m1 : Monoid m, m2 : Monoid m) => m1 = m2 and 2) being able to reify the two Monoid implementations from funcRespId to feed them into step 1. While the former can be simulated with a postulate/assert, it's the latter step that becomes problematic, which is probably related to https://github.com/idris-lang/Idris-dev/issues/4591.
A simpler workaround is to trivialize reification by storing implementations directly in the record:
record MorphismOfMonoids domain codomain where
constructor MkMorphismOfMonoids
func : domain -> codomain
mon1 : Monoid domain
mon2 : Monoid codomain
funcRespId : func (Algebra.neutral @{mon1}) = Algebra.neutral @{mon2}
monoidIdentity : Monoid m => MorphismOfMonoids m m
monoidIdentity @{mon} = MkMorphismOfMonoids id mon mon Refl