Unification in Idris

[Adam Gundry]

Hi Edwin, folks,

How does Idris handle unification? Am I right in thinking (from the
draft paper about the implementation) that it doesn't suspend
constraints, but instead tries various orders for elaboration and fails
if none of them work?

(I'm writing a paper about higher-order pattern unification for
dependent type theory, hence the question.)

Thanks,

Adam