[ warning ] Warn user when impossible clauses are ignored

dunhamsteve · CodingCellist · commit ce0417e5a5db · 2025-11-14T22:09:32.000Z
diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
@@ -37,6 +37,12 @@ should target this file (`CHANGELOG_NEXT`).
 
 ### Backend changes
 
+### Compiler changes
+
+* The compiler now warns the user when `impossible` clauses are ignored. This
+  typically happens when a numeric literal or an ambiguous name appears in an
+  `impossible` clause.
+
 #### RefC Backend
 
 * Fixed an issue to do with `alligned_alloc` not existing on older MacOS
diff --git a/libs/base/Data/Colist1.idr b/libs/base/Data/Colist1.idr
@@ -54,7 +54,6 @@ repeat v = v ::: repeat v
 ||| Create a `Colist1` of `n` replications of the given element.
 public export
 replicate : (n : Nat) -> {auto 0 prf : IsSucc n} -> a -> Colist1 a
-replicate 0     _ impossible
 replicate (S k) x = x ::: replicate k x
 
 ||| Produce a `Colist1` by repeating a sequence
@@ -133,7 +132,6 @@ tail (_ ::: t) = t
 ||| Take up to `n` elements from a `Colist1`
 public export
 take : (n : Nat) -> {auto 0 prf : IsSucc n} -> Colist1 a -> List1 a
-take 0     _          impossible
 take (S k) (x ::: xs) = x ::: take k xs
 
 ||| Take elements from a `Colist1` up to and including the
diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr
@@ -288,7 +288,6 @@ gt left right = lt right left
 
 export
 lteReflectsLTE : (k : Nat) -> (n : Nat) -> lte k n === True -> k `LTE` n
-lteReflectsLTE (S k)  0    _ impossible
 lteReflectsLTE 0      0    _   = LTEZero
 lteReflectsLTE 0     (S k) _   = LTEZero
 lteReflectsLTE (S k) (S j) prf = LTESucc (lteReflectsLTE k j prf)
@@ -305,8 +304,6 @@ public export
 ltOpReflectsLT : (m,n : Nat) -> So (m < n) -> LT m n
 ltOpReflectsLT 0     (S k) prf = LTESucc LTEZero
 ltOpReflectsLT (S k) (S j) prf = LTESucc (ltOpReflectsLT k j prf)
-ltOpReflectsLT (S k) 0     prf impossible
-ltOpReflectsLT 0 0         prf impossible
 
 export
 gtReflectsGT : (k : Nat) -> (n : Nat) -> gt k n === True -> k `GT` n
diff --git a/libs/base/Data/Nat/Order/Properties.idr b/libs/base/Data/Nat/Order/Properties.idr
@@ -83,8 +83,6 @@ minusLTE (S a) (S b) =
 ||| Subtracting a positive number gives a strictly smaller number
 export
 minusPosLT : (a,b : Nat) -> 0 `LT` a -> a `LTE` b -> (b `minus` a) `LT` b
-minusPosLT 0     b     z_lt_z           a_lte_b impossible
-minusPosLT (S a) 0     z_lt_sa          a_lte_b impossible
 minusPosLT (S a) (S b) z_lt_sa          a_lte_b = LTESucc (minusLTE a b)
 
 -- This is the opposite of the convention in `Data.Nat`, but 'monotone on the left' means the below
diff --git a/libs/contrib/Data/Fin/Extra.idr b/libs/contrib/Data/Fin/Extra.idr
@@ -80,7 +80,6 @@ modFin :  (n : Nat)
        -> (m : Nat)
        -> {auto mNZ : NonZero m}
        -> Fin m
-modFin n 0 impossible
 modFin 0 (S k) = FZ
 modFin (S j) (S k) =
   let n' : Nat
diff --git a/libs/contrib/Data/Nat/Order/Strict.idr b/libs/contrib/Data/Nat/Order/Strict.idr
@@ -8,7 +8,6 @@ import Decidable.Order.Strict
 
 public export
 Irreflexive Nat LT where
-  irreflexive {x = 0} _ impossible
   irreflexive {x = S _} (LTESucc prf) =
     irreflexive {rel = Nat.LT} prf
 
diff --git a/libs/contrib/Data/Nat/Properties.idr b/libs/contrib/Data/Nat/Properties.idr
@@ -22,8 +22,6 @@ export
 multRightCancel : (a,b,r : Nat) -> (0 _ : NonZero r) -> a*r = b*r -> a = b
 multRightCancel a      b    0           r_nz ar_eq_br = void (absurd r_nz)
 multRightCancel 0      0    r@(S predr) r_nz ar_eq_br = Refl
