@@ -1375,9 +1375,12 @@ findInstances :: IState -> Term -> [Name]
1375findInstances ist t
1375findInstances ist t
1376 | (P _ n _, _) <- unApply t
1376 | (P _ n _, _) <- unApply t
1377 = case lookupCtxt n (idris_classes ist) of
1377 = case lookupCtxt n (idris_classes ist) of
1378− [CI _ _ _ _ _ ins _] -> ins
1378+ [CI _ _ _ _ _ ins _] -> filter accessible ins
1380 | otherwise = []
1380 | otherwise = []
1381+ where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of
1382+ Just (_, Hidden) -> False
1382-- Try again to solve auto implicits
1385-- Try again to solve auto implicits
1383solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()
1386solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()