In the past I've struggled to navigate the research around inferring 'missing stuff' when elaborating dependently typed languages. This thread by would have been helpful back then for understand what they were all talking about wrt. "higher order unification", etc!
Quote Tweet
pattern unification works by carefully constructing a diff between two types with holes for the information missing on either side, and then rifling madly through the context to see what you’ve got lying around that it can cram into the holes, possibly by turning or hitting them.
Show this thread
2
1
12
