@@ -85,7 +85,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
8585 ty' <- implicit info syn n ty'
8686
8787 let ty = addImpl i ty'
88− inacc = inaccessible 0 ty
88+ inacc = inaccessibleArgs 0 ty
8989 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
9090 logLvl 5 $ "Inaccessible arguments: " ++ show inacc
9191
@@ -166,29 +166,6 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
166166 lst = txt "List"
167167 errrep = txt "ErrorReportPart"
168168
169− saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()
170− saveInaccArgs n is = do
171− ist <- getIState
172− case lookupCtxt n (idris_optimisation ist) of
173− [oi] -> do
174− putIState ist{ idris_optimisation =
175− addDef n oi{ inaccessible = is } (idris_optimisation ist) }
176−
177− _ -> do
178− putIState ist{ idris_optimisation =
179− addDef n (Optimise False False [] [] is) (idris_optimisation ist) }
180− addIBC (IBCOpt n)
181−
182− inaccessible :: Int -> PTerm -> [(Int, Name)]
183− inaccessible i (PPi (Imp _ _ _ _) n Placeholder t)
184− = (i,n) : inaccessible (i+1) t -- unbound implicit
185− inaccessible i (PPi plicity n ty t)
186− | InaccessibleArg `elem` pargopts plicity
187− = (i,n) : inaccessible (i+1) t -- an .{erased : Implicit}
188− | otherwise
189− = inaccessible (i+1) t -- a {regular : Implicit}
190− inaccessible _ _ = []
191−
192169 tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))
193170 (App (P _ (NS (UN m) ns2) _)
194171 (App (P _ (NS (UN l) ns3) _)
@@ -200,6 +177,30 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
200177 , ns4 == map txt ["Errors","Reflection","Language"] = True
201178 tyIsHandler _ = False
202179
180+-- Store the list of inaccessible arguments in the internal state.
181+saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()
182+saveInaccArgs n is = do
183+ ist <- getIState
184+ case lookupCtxt n (idris_optimisation ist) of
185+ [oi] -> do
186+ putIState ist{ idris_optimisation =
187+ addDef n oi{ inaccessible = is } (idris_optimisation ist) }
188+
189+ _ -> do
190+ putIState ist{ idris_optimisation =
191+ addDef n (Optimise False False [] [] is) (idris_optimisation ist) }
192+ addIBC (IBCOpt n)
193+
194+-- Get the list of (index, name) of inaccessible arguments from the type.
195+inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
196+inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)
197+ = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
198+inaccessibleArgs i (PPi plicity n ty t)
199+ | InaccessibleArg `elem` pargopts plicity
200+ = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}
201+ | otherwise
202+ = inaccessibleArgs (i+1) t -- a {regular : Implicit}
203+inaccessibleArgs _ _ = []
203204
204205elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
205206 FC -> FnOpts -> Name -> PTerm -> Idris ()
@@ -891,6 +892,8 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
891892 t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)
892893 let t = addImpl i t_in
893894 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
895+ let inacc = inaccessibleArgs 0 t
896+ logLvl 5 $ "Inaccessible args: " ++ show inacc
894897 ((t', defer, is), log) <-
895898 tclift $ elaborate ctxt n (TType (UVal 0)) []
896899 (errAt "constructor " n (erun fc (build i info False [] n t)))
@@ -908,6 +911,8 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
908911 checkDocs fc argDocs t_in
909912 addDocStr n doc argDocs
910913 addIBC (IBCDoc n)
914+ saveInaccArgs n inacc
915+ addIBC (IBCOpt n)
911916 let fs = map (getNamePos 0 t) forcenames
912917 -- FIXME: 'forcenames' is an almighty hack! Need a better way of
913918 -- erasing non-forceable things