git.iko.soy/Idris-dev
on master help sign in
Fix collapsibility bug
8624d06Edwin Brady
src/Idris/DataOpts.hs+2−2
compare with master
unifiedsplit
@@ -86,8 +86,8 @@ collapseCons ty cons =
86 checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs
86 checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs
87 checkFR fs i (t : xs)
87 checkFR fs i (t : xs)
88 -- must be recursive or type is not collapsible
88 -- must be recursive or type is not collapsible
89− = do let rt = getRetTy t
89+ = do let (rtf, rta) = unApply $ getRetTy t
90− if (ty `elem` freeNames rt)
90+ if (ty `elem` freeNames rtf)
91 then checkFR fs (i+1) xs
91 then checkFR fs (i+1) xs
92 else return False
92 else return False
93
93
src/Idris/ElabDecls.hs+1
@@ -430,6 +430,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
430 else return []
430 else return []
431 let pcover = null pmissing
431 let pcover = null pmissing
432 logLvl 2 $ "Optimising patterns"
432 logLvl 2 $ "Optimising patterns"
433+ logLvl 5 $ show optpdef
433 pdef' <- applyOpts optpdef
434 pdef' <- applyOpts optpdef
434 logLvl 2 $ "Optimised patterns"
435 logLvl 2 $ "Optimised patterns"
435 logLvl 5 $ show pdef'
436 logLvl 5 $ show pdef'