@@ -853,8 +853,10 @@ elab ist info emode opts fn tm
853 ctxt <- get_context
853 ctxt <- get_context
854 let dataCon = isDConName f ctxt
854 let dataCon = isDConName f ctxt
855 annot <- findHighlight f
855 annot <- findHighlight f
856− mapM_ checkKnownImplicit args_in
856+ knowns_m <- mapM getKnownImplicit args_in
857+ let knowns = mapMaybe id knowns_m
857− let args = insertScopedImps fc (normalise ctxt env fty) args_in
858+ args <- insertScopedImps fc f knowns (normalise ctxt env fty) args_in
858 let unmatchableArgs = if pattern
860 let unmatchableArgs = if pattern
859 then getUnmatchable (tt_ctxt ist) f
861 then getUnmatchable (tt_ctxt ist) f
@@ -959,10 +961,10 @@ elab ist info emode opts fn tm
959 es -> do put s
961 es -> do put s
960 elab' ina topfc (PAppImpl tm es)
962 elab' ina topfc (PAppImpl tm es)
962− checkKnownImplicit imp
964+ getKnownImplicit imp
963 | UnknownImp `elem` argopts imp
965 | UnknownImp `elem` argopts imp
964− = lift $ tfail $ UnknownImplicit (pname imp) f
966+ = return Nothing -- lift $ tfail $ UnknownImplicit (pname imp) f
965− checkKnownImplicit _ = return ()
967+ | otherwise = return (Just (pname imp))
967 getReqImps (Bind x (Pi _ (Just i) ty _) sc)
969 getReqImps (Bind x (Pi _ (Just i) ty _) sc)
968 = i : getReqImps sc
970 = i : getReqImps sc
@@ -1519,17 +1521,29 @@ elab ist info emode opts fn tm
1519 findImplicit n (x : xs) = let (arg, rest) = findImplicit n xs in
1521 findImplicit n (x : xs) = let (arg, rest) = findImplicit n xs in
1520 (arg, x : rest)
1522 (arg, x : rest)
1524+ insertScopedImps :: FC -> Name -> [Name] -> Type -> [PArg] -> ElabD [PArg]
1525+ insertScopedImps fc f knowns ty xs =
1526+ do mapM_ (checkKnownImplicit (map fst (getArgTys ty) ++ knowns)) xs
1522− insertScopedImps fc ty@(Bind n (Pi _ im@(Just i) _ _) sc) xs
1529+ doInsert ty@(Bind n (Pi _ im@(Just i) _ _) sc) xs
1523− | (Just arg, xs') <- findImplicit n xs,
1530+ | (Just arg, xs') <- findImplicit n xs,
1524− not (toplevel_imp i)
1531+ not (toplevel_imp i)
1525− = arg : insertScopedImps fc sc xs'
1532+ = liftM (arg :) (doInsert sc xs')
1526− | tcimplementation i && not (toplevel_imp i)
1533+ | tcimplementation i && not (toplevel_imp i)
1527− = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
1534+ = liftM (pimp n (PResolveTC fc) True :) (doInsert sc xs)
1528− | not (toplevel_imp i)
1535+ | not (toplevel_imp i)
1529− = pimp n Placeholder True : insertScopedImps fc sc xs
1536+ = liftM (pimp n Placeholder True :) (doInsert sc xs)
1530− insertScopedImps fc (Bind n (Pi _ _ _ _) sc) (x : xs)
1537+ doInsert (Bind n (Pi _ _ _ _) sc) (x : xs)
1531− = x : insertScopedImps fc sc xs
1538+ = liftM (x :) (doInsert sc xs)
1532− insertScopedImps _ ty xs = xs
1539+ doInsert ty xs = return xs
1541+ -- Any implicit in the application needs to have the name of a
1542+ -- scoped implicit or a top level implicit, otherwise report an error
1543+ checkKnownImplicit ns imp@(PImp{})
1544+ | pname imp `elem` ns = return ()
1545+ | otherwise = lift $ tfail $ At fc $ UnknownImplicit (pname imp) f
1546+ checkKnownImplicit ns _ = return ()
1534 insertImpLam ina t =
1548 insertImpLam ina t =
1535 do ty <- goal
1549 do ty <- goal
@@ -1570,7 +1584,7 @@ elab ist info emode opts fn tm
1570 do fty <- get_type (Var n) -- check for implicits
1584 do fty <- get_type (Var n) -- check for implicits
1571 ctxt <- get_context
1585 ctxt <- get_context
1572 env <- get_env
1586 env <- get_env
1573− let a' = insertScopedImps fc (normalise ctxt env fty) []
1587+ a' <- insertScopedImps fc n [] (normalise ctxt env fty) []
1574 if null a'
1588 if null a'
1575 then erun fc $
1589 then erun fc $
1576 do apply (Var n) []
1590 do apply (Var n) []