<div dir="ltr"><div dir="ltr"><div>The subscript is to avoid shadowing the module parameter DynD.<br></div><div><br></div><div> The problem here is that there are multiple possible candidates for the instance goals. In the first case both DynD and unwrapDynInst are possible, and in the second case both the unnamed ToDyn argument and unwrapDynInst.</div><div><br></div><div> If you don't make unwrapDynInst `instance` it works.</div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Nov 28, 2019 at 7:06 AM Joey Eremondi <<a href="mailto:joey.eremondi@gmail.com">joey.eremondi@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>I'm hitting errors I don't understand with instance search, and I've boiled it down to a (fairly) minimal example:</div><div><br></div><div><div style="color:rgb(171,178,191);background-color:rgb(40,44,52);font-weight:normal;font-size:14px;line-height:19px;white-space:pre-wrap"><div><span style="color:rgb(198,120,221)">module</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">Minimal</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">where</span></div><br><div><span style="color:rgb(198,120,221)">open import</span><span style="color:rgb(171,178,191)"> Relation.Binary.PropositionalEquality</span></div><br><div><span style="color:rgb(198,120,221)">open import</span><span style="color:rgb(171,178,191)"> Agda.Primitive</span></div><br><div><span style="color:rgb(198,120,221)">module</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">A</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">where</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">record</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">ToDyn</span><span style="color:rgb(171,178,191)"> {l} (TheDyn : Set l) (a : Set l) : Set l </span><span style="color:rgb(198,120,221)">where</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">field</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">toDyn</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> a -> TheDyn</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">fromDyn</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> TheDyn -> a</span></div><div><span style="color:rgb(171,178,191)"> </span></div><br><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">open</span><span style="color:rgb(171,178,191)"> ToDyn {{...}} </span><span style="color:rgb(198,120,221)">public</span></div><br><br><div><span style="color:rgb(198,120,221)">module</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">B</span><span style="color:rgb(171,178,191)"> (DynB : ∀ (</span><span style="color:rgb(198,120,221)">l</span><span style="color:rgb(171,178,191)">) -> Set l) </span><span style="color:rgb(198,120,221)">where</span></div><br><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">open</span><span style="color:rgb(171,178,191)"> A</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">record</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">GType</span><span style="color:rgb(171,178,191)"> (l) : Set (lsuc l) </span><span style="color:rgb(198,120,221)">where</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">field</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">~_</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> Set l</span></div><div><span style="color:rgb(171,178,191)"> {{dynInst}} : ToDyn (DynB l) ~_</span></div><br><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">open</span><span style="color:rgb(171,178,191)"> GType </span><span style="color:rgb(198,120,221)">public</span></div><br><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">toG</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(86,182,194)">∀</span><span style="color:rgb(171,178,191)"> {l} -> (t : Set l) -> {{dinst : ToDyn (DynB l) t}} -> GType l</span></div><div><span style="color:rgb(171,178,191)"> toG t {{dinst}} </span><span style="color:rgb(86,182,194)">=</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">record</span><span style="color:rgb(171,178,191)"> {~_ </span><span style="color:rgb(86,182,194)">=</span><span style="color:rgb(171,178,191)"> t ; dynInst </span><span style="color:rgb(86,182,194)">=</span><span style="color:rgb(171,178,191)"> dinst}</span></div><br><br><div><span style="color:rgb(198,120,221)">module</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">C</span><span style="color:rgb(171,178,191)"> (DynC : ∀ (</span><span style="color:rgb(198,120,221)">l</span><span style="color:rgb(171,178,191)">) -> Set l) </span><span style="color:rgb(198,120,221)">where</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">open</span><span style="color:rgb(171,178,191)"> A</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">open</span><span style="color:rgb(171,178,191)"> B DynC</span></div><br><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">record</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">GPi</span><span style="color:rgb(171,178,191)"> {l1 l2} (dom : GType l1) (cod : ~ dom -> GType l2) : Set (l1 ⊔ l2) </span><span style="color:rgb(198,120,221)">where</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">field</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">apply</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> (x : ~ dom) -> ~ (cod x)</span></div><br><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">setPi</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(86,182,194)">∀</span><span style="color:rgb(171,178,191)"> {l1 l2} -> (dom : Set l1) -> (cod : ( dom) -> Set l2) -> </span></div><div><span style="color:rgb(171,178,191)"> {{ idom2 : ToDyn (DynC l1) dom}} -> {{ icod2 : {x : dom} -> ToDyn (DynC l2) (cod x)}} -> Set (l1 ⊔ l2)</span></div><div><span style="color:rgb(171,178,191)"> setPi {l1} {l2} dom cod {{idom2}} {{icod2}} </span><span style="color:rgb(86,182,194)">=</span><span style="color:rgb(171,178,191)"> GPi (toG dom ) </span><span style="color:rgb(86,182,194)">λ</span><span style="color:rgb(171,178,191)"> x </span><span style="color:rgb(86,182,194)">→</span><span style="color:rgb(171,178,191)"> toG (cod x) </span></div><br><br><br><div><span style="color:rgb(198,120,221)">module</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">D</span><span style="color:rgb(171,178,191)"> (DynD : ∀ (</span><span style="color:rgb(198,120,221)">l</span><span style="color:rgb(171,178,191)">) -> Set l) </span><span style="color:rgb(198,120,221)">where</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">open</span><span style="color:rgb(171,178,191)"> A</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">open</span><span style="color:rgb(171,178,191)"> B DynD</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">open</span><span style="color:rgb(171,178,191)"> C DynD</span></div><br><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">data</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">Nat</span><span style="color:rgb(171,178,191)"> : Set </span><span style="color:rgb(198,120,221)">where</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">NZ</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> Nat</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">NS</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> Nat -> Nat</span></div><br><div><span style="color:rgb(171,178,191)"> instance</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">unwrapDynInst</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(86,182,194)">∀</span><span style="color:rgb(171,178,191)"> {l} { a : GType l} -> ToDyn (DynD l) (~ a)</span></div><div><span style="color:rgb(171,178,191)"> unwrapDynInst {l} {</span><span style="color:rgb(198,120,221)">record</span><span style="color:rgb(171,178,191)"> { ~_ </span><span style="color:rgb(86,182,194)">=</span><span style="color:rgb(171,178,191)"> ~_ ; dynInst </span><span style="color:rgb(86,182,194)">=</span><span style="color:rgb(171,178,191)"> dynInst }} </span><span style="color:rgb(86,182,194)">=</span><span style="color:rgb(171,178,191)"> dynInst</span></div><br><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">someFun</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> {{_ : ToDyn (DynD lzero) Nat}} -> setPi Nat (\ _ -> Nat) </span></div><div><span style="color:rgb(171,178,191)"> someFun </span><span style="color:rgb(86,182,194)">=</span><span style="color:rgb(171,178,191)"> {!!}</span></div><br><div><span style="color:rgb(171,178,191)"> </span></div><br></div></div><div><br></div><div>I've got four modules:</div><div>* Module A defines a record (i.e. typeclass) with some functions</div><div>* Module B defines an existential type along with the class from module A</div><div>* Module C defines Pi types over these existential types</div><div>* Module D tries to construct a function of this Pi type</div><div><br></div><div>You can run the code yourself, but on Agda 2.6.0.1 I get the following error:</div><div><br></div><div><div style="color:rgb(171,178,191);background-color:rgb(40,44,52);font-weight:normal;font-size:14px;line-height:19px;white-space:pre-wrap"><div><span style="color:rgb(171,178,191)">Failed to solve the following constraints:</span></div><div><span style="color:rgb(171,178,191)"> Resolve instance argument</span></div><div><span style="color:rgb(171,178,191)"> _icod2_66</span></div><div><span style="color:rgb(171,178,191)"> : (DynD₁ : (l : Level) </span><span style="color:rgb(86,182,194)">→</span><span style="color:rgb(171,178,191)"> Set l) ⦃ _ </span><span style="color:rgb(86,182,194)">=</span><span style="color:rgb(171,178,191)"> z : ToDyn (DynD₁ lzero) Nat ⦄</span></div><div><span style="color:rgb(171,178,191)"> {x : Nat} </span><span style="color:rgb(86,182,194)">→</span></div><div><span style="color:rgb(171,178,191)"> ToDyn (DynD₁ lzero) Nat</span></div><div><span style="color:rgb(171,178,191)"> Candidates</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">DynD</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> ToDyn (@</span><span style="color:rgb(209,154,102)">2</span><span style="color:rgb(171,178,191)"> lzero) Nat</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(86,182,194)">λ</span><span style="color:rgb(171,178,191)"> {l} </span><span style="color:rgb(86,182,194)">→</span><span style="color:rgb(171,178,191)"> unwrapDynInst :</span></div><div><span style="color:rgb(171,178,191)"> {l : Level} {a : GType l} </span><span style="color:rgb(86,182,194)">→</span><span style="color:rgb(171,178,191)"> ToDyn (@</span><span style="color:rgb(209,154,102)">4</span><span style="color:rgb(171,178,191)"> l) (~ a)</span></div><div><span style="color:rgb(171,178,191)"> Resolve instance argument</span></div><div><span style="color:rgb(171,178,191)"> _idom2_65</span></div><div><span style="color:rgb(171,178,191)"> : (DynD₁ : (l : Level) </span><span style="color:rgb(86,182,194)">→</span><span style="color:rgb(171,178,191)"> Set l)</span></div><div><span style="color:rgb(171,178,191)"> ⦃ _ </span><span style="color:rgb(86,182,194)">=</span><span style="color:rgb(171,178,191)"> z : ToDyn (DynD₁ lzero) Nat ⦄ </span><span style="color:rgb(86,182,194)">→</span></div><div><span style="color:rgb(171,178,191)"> ToDyn (DynD₁ lzero) Nat</span></div><div><span style="color:rgb(171,178,191)"> Candidates</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(97,175,239)">_</span><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(198,120,221)">:</span><span style="color:rgb(171,178,191)"> ToDyn (DynD lzero) Nat</span></div><div><span style="color:rgb(171,178,191)"> </span><span style="color:rgb(86,182,194)">λ</span><span style="color:rgb(171,178,191)"> {l} </span><span style="color:rgb(86,182,194)">→</span><span style="color:rgb(171,178,191)"> unwrapDynInst :</span></div><div><span style="color:rgb(171,178,191)"> {l : Level} {a : GType l} </span><span style="color:rgb(86,182,194)">→</span><span style="color:rgb(171,178,191)"> ToDyn (DynD l) (~ a)</span></div><br></div></div><div><br></div><div>And here's my confusion: it's looking for ToDyn (DynD₁ lzero) Nat and it has a candidate ToDyn (DynD lzero) Nat.</div><div><br></div><div>So, what is the subscript 1 on DynD? Why does it think there are two different versions of DynD, that it doesn't unify? Is this a bug, or behaviour I just don't understand? And is there a way to work around this without manually writing the instances everywhere (which defeats the point of instance arguments)?</div><div><br></div><div>Thanks!<br></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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></div>