git.iko.soy/Idris-dev
on master help sign in
Insert _ for implicit methods

There is no obvious reason for inserting the argument names explicitly, and everything still works if we don't. I suspect this was to work around an old bug in unificiation, but it turns out to cause problems for interesting dependent interfaces. Fixes #2989

commitcda5443c0163df17ee63930c4aeee251ce779a99 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 27 Feb 2016, 10:18 (11 years ago) parent6520891
1 file changed+3−3
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+3−3
src/Idris/AbsSyntax.hs+3−3
@@ -1902,9 +1902,9 @@ aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
19021902 case find n imps [] of
19031903 Just (tm, imps') ->
19041904 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1905− Nothing -> let ph = if f `elem` imp_meths then PRef fc [] n else Placeholder in
1906− PImp p True l n ph :
1907− insImpAcc (M.insert n ph pnas) ps given imps
1905+ Nothing ->
1906+ PImp p True l n Placeholder :
1907+ insImpAcc (M.insert n Placeholder pnas) ps given imps
19081908 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
19091909 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
19101910 case find n imps [] of