<div dir="ltr"><div>Hi Conal,</div><div><br></div><div>I believe you're being bitten by the automatic insertion of implicit lambda abstractions. When Agda tries to check an expression at an implicit pi type like ∀ `{A : Magma 0ℓ 0ℓ} → A ⇒ A`, it will automatically insert an abstraction `λ {A} → ...` Likewise, when checking `id` it will automatically insert an implicit argument `{_}`. So the expression Agda actually tries to check is not `id` but `λ {A} →id {_}`. But now there's many possible solutions for the `_`, and Agda doesn't know which one to pick!</div><div><br></div><div>To work around the automatic insertion, you need to pass the `A` explicitly, for example like this:</div><div><br></div><div>```<br></div><div>id' : ∀ {A : Magma 0ℓ 0ℓ} → A ⇒ A<br>id' {A} = id {A}</div><div>```</div><div><br></div><div>There were two papers at ICFP this year that propose more intelligent strategies for the insertion of implicits (<a href="https://dl.acm.org/doi/10.1145/3408971">https://dl.acm.org/doi/10.1145/3408971</a> and <a href="https://dl.acm.org/doi/10.1145/3408983">https://dl.acm.org/doi/10.1145/3408983</a>), but neither of them has been implemented for Agda so far.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Nov 10, 2020 at 5:40 AM Conal Elliott <<a href="mailto:conal@conal.net">conal@conal.net</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"><p style="margin-bottom:1em;color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px">I’ve been encountering inference difficulties working with agda-categories. I’ve whittled down the problem to a simplified example that doesn’t use agda-categories (source also attached as T8.agda):</p><div id="gmail-m_-6517219575474230040gmail-cb3" style="overflow:auto;margin:1em 0px;color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px"><pre style="margin:0.5em 1.5em;border:1px solid rgb(221,221,221);overflow:auto;border-radius:0.3em;padding:0.5em 1em 0.5em 0.5em;background:rgba(255,255,0,0.15) none repeat scroll 0% 0%"><code style="font-size:16.91px;background:transparent none repeat scroll 0% 0%;border:medium none;overflow:visible;font-family:Menlo,"Lucida Console",Monaco,monospace;display:block;padding:0em"><a id="gmail-m_-6517219575474230040gmail-cb3-1" title="1" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span style="color:rgb(0,112,32);font-weight:bold">open</span> <span style="color:rgb(0,112,32);font-weight:bold">import</span> Level</a>
<a id="gmail-m_-6517219575474230040gmail-cb3-2" title="2" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span style="color:rgb(0,112,32);font-weight:bold">open</span> <span style="color:rgb(0,112,32);font-weight:bold">import</span> Algebra<span style="color:rgb(0,112,32)">.</span>Bundles <span style="color:rgb(0,112,32);font-weight:bold">using</span> <span style="color:rgb(0,112,32)">(</span>Magma<span style="color:rgb(0,112,32)">)</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-3" title="3" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span style="color:rgb(0,112,32);font-weight:bold">open</span> <span style="color:rgb(0,112,32);font-weight:bold">import</span> Relation<span style="color:rgb(0,112,32)">.</span>Binary <span style="color:rgb(0,112,32);font-weight:bold">using</span> <span style="color:rgb(0,112,32)">(</span>Rel<span style="color:rgb(0,112,32)">)</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-4" title="4" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span style="color:rgb(0,112,32);font-weight:bold">open</span> <span style="color:rgb(0,112,32);font-weight:bold">import</span> Function<span style="color:rgb(0,112,32)">.</span>Equality <span style="color:rgb(0,112,32);font-weight:bold">using</span> <span style="color:rgb(0,112,32)">(_</span>⟶<span style="color:rgb(0,112,32)">_)</span> <span style="color:rgb(0,112,32);font-weight:bold">renaming</span> <span style="color:rgb(0,112,32)">(</span>id <span style="color:rgb(0,112,32);font-weight:bold">to</span> ⟶-id<span style="color:rgb(0,112,32)">)</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-5" title="5" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit;height:1.2em"></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-6" title="6" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span style="color:rgb(0,112,32);font-weight:bold">record</span> Cat <span style="color:rgb(0,112,32)">(</span>o ℓ <span style="color:rgb(0,112,32)">:</span> Level<span style="color:rgb(0,112,32)">)</span> <span style="color:rgb(0,112,32)">:</span> <span style="color:rgb(144,32,0)">Set</span> <span style="color:rgb(0,112,32)">(</span>suc <span style="color:rgb(0,112,32)">(</span>o ⊔ ℓ<span style="color:rgb(0,112,32)">))</span> <span style="color:rgb(0,112,32);font-weight:bold">where</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-7" title="7" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span style="color:rgb(0,112,32);font-weight:bold">infix</span> <span style="color:rgb(64,160,112)">4</span> <span style="color:rgb(0,112,32)">_</span>⇒<span style="color:rgb(0,112,32)">_</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-8" title="8" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span style="color:rgb(0,112,32);font-weight:bold">field</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-9" title="9" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> Obj <span style="color:rgb(0,112,32)">:</span> <span style="color:rgb(144,32,0)">Set</span> o</a>
<a id="gmail-m_-6517219575474230040gmail-cb3-10" title="10" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span style="color:rgb(0,112,32)">_</span>⇒<span style="color:rgb(0,112,32)">_</span> <span style="color:rgb(0,112,32)">:</span> Rel Obj ℓ</a>
<a id="gmail-m_-6517219575474230040gmail-cb3-11" title="11" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> id <span style="color:rgb(0,112,32)">:</span> <span style="color:rgb(0,112,32)">∀</span> <span style="color:rgb(0,112,32)">{</span>A<span style="color:rgb(0,112,32)">}</span> <span style="color:rgb(0,112,32)">→</span> A ⇒ A</a>
<a id="gmail-m_-6517219575474230040gmail-cb3-12" title="12" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span style="color:rgb(96,160,176);font-style:italic">-- ... elided</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-13" title="13" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit;height:1.2em"></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-14" title="14" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit">M <span style="color:rgb(0,112,32)">:</span> Cat <span style="color:rgb(0,112,32)">_</span> <span style="color:rgb(0,112,32)">_</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-15" title="15" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit">M <span style="color:rgb(0,112,32)">=</span> <span style="color:rgb(0,112,32);font-weight:bold">record</span> <span style="color:rgb(0,112,32)">{</span> Obj <span style="color:rgb(0,112,32)">=</span> Magma 0ℓ 0ℓ</a>
<a id="gmail-m_-6517219575474230040gmail-cb3-16" title="16" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span style="color:rgb(0,112,32)">;</span> <span style="color:rgb(0,112,32)">_</span>⇒<span style="color:rgb(0,112,32)">_</span> <span style="color:rgb(0,112,32)">=</span> <span style="color:rgb(0,112,32)">λ</span> A B <span style="color:rgb(0,112,32)">→</span> Magma<span style="color:rgb(0,112,32)">.</span>setoid A ⟶ Magma<span style="color:rgb(0,112,32)">.</span>setoid B</a>
<a id="gmail-m_-6517219575474230040gmail-cb3-17" title="17" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span style="color:rgb(0,112,32)">;</span> id <span style="color:rgb(0,112,32)">=</span> ⟶-id</a>
<a id="gmail-m_-6517219575474230040gmail-cb3-18" title="18" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span style="color:rgb(96,160,176);font-style:italic">-- ...</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-19" title="19" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span style="color:rgb(0,112,32)">}</span> </a>
<a id="gmail-m_-6517219575474230040gmail-cb3-20" title="20" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit;height:1.2em"></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-21" title="21" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span style="color:rgb(0,112,32);font-weight:bold">open</span> Cat M</a>
<a id="gmail-m_-6517219575474230040gmail-cb3-22" title="22" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit;height:1.2em"></a>
<a id="gmail-m_-6517219575474230040gmail-cb3-23" title="23" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span style="color:rgb(0,112,32)">_</span> <span style="color:rgb(0,112,32)">:</span> <span style="color:rgb(0,112,32)">∀</span> <span style="color:rgb(0,112,32)">{</span>A <span style="color:rgb(0,112,32)">:</span> Magma 0ℓ 0ℓ<span style="color:rgb(0,112,32)">}</span> <span style="color:rgb(0,112,32)">→</span> A ⇒ A</a>
<a id="gmail-m_-6517219575474230040gmail-cb3-24" title="24" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span style="color:rgb(0,112,32)">_</span> <span style="color:rgb(0,112,32)">=</span> id</a></code></pre></div><p style="margin-bottom:1em;color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px">The error message (referring to the use of <code style="font-size:16.91px;background:transparent none repeat scroll 0% 0%;border:medium none;overflow:visible;font-family:Menlo,"Lucida Console",Monaco,monospace;white-space:pre-wrap"><span style="color:rgb(6,40,126)">id</span></code> in the last line):</p><div id="gmail-m_-6517219575474230040gmail-cb4" style="overflow:auto;margin:1em 0px;color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px"><pre style="margin:0.5em 1.5em;border:1px solid rgb(221,221,221);overflow:auto;border-radius:0.3em;padding:0.5em 1em 0.5em 0.5em;background:rgba(255,255,0,0.15) none repeat scroll 0% 0%"><code style="font-size:16.91px;background:transparent none repeat scroll 0% 0%;border:medium none;overflow:visible;font-family:Menlo,"Lucida Console",Monaco,monospace;display:block;padding:0em"><a id="gmail-m_-6517219575474230040gmail-cb4-1" title="1" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span style="color:rgb(0,112,32)">__</span>∙<span style="color:rgb(0,112,32)">__</span><span style="color:rgb(64,160,112)">27</span> <span style="color:rgb(0,112,32)">:</span> Algebra<span style="color:rgb(0,112,32)">.</span>Core<span style="color:rgb(0,112,32)">.</span>Op₂ <span style="color:rgb(0,112,32)">(</span>Magma<span style="color:rgb(0,112,32)">.</span>Carrier A<span style="color:rgb(0,112,32)">)</span> [ at /Users/conal/Agda/cat-linear/src/T8<span style="color:rgb(0,112,32)">.</span>agda:24,5-7 ]</a>
<a id="gmail-m_-6517219575474230040gmail-cb4-2" title="2" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span style="color:rgb(0,112,32)">_</span>∙-cong<span style="color:rgb(0,112,32)">_</span><span style="color:rgb(64,160,112)">30</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb4-3" title="3" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span style="color:rgb(0,112,32)">:</span> Algebra<span style="color:rgb(0,112,32)">.</span>Definitions<span style="color:rgb(0,112,32)">.</span>Congruent₂ <span style="color:rgb(0,112,32)">(λ</span> z z₁ <span style="color:rgb(0,112,32)">→</span> <span style="color:rgb(0,112,32)">(</span>A Magma<span style="color:rgb(0,112,32)">.</span>≈ z<span style="color:rgb(0,112,32)">)</span> z₁<span style="color:rgb(0,112,32)">)</span></a>
<a id="gmail-m_-6517219575474230040gmail-cb4-4" title="4" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span style="color:rgb(0,112,32)">__</span>∙<span style="color:rgb(0,112,32)">__</span><span style="color:rgb(64,160,112)">27</span> [ at /Users/conal/Agda/cat-linear/src/T8<span style="color:rgb(0,112,32)">.</span>agda:24,5-7 ]</a></code></pre></div><p style="margin-bottom:1em;color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px">If I replace <code style="font-size:16.91px;background:transparent none repeat scroll 0% 0%;border:medium none;overflow:visible;font-family:Menlo,"Lucida Console",Monaco,monospace;white-space:pre-wrap"><span style="color:rgb(144,32,0)">Magma</span></code> by a structure with more operations, such as <code style="font-size:16.91px;background:transparent none repeat scroll 0% 0%;border:medium none;overflow:visible;font-family:Menlo,"Lucida Console",Monaco,monospace;white-space:pre-wrap"><span style="color:rgb(144,32,0)">Ring</span></code>, I see more such errors, failing to infer each operation and associated property.</p><p style="margin-bottom:1em;color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px">I’m stumped and would appreciate any insights about causes and cures for this inference failure.</p><p style="margin-bottom:1em;color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px">– Conal</p></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>