[ fix #899 ] Be careful when generating an impossible LHS (#1081)

libs/base/Data/Nat.idr

@@ -72,6 +72,10 @@ export
 Uninhabited (LTE (S n) Z) where
   uninhabited LTEZero impossible
 
+export
+Uninhabited (LTE m n) => Uninhabited (LTE (S m) (S n)) where
+  uninhabited (LTESucc lte) = uninhabited lte
+
 public export
 GTE : Nat -> Nat -> Type
 GTE left right = LTE right left

libs/base/Data/So.idr

@@ -60,9 +60,7 @@ export
 soOr : {a : Bool} -> So (a || b) -> Either (So a) (So b)
 soOr soab with (choose a)
   soOr {a=True}  _    | Left Oh = Left Oh
-  soOr {a=False} _    | Left Oh impossible
   soOr {a=False} soab | Right Oh = Right soab
-  soOr {a=True}  _    | Right Oh impossible
 
 export
 orSo : Either (So a) (So b) -> So (a || b)

src/Core/CaseBuilder.idr

@@ -798,11 +798,19 @@ mutual
   -- has the most distinct constructors (via pickNext)
   match {todo = (_ :: _)} fc fn phase clauses err
       = do (n ** MkNVar next) <- pickNext fc phase fn (map getNPs clauses)
+           log "compile.casetree" 25 $ "Picked " ++ show n ++ " as the next split"
            let clauses' = map (shuffleVars next) clauses
+           log "compile.casetree" 25 $ "Using clauses " ++ show clauses'
            let ps = partition phase clauses'
-           maybe (pure (Unmatched "No clauses"))
-                 Core.pure
-                !(mixture fc fn phase ps err)
+           log "compile.casetree" 25 $ "Got Partition " ++ show ps
+           mix <- mixture fc fn phase ps err
+           case mix of
+             Nothing =>
+               do log "compile.casetree" 25 "match: No clauses"
+                  pure (Unmatched "No clauses")
+             Just m =>
+               do log "compile.casetree" 25 $ "match: new case tree " ++ show m
+                  Core.pure m
   match {todo = []} fc fn phase [] err
        = maybe (pure (Unmatched "No patterns"))
                pure err
@@ -915,7 +923,10 @@ mkPat args orig (Ref fc Func n)
        mtm <- normalisePrims (const True) isPConst prims n args orig []
        case mtm of
          Just tm => mkPat [] tm tm
-         Nothing => pure $ PUnmatchable (getLoc orig) orig
+         Nothing =>
+           do log "compile.casetree" 10 $
+                "Unmatchable function: " ++ show n
+              pure $ PUnmatchable (getLoc orig) orig
 mkPat args orig (Bind fc x (Pi _ _ _ s) t)
     = let t' = subst (Erased fc False) t in
       pure $ PArrow fc x !(mkPat [] s s) !(mkPat [] t' t')
@@ -933,7 +944,10 @@ mkPat args orig (PrimVal fc c)
          then PConst fc c
          else PTyCon fc (UN (show c)) 0 []
 mkPat args orig (TType fc) = pure $ PTyCon fc (UN "Type") 0 []
-mkPat args orig tm = pure $ PUnmatchable (getLoc orig) orig
+mkPat args orig tm
+   = do log "compile.casetree" 10 $
+          "Catchall: marking " ++ show tm ++ " as unmatchable"
+        pure $ PUnmatchable (getLoc orig) orig
 
 export
 argToPat : {auto c : Ref Ctxt Defs} -> ClosedTerm -> Core Pat
@@ -951,6 +965,9 @@ mkPatClause fc fn args ty pid (ps, rhs)
                do defs <- get Ctxt
                   nty <- nf defs [] ty
                   ns <- mkNames args ps eq (Just nty)
+                  log "compile.casetree" 20 $
+                    "Make pat clause for names " ++ show ns
+                     ++ " in LHS " ++ show ps
                   pure (MkPatClause [] ns pid
                           (rewrite sym (appendNilRightNeutral args) in
                                    (weakenNs (mkSizeOf args) rhs))))
