@@ -1697,18 +1697,7 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as
16971697 insertImpl ps as
16981698 = let (as', badimpls) = partition (impIn ps) as in
16991699 map addUnknownImp badimpls ++
1700− insImpAcc M.empty ps (filter exp as') (filter (not . exp) as')
1701−
1702− -- return True if the second argument is an implicit argument which is
1703− -- expected in the implicits, or if it's not an implicit
1704− impIn :: [PArg] -> PArg -> Bool
1705− impIn ps (PExp _ _ _ _) = True
1706− impIn ps (PConstraint _ _ _ _) = True
1707− impIn ps arg = any (\p -> pname arg == pname p) ps
1708−
1709− exp (PExp _ _ _ _) = True
1710− exp (PConstraint _ _ _ _) = True
1711− exp _ = False
1700+ insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')
17121701
17131702 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
17141703 -> [PArg] -- parameters
@@ -1752,6 +1741,17 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as
17521741 find n (PTacImplicit _ _ n' _ t : gs) acc
17531742 | n == n' = Just (t, reverse acc ++ gs)
17541743 find n (g : gs) acc = find n gs (g : acc)
1744+
1745+-- return True if the second argument is an implicit argument which is
1746+-- expected in the implicits, or if it's not an implicit
1747+impIn :: [PArg] -> PArg -> Bool
1748+impIn ps (PExp _ _ _ _) = True
1749+impIn ps (PConstraint _ _ _ _) = True
1750+impIn ps arg = any (\p -> not (expArg arg) && pname arg == pname p) ps
1751+
1752+expArg (PExp _ _ _ _) = True
1753+expArg (PConstraint _ _ _ _) = True
1754+expArg _ = False
17551755
17561756-- replace non-linear occurrences with _
17571757
@@ -1838,7 +1838,8 @@ stripUnmatchable i tm = tm
18381838
18391839mkPApp fc a f [] = f
18401840mkPApp fc a f as = let rest = drop a as in
1841− appRest fc (PApp fc f (take a as)) rest
1841+ if a == 0 then appRest fc f rest
1842+ else appRest fc (PApp fc f (take a as)) rest
18421843 where
18431844 appRest fc f [] = f
18441845 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as