-multRightCancel 0     (S b) r@(S predr) r_nz ar_eq_br impossible
-multRightCancel (S a)  0    r@(S predr) r_nz ar_eq_br impossible
 multRightCancel (S a) (S b) r@(S predr) r_nz ar_eq_br =
   cong S $ multRightCancel a b r r_nz
          $ plusLeftCancel r (a*r) (b*r) ar_eq_br
diff --git a/libs/papers/Language/IntrinsicTyping/Krivine.idr b/libs/papers/Language/IntrinsicTyping/Krivine.idr
@@ -614,7 +614,6 @@ namespace Machine
           (trace (Element ctx (snd pctx)) sc (Element (arg :: env) (fst pctx, penv)) tr)
   trace (Element [] pctx) (Lam sc) env tr
     = case tr of
-        Beta {arg = Element _ _, ctx = Element _ _} _ impossible
         Done sc .(fst env) => rewrite irrelevantUnit pctx in Done
 
   public export
diff --git a/src/TTImp/Impossible.idr b/src/TTImp/Impossible.idr
@@ -19,7 +19,7 @@ import Data.List
 -- only guessing! But we can still do some type-directed disambiguation of
 -- names.
 -- Constants (fromInteger/fromString etc) won't be supported, because in general
--- they involve resoling interfaces - they'll just become unmatchable patterns.
+-- they involve resolving interfaces - they'll just become unmatchable patterns.
 
 match : {auto c : Ref Ctxt Defs} ->
         ClosedNF -> (Name, Int, ClosedTerm) -> Core Bool
@@ -57,11 +57,11 @@ nextVar fc
          put QVar (i + 1)
          pure (Ref fc Bound (MN "imp" i))
 
-badClause : ClosedTerm -> List RawImp -> List RawImp -> List (Name, RawImp) -> Core a
+badClause : {auto c : Ref Ctxt Defs} -> ClosedTerm -> List RawImp -> List RawImp -> List (Name, RawImp) -> Core a
 badClause fn exps autos named
    = throw (GenericMsg (getLoc fn)
             ("Badly formed impossible clause "
-               ++ show (fn, exps, autos, named)))
+               ++ show (!(toFullNames fn), exps, autos, named)))
 
 mutual
   processArgs : {auto c : Ref Ctxt Defs} ->
@@ -115,6 +115,8 @@ mutual
                            processArgs (App fc fn e') !(sc defs (toClosure defaultOpts Env.empty e'))
                                        exps [] named'
   processArgs fn ty [] [] [] = pure fn
+  processArgs fn ty (x :: _) autos named
+     = throw $ GenericMsg (getFC x) "Too many arguments"
   processArgs fn ty exps autos named
      = badClause fn exps autos named
 
@@ -129,11 +131,15 @@ mutual
       = do defs <- get Ctxt
            prims <- getPrimitiveNames
            when (n `elem` prims) $
-               throw (InternalError "Can't deal with constants here yet")
+               throw (GenericMsg fc "Can't deal with \{show n} in impossible clauses yet")
 
            gdefs <- lookupNameBy id n (gamma defs)