@@ -1043,7 +1060,7 @@ simpleCase : {auto c : Ref Ctxt Defs} ->
 simpleCase fc phase fn ty def clauses
     = do logC "compile.casetree" 5 $
                 do cs <- traverse (\ (c,d) => [| MkPair (toFullNames c) (toFullNames d) |]) clauses
-                   pure $ "Clauses:\n" ++ show (
+                   pure $ "simpleCase: Clauses:\n" ++ show (
                      indent {ann = ()} 2 $ vcat $ flip map cs $ \ (lrhs) =>
                        pretty {ann = ()} (fst lrhs) <++> pretty "=" <++> pretty (snd lrhs))
          ps <- traverse (toPatClause fc fn) clauses
@@ -1070,7 +1087,8 @@ getPMDef : {auto c : Ref Ctxt Defs} ->
 -- for the type, which we can use in coverage checking to ensure that one of
 -- the arguments has an empty type
 getPMDef fc phase fn ty []
-    = do defs <- get Ctxt
+    = do log "compile.casetree" 20 "getPMDef: No clauses!"
+         defs <- get Ctxt
          pure (!(getArgs 0 !(nf defs [] ty)) ** (Unmatched "No clauses", []))
   where
     getArgs : Int -> NF [] -> Core (List Name)
@@ -1083,6 +1101,8 @@ getPMDef fc phase fn ty clauses
     = do defs <- get Ctxt
          let cs = map (toClosed defs) (labelPat 0 clauses)
          (_ ** t) <- simpleCase fc phase fn ty Nothing cs
+         logC "compile.casetree" 20 $
+           pure $ "Compiled to: " ++ show !(toFullNames t)
          let reached = findReached t
          pure (_ ** (t, getUnreachable 0 reached clauses))
   where

src/Core/Context.idr

@@ -1730,7 +1730,7 @@ addHintFor fc tyn_in hintn_in direct loading
 
 export
 addGlobalHint : {auto c : Ref Ctxt Defs} ->
-					      Name -> Bool -> Core ()
+                Name -> Bool -> Core ()
 addGlobalHint hintn_in isdef
     = do defs <- get Ctxt
          hintn <- toResolvedNames hintn_in

src/Core/Coverage.idr

@@ -10,6 +10,7 @@ import Core.Value
 
 import Libraries.Data.Bool.Extra
 import Data.List
+import Data.Strings
 import Libraries.Data.NameMap
 
 import Libraries.Text.PrettyPrint.Prettyprinter
@@ -380,6 +381,10 @@ getMissing fc n ctree
    = do defs <- get Ctxt
         let psIn = map (Ref fc Bound) vars
         pats <- buildArgs fc defs [] [] psIn ctree
+        logC "coverage.missing" 20 $ map unlines $
+          flip traverse (concat pats) $ \ pat =>
+            do pat' <- toFullNames pat
+               pure (show pat')
         pure (map (apply fc (Ref fc Func n)) pats)
 
 -- For the given name, get the names it refers to which are not themselves

src/Core/Normalise.idr

@@ -1232,9 +1232,10 @@ logEnv : {vars : _} ->
          String -> Nat -> String -> Env Term vars -> Core ()
 logEnv str n msg env
     = do opts <- getSession
-         if keepLog lvl (logLevel opts)
-            then dumpEnv env
-            else pure ()
+         when (keepLog lvl (logLevel opts)) $ do
+           coreLift (putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg)
+           dumpEnv env
+
   where
     lvl : LogLevel
     lvl = mkLogLevel str n

src/TTImp/Impossible.idr

@@ -44,13 +44,13 @@ match nty (n, i, rty)
     sameRet _ _ = pure False
 
 dropNoMatch : {auto c : Ref Ctxt Defs} ->
-              Maybe (NF []) -> List (Name, Int, ClosedTerm) ->
-              Core (List (Name, Int, ClosedTerm))
+              Maybe (NF []) -> List (Name, Int, GlobalDef) ->
+              Core (List (Name, Int, GlobalDef))
 dropNoMatch _ [t] = pure [t]
 dropNoMatch Nothing ts = pure ts
 dropNoMatch (Just nty) ts
     = -- if the return type of a thing in ts doesn't match nty, drop it
-      filterM (match nty) ts
+      filterM (match nty . map (map type)) ts
 
 nextVar : {auto q : Ref QVar Int} ->
           FC -> Core (Term [])
@@ -133,12 +133,22 @@ mutual
            when (n `elem` prims) $
                throw (InternalError "Can't deal with constants here yet")
 
-           tys <- lookupTyName n (gamma defs)
-           [(n', _, ty)] <- dropNoMatch mty tys
+           gdefs <- lookupNameBy id n (gamma defs)
+           [(n', _, gdef)] <- dropNoMatch mty gdefs
               | [] => throw (UndefinedName fc n)
               | ts => throw (AmbiguousName fc (map fst ts))
-           tynf <- nf defs [] ty
-           processArgs (Ref fc Func n') tynf exps autos named
+           tynf <- nf defs [] (type gdef)
+           -- #899 we need to make sure that type & data constructors are marked
+           -- as such so that the coverage checker actually uses the matches in
+           -- `impossible` branches to generate parts of the case tree.
+           -- When `head` is `Func`, the pattern will be marked as forced and
+           -- the coverage checker will considers that all the cases have been
+           -- covered!
+           let head = case definition gdef of
+                        DCon t a _ => DataCon t a
+                        TCon t a _ _ _ _ _ _ => TyCon t a
+                        _ => Func
+           processArgs (Ref fc head n') tynf exps autos named
 
   mkTerm : {auto c : Ref Ctxt Defs} ->
            {auto q : Ref QVar Int} ->

src/TTImp/ProcessDef.idr

@@ -855,7 +855,7 @@ processDef opts nest env fc n_in cs_in
     getClause : Either RawImp Clause -> Core (Maybe Clause)
     getClause (Left rawlhs)
         = catch (do lhsp <- getImpossibleTerm env nest rawlhs
-                    log "declare.def" 3 $ "Generated impossible LHS: " ++ show lhsp
+                    log "declare.def.impossible" 3 $ "Generated impossible LHS: " ++ show lhsp
                     pure $ Just $ MkClause [] lhsp (Erased (getFC rawlhs) True))
                 (\e => do log "declare.def" 5 $ "Error in getClause " ++ show e
                           pure Nothing)
@@ -866,6 +866,7 @@ processDef opts nest env fc n_in cs_in
                     Core Covering
     checkCoverage n ty mult cs
         = do covcs' <- traverse getClause cs -- Make stand in LHS for impossible clauses
+             log "declare.def" 5 $ "Using clauses :" ++ show !(traverse toFullNames covcs')
              let covcs = mapMaybe id covcs'
              (_ ** (ctree, _)) <-
                  getPMDef fc (CompileTime mult) (Resolved n) ty covcs

tests/Main.idr

@@ -53,7 +53,7 @@ idrisTestsCoverage = MkTestPool []
        -- Coverage checking
       ["coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006", "coverage007", "coverage008",
-       "coverage009", "coverage010", "coverage011"]
+       "coverage009", "coverage010", "coverage011", "coverage012"]
 
 idrisTestsError : TestPool
 idrisTestsError = MkTestPool []

tests/idris2/coverage012/Issue899.idr

@@ -0,0 +1,4 @@
+%default total
+
+zeroImpossible : (k : Nat) -> k === Z -> Void
+zeroImpossible (S k) eq impossible

tests/idris2/coverage012/expected

@@ -0,0 +1,12 @@
+1/1: Building Issue899 (Issue899.idr)
+Error: zeroImpossible is not covering.
+
+Issue899.idr:3:1--3:46
+ 1 | %default total
+ 2 | 
+ 3 | zeroImpossible : (k : Nat) -> k === Z -> Void
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    zeroImpossible 0 _
+

tests/idris2/coverage012/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --check Issue899.idr
+
+rm -rf build

tests/idris2/reflection004/refdecl.idr

@@ -3,13 +3,12 @@ import Data.Vect
 import Language.Reflection
 
 %language ElabReflection
-
 axes : (n : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Vect n String
 axes 1 = ["x"]
 axes 2 = "y" :: axes 1
 axes 3 = "z" :: axes 2
 axes 4  = "w" :: axes 3
-axes (S (S (S (S (S _))))) {lte = (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc _)))))} impossible
+axes (S (S (S (S (S _))))) {lte} = absurd lte
 
 mkPoint : (n : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Decl
 mkPoint n