@@ -1536,18 +1536,15 @@ implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
15361536implicit' info syn ignore n ptm
15371537 = do i <- getIState
15381538 auto <- getAutoImpls
1539− if not auto
1540− then return ptm
1541− else do
1542− let (tm', impdata) = implicitise syn ignore i ptm
1543− defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1544− -- let (tm'', spos) = findStatics i tm'
1545− putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1546− addIBC (IBCImp n)
1547− logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1548− -- i <- get
1549− -- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1550− return tm'
1539+ let (tm', impdata) = implicitise auto syn ignore i ptm
1540+ defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1541+-- let (tm'', spos) = findStatics i tm'
1542+ putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1543+ addIBC (IBCImp n)
1544+ logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1545+-- i <- get
1546+-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1547+ return tm'
15511548 where
15521549 -- Detect unknown names in default arguments and throw error if found.
15531550 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
@@ -1566,15 +1563,17 @@ implicit' info syn ignore n ptm
15661563 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
15671564 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
15681565
1569−implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1570−implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1566+-- Even if auto_implicits is off, we need to call this so we record which
1567+-- arguments are implicit
1568+implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1569+implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
15711570 let (declimps, ns') = execState (imps True [] tm) ([], [])
1572− ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1571+ ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
15731572 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
15741573 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
15751574 if null ns
15761575 then (tm, reverse declimps)
1577− else implicitise syn ignore ist (pibind uvars nsOrder tm)
1576+ else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
15781577 where
15791578 uvars = map ipair (filter uimplicit (using syn))
15801579 pvars = syn_params syn