@@ -44,6 +44,7 @@ import Idris.Core.Evaluate
45import Control.Applicative
45import Control.Applicative
46import Control.Monad
46import Control.Monad
47+import Control.Monad.Error (throwError, catchError)
47import Control.Monad.State.Strict
48import Control.Monad.State.Strict
49import Data.Maybe
50import Data.Maybe
@@ -867,8 +868,13 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st
867 ty <- iName []
868 ty <- iName []
868 ns <- sepBy1 name (lchar ',')
869 ns <- sepBy1 name (lchar ',')
869 return [PDirective
870 return [PDirective
872+ ty' <- case lookupCtxtName ty (idris_implicits i) of
873+ [(tyn, _)] -> return tyn
874+ [] -> throwError (NoSuchVariable ty)
875+ tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
870− (do mapM_ (addNameHint ty) ns
876+ mapM_ (addNameHint ty') ns
871− mapM_ (\n -> addIBC (IBCNameHint (ty, n))) ns)]
877+ mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
872 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
878 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
873 return [PDirective (addLangExt ext)]
879 return [PDirective (addLangExt ext)]
874 <?> "directive"
880 <?> "directive"