1df4d97 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tweak alternative pruning

Don't remove overloadings where there's a blocked function name in the type, because further information may reveal it's a valid overloading.

commit1df4d970902c8aa338461a714db22f59d79385df authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 15 Apr 2016, 23:25 (11 years ago) parent951b631

1 file changed+3

unifiedsplit

src/Idris/Elab/Term.hs+3

@@ -1640,6 +1640,9 @@ pruneByType env (P _ n _) goalty ist as

16401640 -- Binders are a plausible match, so keep them

16411641 matching (Bind n _ sc) _ = True

16421642 matching _ (Bind n _ sc) = True

1643+ -- If we hit a function name, it's a plausible match

1644+ matching (App _ (P _ f _) _) _ | not (isConName f ctxt) = True

1645+ matching _ (App _ (P _ f _) _) | not (isConName f ctxt) = True

16431646 -- Otherwise, match the rest of the structure

16441647 matching (App _ f a) (App _ f' a') = matching f f' && matching a a'

16451648 matching (TType _) (TType _) = True