[Agda] Another potential typeclass bug in release-candidate/master

[David Darais]

Hi Ulf,

Ah, I see. Your `Reflexive[PackPack]` example was very helpful. I agree it’s
better for Agda to not pick instances too eagerly in situations like this,
because of your second point about breaking existing code with unrelated
instances.

I would still love for small setoid-like examples like this to be resolvable
with typeclasses. If anyone has ideas for how I can restructure the example to
go through (i.e. not having to manually supply the instance), I would love to
hear it. I suppose it would come down to encoding that `_<_` is unique given
`A` in some way (a bit like Haskell's functional dependencies?) and maybe
there's an existing trick I'm just missing.

Thanks again,
David Darais

> On Feb 18, 2016, at 2:40 AM, Ulf Norell <ulf.norell at gmail.com> wrote:
> 
> This is the correct behaviour. Instance search has become more conservative about solving metas based on which instances are available. In your example, there could in principle be another choice of A if there were other instances around. For instance (after making your definitions level polymorphic),
> 
> instance
>   Reflexive[PackPack] : ∀ {a} {A : Pack a} → Reflexive ⟪ ⇧ ⟪ A ⟫ ⟫
>   _<_         {{Reflexive[PackPack] {A = A}}} ⟨ x ⟩ ⟨ y ⟩ = x < y
>   reflexivity {{Reflexive[PackPack] {A = A}}} {⟨ ⟨ x ⟩ ⟩} = ⟨ reflexivityᵈ A x ⟩
> 
> stuck : ∀ {a} {A : Pack a} (x : ⟪ A ⟫) → x < x
> stuck x = reflexivity {{Reflexive[PackPack]}} {x = ⟨ x ⟩}
> 
> There are two reasons for this restriction:
> - allowing metas to be solved by instance search can make the search loop, solving metas with more and more fantastical terms to fit the existing instances
> - it leads to brittle code, where adding a completely unrelated instance might break existing code
> 
> You can read more here: http://agda.readthedocs.org/en/latest/language/instance-arguments.html#instance-resolution
> 
> / Ulf
> 
> 
> On Thu, Feb 18, 2016 at 5:15 AM, David Darais <darais at cs.umd.edu> wrote:
> Hi,
> 
> I have another use of typeclasses that fails to typecheck with both the release
> candidate 2.5.0.20160213 and master, and which typechecks successfully with
> 2.4.2.5.
> 
> The problem is that typeclass resolution can't resolve metas in a rather simple
> setting. In the definition of `stuck` in the code below, the unifier can't
> determine some very basic information, like `A : Set` and `x : A`, and as a
> result the typeclass instance `REFL : Reflexive A` can't be found. Agda had no
> problem determining `A = ⟪ A ⟫` in 2.4.2.5 and I think it should continue to be
> able to handle unification problems like this in the presence of type classes.
> 
> I tried to reduce the problem to be minimal. The first part of the setup is a
> typeclass `Reflexive` for types `A : Set` which have a reflexive relation `_<_`
> and proof of reflexivity `reflexivity : ∀ {x : A} → x < x`. The second part of
> the setup is a type `Pack` which packages a type `A : Set` together with its
> typeclass instance `Reflexive A`, and a type `⟪ A ⟫` which holds elements of
> types packaged inside `A : Pack`. I then give a `Reflexive` instance for `⟪_⟫`
> which the `stuck` definition is unable to find, although I think it should (and
> so does Agda 2.4.2.5).
> 
> Thanks!
> David
> 
> -- Code --
> -- works in 2.4.2.5; unsolved metas in 2.5.0.20160213 and master --
> 
> -- A relation which is reflexive
> record Reflexive (A : Set) : Set₁ where
>   field
>     _<_ : A → A → Set
>     reflexivity : ∀ {x} → x < x
> open Reflexive {{...}}
> 
> -- Packing a type with its reflexive relation
> data Pack : Set₁ where
>   ⇧ : ∀ (A : Set) {{_ : Reflexive A}} → Pack
> 
> -- Projecting the raw type from a packed type
> dom : Pack → Set
> dom (⇧ A) = A
> 
> -- Elements of a packed type
> data ⟪_⟫ (A : Pack) : Set where
>   ⟨_⟩ : dom A → ⟪ A ⟫
> 
> -- The ordering between projected types is the original reflexive relation
> [_]_<ᵈ_ : ∀ (A : Pack) → dom A → dom A → Set
> [ ⇧ A ] x <ᵈ y = x < y
> 
> -- Reflexivity between projected types
> reflexivityᵈ : ∀ (A : Pack) (x : dom A) → [ A ] x <ᵈ x
> reflexivityᵈ (⇧ A {{R}}) x = reflexivity {{R}}
> 
> -- The relation on packed elements, through projection
> data _<⇧_ {A : Pack} : ⟪ A ⟫ → ⟪ A ⟫ → Set where
>   ⟨_⟩ : ∀ {x y} → [ A ] x <ᵈ y → ⟨ x ⟩ <⇧ ⟨ y ⟩
> 
> -- The Reflexive instance for Pack
> instance
>   Reflexive[Pack] : ∀ {A : Pack} → Reflexive ⟪ A ⟫
>   Reflexive[Pack] {A} = record
>     { _<_ = _<⇧_
>     ; reflexivity = λ{ {⟨ x ⟩} → ⟨ reflexivityᵈ A x ⟩ }
>     }
> 
> -- Works
> goal₁ : ∀ {A : Pack} → ⟪ A ⟫ → ⟪ A ⟫ → Set
> goal₁ = _<_
> 
> -- Resolving (A : Set) explicitly works
> goal₃ : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x
> goal₃ {A} x = reflexivity {⟪ A ⟫} {_}
> 
> -- Resolving (r : Reflexive A) explicitly works
> goal₅ : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x
> goal₅ {A} x = reflexivity {_} {{Reflexive[Pack]}} {_}
> 
> -- Resolving (x : A) explicitly works
> goal₄ : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x
> goal₄ {A} x = reflexivity {_} {x}
> 
> -- Weird unsolved metas: (A : Set), (r : Reflexive A), (x : A), and
> -- two others (? : x <⇧ x)
> --
> -- Why can't type class resolution solve this?
> stuck : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x
> stuck x = reflexivity
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>