Fix coverage checker issue

Don't use the type of a scrutinee to restrict possible patterns, because
it might have been refined by a Rig0 argument that has a missing case.
Instead, generate all the possible cases and check that the generated
ones are impossible (there's no obvious change in performance)

src/Core/CaseBuilder.idr

@@ -421,7 +421,7 @@ groupCons fc fn pvars cs
     -- The type of 'ConGroup' ensures that we refer to the arguments by
     -- the same name in each of the clauses
     addConG {todo} n tag pargs pats rhs [] 
-        = do cty <- the (Core (NF vars)) $if n == UN "->"
+        = do cty <- the (Core (NF vars)) $ if n == UN "->"
                       then pure $ NBind fc (MN "_" 0) (Pi RigW Explicit (NType fc)) $
                               (\d, a => pure $ NBind fc (MN "_" 1) (Pi RigW Explicit (NErased fc))
                                 (\d, a => pure $ NType fc))
@@ -689,9 +689,10 @@ pickNext' {ps = []} allowRig0 fc fn npss
 pickNext' {ps = q :: qs} allowRig0 fc fn npss
     = if samePat allowRig0 npss
          then pure (MkVar First)
-         else
-            do (MkVar var) <- pickNext' allowRig0 fc fn (map tail npss)
-               pure (MkVar (Later var))
+         else  case !(getScore fc fn npss) of
+                    Right () => pure (MkVar First)
+                    _ => do (MkVar var) <- pickNext' allowRig0 fc fn (map tail npss)
+                            pure (MkVar (Later var))
 
 -- Pick the leftmost matchable (non-Rig0) thing with all constructors in the
 -- same family, or all variables, or all the same type constructor.
@@ -702,8 +703,9 @@ pickNext : {auto i : Ref PName Int} ->
            FC -> Name -> List (NamedPats ns (p :: ps)) -> 
            Core (Var (p :: ps))
 pickNext fc fn npss
-    = catch (pickNext' False fc fn npss)
-            (\err => pickNext' True fc fn npss)
+    = pickNext' True fc fn npss
+--     = catch (pickNext' False fc fn npss)
+--             (\err => pickNext' True fc fn npss)
 
 moveFirst : {idx : Nat} -> .(el : IsVar name idx ps) -> NamedPats ns ps ->
             NamedPats ns (name :: dropVar ps el)

src/Core/Coverage.idr

@@ -81,30 +81,6 @@ getCons defs (NTCon _ tn _ _ _)
                   _ => pure Nothing
 getCons defs _ = pure []
 
-mutual
-  matchArgs : Defs -> List (Closure vars) -> List (Closure []) -> Core Bool
-  matchArgs defs [] [] = pure True
-  matchArgs defs (c :: cs) (c' :: cs') 
-      = do cnf <- evalClosure defs c 
-           cnf' <- evalClosure defs c'
-           pure $ !(matchNF defs cnf cnf') && !(matchArgs defs cs cs')
-  matchArgs defs _ _ = pure False
-
-  -- Is the first type a possible match for a constructor of the second type?
-  matchNF : Defs -> NF vars -> NF [] -> Core Bool
-  matchNF defs t (NBind fc x b sc)
-     = matchNF defs t !(sc defs (toClosure defaultOpts [] (Erased fc)))
-  matchNF defs (NDCon _ n t a args) (NDCon _ n' t' a' args')
-     = if t == t'
-          then matchArgs defs args args'
-          else pure False
-  matchNF defs (NTCon _ n t a args) (NTCon _ n' t' a' args')
-     = if n == n'
-          then matchArgs defs args args'
-          else pure False
-  matchNF defs (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')
-  matchNF _ _ _ = pure True
-
 emptyRHS : FC -> CaseTree vars -> CaseTree vars
 emptyRHS fc (Case idx el sc alts) = Case idx el sc (map emptyRHSalt alts)
   where
@@ -153,9 +129,8 @@ getMissingAlts fc defs (NType _) alts
     isDefault _ = False
 getMissingAlts fc defs nfty alts
     = do allCons <- getCons defs nfty 
-         validCons <- filterM (\x => matchNF defs nfty (fst x)) allCons
          pure (filter (noneOf alts) 
-                 (map (mkAlt fc (Unmatched "Coverage check") . snd) validCons))
+                 (map (mkAlt fc (Unmatched "Coverage check") . snd) allCons))
   where
     -- Return whether the alternative c matches none of the given cases in alts
     noneOf : List (CaseAlt vars) -> CaseAlt vars -> Bool

src/TTImp/ProcessDef.idr

@@ -613,7 +613,6 @@ processDef opts nest env fc n_in cs_in
          when (not (elem InCase opts)) $
            compileRunTime
 
-
          cov <- checkCoverage nidx mult cs tree_ct
          setCovering fc n cov
 

src/TTImp/ProcessType.idr

@@ -63,6 +63,11 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          log 1 $ "Processing " ++ show n
          log 5 $ "Checking type decl " ++ show n ++ " : " ++ show ty_raw
          idx <- resolveName n 
+
+         -- Check 'n' is undefined
+         defs <- get Ctxt
+         Nothing <- lookupCtxtExact (Resolved idx) (gamma defs)
+              | Just _ => throw (AlreadyDefined fc n)
          
          ty <- 
              wrapError (InType fc n) $

tests/idris2/coverage002/expected

@@ -3,6 +3,6 @@ Welcome to Idris 2 version 0.0. Enjoy yourself!
 Main> Main.append: All cases covered
 Main> Main.funny: All cases covered
 Main> Main.notFunny:
-notFunny [False, False, True, True]
-notFunny [False, True, True, True]
+notFunny (False :: (False :: (True :: (True :: _))))
+notFunny (False :: (True :: (True :: (True :: _))))
 Main> Bye for now!

tests/idris2/total003/expected

@@ -5,6 +5,5 @@ onlyOne _
 Main> Main.covered: All cases covered
 Main> Main.matchInt: All cases covered
 Main> Main.matchInt':
-matchInt' _ _ IsZero
-matchInt' _ _ IsSuc
+matchInt' _ _ _
 Main> Bye for now!