@@ -8,6 +8,7 @@ import Idris.AbsSyntax
88import Idris.Delaborate
99
1010import Idris.Core.TT
11+import Idris.Core.CaseTree
1112import Idris.Core.Evaluate
1213
1314import Control.Monad.State
@@ -298,7 +299,8 @@ getSpecApps ist env tm = ga env (explicitNames tm) where
298299 case (lookupCtxtExact n (idris_statics ist),
299300 lookupCtxtExact n (idris_implicits ist)) of
300301 (Just statics, Just imps) ->
301− if (length statics == length args && or statics) then
302+ if (length statics == length args && or statics
303+ && specialisable (tt_ctxt ist) n) then
302304 case buildApp env statics imps args [0..] of
303305 args -> [(n, args)]
304306-- _ -> []
@@ -308,4 +310,29 @@ getSpecApps ist env tm = ga env (explicitNames tm) where
308310 ga env (Bind n t sc) = ga (n : env) sc
309311 ga env t = []
310312
313+ -- A function is only specialisable if there are no overlapping
314+ -- cases in the case tree (otherwise the partial evaluation could
315+ -- easily get stuck)
316+ specialisable :: Context -> Name -> Bool
317+ specialisable ctxt n = case lookupDefExact n ctxt of
318+ Just (CaseOp _ _ _ _ _ cds) ->
319+ noOverlap (snd (cases_compiletime cds))
320+ _ -> False
321+
322+ noOverlap :: SC -> Bool
323+ noOverlap (Case _ _ [DefaultCase sc]) = noOverlap sc
324+ noOverlap (Case _ _ alts) = noOverlapAlts alts
325+ noOverlap _ = True
326+
327+ -- There's an overlap if the case tree has a default case along with
328+ -- some other cases. It's fine if there's a default case on its own.
329+ noOverlapAlts (ConCase _ _ _ sc : rest)
330+ = noOverlapAlts rest && noOverlap sc
331+ noOverlapAlts (FnCase _ _ sc : rest) = noOverlapAlts rest
332+ noOverlapAlts (ConstCase _ sc : rest)
333+ = noOverlapAlts rest && noOverlap sc
334+ noOverlapAlts (SucCase _ sc : rest)
335+ = noOverlapAlts rest && noOverlap sc
336+ noOverlapAlts (DefaultCase _ : _) = False
337+ noOverlapAlts _ = True
311338