@@ -1250,18 +1250,24 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1250 | otherwise = x : dropAll xs ys
1250 | otherwise = x : dropAll xs ys
1251 dropAll [] ys = []
1251 dropAll [] ys = []
1253+ -- Find names in argument position in a type, suitable for implicit
1255+ -- Not the function position, but do everything else...
1256+ implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1257+ implNamesIn uv t = namesIn uv ist t
1253 imps top env (PApp _ f as)
1259 imps top env (PApp _ f as)
1254 = do (decls, ns) <- get
1260 = do (decls, ns) <- get
1255 let isn = concatMap (namesIn uvars ist) (map getTm as)
1261 let isn = concatMap (namesIn uvars ist) (map getTm as)
1256 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1262 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1257 imps top env (PPi (Imp l _ _) n ty sc)
1263 imps top env (PPi (Imp l _ _) n ty sc)
1258− = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1264+ = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1259 (decls , ns) <- get
1265 (decls , ns) <- get
1260 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1266 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1261 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1267 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1262 imps True (n:env) sc
1268 imps True (n:env) sc
1263 imps top env (PPi (Exp l _ _) n ty sc)
1269 imps top env (PPi (Exp l _ _) n ty sc)
1264− = do let isn = nub (namesIn uvars ist ty ++ case sc of
1270+ = do let isn = nub (implNamesIn uvars ty ++ case sc of
1265 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1271 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1266 _ -> [])
1272 _ -> [])
1267 (decls, ns) <- get -- ignore decls in HO types
1273 (decls, ns) <- get -- ignore decls in HO types
@@ -1269,7 +1275,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1269 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1275 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1270 imps True (n:env) sc
1276 imps True (n:env) sc
1271 imps top env (PPi (Constraint l _) n ty sc)
1277 imps top env (PPi (Constraint l _) n ty sc)
1272− = do let isn = nub (namesIn uvars ist ty ++ case sc of
1278+ = do let isn = nub (implNamesIn uvars ty ++ case sc of
1273 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1279 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1274 _ -> [])
1280 _ -> [])
1275 (decls, ns) <- get -- ignore decls in HO types
1281 (decls, ns) <- get -- ignore decls in HO types
@@ -1277,7 +1283,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1277 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1283 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1278 imps True (n:env) sc
1284 imps True (n:env) sc
1279 imps top env (PPi (TacImp l _ scr) n ty sc)
1285 imps top env (PPi (TacImp l _ scr) n ty sc)
1280− = do let isn = nub (namesIn uvars ist ty ++ case sc of
1286+ = do let isn = nub (implNamesIn uvars ty ++ case sc of
1281 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1287 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1282 _ -> [])
1288 _ -> [])
1283 (decls, ns) <- get -- ignore decls in HO types
1289 (decls, ns) <- get -- ignore decls in HO types