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

[Ulf Norell]

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/20160218/4fee0308/attachment.html