All functions now need to be covering by default

This has caught a couple of things in the Idris 2 code base itself. Some
tests needed partial annotations too.

CHANGELOG.md

@@ -8,6 +8,9 @@ or build from the generated Scheme, using `make bootstrap`.
 Language changes:
 
 * `total`, `covering` and `partial` flags on functions now have an effect.
+* `%default <totality status>` has been implemented. By default, functions must
+  be at least `covering`
+  + That is, `%default covering` is the default status.
 * Fields of records can be accessed (and updated) using the dot syntax,
   such as `r.field1.field2` or `record { field1.field2 = 42 }`.
   For details, see https://idris2.readthedocs.io/en/latest/reference/records.html

docs/source/typedd/typedd.rst

@@ -77,6 +77,9 @@ confusing and potentially error prone. Instead, there is ``stringToNatOrZ`` in
 In ``Loops.idr`` and ``ReadNum.idr`` add ``import Data.Strings`` and change ``cast`` to
 ``stringToNatOrZ``
 
+In ``ReadNum.idr``, since functions must now be ``covering`` by default, add
+a ``partial`` annotation to ``readNumber_v2``.
+
 Chapter 6
 ---------
 
@@ -137,6 +140,9 @@ longer part of the prelude, so add ``import Decidable.Equality``.
 
 In ``ReverseVec.idr``, add ``import Data.Nat`` for the ``Nat`` proofs.
 
+In ``Void.idr``, since functions must now be ``covering`` by default, add
+a ``partial`` annotation to ``nohead`` and its helper function ``getHead``.
+
 Chapter 9
 ---------
 
@@ -306,6 +312,8 @@ In ``ArithCmd.idr``, update ``DivBy`` and ``import Data.Strings`` as above. Also
 since export rules are per-namespace now, rather than per-file, you need to
 export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``.
 
+In ``StreamFail.idr``, add a ``partial`` annotation to ``labelWith``.
+
 Chapter 12
 ----------
 

docs/source/updates/updates.rst

@@ -428,8 +428,11 @@ used with care. Too many hints can lead to a large search space!
 Totality and Coverage
 ---------------------
 
-``%default covering`` is now the default status [Actually still TODO, but
-planned soon!]
+``%default covering`` is now the default status, so all functions must cover
+all their inputs unless stated otherwise with a ``partial`` annotation, or
+switching to ``%default partial`` (which is not recommended - use a ``partial``
+annotation instead to have the smallest possible place where functions are
+partial).
 
 Build artefacts
 ---------------

libs/base/Data/Strings.idr

@@ -167,11 +167,11 @@ export
 toLower : String -> String
 toLower str = pack (map toLower (unpack str))
 
-export
+export partial
 strIndex : String -> Int -> Char
 strIndex = prim__strIndex
 
-export
+export partial
 strTail : String -> String
 strTail = prim__strTail
 

src/Core/Options.idr

@@ -159,7 +159,7 @@ defaultSession = MkSessionOpts False False False Chez 0 False False
 
 export
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True PartialOK 3 True
+defaultElab = MkElabDirectives True True CoveringOnly 3 True
 
 export
 defaults : Options

src/Idris/Elab/Interface.idr

@@ -393,6 +393,9 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
         changeName : Name -> ImpClause -> ImpClause
         changeName dn (PatClause fc lhs rhs)
             = PatClause fc (changeNameTerm dn lhs) rhs
+        changeName dn (WithClause fc lhs wval cs)
+            = WithClause fc (changeNameTerm dn lhs) wval
+                         (map (changeName dn) cs)
         changeName dn (ImpossibleClause fc lhs)
             = ImpossibleClause fc (changeNameTerm dn lhs)
 

src/Utils/Hex.idr

@@ -19,6 +19,7 @@ hexDigit 12 = 'c'
 hexDigit 13 = 'd'
 hexDigit 14 = 'e'
 hexDigit 15 = 'f'
+hexDigit _ = 'X' -- TMP HACK: Ideally we'd have a bounds proof, generated below
 
 ||| Convert a positive integer into a list of (lower case) hexadecimal characters
 export

src/Utils/Octal.idr

@@ -11,6 +11,7 @@ octDigit 4 = '4'
 octDigit 5 = '5'
 octDigit 6 = '6'
 octDigit 7 = '7'
+octDigit _ = 'X' -- TMP HACK: Ideally we'd have a bounds proof, generated below
 
 ||| Convert a positive integer into a list of octal characters
 export

tests/chez/chez006/TypeCase.idr

@@ -13,6 +13,7 @@ strangeId : {a : Type} -> a -> a
 strangeId {a=Integer} x = x+1
 strangeId x = x
 
+partial
 strangeId' : {a : Type} -> a -> a
 strangeId' {a=Integer} x = x+1
 

tests/chez/chez015/Numbers.idr

@@ -2,6 +2,8 @@ module Main
 
 import Data.List
 
+%default partial
+
 large : (a: Type) -> a
 -- integer larger than 64 bits
 large Integer = 3518437212345678901234567890123

tests/chez/chez019/expected

@@ -1,6 +1,6 @@
-ERROR: Unhandled input for Main.foo at partial.idr:2:1--4:1
+ERROR: Unhandled input for Main.foo at partial.idr:4:1--6:1
 2