-           [(n', i, gdef)] <- dropNoMatch !(traverseOpt (evalClosure defs) mty) gdefs
-              | ts => ambiguousName fc n (map fst ts)
+           mty' <- traverseOpt (evalClosure defs) mty
+           [(n', i, gdef)] <- dropNoMatch mty' gdefs
+              | [] => if length gdefs == 0
+                        then undefinedName fc n
+                        else throw $ GenericMsg fc "\{show n} does not match expected type"
+              | ts => throw $ AmbiguousName fc (map fst ts)
            tynf <- nf defs Env.empty (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
@@ -165,6 +171,9 @@ mutual
   mkTerm (IMustUnify fc r tm) mty exps autos named
      = Erased fc . Dotted <$> mkTerm tm mty exps autos named
   mkTerm (IPrimVal fc c) _ _ _ _ = pure (PrimVal fc c)
+  -- We're taking UniqueDefault here, _and_ we're falling through to nextVar otherwise, which is sketchy.
+  -- On option is to try each and emit an AmbiguousElab?  We maybe should respect `UniqueDefault` if there
+  -- is no evidence (mty), but we should _try_ to resolve here if there is an mty.
   mkTerm (IAlternative _ (UniqueDefault tm) _) mty exps autos named
      = mkTerm tm mty exps autos named
   mkTerm tm _ _ _ _ = nextVar (getFC tm)
diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr
@@ -1122,6 +1122,7 @@ processDef opts nest env fc n_in cs_in
                     log "declare.def.impossible" 3 $ "Generated impossible LHS: " ++ show lhsp
                     pure $ Just $ MkClause Env.empty lhsp (Erased (getFC rawlhs) Impossible))
                 (\e => do log "declare.def" 5 $ "Error in getClause " ++ show e
+                          recordWarning $ GenericWarn (fromMaybe (getFC rawlhs) $ getErrorLoc e) (show e)
                           pure Nothing)
     getClause (Right c) = pure (Just c)
 
diff --git a/tests/idris2/coverage/coverage001/expected b/tests/idris2/coverage/coverage001/expected
@@ -15,3 +15,13 @@ Vect2:8:1--8:21
      ^^^^^^^^^^^^^^^^^^^^
 
 1/1: Building Vect3 (Vect3.idr)
+Warning: Vect3:9:8--9:9:Z does not match expected type
+
+Vect3:9:8--9:9
+ 5 |      Nil  : Vect Z a
+ 6 |      (::) : a -> Vect k a -> Vect (S k) a
+ 7 | 
+ 8 | zip : Vect n a -> Vect n b -> Vect n (a, b)
+ 9 | zip [] Z impossible
+            ^
+
diff --git a/tests/idris2/coverage/coverage021/expected b/tests/idris2/coverage/coverage021/expected
@@ -1,4 +1,14 @@
 1/1: Building Issue2250a (Issue2250a.idr)
+Warning: Issue2250a:15:5--15:9:Refl does not match expected type
+
+Issue2250a:15:5--15:9
+ 11 | Ex1 : 3 `LessThanOrEqualTo` 5
+ 12 | Ex1 = Choose 2
+ 13 | 
+ 14 | Bug : Not (3 `LessThanOrEqualTo` 5)
+ 15 | Bug Refl impossible
+          ^^^^
+
 Error: Bug is not covering.
 
 Issue2250a:14:1--14:36
@@ -24,6 +34,16 @@ Issue2250a:17:1--17:13
 
 Calls non covering function Main.Bug
 1/1: Building Issue2250b (Issue2250b.idr)
+Warning: Issue2250b:6:3--6:4:Z does not match expected type
+
+Issue2250b:6:3--6:4
+ 2 | 
+ 3 | %default total
+ 4 | 
+ 5 | f : n `LTE` m -> Void
+ 6 | f Z impossible
+       ^
+
 Error: f is not covering.
 
 Issue2250b:5:1--5:22
@@ -49,6 +69,15 @@ Issue2250b:9:1--9:9
 
 Calls non covering function Main.f
 1/1: Building Issue2250c (Issue2250c.idr)
+Warning: Issue2250c:4:3--4:5:MkUnit does not match expected type
+
+Issue2250c:4:3--4:5
+ 1 | %default total
+ 2 | 
+ 3 | g : Not Bool
+ 4 | g () impossible
+       ^^
+
 Error: f is not covering.
 
 Issue2250c:6:1--6:9
@@ -72,6 +101,16 @@ Missing cases:
     g _
 
 1/1: Building Issue3276 (Issue3276.idr)
+Warning: Issue3276:20:23--20:27:Refl does not match expected type
+
+Issue3276:20:23--20:27
+ 16 | prf1 : Digit 51
+ 17 | prf1 = MkDigit 51
+ 18 | 
+ 19 | dis0 : Digit 51 -> Void
+ 20 | dis0 (MkDigit _ {prf1=Refl}) impossible
+                            ^^^^
+
 Error: dis0 is not covering.
 
 Issue3276:19:1--19:24
@@ -86,6 +125,16 @@ Missing cases:
     dis0 _
 
 1/1: Building Visibility (Visibility.idr)
+Warning: Visibility:8:6--8:7:Z does not match expected type
+
+Visibility:8:6--8:7
+ 4 |     data Foo : Type where
+ 5 |         MkFoo : Foo
+ 6 | 
+ 7 | boom : Foo -> Void
+ 8 | boom Z impossible
+          ^
+
 Error: boom is not covering.
 
 Visibility:7:1--7:19
@@ -100,6 +149,25 @@ Missing cases:
     boom _
 
 1/1: Building Head (Head.idr)
+Warning: Head:4:6--4:8:MkUnit does not match expected type
+
+Head:4:6--4:8
+ 1 | total
+ 2 | head : List a -> a
+ 3 | head (x :: xs) = x
+ 4 | head () impossible
+          ^^
+
+Warning: Head:9:7--9:8:Z does not match expected type
+
+Head:9:7--9:8
+ 5 | 
+ 6 | total
+ 7 | head' : List a -> a
+ 8 | head' (x :: xs) = x
+ 9 | head' Z impossible
+           ^
+
 Error: head is not covering.
 
 Head:1:1--2:19
diff --git a/tests/idris2/total/total003/Total.idr b/tests/idris2/total/total003/Total.idr
@@ -18,10 +18,6 @@ matchInt : (0 x : Integer) -> (n : Nat) -> IntNat x n -> String
 matchInt 0 Z IsZero = "Zero"
 matchInt 1 (S k) IsSuc = "Non Zero"
 
--- Should be identified as covering but isn't yet since the checker requires
--- a catch all case. This does at least test that the declared 'impossible'
--- case really is impossible; we can update it when the checker improves!
 matchInt' : (x : Integer) -> (n : Nat) -> IntNat x n -> String
 matchInt' 0 Z IsZero = "Zero"
 matchInt' 1 (S k) IsSuc = "Non Zero"
-matchInt' 0 (S k) x impossible
diff --git a/tests/idris2/warning/warning006/Issue2325.idr b/tests/idris2/warning/warning006/Issue2325.idr
@@ -0,0 +1,4 @@
+fnc : (a : Nat) -> (b : Nat) -> (a > b) = True -> Type
+fnc 0 0 Refl impossible
+fnc 0 (S _) Refl impossible
+fnc (S k) b prf = ?fnc_rhs_1
diff --git a/tests/idris2/warning/warning006/Main.idr b/tests/idris2/warning/warning006/Main.idr
@@ -0,0 +1,19 @@
+
+import Data.Vect
+
+-- fromInteger on LHS
+head : (n : Nat) -> {auto 0 prf : IsSucc n} -> Vect n a -> a
+head 0 _ impossible
+head (S k) (x :: xs) = x
+
+data Foo = Z | S Foo
+
+-- No matching constuctor of a known type
+head' : (n : Nat) -> {auto 0 prf : IsSucc n} -> (Foo,Foo) -> Vect n a -> a
+head' Z Z _ impossible
+head' (S k) _ (x :: xs) = x
+
+-- Ambiguous constructor of unknown type
+head'' : (n : Nat) -> {auto 0 prf : IsSucc n} -> (Foo,Foo) -> Vect n a -> a
+head'' Z (Z,_) _ impossible
+head'' (S k) _ (x :: xs) = x
diff --git a/tests/idris2/warning/warning006/expected b/tests/idris2/warning/warning006/expected
@@ -0,0 +1,56 @@
+1/1: Building Main (Main.idr)
+Warning: Main:6:6--6:7:Can't deal with fromInteger in impossible clauses yet
+
+Main:6:6--6:7
+ 2 | import Data.Vect
+ 3 | 
+ 4 | -- fromInteger on LHS
+ 5 | head : (n : Nat) -> {auto 0 prf : IsSucc n} -> Vect n a -> a
+ 6 | head 0 _ impossible
+          ^
+
+Warning: Main:13:9--13:10:Z does not match expected type
+
+Main:13:9--13:10
+ 09 | data Foo = Z | S Foo
+ 10 | 
+ 11 | -- No matching constuctor of a known type
+ 12 | head' : (n : Nat) -> {auto 0 prf : IsSucc n} -> (Foo,Foo) -> Vect n a -> a
+ 13 | head' Z Z _ impossible
+              ^
+
+Warning: Main:18:11--18:12:Ambiguous name [Main.Z, Prelude.Types.Z]
+
+Main:18:11--18:12
+ 14 | head' (S k) _ (x :: xs) = x
+ 15 | 
+ 16 | -- Ambiguous constructor of unknown type
+ 17 | head'' : (n : Nat) -> {auto 0 prf : IsSucc n} -> (Foo,Foo) -> Vect n a -> a
+ 18 | head'' Z (Z,_) _ impossible
+                ^
+
+1/1: Building Issue2325 (Issue2325.idr)
+Warning: Issue2325:2:5--2:6:Can't deal with fromInteger in impossible clauses yet
+
+Issue2325:2:5--2:6
+ 1 | fnc : (a : Nat) -> (b : Nat) -> (a > b) = True -> Type
+ 2 | fnc 0 0 Refl impossible
+         ^
+
+Warning: Issue2325:3:5--3:6:Can't deal with fromInteger in impossible clauses yet
+
+Issue2325:3:5--3:6
+ 1 | fnc : (a : Nat) -> (b : Nat) -> (a > b) = True -> Type
+ 2 | fnc 0 0 Refl impossible
+ 3 | fnc 0 (S _) Refl impossible
+         ^
+
+Error: fnc is not covering.
+
+Issue2325:1:1--1:55
+ 1 | fnc : (a : Nat) -> (b : Nat) -> (a > b) = True -> Type
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    fnc 0 _ _
+
diff --git a/tests/idris2/warning/warning006/run b/tests/idris2/warning/warning006/run
@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+check Main.idr
+check Issue2325.idr
