<div dir="ltr">> <span style="font-size:12.8px">I'm surprised that the constraint `_10 x1 x0 = x1` does not lead to the unique solution `_10 := λ x1 x0 → x1`.</span><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">The reason for this is that x0 is not a variable but a postulate. You get the expected solution if you change the code to</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">```agda</span></div><div><div><span style="font-size:12.8px">postulate</span></div><div><span style="font-size:12.8px">  A : Set</span></div><div><span style="font-size:12.8px">  f : (B : A → Set) (x : A) → B x → B x</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">module _ (x0 : A) where</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">  test : (B : A → Set) (x : A) → B x → B x</span></div><div><span style="font-size:12.8px">  test B1 x1 bx1 = f (λ x2 → B1 {!x1!}) x0 bx1</span></div><div style="font-size:12.8px">```</div></div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">The idea for custom solvers would be to let you program them with the reflection machinery. Currently it doesn't let you access unsolved constraints, but that would be a reasonable extension to add.</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Sep 8, 2017 at 12:59 AM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">The below code type-checks if the hole is filled with `x1`. I believe that this is the unique solution (which Agda fails to solve).<br>
<br>
```agda<br>
postulate<br>
  A : Set<br>
  f : (B : A → Set) (x : A) → B x → B x<br>
  x0 : A<br>
<br>
test : (B : A → Set) (x : A) → B x → B x<br>
test B1 x1 bx1 = f (λ x2 → B1 {!x1!}) x0 bx1<br>
```<br>
<br>
`show-constraints` reports:<br>
<br>
    ?0 := _10 x1 x2<br>
    _13 := λ B1 x1 bx1 → f (λ x2 → B1 (_10 x1 x2)) x0 (_12 B1 x1 bx1) [blocked by problem 19]<br>
    [19,20] (_10 x1 x0) = x1 : A<br>
    _11 := λ B1 x1 bx1 → bx1 [blocked by problem 17]<br>
    [17,18] x1 = (_10 x1 x0) : A<br>
<br>
I'm surprised that the constraint `_10 x1 x0 = x1` does not lead to the unique solution `_10 := λ x1 x0 → x1`. Taking a look at the debug output, I gather that Agda's failure to solve has something to do with metas being "frozen" and/or a failure to "prune" (though I don't know what that all means).<br>
<br>
* Am I right that there is a unique solution which Agda is failing to find?<br>
<br>
* I'm guessing that problems like this are the inevitable result of undecidability. Is that right? And so it's not a bug? And so I shouldn't bother reporting such things?<br>
<br>
* Is the constraint-solver written-up somewhere separately from the code? With explanations of "pruning" and "freezing", etc.?<br>
<br>
* Barring a fix, I'm hunting for possible workarounds. The notion of a "custom meta solver" is mentioned in Agda issue #2513. I take it that that refers to a possible enhancement somewhere down the road for Agda. Roughly speaking, how would that work? Would that allow an Agda programmer to "hook-in" to the built-in solver and then nudge it towards finding the unique solution to the above? Or is the idea instead to allow only for solvers that are implemented completely separately from the existing machinery?<br>
<br>
______________________________<wbr>_________________<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/mail<wbr>man/listinfo/agda</a><br>
</blockquote></div><br></div>