-ERROR: Unhandled input for Main.lookup' at partial.idr:17:1--19:1
-ERROR: Unhandled input for Main.lookup' at partial.idr:17:1--19:1
+ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1
+ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1
 1/1: Building partial (partial.idr)
 Main> Main> Main> Main> Main> Bye for now!

tests/chez/chez019/partial.idr

@@ -1,3 +1,5 @@
+%default partial
+
 foo : Maybe a -> a
 foo (Just x) = x
 

tests/idris2/basic011/Dots1.idr

@@ -1,3 +1,4 @@
+partial
 bar : (n : Nat) -> (m : Nat) -> n = m -> Nat
 bar (S m) (S m) (Refl {x = S m}) = m
 

tests/idris2/basic018/Fin.idr

@@ -18,6 +18,7 @@ data IsJust : Maybe a -> Type where
      ItIsJust : IsJust (Just x)
 
 -- Testing that %allow_overloads lets this one through!
+partial
 fromInteger : {k : Nat} ->
               (n : Integer) ->
               {auto prf : IsJust (integerToFin n k)} ->

tests/idris2/basic018/expected

@@ -1,3 +1,3 @@
 1/1: Building Fin (Fin.idr)
-Fin.idr:33:7--35:1:While processing right hand side of bar at Fin.idr:33:1--35:1:
+Fin.idr:34:7--36:1:While processing right hand side of bar at Fin.idr:34:1--36:1:
 Can't find an implementation for IsJust (integerToFin 8 5)

tests/idris2/coverage001/Vect.idr

@@ -1,3 +1,5 @@
+%default partial
+
 data Vect : Nat -> Type -> Type where
      Nil  : Vect Z a
      (::) : a -> Vect k a -> Vect (S k) a

tests/idris2/coverage002/Vect.idr

@@ -1,3 +1,5 @@
+%default partial
+
 data Vect : Nat -> Type -> Type where
      Nil  : Vect Z a
      (::) : a -> Vect k a -> Vect (S k) a

tests/idris2/coverage003/Cover.idr

@@ -1,3 +1,5 @@
+%default partial
+
 foo : (Nat, Nat) -> Nat
 foo (Z, Z) = Z
 

tests/idris2/coverage003/expected

@@ -1,5 +1,5 @@
 1/1: Building Cover (Cover.idr)
-Cover.idr:14:1--14:8:While processing left hand side of badBar at Cover.idr:14:1--15:1:
+Cover.idr:16:1--16:8:While processing left hand side of badBar at Cover.idr:16:1--17:1:
 Can't match on 0 as it has a polymorphic type
 Main> Main.foo:
 foo (0, S _)

tests/idris2/coverage004/Cover.idr

@@ -1,3 +1,5 @@
+%default partial
+
 data Foo : Type -> Type where
      IsNat : Foo Nat
      IsBool : Foo Bool

tests/idris2/coverage004/expected

@@ -1,5 +1,5 @@
 1/1: Building Cover (Cover.idr)
-Cover.idr:12:1--12:5:While processing left hand side of bad at Cover.idr:12:1--13:1:
+Cover.idr:14:1--14:5:While processing left hand side of bad at Cover.idr:14:1--15:1:
 Can't match on Just (fromInteger 0) as it has a polymorphic type
 Main> Main.okay:
 okay (S _) IsNat

tests/idris2/coverage008/wcov.idr

@@ -1,3 +1,4 @@
+%default partial
 
 data Foo : Int -> Type where
      FZero : Foo 0

tests/idris2/interface001/IFace.idr

@@ -2,6 +2,8 @@ module IFace
 
 import Stuff
 
+%default partial
+
 infixl 5 ==, /=
 
 interface Eq b where

tests/idris2/interface001/IFace1.idr

@@ -2,6 +2,8 @@ module IFace1
 
 import Stuff
 
+%default partial
+
 infixl 5 ==, /=
 
 interface Eq b where

tests/idris2/total001/Total.idr

@@ -1,3 +1,5 @@
+%default partial
+
 data Vect : Nat -> Type -> Type where
      Nil : Vect Z a
      (::) : a -> Vect k a -> Vect (S k) a

tests/idris2/total003/Total.idr

@@ -1,3 +1,5 @@
+%default partial
+
 onlyOne : Int -> Int
 onlyOne 1 = 2
 

tests/typedd-book/chapter05/ReadNum.idr

@@ -23,6 +23,7 @@ readPair = do str1 <- getLine
               str2 <- getLine
               pure (str1, str2)
 
+partial
 readNumbers_v2 : IO (Maybe (Nat, Nat))
 readNumbers_v2 =
   do Just num1_ok <- readNumber

tests/typedd-book/chapter08/Void.idr

@@ -7,8 +7,10 @@ valueNotSuc _ Refl impossible
 loop : Void
 loop = loop
 
+partial
 nohead : Void
 nohead = getHead []
   where
+    partial
     getHead : List Void -> Void
     getHead (x :: xs) = x

tests/typedd-book/chapter11/StreamFail.idr

@@ -1,6 +1,7 @@
 countFrom : Integer -> List Integer
 countFrom n = n :: countFrom (n + 1)
 
+partial
 labelWith : List Integer -> List a -> List (Integer, a)
 labelWith lbls [] = []
 labelWith (lbl :: lbls) (val :: vals) = (lbl, val) :: labelWith lbls vals