on master help sign in
Merge pull request #4732 from ziman/fix-dotted-implicits

Stop ignoring dots for implicits

commit1366f5cab1d9c2da52e188c53a95776db54d3782 authorNiklas Larsson <metaniklas@gmail.com> dateMon 15 Jul 2019, 11:44 (7 years ago) parent611564b813ad24
1 file changed+2−1
src/Idris/AbsSyntax.hs+2−1
src/Idris/AbsSyntax.hs+2−1
@@ -1659,7 +1659,8 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)
16591659 argInfo n (Imp opt _ _ _ _ _) Placeholder
16601660 = (True, PImp 0 True opt n Placeholder)
16611661 argInfo n (Imp opt _ _ _ _ _) t'
1662− = (False, PImp (getPriority i t') True opt n t')
1662+ = (InaccessibleArg `elem` opt,
1663+ PImp (getPriority i t') True opt n t')
16631664 argInfo n (Exp opt _ _ _) t'
16641665 = (InaccessibleArg `elem` opt,
16651666 PExp (getPriority i t') opt n t')