@@ -1118,12 +1118,25 @@ implicitise syn ist tm
11181118 Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
11191119
11201120-- Add implicit arguments in function calls
1121+addImplPat :: IState -> PTerm -> PTerm
1122+addImplPat = addImpl' True []
1123+
1124+addImplBound :: IState -> [Name] -> PTerm -> PTerm
1125+addImplBound ist ns = addImpl' False ns ist
11211126
11221127addImpl :: IState -> PTerm -> PTerm
1123−addImpl ist ptm = ai [] ptm
1128+addImpl = addImpl' False []
1129+
1130+-- TODO: in patterns, don't add implicits to function names guarded by constructors
1131+-- and *not* inside a PHidden
1132+
1133+addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
1134+addImpl' inpat env ist ptm = ai env ptm
11241135 where
11251136 ai env (PRef fc f)
1126− | not (f `elem` env) = aiFn ist fc f []
1137+ | not (f `elem` env) = aiFn inpat ist fc f []
1138+ ai env (PHidden (PRef fc f))
1139+ | not (f `elem` env) = aiFn False ist fc f []
11271140 ai env (PEq fc l r) = let l' = ai env l
11281141 r' = ai env r in
11291142 PEq fc l' r'
@@ -1142,7 +1155,7 @@ addImpl ist ptm = ai [] ptm
11421155 ai env (PApp fc (PRef _ f) as)
11431156 | not (f `elem` env)
11441157 = let as' = map (fmap (ai env)) as in
1145− aiFn ist fc f as'
1158+ aiFn False ist fc f as'
11461159 ai env (PApp fc f as) = let f' = ai env f
11471160 as' = map (fmap (ai env)) as in
11481161 mkPApp fc 1 f' as'
@@ -1165,10 +1178,21 @@ addImpl ist ptm = ai [] ptm
11651178 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
11661179 ai env tm = tm
11671180
1168−aiFn :: IState -> FC -> Name -> [PArg] -> PTerm
1169−aiFn ist fc f as
1181+-- if in a pattern, and there are no arguments, and there's no possible
1182+-- names with zero explicit arguments, don't add implicits.
1183+
1184+aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> PTerm
1185+aiFn True ist fc f []
1186+ = case lookupCtxt Nothing f (idris_implicits ist) of
1187+ [] -> PRef fc f
1188+ alts -> if (any (all imp) alts)
1189+ then aiFn False ist fc f [] -- use it as a constructor
1190+ else PRef fc f
1191+ where imp (PExp _ _ _) = False
1192+ imp _ = True
1193+aiFn inpat ist fc f as
11701194 | f `elem` primNames = PApp fc (PRef fc f) as
1171−aiFn ist fc f as
1195+aiFn inpat ist fc f as
11721196 -- This is where namespaces get resolved by adding PAlternative
11731197 = case lookupCtxtName Nothing f (idris_implicits ist) of
11741198 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)