@@ -44,6 +44,7 @@ import Idris.Core.Evaluate
4444
4545import Control.Applicative
4646import Control.Monad
47+import Control.Monad.Error (throwError, catchError)
4748import Control.Monad.State.Strict
4849
4950import Data.Maybe
@@ -867,8 +868,13 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st
867868 ty <- iName []
868869 ns <- sepBy1 name (lchar ',')
869870 return [PDirective
870− (do mapM_ (addNameHint ty) ns
871− mapM_ (\n -> addIBC (IBCNameHint (ty, n))) ns)]
871+ (do i <- getIState
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)))
876+ mapM_ (addNameHint ty') ns
877+ mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
872878 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
873879 return [PDirective (addLangExt ext)]
874880 <?> "directive"