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

[Ulf Norell]

I would try to split the class in two. Something like this

record ReflexiveRel {a} (A : Set a) : Set (lsuc a) where
  field _<_ : A → A → Set a
open ReflexiveRel {{...}}

record Reflexive {a} (A : Set a) (_<_ : A → A → Set a) : Set a where
  field reflexivity : {x : A} → x < x
open Reflexive {{...}}

/ Ulf

On Fri, Feb 19, 2016 at 12:28 AM, David Darais <darais at cs.umd.edu> wrote:

> 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
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160219/d35e9fcd/attachment.html