Warn about unreachable default clauses (#1942)

* so much experimentation

* tests that show preliminary evidence the new stuff is working.

* small amount of cleanup

* more cleanup of various troubleshooting code.

* new test case added.

* only log unreachable indices if there are any.

* when traversing deeper simply skip over defaults since they have already been reviewed.

* Remove fallback clause that the changes in this PR correctly identified as unreachable.

* tidying up more.

* move some common functions to a new Core.Case.Util module.

* refer to case builder and case tree under new parent module.

* update imports to look for CaseTree in new submodule.

* update api ipkg

* remove unneeded application operators.

* remove or comment out unreachable default clauses caught by the changes in this PR.

* a bit of code documentation and renaming for clarity.

* bump previous version in CI.

* fix API usage of Util module.

* Add issue 1079 test cases.

* forgot to add new test cases file.

* remove commented-out lines by request of RefC author.

* Use a SortedSet instead of nubbing a list.

* update new case tree import.

* Update src/Core/Case/Util.idr

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

* remove function with nothing to offer above and beyond a differently named copy of the same code.

* replace a large tuple with a record; discover not all of the tuple's fields were needed.

* fix shadowing warning.

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

idris2api.ipkg

@@ -43,8 +43,9 @@ modules =
     Core.AutoSearch,
     Core.Binary,
     Core.Binary.Prims,
-    Core.CaseBuilder,
-    Core.CaseTree,
+    Core.Case.CaseBuilder,
+    Core.Case.CaseTree,
+    Core.Case.Util,
     Core.CompileExpr,
     Core.Context,
     Core.Context.Context,

src/Compiler/CompileExpr.idr

@@ -1,6 +1,6 @@
 module Compiler.CompileExpr
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import public Core.CompileExpr
 import Core.Context
 import Core.Env

src/Compiler/RefC/RefC.idr

@@ -80,8 +80,6 @@ cName (Nested i n) = "n__" ++ cCleanString (show i) ++ "_" ++ cName n
 cName (CaseBlock x y) = "case__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
 cName (WithBlock x y) = "with__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
 cName (Resolved i) = "fn__" ++ cCleanString (show i)
-cName n = assert_total $ idris_crash ("INTERNAL ERROR: Unsupported name in C backend " ++ show n)
--- not really total but this way this internal error does not contaminate everything else
 
 escapeChar : Char -> String
 escapeChar c = if isAlphaNum c || isNL c
@@ -135,8 +133,6 @@ cConstant Bits8Type = "Bits8"
 cConstant Bits16Type = "Bits16"
 cConstant Bits32Type = "Bits32"
 cConstant Bits64Type = "Bits64"
-cConstant n = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw constant in C backend: " ++ show n)
--- not really total but this way this internal error does not contaminate everything else
 
 extractConstant : Constant -> String
 extractConstant (I x) = show x

src/Core/Binary.idr

@@ -4,7 +4,7 @@
 module Core.Binary
 
 import public Core.Binary.Prims
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/Core/Case/CaseBuilder.idr

@@ -1,6 +1,7 @@
-module Core.CaseBuilder
+module Core.Case.CaseBuilder
 
-import Core.CaseTree
+import Core.Case.CaseTree
+import Core.Case.Util
 import Core.Context
 import Core.Context.Log
 import Core.Core
@@ -10,9 +11,10 @@ import Core.Options
 import Core.TT
 import Core.Value
 
-import Libraries.Data.LengthMatch
 import Data.List
 import Data.Vect
+import Libraries.Data.LengthMatch
+import Libraries.Data.SortedSet
 
 import Decidable.Equality
 
@@ -385,7 +387,7 @@ data Group : List Name -> -- variables in scope
   show (ConstGroup c cs) = "Const " ++ show c ++ ": " ++ show cs
 
 data GroupMatch : ConType -> List Pat -> Group vars todo -> Type where
-  ConMatch : LengthMatch ps newargs ->
+  ConMatch : {tag : Int} -> LengthMatch ps newargs ->
              GroupMatch (CName n tag) ps
                (ConGroup {newargs} n tag (MkPatClause pvs pats pid rhs :: rest))
   DelayMatch : GroupMatch CDelay []
@@ -1226,16 +1228,90 @@ simpleCase fc phase fn ty def clauses
          defs <- get Ctxt
          patCompile fc fn phase ty ps def
 
-findReached : CaseTree ns -> List Int
-findReached (Case _ _ _ alts) = concatMap findRAlts alts
+mutual
+  findReachedAlts : CaseAlt ns' -> List Int
+  findReachedAlts (ConCase _ _ _ t) = findReached t
+  findReachedAlts (DelayCase _ _ t) = findReached t
+  findReachedAlts (ConstCase _ t) = findReached t
+  findReachedAlts (DefaultCase t) = findReached t
+
+  findReached : CaseTree ns -> List Int
+  findReached (Case _ _ _ alts) = concatMap findReachedAlts alts
+  findReached (STerm i _) = [i]
+  findReached _ = []
+
+-- Replace a default case with explicit branches for the constructors.
+-- This is easier than checking whether a default is needed when traversing
+-- the tree (just one constructor lookup up front).
+-- Unreachable defaults are those that when replaced by all possible constructors
+-- followed by a removal of duplicate cases there is one _fewer_ total case alts.
+identifyUnreachableDefaults : {auto c : Ref Ctxt Defs} ->
+                              {vars : _} ->
+                              FC -> Defs -> NF vars -> List (CaseAlt vars) ->
+                              Core (SortedSet Int)
+-- Leave it alone if it's a primitive type though, since we need the catch
+-- all case there
+identifyUnreachableDefaults fc defs (NPrimVal _ _) cs = pure empty
+identifyUnreachableDefaults fc defs (NType _) cs = pure empty
+identifyUnreachableDefaults fc defs nfty cs
+    = do cs' <- traverse rep cs
+         let (cs'', extraClauseIdxs) = dropRep (concat cs') empty
+         let extraClauseIdxs' =
+           if (length cs == (length cs'' + 1))
+              then extraClauseIdxs
+              else empty
+         -- if a clause is unreachable under all the branches it can be found under
+         -- then it is entirely unreachable.
+         when (not $ null extraClauseIdxs') $
+           log "compile.casetree.clauses" 25 $
+             "Marking the following clause indices as unreachable under the current branch of the tree: " ++ (show extraClauseIdxs')
+         pure extraClauseIdxs'
   where
-    findRAlts : CaseAlt ns' -> List Int
-    findRAlts (ConCase _ _ _ t) = findReached t
-    findRAlts (DelayCase _ _ t) = findReached t
-    findRAlts (ConstCase _ t) = findReached t
-    findRAlts (DefaultCase t) = findReached t
-findReached (STerm i _) = [i]
-findReached _ = []
+    rep : CaseAlt vars -> Core (List (CaseAlt vars))
+    rep (DefaultCase sc)
+        = do allCons <- getCons defs nfty
+             pure (map (mkAlt fc sc) allCons)
+    rep c = pure [c]
+
+    dropRep : List (CaseAlt vars) -> SortedSet Int -> (List (CaseAlt vars), SortedSet Int)
+    dropRep [] extra = ([], extra)
+    dropRep (c@(ConCase n t args sc) :: rest) extra
+          -- assumption is that there's no defaultcase in 'rest' because
+          -- we've just removed it
+        = let (filteredClauses, extraCases) = partition (not . tagIs t) rest
+              extraClauses = extraCases >>= findReachedAlts
+              (rest', extra') = dropRep filteredClauses $ fromList extraClauses
+          in  (c :: rest', extra `union` extra')
+    dropRep (c :: rest) extra
+        = let (rest', extra') = dropRep rest extra
+          in  (c :: rest', extra')
+
+||| Find unreachable default paths through the tree for each clause.
+||| This is accomplished by expanding default clases into all concrete constructions
+||| and then listing the clauses reached.
+||| This list of clauses can be substracted from the list of "reachable" clauses
+||| and if it turns out that the number of unreachable ways to use a clause is equal
+||| to the number of ways to reach a RHS for that clause then the clause is totally
+||| superfluous (it will never be reached).
+findExtraDefaults : {auto c : Ref Ctxt Defs} ->
+                   {vars : _} ->
+                   FC -> Defs -> CaseTree vars ->
+                   Core (List Int)
+findExtraDefaults fc defs ctree@(Case {name = var} idx el ty altsIn)
+  = do let fenv = mkEnv fc _
+       nfty <- nf defs fenv ty
+       extraCases <- identifyUnreachableDefaults fc defs nfty altsIn
+       extraCases' <- concat <$> traverse findExtraAlts altsIn
+       pure (SortedSet.toList extraCases ++ extraCases')
+  where
+    findExtraAlts : CaseAlt vars -> Core (List Int)
+    findExtraAlts (ConCase x tag args ctree') = findExtraDefaults fc defs ctree'
+    findExtraAlts (DelayCase x arg ctree') = findExtraDefaults fc defs ctree'
+    findExtraAlts (ConstCase x ctree') = findExtraDefaults fc defs ctree'
+    -- already handled defaults by elaborating them to all possible cons
+    findExtraAlts (DefaultCase ctree') = pure []
+
+findExtraDefaults fc defs ctree = pure []
 
 -- Returns the case tree, and a list of the clauses that aren't reachable
 export
@@ -1263,7 +1339,11 @@ getPMDef fc phase fn ty clauses
          logC "compile.casetree.getpmdef" 20 $
            pure $ "Compiled to: " ++ show !(toFullNames t)
          let reached = findReached t
-         pure (_ ** (t, getUnreachable 0 reached clauses))
+         log "compile.casetree.clauses" 25 $
+           "Reached clauses: " ++ (show reached)
+         extraDefaults <- findExtraDefaults fc defs t
+         let unreachable = getUnreachable 0 (reached \\ extraDefaults) clauses
+         pure (_ ** (t, unreachable))
   where
     getUnreachable : Int -> List Int -> List Clause -> List Clause
     getUnreachable i is [] = []

src/Core/Case/CaseTree.idr

@@ -1,4 +1,4 @@
-module Core.CaseTree
+module Core.Case.CaseTree
 
 import Core.TT
 

src/Core/Case/Util.idr

@@ -0,0 +1,63 @@
+module Core.Case.Util
+
+import Core.Case.CaseTree
+import Core.Context
+import Core.Env
+import Core.Normalise
+import Core.Value
+
+public export
+record DataCon where
+  constructor MkDataCon
+  name  : Name
+  tag   : Int
+  arity : Nat
+
+||| Given a normalised type, get all the possible constructors for that
+||| type family, with their type, name, tag, and arity.
+export
+getCons : {auto c : Ref Ctxt Defs} ->
+          {vars : _} ->
+          Defs -> NF vars -> Core (List DataCon)
+getCons defs (NTCon _ tn _ _ _)
+    = case !(lookupDefExact tn (gamma defs)) of
+           Just (TCon _ _ _ _ _ _ cons _) =>
+                do cs' <- traverse addTy cons
+                   pure (catMaybes cs')
+           _ => throw (InternalError "Called `getCons` on something that is not a Type constructor")
+  where
+    addTy : Name -> Core (Maybe DataCon)
+    addTy cn
+        = do Just gdef <- lookupCtxtExact cn (gamma defs)
+                  | _ => pure Nothing
+             case (gdef.definition, gdef.type) of
+                  (DCon t arity _, ty) =>
+                        pure . Just $ MkDataCon cn t arity
+                  _ => pure Nothing
+getCons defs _ = pure []
+
+emptyRHS : FC -> CaseTree vars -> CaseTree vars
+emptyRHS fc (Case idx el sc alts) = Case idx el sc (map emptyRHSalt alts)
+  where
+    emptyRHSalt : CaseAlt vars -> CaseAlt vars
+    emptyRHSalt (ConCase n t args sc) = ConCase n t args (emptyRHS fc sc)
+    emptyRHSalt (DelayCase c arg sc) = DelayCase c arg (emptyRHS fc sc)
+    emptyRHSalt (ConstCase c sc) = ConstCase c (emptyRHS fc sc)
+    emptyRHSalt (DefaultCase sc) = DefaultCase (emptyRHS fc sc)
+emptyRHS fc (STerm i s) = STerm i (Erased fc False)
+emptyRHS fc sc = sc
+
+export
+mkAlt : {vars : _} ->
+        FC -> CaseTree vars -> DataCon -> CaseAlt vars
+mkAlt fc sc (MkDataCon cn t ar)
+    = ConCase cn t (map (MN "m") (take ar [0..]))
+              (weakenNs (map take) (emptyRHS fc sc))
+
+export
+tagIs : Int -> CaseAlt vars -> Bool
+tagIs t (ConCase _ t' _ _) = t == t'
+tagIs t (ConstCase _ _) = False
+tagIs t (DelayCase _ _ _) = False
+tagIs t (DefaultCase _) = True
+

src/Core/Context.idr

@@ -1,6 +1,6 @@
 module Core.Context
 
-import        Core.CaseTree
+import        Core.Case.CaseTree
 import        Core.CompileExpr
 import public Core.Context.Context
 import public Core.Core

src/Core/Context/Context.idr

@@ -1,6 +1,6 @@
 module Core.Context.Context
 
-import        Core.CaseTree
+import        Core.Case.CaseTree
 import        Core.CompileExpr
 import        Core.Env
 import        Core.Hash

src/Core/Coverage.idr

@@ -1,6 +1,7 @@
 module Core.Coverage
 
-import Core.CaseTree
+import Core.Case.CaseTree
+import Core.Case.Util
 import Core.Context
 import Core.Context.Log
 import Core.Env
@@ -13,8 +14,8 @@ import Data.Maybe
 import Data.String
 
 import Libraries.Data.NameMap
-import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Data.String.Extra
+import Libraries.Text.PrettyPrint.Prettyprinter
 
 %hide Data.String.lines
 %hide Data.String.lines'
@@ -149,50 +150,6 @@ isEmpty defs env (NTCon fc n t a args)
             _ => pure False
 isEmpty defs env _ = pure False
 
--- Need this to get a NF from a Term; the names are free in any case
-freeEnv : FC -> (vs : List Name) -> Env Term vs
-freeEnv fc [] = []
-freeEnv fc (n :: ns) = PVar fc top Explicit (Erased fc False) :: freeEnv fc ns
-
--- Given a normalised type, get all the possible constructors for that
--- type family, with their type, name, tag, and arity
-getCons : {auto c : Ref Ctxt Defs} ->
-          {vars : _} ->
-          Defs -> NF vars -> Core (List (NF [], Name, Int, Nat))
-getCons defs (NTCon _ tn _ _ _)
-    = case !(lookupDefExact tn (gamma defs)) of
-           Just (TCon _ _ _ _ _ _ cons _) =>
-                do cs' <- traverse addTy cons
-                   pure (mapMaybe id cs')
-           _ => throw (InternalError "Called `getCons` on something that is not a Type constructor")
-  where
-    addTy : Name -> Core (Maybe (NF [], Name, Int, Nat))
-    addTy cn
-        = do Just gdef <- lookupCtxtExact cn (gamma defs)
-                  | _ => pure Nothing
-             case (definition gdef, type gdef) of
-                  (DCon t arity _, ty) =>
-                        pure (Just (!(nf defs [] ty), cn, t, arity))
-                  _ => pure Nothing
-getCons defs _ = pure []
-
-emptyRHS : FC -> CaseTree vars -> CaseTree vars
-emptyRHS fc (Case idx el sc alts) = Case idx el sc (map emptyRHSalt alts)
-  where
-    emptyRHSalt : CaseAlt vars -> CaseAlt vars
-    emptyRHSalt (ConCase n t args sc) = ConCase n t args (emptyRHS fc sc)
-    emptyRHSalt (DelayCase c arg sc) = DelayCase c arg (emptyRHS fc sc)
-    emptyRHSalt (ConstCase c sc) = ConstCase c (emptyRHS fc sc)
-    emptyRHSalt (DefaultCase sc) = DefaultCase (emptyRHS fc sc)
-emptyRHS fc (STerm i s) = STerm i (Erased fc False)
-emptyRHS fc sc = sc
-
-mkAlt : {vars : _} ->
-        FC -> CaseTree vars -> (Name, Int, Nat) -> CaseAlt vars
-mkAlt fc sc (cn, t, ar)
-    = ConCase cn t (map (MN "m") (take ar [0..]))
-              (weakenNs (map take) (emptyRHS fc sc))
-
 altMatch : CaseAlt vars -> CaseAlt vars -> Bool
 altMatch _ (DefaultCase _) = True
 altMatch (DelayCase _ _ t) (DelayCase _ _ t') = True
@@ -230,7 +187,7 @@ getMissingAlts fc defs nfty alts
          logNF "coverage.missing" 20 "Getting constructors for" (mkEnv fc _) nfty
          allCons <- getCons defs nfty
          pure (filter (noneOf alts)
-                 (map (mkAlt fc (Unmatched "Coverage check") . snd) allCons))
+                 (map (mkAlt fc (Unmatched "Coverage check")) allCons))
   where
     -- Return whether the alternative c matches none of the given cases in alts
     noneOf : List (CaseAlt vars) -> CaseAlt vars -> Bool
@@ -274,12 +231,6 @@ addNot v t ((v', ts) :: xs)
          then ((v', t :: ts) :: xs)
          else ((v', ts) :: addNot v t xs)
 
-tagIs : Int -> CaseAlt vars -> Bool
-tagIs t (ConCase _ t' _ _) = t == t'
-tagIs t (ConstCase _ _) = False
-tagIs t (DelayCase _ _ _) = False
-tagIs t (DefaultCase _) = True
-
 tagIsNot : List Int -> CaseAlt vars -> Bool
 tagIsNot ts (ConCase _ t' _ _) = not (t' `elem` ts)
 tagIsNot ts (ConstCase _ _) = True
@@ -304,7 +255,7 @@ replaceDefaults fc defs nfty cs
     rep : CaseAlt vars -> Core (List (CaseAlt vars))
     rep (DefaultCase sc)
         = do allCons <- getCons defs nfty
-             pure (map (mkAlt fc sc . snd) allCons)
+             pure (map (mkAlt fc sc) allCons)
     rep c = pure [c]
 
     dropRep : List (CaseAlt vars) -> List (CaseAlt vars)
@@ -332,7 +283,7 @@ buildArgs fc defs known not ps cs@(Case {name = var} idx el ty altsIn)
   -- to the tag we already know. Otherwise, add missing cases and filter out
   -- the ones it can't possibly be (the 'not') because a previous case
   -- has matched.
-    = do let fenv = freeEnv fc _
+    = do let fenv = mkEnv fc _
          nfty <- nf defs fenv ty
          alts <- replaceDefaults fc defs nfty altsIn
          let alts' = alts ++ !(getMissingAlts fc defs nfty alts)
@@ -353,8 +304,8 @@ buildArgs fc defs known not ps cs@(Case {name = var} idx el ty altsIn)
              buildArgs fc defs (weakenNs l ((MkVar el, t) :: known))
                                (weakenNs l not') ps' sc
     buildArgAlt not' (DelayCase t a sc)
-        = let l = mkSizeOf [t, a] in
-          let ps' = map (substName var (TDelay fc LUnknown
+        = let l = mkSizeOf [t, a]
+              ps' = map (substName var (TDelay fc LUnknown
                                              (Ref fc Bound t)
                                              (Ref fc Bound a))) ps in
               buildArgs fc defs (weakenNs l known) (weakenNs l not')

src/Core/GetType.idr

@@ -1,10 +1,10 @@
 module Core.GetType
 
-import Core.CaseTree
-import Core.TT
+import Core.Case.CaseTree
 import Core.Context
 import Core.Env
 import Core.Normalise
+import Core.TT
 import Core.Value
 
 %default covering

src/Core/Hash.idr

@@ -1,8 +1,8 @@
 module Core.Hash
 
-import Core.CaseTree
-import Core.TT
+import Core.Case.CaseTree
 import Core.CompileExpr
+import Core.TT
 
 import Data.List
 import Data.List1

src/Core/LinearCheck.idr

@@ -1,6 +1,6 @@
 module Core.LinearCheck
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/Core/Normalise.idr

@@ -4,7 +4,7 @@ import public Core.Normalise.Convert
 import public Core.Normalise.Eval
 import public Core.Normalise.Quote
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/Core/Normalise/Convert.idr

@@ -3,7 +3,7 @@ module Core.Normalise.Convert
 import public Core.Normalise.Eval
 import public Core.Normalise.Quote
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/Core/Normalise/Eval.idr

@@ -1,6 +1,6 @@
 module Core.Normalise.Eval
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/Core/Normalise/Quote.idr

@@ -1,6 +1,6 @@
 module Core.Normalise.Quote
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/Core/SchemeEval/Compile.idr

@@ -13,7 +13,7 @@ Advanced TODO (possibly not worth it...):
 
 import Algebra.ZeroOneOmega
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Core
 import Core.Directory

src/Core/TTC.idr

@@ -1,7 +1,7 @@
 module Core.TTC
 
 import Core.Binary.Prims
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.CompileExpr
 import Core.Context
 import Core.Core

src/Core/Termination.idr

@@ -1,6 +1,6 @@
 module Core.Termination
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Env

src/Core/Unify.idr

@@ -1,6 +1,6 @@
 module Core.Unify
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/Core/UnifyState.idr

@@ -1,7 +1,7 @@
 
 module Core.UnifyState
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core
@@ -12,12 +12,12 @@ import Core.Options
 import Core.TT
 import Core.TTC
 import Core.Value
-import Libraries.Utils.Binary
 
-import Libraries.Data.IntMap
 import Data.List
+import Libraries.Data.IntMap
 import Libraries.Data.NameMap
 import Libraries.Data.StringMap
+import Libraries.Utils.Binary
 
 %default covering
 

src/Idris/Error.idr

@@ -1,6 +1,6 @@
 module Idris.Error
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Core
 import Core.Context
 import Core.Env

src/Idris/REPL.idr

@@ -11,7 +11,7 @@ import Compiler.RefC.RefC
 import Compiler.Inline
 
 import Core.AutoSearch
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.CompileExpr
 import Core.Context
 import Core.Context.Log

src/Idris/REPL/FuzzySearch.idr

@@ -1,7 +1,7 @@
 module Idris.REPL.FuzzySearch
 
 import Core.AutoSearch
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.CompileExpr
 import Core.Context
 import Core.Context.Log
@@ -11,8 +11,8 @@ import Core.LinearCheck
 import Core.Metadata
 import Core.Normalise
 import Core.Options
-import Core.Termination
 import Core.TT
+import Core.Termination
 import Core.Unify
 
 import Idris.Desugar

src/Libraries/Data/SortedSet.idr

@@ -67,6 +67,10 @@ export
 Ord k => Monoid (SortedSet k) where
   neutral = empty
 
+export
+Show k => Show (SortedSet k) where
+  show = show . SortedSet.toList
+
 export
 keySet : SortedMap k v -> SortedSet k
 keySet = SetWrapper . map (const ())

src/TTImp/Elab/App.idr

@@ -1,6 +1,6 @@
 module TTImp.Elab.App
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/TTImp/Elab/Case.idr

@@ -1,6 +1,6 @@
 module TTImp.Elab.Case
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/TTImp/Elab/Delayed.idr

@@ -1,6 +1,6 @@
 module TTImp.Elab.Delayed
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/TTImp/Elab/ImplicitBind.idr

@@ -491,7 +491,6 @@ checkPolyConstraint (MkPolyConstraint fc env arg x y)
                                  throw (MatchTooSpecific fc env arg)
                          else pure ()
               _ => pure ()
-checkPolyConstraint _ = pure ()
 
 solvePolyConstraint :
             {auto c : Ref Ctxt Defs} ->

src/TTImp/Elab/Local.idr

@@ -1,6 +1,6 @@
 module TTImp.Elab.Local
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/TTImp/Elab/Utils.idr

@@ -1,6 +1,6 @@
 module TTImp.Elab.Utils
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Core
 import Core.Env

src/TTImp/Interactive/ExprSearch.idr

@@ -11,7 +11,7 @@ module TTImp.Interactive.ExprSearch
 -- depth.
 
 import Core.AutoSearch
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Env
@@ -19,8 +19,8 @@ import Core.LinearCheck
 import Core.Metadata
 import Core.Normalise
 import Core.Options
-import Core.Unify
 import Core.TT
+import Core.Unify
 import Core.Value
 
 import TTImp.Elab.Check

src/TTImp/PartialEval.idr

@@ -1,6 +1,6 @@
 module TTImp.PartialEval
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/TTImp/ProcessBuiltin.idr

@@ -7,7 +7,7 @@ import Data.List
 import Libraries.Data.Fin as Libs
 import Libraries.Data.NameMap
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Core
 import Core.Context
 import Core.Context.Log

src/TTImp/ProcessDef.idr

@@ -1,7 +1,7 @@
 module TTImp.ProcessDef
 
-import Core.CaseBuilder
-import Core.CaseTree
+import Core.Case.CaseBuilder
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Core

src/TTImp/Unelab.idr

@@ -1,6 +1,6 @@
 module TTImp.Unelab
 
-import Core.CaseTree
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Env
@@ -268,9 +268,6 @@ mutual
   unelabTy' umode nest env (PrimVal fc c) = pure (IPrimVal fc c, gErased fc)
   unelabTy' umode nest env (Erased fc _) = pure (Implicit fc True, gErased fc)
   unelabTy' umode nest env (TType fc) = pure (IType fc, gType fc)
-  unelabTy' umode nest _ tm
-      = let fc = getLoc tm in
-            pure (Implicit fc False, gErased fc)
 
   unelabPi : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->

tests/Main.idr

@@ -56,7 +56,7 @@ idrisTestsCoverage = MkTestPool "Coverage checking" [] Nothing
 idrisTestsCasetree : TestPool
 idrisTestsCasetree = MkTestPool "Case tree building" [] Nothing
        -- Case tree building
-      ["casetree001"]
+      ["casetree001", "casetree002"]
 
 idrisTestsWarning : TestPool
 idrisTestsWarning = MkTestPool "Warnings" [] Nothing

tests/chez/chez020/Popen.idr

@@ -26,5 +26,4 @@ main = do
     pclose fh
     putStrLn "closed"
     let (idris2 ::: _) = split ((==) ',') output
-        | _ => printLn "Unexpected result"
     putStrLn idris2

tests/idris2/casetree002/DefaultCases.idr

@@ -0,0 +1,50 @@
+%default total
+
+data MyBit = A | B
+
+fullCoverage : MyBit -> Int
+fullCoverage A = 1
+fullCoverage B = 2
+
+extraDefault : MyBit -> Int
+extraDefault A = 1
+extraDefault B = 2
+extraDefault _ = 3
+
+usefulDefault : MyBit -> Int
+usefulDefault A = 1
+usefulDefault _ = 2
+
+earlyDefault : MyBit -> Int
+earlyDefault _ = 1
+earlyDefault A = 2
+
+onlyDefault : MyBit -> Int
+onlyDefault _ = 1
+
+nestedFullCoverage : MyBit -> MyBit -> Int
+nestedFullCoverage A A = 1
+nestedFullCoverage A B = 2
+nestedFullCoverage B A = 3
+nestedFullCoverage B B = 4
+
+nestedExtraDefault : MyBit -> MyBit -> Int
+nestedExtraDefault A A = 1
+nestedExtraDefault A B = 2
+nestedExtraDefault B A = 3
+nestedExtraDefault B B = 4
+nestedExtraDefault _ _ = 5
+
+nestedUsefulDefault : MyBit -> MyBit -> Int
+nestedUsefulDefault A A = 1
+nestedUsefulDefault A B = 2
+nestedUsefulDefault B A = 3
+nestedUsefulDefault _ _ = 4
+
+nestedEarlyDefault : MyBit -> MyBit -> Int
+nestedEarlyDefault A A = 1
+nestedEarlyDefault A B = 2
+nestedEarlyDefault B A = 3
+nestedEarlyDefault _ _ = 4
+nestedEarlyDefault B B = 5
+

tests/idris2/casetree002/Issue1079.idr

@@ -0,0 +1,14 @@
+%default total
+
+g3 : (Nat, Nat) -> Nat
+g3 (x, y) = x
+g3 _ = 6
+
+f : Monad m => m (Nat, Nat)
+
+h3 : Monad m => m Nat
+h3 = do
+  (x, y) <- f
+    | _ => pure 5
+  pure x
+

tests/idris2/casetree002/expected

@@ -0,0 +1,64 @@
+1/1: Building DefaultCases (DefaultCases.idr)
+Warning: Unreachable clause: extraDefault _
+
+DefaultCases:12:1--12:15
+ 08 | 
+ 09 | extraDefault : MyBit -> Int
+ 10 | extraDefault A = 1
+ 11 | extraDefault B = 2
+ 12 | extraDefault _ = 3
+      ^^^^^^^^^^^^^^
+
+Warning: Unreachable clause: earlyDefault A
+
+DefaultCases:20:1--20:15
+ 16 | usefulDefault _ = 2
+ 17 | 
+ 18 | earlyDefault : MyBit -> Int
+ 19 | earlyDefault _ = 1
+ 20 | earlyDefault A = 2
+      ^^^^^^^^^^^^^^
+
+Warning: Unreachable clause: nestedExtraDefault _ _
+
+DefaultCases:36:1--36:23
+ 32 | nestedExtraDefault A A = 1
+ 33 | nestedExtraDefault A B = 2
+ 34 | nestedExtraDefault B A = 3
+ 35 | nestedExtraDefault B B = 4
+ 36 | nestedExtraDefault _ _ = 5
+      ^^^^^^^^^^^^^^^^^^^^^^
+
+Warning: Unreachable clause: nestedEarlyDefault B B
+
+DefaultCases:49:1--49:23
+ 45 | nestedEarlyDefault A A = 1
+ 46 | nestedEarlyDefault A B = 2
+ 47 | nestedEarlyDefault B A = 3
+ 48 | nestedEarlyDefault _ _ = 4
+ 49 | nestedEarlyDefault B B = 5
+      ^^^^^^^^^^^^^^^^^^^^^^
+
+1/1: Building Issue1079 (Issue1079.idr)
+Warning: Unreachable clause: g3 _
+
+Issue1079:5:1--5:5
+ 1 | %default total
+ 2 | 
+ 3 | g3 : (Nat, Nat) -> Nat
+ 4 | g3 (x, y) = x
+ 5 | g3 _ = 6
+     ^^^^
+
+Warning: Unreachable clause: case _ of
+                             {(x, y) => pure x;
+                             _ => pure 5}
+
+Issue1079:12:7--12:18
+ 08 | 
+ 09 | h3 : Monad m => m Nat
+ 10 | h3 = do
+ 11 |   (x, y) <- f
+ 12 |     | _ => pure 5
+            ^^^^^^^^^^^
+

tests/idris2/casetree002/run

@@ -0,0 +1,5 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check DefaultCases.idr
+$1 --no-color --console-width 0 --no-banner --check Issue1079.idr
+