@@ -621,7 +621,8 @@ implicit' syn ignore n ptm
621implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
621implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
622implicitise syn ignore ist tm
622implicitise syn ignore ist tm
623 = let (declimps, ns') = execState (imps True [] tm) ([], [])
623 = let (declimps, ns') = execState (imps True [] tm) ([], [])
624+ ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
624− ns = ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
625+ ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
625 if null ns
626 if null ns
626 then (tm, reverse declimps)
627 then (tm, reverse declimps)
627 else implicitise syn ignore ist (pibind uvars ns tm)
628 else implicitise syn ignore ist (pibind uvars ns tm)
@@ -700,7 +701,10 @@ implicitise syn ignore ist tm
700 pibind using (n:ns) sc
701 pibind using (n:ns) sc
701 = case lookup n using of
702 = case lookup n using of
702 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
703 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)
704+ Nothing -> if (implicitable n)
703− Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc)
705+ then PPi (Imp False Dynamic) n Placeholder
706+ (pibind using ns sc)
707+ else pibind using ns sc
705-- Add implicit arguments in function calls
709-- Add implicit arguments in function calls
706addImplPat :: IState -> PTerm -> PTerm
710addImplPat :: IState -> PTerm -> PTerm