8624d06 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix collapsibility bug

commit8624d06f728a8e66c5d9ea371ae300c014508742 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 5 Apr 2013, 14:59 (14 years ago) parent34506e9

2 files changed+3−2

unifiedsplit

src/Idris/DataOpts.hs+2−2

@@ -86,8 +86,8 @@ collapseCons ty cons =

8686 checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs

8787 checkFR fs i (t : xs)

8888 -- must be recursive or type is not collapsible

89− = do let rt = getRetTy t

90− if (ty `elem` freeNames rt)

89+ = do let (rtf, rta) = unApply $ getRetTy t

90+ if (ty `elem` freeNames rtf)

9191 then checkFR fs (i+1) xs

9292 else return False

9393

src/Idris/ElabDecls.hs+1

@@ -430,6 +430,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

430430 else return []

431431 let pcover = null pmissing

432432 logLvl 2 $ "Optimising patterns"

433+ logLvl 5 $ show optpdef

433434 pdef' <- applyOpts optpdef

434435 logLvl 2 $ "Optimised patterns"

435436 logLvl 5 $ show pdef'