on master help sign in
Stop ignoring dots for implicits.
813ad24Matus Tejiscak
src/Idris/AbsSyntax.hs+2−1
@@ -1659,7 +1659,8 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)
1659 argInfo n (Imp opt _ _ _ _ _) Placeholder
1659 argInfo n (Imp opt _ _ _ _ _) Placeholder
1660 = (True, PImp 0 True opt n Placeholder)
1660 = (True, PImp 0 True opt n Placeholder)
1661 argInfo n (Imp opt _ _ _ _ _) t'
1661 argInfo n (Imp opt _ _ _ _ _) t'
1662+ = (InaccessibleArg `elem` opt,
1662− = (False, PImp (getPriority i t') True opt n t')
1663+ PImp (getPriority i t') True opt n t')
1663 argInfo n (Exp opt _ _ _) t'
1664 argInfo n (Exp opt _ _ _) t'
1664 = (InaccessibleArg `elem` opt,
1665 = (InaccessibleArg `elem` opt,
1665 PExp (getPriority i t') opt n t')
1666 PExp (getPriority i t') opt n t')