<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"><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"><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>