<div dir="ltr">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),<div><br></div><div><div>instance</div><div> Reflexive[PackPack] : ∀ {a} {A : Pack a} → Reflexive ⟪ ⇧ ⟪ A ⟫ ⟫</div><div> _<_ {{Reflexive[PackPack] {A = A}}} ⟨ x ⟩ ⟨ y ⟩ = x < y</div><div> reflexivity {{Reflexive[PackPack] {A = A}}} {⟨ ⟨ x ⟩ ⟩} = ⟨ reflexivityᵈ A x ⟩</div><div><br></div><div>stuck : ∀ {a} {A : Pack a} (x : ⟪ A ⟫) → x < x</div><div>stuck x = reflexivity {{Reflexive[PackPack]}} {x = ⟨ x ⟩}</div></div><div><br></div><div>There are two reasons for this restriction:</div><div>- 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</div><div>- it leads to brittle code, where adding a completely unrelated instance might break existing code</div><div><br></div><div>You can read more here: <a href="http://agda.readthedocs.org/en/latest/language/instance-arguments.html#instance-resolution">http://agda.readthedocs.org/en/latest/language/instance-arguments.html#instance-resolution</a></div><div><br></div><div>/ Ulf</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 18, 2016 at 5:15 AM, David Darais <span dir="ltr"><<a href="mailto:darais@cs.umd.edu" target="_blank">darais@cs.umd.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
I have another use of typeclasses that fails to typecheck with both the release<br>
candidate 2.5.0.20160213 and master, and which typechecks successfully with<br>
2.4.2.5.<br>
<br>
The problem is that typeclass resolution can't resolve metas in a rather simple<br>
setting. In the definition of `stuck` in the code below, the unifier can't<br>
determine some very basic information, like `A : Set` and `x : A`, and as a<br>
result the typeclass instance `REFL : Reflexive A` can't be found. Agda had no<br>
problem determining `A = ⟪ A ⟫` in 2.4.2.5 and I think it should continue to be<br>
able to handle unification problems like this in the presence of type classes.<br>
<br>
I tried to reduce the problem to be minimal. The first part of the setup is a<br>
typeclass `Reflexive` for types `A : Set` which have a reflexive relation `_<_`<br>
and proof of reflexivity `reflexivity : ∀ {x : A} → x < x`. The second part of<br>
the setup is a type `Pack` which packages a type `A : Set` together with its<br>
typeclass instance `Reflexive A`, and a type `⟪ A ⟫` which holds elements of<br>
types packaged inside `A : Pack`. I then give a `Reflexive` instance for `⟪_⟫`<br>
which the `stuck` definition is unable to find, although I think it should (and<br>
so does Agda 2.4.2.5).<br>
<br>
Thanks!<br>
David<br>
<br>
-- Code --<br>
-- works in 2.4.2.5; unsolved metas in 2.5.0.20160213 and master --<br>
<br>
-- A relation which is reflexive<br>
record Reflexive (A : Set) : Set₁ where<br>
field<br>
_<_ : A → A → Set<br>
reflexivity : ∀ {x} → x < x<br>
open Reflexive {{...}}<br>
<br>
-- Packing a type with its reflexive relation<br>
data Pack : Set₁ where<br>
⇧ : ∀ (A : Set) {{_ : Reflexive A}} → Pack<br>
<br>
-- Projecting the raw type from a packed type<br>
dom : Pack → Set<br>
dom (⇧ A) = A<br>
<br>
-- Elements of a packed type<br>
data ⟪_⟫ (A : Pack) : Set where<br>
⟨_⟩ : dom A → ⟪ A ⟫<br>
<br>
-- The ordering between projected types is the original reflexive relation<br>
[_]_<ᵈ_ : ∀ (A : Pack) → dom A → dom A → Set<br>
[ ⇧ A ] x <ᵈ y = x < y<br>
<br>
-- Reflexivity between projected types<br>
reflexivityᵈ : ∀ (A : Pack) (x : dom A) → [ A ] x <ᵈ x<br>
reflexivityᵈ (⇧ A {{R}}) x = reflexivity {{R}}<br>
<br>
-- The relation on packed elements, through projection<br>
data _<⇧_ {A : Pack} : ⟪ A ⟫ → ⟪ A ⟫ → Set where<br>
⟨_⟩ : ∀ {x y} → [ A ] x <ᵈ y → ⟨ x ⟩ <⇧ ⟨ y ⟩<br>
<br>
-- The Reflexive instance for Pack<br>
instance<br>
Reflexive[Pack] : ∀ {A : Pack} → Reflexive ⟪ A ⟫<br>
Reflexive[Pack] {A} = record<br>
{ _<_ = _<⇧_<br>
; reflexivity = λ{ {⟨ x ⟩} → ⟨ reflexivityᵈ A x ⟩ }<br>
}<br>
<br>
-- Works<br>
goal₁ : ∀ {A : Pack} → ⟪ A ⟫ → ⟪ A ⟫ → Set<br>
goal₁ = _<_<br>
<br>
-- Resolving (A : Set) explicitly works<br>
goal₃ : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x<br>
goal₃ {A} x = reflexivity {⟪ A ⟫} {_}<br>
<br>
-- Resolving (r : Reflexive A) explicitly works<br>
goal₅ : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x<br>
goal₅ {A} x = reflexivity {_} {{Reflexive[Pack]}} {_}<br>
<br>
-- Resolving (x : A) explicitly works<br>
goal₄ : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x<br>
goal₄ {A} x = reflexivity {_} {x}<br>
<br>
-- Weird unsolved metas: (A : Set), (r : Reflexive A), (x : A), and<br>
-- two others (? : x <⇧ x)<br>
--<br>
-- Why can't type class resolution solve this?<br>
stuck : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x<br>
stuck x = reflexivity<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>