Idris - use same interface instance

Question

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?

Alexander Gryzlov Alexander Gryzlov · Accepted Answer · 2019-02-22T20:38:22

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

Idris - use same interface instance

1 Answers