Improve rewriter for Fin.fromInteger

It now offers different errors when it couldn't prove the lemma due to
having a variable for the Integer, or when it couldn't prove it due to
having concrete values that are directly incorrect.

libs/base/Data/Fin.idr

@@ -1,6 +1,7 @@
 module Data.Fin
 
 %default total
+%access public
 
 ||| Numbers strictly less than some bound.  The name comes from "finite sets".
 |||
@@ -143,19 +144,35 @@ fromInteger {n} x {prf} with (integerToFin x n)
   fromInteger {n} x {prf = ItIsJust} | Just y = y
 
 %language ErrorReflection
-
+total private
+mkFinIntegerErr : TT -> TT -> List ErrorReportPart -> Maybe (List ErrorReportPart)
+mkFinIntegerErr lit finSize subErr
+  = Just [ TextPart "When using", TermPart lit
+         , TextPart "as a literal for a"
+         , TermPart `(Fin ~finSize)
+         , SubReport subErr
+         ]
 total
 finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)
+finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(TConst c) ~m)) err xs y)
+  = mkFinIntegerErr (TConst c) m
+      [ TermPart (TConst c)
+      , TextPart "is not strictly less than"
+      , TermPart m
+      ]
+finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m)) err xs y)
+  = mkFinIntegerErr (P Bound n t) m
+      [ TextPart "Could not show that", TermPart (P Bound n t)
+      , TextPart "is less than", TermPart m
+      , TextPart "because", TermPart (P Bound n t)
+      , TextPart "is a bound variable instead of a constant"
+      , TermPart (TConst (AType (ATInt ITBig)))
+      ]
 finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
-  = Just [ TextPart "When using", TermPart n
-         , TextPart "as a literal for a"
-         , TermPart `(Fin ~m)
-         , SubReport [ TextPart "Could not show that"
-                     , TermPart n
-                     , TextPart "is less than"
-                     , TermPart m
-                     ]
-         ]
+  = mkFinIntegerErr n m
+      [ TextPart "Could not show that" , TermPart n
+      , TextPart "is less than" , TermPart m
+      ]
 finFromIntegerErrors _ = Nothing
 
 %error_handlers Data.Fin.fromInteger prf finFromIntegerErrors

test/error005/error005.idr

@@ -18,3 +18,8 @@ ok n = 1
 
 notOk : (n : Nat) -> Fin (plus 2 n)
 notOk n = 2
+
+b0rken : Integer -> Fin 3
+b0rken n = fromInteger n
+
+

test/error005/expected

@@ -1,12 +1,16 @@
 error005.idr:13:1:When elaborating right hand side of two:
 When elaborating argument prf to function Data.Fin.fromInteger:
         When using 2 as a literal for a Fin 2 
-                Could not show that 2 is less than 2
+                2 is not strictly less than 2
 error005.idr:16:1:When elaborating right hand side of hahaha:
 When elaborating argument prf to function Data.Fin.fromInteger:
         When using 0 as a literal for a Fin n 
-                Could not show that 0 is less than n
-error005.idr:21:1:When elaborating right hand side of notOk:
+                0 is not strictly less than n
+error005.idr:22:1:When elaborating right hand side of notOk:
 When elaborating argument prf to function Data.Fin.fromInteger:
         When using 2 as a literal for a Fin (S (S n)) 
-                Could not show that 2 is less than S (S n)
+                2 is not strictly less than S (S n)
+error005.idr:23:24:When elaborating right hand side of b0rken:
+When elaborating argument prf to function Data.Fin.fromInteger:
+        When using n as a literal for a Fin 3 
+                Could not show that n is less than 3 because n is a bound variable instead of a constant Integer