@@ -266,6 +266,8 @@ irTerm vs env tm@(App f a) = case unApply tm of
266266 -- otherwise, just apply the name
267267 _ -> applyName n ist args
268268
269+ (V i, args) -> irTerm vs env (P Bound (env !! i) Erased)
270+
269271 (f, args)
270272 -> LApp False
271273 <$> irTerm vs env f
@@ -288,7 +290,12 @@ irTerm vs env tm@(App f a) = case unApply tm of
288290 [] -> 0 -- no definition, probably local name => can't erase anything
289291 def -> error $ "unknown arity: " ++ show (n, def)
290292
291− used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)
293+ -- name for purposes of usage info lookup
294+ uName
295+ | Just n' <- viMethod =<< M.lookup n vs = n'
296+ | otherwise = n
297+
298+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
292299 fst4 (x,_,_,_) = x
293300
294301irTerm vs env (P _ n _) = return $ LV (Glob n)