git.iko.soy/Idris-dev
on c614366 help sign in
history ofsrc/Core/Unify.hs
all commits
c55f8c2Unification fix to avoid giving up on recoverable errorsEdwin Brady c710867Better unification errors when name is out of scope In particular, a unification problem which cannot be solved because it uses a variable not in scope where the metavariable is bound. Fixes #342Edwin Brady 02367f9Unification fix If f x = g y fails to unify due to f and g failing to unify, record the whole application as failed, otherwise we might accidentally unify x and y. Fixes #409Edwin Brady fa80591Fix let scope leakage bugEdwin Brady ce7e45bEXPERIMENTAL: Syntax for applying functions by expected type "t <== f" applies a function f to arguments in such a way that it returns something of type t. The <== is a placeholder syntax until someone comes up with something better. (Alternative: t by f, but that uses up a new keyword)Edwin Brady c7fded1Added 'mrefine' tactic Like refine, but uses matching instead of unification to resolve implicit arguments. All will become clear, I hope :). This is intended for an additional style of pattern matching (on types) for better explanation of proofs.Edwin Brady 7bfa10cSome unification fixesEdwin Brady 99a8a66Check that explicitly given implicit args unify with inferred versions Also exposed a unification bug which unified things which shouldn't be: f x = f y does not imply x = y unless f is injective, and this was not properly checked.Edwin Brady 93819edUnification fixEdwin Brady 1a87674Improved type-directed name disambiguationEdwin Brady 8b96fc7Fix another unification problem (solving things which shouldn't be)Edwin Brady 2686158Be more careful when unifying metavariable applications Otherwise things get solved which shouldn't be. Fixes issue #227Edwin Brady e5706d3HNF in unification to speed things upEdwin Brady 67de7f7Add a reducing version of believe_me (be careful!)Edwin Brady 8f76315Changed approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration.Edwin Brady 187f42fUndo unification changes... because it's broken...Edwin Brady 6be4eb2Fix compile errorEdwin Brady 265d9a4Improve elaboration efficiency by cutting down on excessive backtrackingEdwin Brady 7a66adcMake unification faster by computing HNF rather than normalisingEdwin Brady 1677c30Better dealing with name shadowing while building instances ...and while type checking completed termsEdwin Brady 56223efDon't normalise everywhere!Edwin Brady f9678b7Remove priority ordering on function arguments Should no longer be necessary since unification is improved, and causes problems when it guesses wrong.Edwin Brady fad1c1cWarn when generating a setter for a record fails ...rather than failing (since it may just not work for dependent records)Edwin Brady 6f54612Fix unification error that led to some trivial things not checkingEdwin Brady 3c641aeAdded --dumpdefuns flagEdwin Brady b894841Improve some error messagesEdwin Brady 72d4d96Starting unused argument analysisEdwin Brady 611dd97Improve speed of type checking by spotting unification failure quickerEdwin Brady 0de6d2dFix resource language, add extra test for itEdwin Brady 16027ddFix with parsing bugEdwin Brady 23ab26fSpeed improvements when code contains type errors Identify "unrecoverable" unification failures so that type checking doesn't continue to search all the alternative overloadings and orderings.Edwin Brady 6b46ffcNew RTS almost ready, but for garbage collection problemEdwin Brady 6cb70bcFix for simple function applicationsEdwin Brady e1c7b0fAdd "--errorcontext" flag, and :set and :unset in the REPL. :set errorcontext will cause unification errors to also dump the current context.Edwin Brady 392c225Check definitions structurally as well as by name in conversionEdwin Brady 33bf2bdUnification tweakEdwin Brady d1d672eCollect all unification errors instead of immediately reporting failureEdwin Brady 38732d8Heuristic for picking best error message when overloaded alternatives all failEdwin Brady 79aae2fUnification tweak - try a different order on failureEdwin Brady 1823cf9Postpone injectivity check until after unificationEdwin Brady 6cc3c32Fix small elaboration bugEdwin Brady 6757c47Added case analysis on types, but only when enabled with --typecase (since it breaks parametricity)Edwin Brady 2c4ff83Change unification in function applicationsEdwin Brady 070b0faSome unification/evaluation bug fixesEdwin Brady f9fb363Tinkering with error reportingEdwin Brady 019fabaFixed unification; added well-typed interpreterEdwin Brady 739e0b5Some error handlingEdwin Brady ff5f762Rename Core to TTEdwin Brady 0ae24f1Shift core TT into a separate directory (for ease of reuse)Edwin Brady