<div dir="ltr"><div><div>I am trying to simplify my code by using instance arguments and thus letting agda fill them.<br><br></div>I am wondering why Agda does not allow to pick variables that are not instance tagged as solutions if there is a unique such solution in the context.<br><br></div>A similar feature is the 'auto' in Idris. In this case, auto specifies which implicit arguments to automatically fill , with anything found in the context.<br></div>