@@ -698,13 +698,18 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where
698698 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
699699 runT (Exact tm) = do elab ist toplevel False tm
700700 when autoSolve solveAll
701− runT (Refine fn []) = do let imps = case lookupCtxt fn (idris_implicits ist) of
702− Nothing -> []
703− Just args -> map isImp args
701+ runT (Refine fn []) = do imps <- case lookupCtxt fn (idris_implicits ist) of
702+ Nothing -> envArgs fn
703+ Just args -> return $ map isImp args
704704 ns <- apply (Var fn) imps
705705 when autoSolve solveAll
706706 where isImp (PImp _ _ _ _) = True
707707 isImp _ = False
708+ envArgs n = do e <- get_env
709+ case lookup n e of
710+ Just t -> return $ map (const False)
711+ (getArgTys (binderTy t))
712+ _ -> return []
708713 runT (Refine fn imps) = do ns <- apply (Var fn) imps
709714 when autoSolve solveAll
710715 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that