[Agda] Using instance arguments for pointed types

[Guillaume Brunerie]

Hi all,

I’m trying to use instance arguments to implement various things
related to pointed types but I’m facing a problem that I can’t solve.

A pointed type is a type [A] together with a point [a : A]. I want to
implement pointed types in such a way that by just writing [A], Agda
can guess what the base point is. This is easy to do, just define a
record [Pointed A] with a single field of type [A], and whenever you
need a pointed type [A], add an instance argument of type [Pointed A].
Then you can define terms of type [Pointed A] for various types [A]
and Agda will automatically find the base point when needed.

Problems arise when I want to define the iterated loop space of a
pointed type [A].
The loop space of a pointed type [A] (called [Loop A]) is the type [a
== a] (propositional equality) where [a] is the base point of [A],
pointed by the reflexivity path.
Then the n-iterated loop space of a pointed type [A] is defined by:

    Loop^ 0 A = A
    Loop^ (S n) A = Loop (Loop^ n A)

It is clear that for all [n] and [A], [Loop^ n A] is pointed because
both [A] and [Loop _] are. But Agda does not guess it automatically,
so we need to prove it simultaneously (this is needed for [Loop (Loop^
n A)] to type check).

But the problem is that given that [Loop^ 0 A = A], there are now two
different proofs that [A] is pointed, so Agda complains whenever you
want to do anything with [A].
And if [A] is itself a loop space, the problem is even worse.

This is related to issue 899 (Instance search fails if there are
several definitionally equal values in scope) but also (I think) to
issue 751 (Non-unifiable terms defined by pattern matching are not
detected as such) because I think that Agda would not be able to solve
the metas in the constraint [Loop^ ? ? = A] (which make sense given
that if [A] is a loop space there are several solutions).

Is it possible to workaround this problem?
Or do you think it would be possible to fix it? I’d be willing to try,
but I don’t know much work this could represent.

Thanks,

Guillaume Brunerie