@@ -222,10 +222,9 @@ instance ToIR (TT Name) where
222222
223223 | (P (DCon t a) n _, args) <- unApply tm = do
224224 cg <- idris_callgraph <$> getIState
225− case lookupCtxtExact n cg of
226− Just (CGInfo _ _ _ _ usedpos)
227− -> irCon env t a n [if i `elem` map fst usedpos then a else Erased | (i,a) <- zip [0..] args]
228− Nothing -> return LNothing -- no usage info -> not used at all
225+ let used = maybe [] (map fst . usedpos) $ lookupCtxtExact n cg
226+ args' = [if i `elem` used then a else Erased | (i,a) <- zip [0..] args]
227+ irCon env t a n args'
229228
230229 | (P (TCon t a) n _, args) <- unApply tm
231230 = return LNothing
@@ -238,14 +237,19 @@ instance ToIR (TT Name) where
238237 Just (arity, op) | length args == arity
239238 -> LOp op <$> mapM (ir' env) args
240239
240+ _ -> applyName n ist args
241+
242+{- collapsibility is turned off for now
241243 _
242244 -- if it's collapsible, compile to LNothing
243245 | (collapsible <$> lookupCtxtExact n (idris_optimisation ist)) == Just True
244246 -> return LNothing
245−
247+
246248 -- otherwise, compile normally
247249 | otherwise -> applyName n ist args
248250
251+-}
252+
249253 | (f, args) <- unApply tm
250254 = do f' <- ir' env f
251255 args' <- mapM (ir' env) args
@@ -266,7 +270,7 @@ instance ToIR (TT Name) where
266270 [Operator ty ar op] -> ar
267271 _ -> 0
268272
269− used = fromMaybe [] (map fst . usedpos <$> lookupCtxtExact n (idris_callgraph ist))
273+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)
270274 fst4 (x,_,_,_) = x
271275
272276-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)