@@ -360,27 +360,27 @@ irTerm vs env tm@(App f a) = case unApply tm of
360360
361361 applyName :: Name -> IState -> [Term] -> Idris LExp
362362 applyName n ist args =
363− LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
364− where
365− erase (i, x)
366− | i >= arity || i `elem` used = x
367− | otherwise = Erased
368−
369− arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
370− Just (CaseOp ci ty tys def tot cdefs) -> length tys
371− Just (TyDecl (DCon tag ar) _) -> ar
372− Just (TyDecl Ref ty) -> length $ getArgTys ty
373− Just (Operator ty ar op) -> ar
374− Just def -> error $ "unknown arity: " ++ show (n, def)
375− Nothing -> 0 -- no definition, probably local name => can't erase anything
376−
377− -- name for purposes of usage info lookup
378− uName
379− | Just n' <- viMethod =<< M.lookup n vs = n'
380− | otherwise = n
381−
382− used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
383− fst4 (x,_,_,_) = x
363+ LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
364+ where
365+ erase (i, x)
366+ | i >= arity || i `elem` used = x
367+ | otherwise = Erased
368+
369+ arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
370+ Just (CaseOp ci ty tys def tot cdefs) -> length tys
371+ Just (TyDecl (DCon tag ar) _) -> ar
372+ Just (TyDecl Ref ty) -> length $ getArgTys ty
373+ Just (Operator ty ar op) -> ar
374+ Just def -> error $ "unknown arity: " ++ show (n, def)
375+ Nothing -> 0 -- no definition, probably local name => can't erase anything
376+
377+ -- name for purposes of usage info lookup
378+ uName
379+ | Just n' <- viMethod =<< M.lookup n vs = n'
380+ | otherwise = n
381+
382+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
383+ fst4 (x,_,_,_) = x
384384
385385irTerm vs env (P _ n _) = return $ LV (Glob n)
386386irTerm vs env (V i)