%default doesn't affect interface methods

The required totality of interface methods is now only affected if
there's an explicit modifier on the method. This allows us to set
%default total on the Prelude, which is a good thing to do anyway,
without also requiring that every implementation of the interface in the
prelude has to be total, which would potentially be a pain.

Another good affect is that it speeds up totality checking elsewhere
because totality checking is done lazily, and so with the total flag set
we know in advance that prelude functions are total.

libs/prelude/Prelude.idr

@@ -3,6 +3,8 @@ module Prelude
 import public Builtin
 import public PrimIO
 
+%default total
+
 {-
 The Prelude is minimal (since it is effectively part of the language
 specification, this seems to be desirable - we should, nevertheless, aim to

src/Core/Binary.idr

@@ -30,7 +30,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 30
+ttcVersion = 31
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Idris/Elab/Implementation.idr

@@ -215,6 +215,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                unsetFlag fc impName BlockedHint
 
                setFlag fc impName TCInline
+               -- it's the methods we're interested in, not the implementation
+               setFlag fc impName (SetTotal PartialOK)
 
                -- 4. (TODO: Order method bodies to be in declaration order, in
                --    case of dependencies)
@@ -274,7 +276,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     -- inserted in the right place
     mkMethField : List (Name, RigCount, RawImp) ->
                   List (Name, List (Name, RigCount, PiInfo RawImp)) ->
-                  (Name, Name, List (String, String), RigCount, TotalReq, RawImp) -> RawImp
+                  (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> RawImp
     mkMethField methImps fldTys (topn, n, upds, c, treq, ty)
         = let argns = map applyUpdate (maybe [] id (lookup (dropNS topn) fldTys))
               imps = map fst methImps in
@@ -315,8 +317,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     topMethType : List (Name, RawImp) ->
                   Name -> List (Name, RigCount, RawImp) ->
                   List String -> List Name -> List Name ->
-                  (Name, RigCount, TotalReq, (Bool, RawImp)) ->
-                  Core ((Name, Name, List (String, String), RigCount, TotalReq, RawImp),
+                  (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) ->
+                  Core ((Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp),
                            List (Name, RawImp))
     topMethType methupds impName methImps impsp pnames allmeths (mn, c, treq, (d, mty_in))
         = do -- Get the specialised type by applying the method to the
@@ -357,17 +359,18 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     topMethTypes : List (Name, RawImp) ->
                    Name -> List (Name, RigCount, RawImp) ->
                    List String -> List Name -> List Name ->
-                   List (Name, RigCount, TotalReq, (Bool, RawImp)) ->
-                   Core (List (Name, Name, List (String, String), RigCount, TotalReq, RawImp))
+                   List (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) ->
+                   Core (List (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp))
     topMethTypes upds impName methImps impsp pnames allmeths [] = pure []
     topMethTypes upds impName methImps impsp pnames allmeths (m :: ms)
         = do (m', newupds) <- topMethType upds impName methImps impsp pnames allmeths m
              ms' <- topMethTypes (newupds ++ upds) impName methImps impsp pnames allmeths ms
              pure (m' :: ms')
 
-    mkTopMethDecl : (Name, Name, List (String, String), RigCount, TotalReq, RawImp) -> ImpDecl
+    mkTopMethDecl : (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> ImpDecl
     mkTopMethDecl (mn, n, upds, c, treq, mty)
-        = IClaim fc c vis (Totality treq :: opts_in) (MkImpTy fc n mty)
+        = let opts = maybe opts_in (\t => Totality t :: opts_in) treq in
+              IClaim fc c vis opts (MkImpTy fc n mty)
 
     -- Given the method type (result of topMethType) return the mapping from
     -- top level method name to current implementation's method name
@@ -418,7 +421,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                    "Implementation body can only contain definitions")
 
     addTransform : Name -> List (Name, Name) ->
-                   (Name, RigCount, TotalReq, Bool, RawImp) ->
+                   (Name, RigCount, Maybe TotalReq, Bool, RawImp) ->
                    Core ()
     addTransform iname ns (top, _, _, _, ty)
         = do log 3 $ "Adding transform for " ++ show top ++ " : " ++ show ty ++

src/Idris/Elab/Interface.idr

@@ -243,9 +243,9 @@ updateIfaceSyn iname cn ps cs ms ds
     findSetTotal (_ :: xs) = findSetTotal xs
 
     totMeth : (Name, RigCount, List FnOpt, (Bool, RawImp)) ->
-              Core (Name, RigCount, TotalReq, (Bool, RawImp))
+              Core (Name, RigCount, Maybe TotalReq, (Bool, RawImp))
     totMeth (n, c, opts, t)
-        = do let treq = fromMaybe !getDefaultTotalityOption (findSetTotal opts)
+        = do let treq = findSetTotal opts
              pure (n, c, treq, t)
 
 export

src/Idris/Syntax.idr

@@ -503,7 +503,7 @@ record IFaceInfo where
   iconstructor : Name
   params : List Name
   parents : List RawImp
-  methods : List (Name, RigCount, TotalReq, Bool, RawImp)
+  methods : List (Name, RigCount, Maybe TotalReq, Bool, RawImp)
      -- ^ name, whether a data method, and desugared type (without constraint)
   defaults : List (Name, List ImpClause)
 

src/TTImp/TTImp.idr

@@ -328,7 +328,7 @@ mutual
 
   export
   Show ImpDecl where
-    show (IClaim _ _ _ _ ty) = show ty
+    show (IClaim _ _ _ opts ty) = show opts ++ " " ++ show ty
     show (IData _ _ d) = show d
     show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")"
     show (IParameters _ ps ds)