Type constructor arguments are unused at run-time
They were being marked as "direct uses", which is wrong, because type
constructors do not get compiled, so that usage information was
propagating and leaving irrelevant arguments in the code...
commit32b66c526841209119e517ee015195a9ebb518bc
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 19 Jan 2014, 18:58 (13 years ago)
parentbee7fc8
src/Idris/Core/CaseTree.hs+1
@@ -157,6 +157,7 @@ directUse (Bind n (Let t v) sc) = nub $ directUse v ++ (directUse sc \\ [n])
157157directUse (Bind n b sc) = nub $ directUse (binderTy b) ++ (directUse sc \\ [n])
158158directUse fn@(App f a)
159159 | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them
160+ | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime
160161 | otherwise = nub $ directUse f ++ directUse a
161162directUse (Proj x i) = nub $ directUse x
162163directUse _ = []