[Agda] instance arguments proposal and crash

[Paolo Capriotti]

Hi all,

I'm currently experimenting with ways to squeeze as much overloading as possible
out of Agda's instance arguments. My simplified use case looks something like
this:

    record IsMonoid (M : Set) : Set where
      field
        unit : M
        _*_ : M → M → M

    record IsGroup (M : Set) : Set where
      field
        is-mon : IsMonoid M
        inv : M → M

    record Monoid : Set₁ where
      field
        carrier : Set
        is-mon : IsMonoid carrier

    record Group : Set₁ where
      field
        carrier : Set
        is-grp : IsGroup carrier

Now, I want to be able to define a function like:

    f : (M : Monoid)(G : Group)
      → Monoid.carrier M × Monoid.carrier G

by simply writing

    f M G = unit , unit

without any qualification on unit. This is particularly important for infix
operators, because qualifying them is horrible, and always renaming them is
error prone, confusing and unmaintainable.

So, my idea is to define a record for "supertypes" of Monoid:

    record MonoidLike : Set₂ where
      field
        Sort : Set₁
        C : Sort → Set
        struct : (X : Sort) → IsMonoid (C X)

and define an instance for every actual supertype:

    mon-monlike = record
      { Sort = Monoid
      ; C = Monoid.carrier
      ; struct = Monoid.is-mon }

    grp-monlike = record
      { Sort = Group
      ; C = Group.carrier
      ; struct = λ G → IsGroup.is-mon (Group.is-grp) }

Now, to enable overloading of unit and _*_ over any MonoidLike, I'd like to
write something like:

    module MonoidInterface ⦃ ml : MonoidLike ⦄
                           ⦃ X : MonoidLike.Sort ml ⦄ where
      open IsMonoid (MonoidLike.struct ml X) public

Unfortunately, this doesn't quite work. I think the problem is that instance
arguments are resolved individually, and since there are two terms of type
MonoidLike in scope, ml is not resolved.

So what would be nice to have, here, is a way to instruct the instance
resolution mechanism to search for ml and X "at the same time". Basically, that
means that for every ml : MonoidLike in scope, all MonoidLike.Sort ml should be
searched, and if this search _globally_ returns a single value, then resolution
should succeed.

The best we can do with the way instance arguments currently work is to combine
ml and X above in a single Σ type, but then resolution will fail unless we
explicit bring the right pairs into scope, which can be cumbersome, as the
number of pairs is quadratic in the number of structures and instances.

Anyway, in one of my earlier attempts at tackling this problem, I stumbled upon
a crash. Here's the code triggering it:

    module bug where

    record IsMonoid (M : Set) : Set where
      field
        unit : M
        _*_ : M → M → M

    record Monoid : Set₁ where
      field
        carrier : Set
        is-mon : IsMonoid carrier

    record Structure (Struct : Set₁)
                     (HasStruct : Set → Set)
                     (carrier : Struct → Set) : Set₁ where
      field
        has-struct : (X : Struct) → HasStruct (carrier X)

    mon-mon-struct : Structure Monoid IsMonoid Monoid.carrier
    mon-mon-struct = record
      { has-struct = Monoid.is-mon }

    mon-mon-struct' : Structure Monoid IsMonoid Monoid.carrier
    mon-mon-struct' = record
      { has-struct = Monoid.is-mon }

    unit : {Struct : Set₁}{C : Struct → Set}
         → ⦃ X : Struct ⦄
         → ⦃ struct : Structure Struct IsMonoid C ⦄
         → C X
    unit {Struct}{C} ⦃ X ⦄ ⦃ struct ⦄ = IsMonoid.unit
(Structure.has-struct struct X)

    f : (M : Monoid) → Monoid.carrier M
    f M = unit

This gives: An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Eliminators.hs:45.

BR,
Paolo