<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 class="gmail-sourceCode" id="gmail-cb3" style="overflow:auto;margin:1em 0px;color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px"><pre class="gmail-sourceCode gmail-agda" 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)"><code class="gmail-sourceCode gmail-agda" style="font-size:16.91px;background:transparent;border:none;overflow:visible;font-family:Menlo,"Lucida Console",Monaco,monospace;display:block;padding:0em"><a class="gmail-sourceLine" id="gmail-cb3-1" title="1" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">open</span> <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">import</span> Level</a>
<a class="gmail-sourceLine" id="gmail-cb3-2" title="2" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">open</span> <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">import</span> Algebra<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>Bundles <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">using</span> <span class="gmail-ot" style="color:rgb(0,112,32)">(</span>Magma<span class="gmail-ot" style="color:rgb(0,112,32)">)</span></a>
<a class="gmail-sourceLine" id="gmail-cb3-3" title="3" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">open</span> <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">import</span> Relation<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>Binary <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">using</span> <span class="gmail-ot" style="color:rgb(0,112,32)">(</span>Rel<span class="gmail-ot" style="color:rgb(0,112,32)">)</span></a>
<a class="gmail-sourceLine" id="gmail-cb3-4" title="4" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">open</span> <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">import</span> Function<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>Equality <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">using</span> <span class="gmail-ot" style="color:rgb(0,112,32)">(_</span>⟶<span class="gmail-ot" style="color:rgb(0,112,32)">_)</span> <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">renaming</span> <span class="gmail-ot" style="color:rgb(0,112,32)">(</span>id <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">to</span> ⟶-id<span class="gmail-ot" style="color:rgb(0,112,32)">)</span></a>
<a class="gmail-sourceLine" id="gmail-cb3-5" title="5" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit;height:1.2em"></a>
<a class="gmail-sourceLine" id="gmail-cb3-6" title="6" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">record</span> Cat <span class="gmail-ot" style="color:rgb(0,112,32)">(</span>o ℓ <span class="gmail-ot" style="color:rgb(0,112,32)">:</span> Level<span class="gmail-ot" style="color:rgb(0,112,32)">)</span> <span class="gmail-ot" style="color:rgb(0,112,32)">:</span> <span class="gmail-dt" style="color:rgb(144,32,0)">Set</span> <span class="gmail-ot" style="color:rgb(0,112,32)">(</span>suc <span class="gmail-ot" style="color:rgb(0,112,32)">(</span>o ⊔ ℓ<span class="gmail-ot" style="color:rgb(0,112,32)">))</span> <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">where</span></a>
<a class="gmail-sourceLine" id="gmail-cb3-7" title="7" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">infix</span> <span class="gmail-dv" style="color:rgb(64,160,112)">4</span> <span class="gmail-ot" style="color:rgb(0,112,32)">_</span>⇒<span class="gmail-ot" style="color:rgb(0,112,32)">_</span></a>
<a class="gmail-sourceLine" id="gmail-cb3-8" title="8" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">field</span></a>
<a class="gmail-sourceLine" id="gmail-cb3-9" title="9" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> Obj <span class="gmail-ot" style="color:rgb(0,112,32)">:</span> <span class="gmail-dt" style="color:rgb(144,32,0)">Set</span> o</a>
<a class="gmail-sourceLine" id="gmail-cb3-10" title="10" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span class="gmail-ot" style="color:rgb(0,112,32)">_</span>⇒<span class="gmail-ot" style="color:rgb(0,112,32)">_</span> <span class="gmail-ot" style="color:rgb(0,112,32)">:</span> Rel Obj ℓ</a>
<a class="gmail-sourceLine" id="gmail-cb3-11" title="11" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> id <span class="gmail-ot" style="color:rgb(0,112,32)">:</span> <span class="gmail-ot" style="color:rgb(0,112,32)">∀</span> <span class="gmail-ot" style="color:rgb(0,112,32)">{</span>A<span class="gmail-ot" style="color:rgb(0,112,32)">}</span> <span class="gmail-ot" style="color:rgb(0,112,32)">→</span> A ⇒ A</a>
<a class="gmail-sourceLine" id="gmail-cb3-12" title="12" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span class="gmail-co" style="color:rgb(96,160,176);font-style:italic">-- ... elided</span></a>
<a class="gmail-sourceLine" id="gmail-cb3-13" title="13" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit;height:1.2em"></a>
<a class="gmail-sourceLine" id="gmail-cb3-14" title="14" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit">M <span class="gmail-ot" style="color:rgb(0,112,32)">:</span> Cat <span class="gmail-ot" style="color:rgb(0,112,32)">_</span> <span class="gmail-ot" style="color:rgb(0,112,32)">_</span></a>
<a class="gmail-sourceLine" id="gmail-cb3-15" title="15" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit">M <span class="gmail-ot" style="color:rgb(0,112,32)">=</span> <span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">record</span> <span class="gmail-ot" style="color:rgb(0,112,32)">{</span> Obj <span class="gmail-ot" style="color:rgb(0,112,32)">=</span> Magma 0ℓ 0ℓ</a>
<a class="gmail-sourceLine" id="gmail-cb3-16" title="16" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span class="gmail-ot" style="color:rgb(0,112,32)">;</span> <span class="gmail-ot" style="color:rgb(0,112,32)">_</span>⇒<span class="gmail-ot" style="color:rgb(0,112,32)">_</span> <span class="gmail-ot" style="color:rgb(0,112,32)">=</span> <span class="gmail-ot" style="color:rgb(0,112,32)">λ</span> A B <span class="gmail-ot" style="color:rgb(0,112,32)">→</span> Magma<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>setoid A ⟶ Magma<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>setoid B</a>
<a class="gmail-sourceLine" id="gmail-cb3-17" title="17" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span class="gmail-ot" style="color:rgb(0,112,32)">;</span> id <span class="gmail-ot" style="color:rgb(0,112,32)">=</span> ⟶-id</a>
<a class="gmail-sourceLine" id="gmail-cb3-18" title="18" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span class="gmail-co" style="color:rgb(96,160,176);font-style:italic">-- ...</span></a>
<a class="gmail-sourceLine" id="gmail-cb3-19" title="19" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span class="gmail-ot" style="color:rgb(0,112,32)">}</span> </a>
<a class="gmail-sourceLine" id="gmail-cb3-20" title="20" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit;height:1.2em"></a>
<a class="gmail-sourceLine" id="gmail-cb3-21" title="21" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span class="gmail-kw" style="color:rgb(0,112,32);font-weight:bold">open</span> Cat M</a>
<a class="gmail-sourceLine" id="gmail-cb3-22" title="22" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit;height:1.2em"></a>
<a class="gmail-sourceLine" id="gmail-cb3-23" title="23" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span class="gmail-ot" style="color:rgb(0,112,32)">_</span> <span class="gmail-ot" style="color:rgb(0,112,32)">:</span> <span class="gmail-ot" style="color:rgb(0,112,32)">∀</span> <span class="gmail-ot" style="color:rgb(0,112,32)">{</span>A <span class="gmail-ot" style="color:rgb(0,112,32)">:</span> Magma 0ℓ 0ℓ<span class="gmail-ot" style="color:rgb(0,112,32)">}</span> <span class="gmail-ot" style="color:rgb(0,112,32)">→</span> A ⇒ A</a>
<a class="gmail-sourceLine" id="gmail-cb3-24" title="24" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span class="gmail-ot" style="color:rgb(0,112,32)">_</span> <span class="gmail-ot" 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 class="gmail-sourceCode gmail-haskell" style="font-size:16.91px;background:transparent;border:none;overflow:visible;font-family:Menlo,"Lucida Console",Monaco,monospace;white-space:pre"><span class="gmail-fu" style="color:rgb(6,40,126)">id</span></code> in the last line):</p><div class="gmail-sourceCode" id="gmail-cb4" style="overflow:auto;margin:1em 0px;color:rgb(0,0,0);font-family:sans-serif;font-size:17.8px"><pre class="gmail-sourceCode gmail-agda" 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)"><code class="gmail-sourceCode gmail-agda" style="font-size:16.91px;background:transparent;border:none;overflow:visible;font-family:Menlo,"Lucida Console",Monaco,monospace;display:block;padding:0em"><a class="gmail-sourceLine" id="gmail-cb4-1" title="1" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span class="gmail-ot" style="color:rgb(0,112,32)">__</span>∙<span class="gmail-ot" style="color:rgb(0,112,32)">__</span><span class="gmail-dv" style="color:rgb(64,160,112)">27</span> <span class="gmail-ot" style="color:rgb(0,112,32)">:</span> Algebra<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>Core<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>Op₂ <span class="gmail-ot" style="color:rgb(0,112,32)">(</span>Magma<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>Carrier A<span class="gmail-ot" style="color:rgb(0,112,32)">)</span> [ at /Users/conal/Agda/cat-linear/src/T8<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>agda:24,5-7 ]</a>
<a class="gmail-sourceLine" id="gmail-cb4-2" title="2" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"><span class="gmail-ot" style="color:rgb(0,112,32)">_</span>∙-cong<span class="gmail-ot" style="color:rgb(0,112,32)">_</span><span class="gmail-dv" style="color:rgb(64,160,112)">30</span></a>
<a class="gmail-sourceLine" id="gmail-cb4-3" title="3" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span class="gmail-ot" style="color:rgb(0,112,32)">:</span> Algebra<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>Definitions<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>Congruent₂ <span class="gmail-ot" style="color:rgb(0,112,32)">(λ</span> z z₁ <span class="gmail-ot" style="color:rgb(0,112,32)">→</span> <span class="gmail-ot" style="color:rgb(0,112,32)">(</span>A Magma<span class="gmail-ot" style="color:rgb(0,112,32)">.</span>≈ z<span class="gmail-ot" style="color:rgb(0,112,32)">)</span> z₁<span class="gmail-ot" style="color:rgb(0,112,32)">)</span></a>
<a class="gmail-sourceLine" id="gmail-cb4-4" title="4" style="display:inline-block;line-height:1.25;color:inherit;text-decoration:inherit"> <span class="gmail-ot" style="color:rgb(0,112,32)">__</span>∙<span class="gmail-ot" style="color:rgb(0,112,32)">__</span><span class="gmail-dv" style="color:rgb(64,160,112)">27</span> [ at /Users/conal/Agda/cat-linear/src/T8<span class="gmail-ot" 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 class="gmail-sourceCode gmail-haskell" style="font-size:16.91px;background:transparent;border:none;overflow:visible;font-family:Menlo,"Lucida Console",Monaco,monospace;white-space:pre"><span class="gmail-dt" style="color:rgb(144,32,0)">Magma</span></code> by a structure with more operations, such as <code class="gmail-sourceCode gmail-haskell" style="font-size:16.91px;background:transparent;border:none;overflow:visible;font-family:Menlo,"Lucida Console",Monaco,monospace;white-space:pre"><span class="gmail-dt" 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>