[ fix #3437 ] Add a check for multiple totality modifiers

src/Core/Context.idr

@@ -1628,6 +1628,14 @@ hasFlag fc n fl
               | Nothing => undefinedName fc n
          pure (fl `elem` flags def)
 
+export
+hasSetTotal : {auto c : Ref Ctxt Defs} -> FC -> Name -> Core Bool
+hasSetTotal fc n
+    = do defs <- get Ctxt
+         Just def <- lookupCtxtExact n (gamma defs)
+             | Nothing => undefinedName fc n
+         pure $ isJust $ findSetTotal def.flags
+
 export
 setSizeChange : {auto c : Ref Ctxt Defs} ->
                 FC -> Name -> List SCCall -> Core ()

src/Idris/Desugar.idr

@@ -1033,6 +1033,40 @@ mutual
   displayFixity (Just vis) NotBinding fix prec op = "\{show vis} \{show fix} \{show  prec} \{show op}"
   displayFixity (Just vis) bind fix prec op = "\{show vis} \{show bind} \{show fix} \{show  prec} \{show op}"
 
+  verifyTotalityModifiers : {auto c : Ref Ctxt Defs} ->
+                            FC -> List FnOpt -> Core ()
+  verifyTotalityModifiers fc opts =
+    when (count isTotalityReq opts > 1) $ do
+      let totalities = sort $ mapMaybe extractTotality opts
+      let dedupTotalities = dedup totalities
+      defaultTotality <- getDefaultTotalityOption
+      throw $ GenericMsgSol fc "Multiple totality modifiers" "Possible solutions" $
+        catMaybes $
+          [ checkDuplicates totalities dedupTotalities
+          , checkCompability dedupTotalities
+          , checkDefault defaultTotality dedupTotalities
+          ]
+    where
+      showModifiers : Show a => List a -> String
+      showModifiers = concat . intersperse ", " . map (\s => "`\{show s}`")
+
+      checkCompability : List TotalReq -> Maybe String
+      checkCompability totalities =
+        toMaybe (length totalities > 1) $
+          "Leave only one modifier out of " ++ showModifiers totalities
+
+      checkDuplicates : List TotalReq -> List TotalReq -> Maybe String
+      checkDuplicates totalities dedupTotalities =
+        toMaybe (totalities /= dedupTotalities) $ do
+          let repeated = filter (\x => count (x ==) totalities > 1) dedupTotalities
+          "Remove duplicates of " ++ showModifiers repeated
+
+      checkDefault : TotalReq -> List TotalReq -> Maybe String
+      checkDefault def totalities =
+        toMaybe (def `elem` totalities) $
+          "Remove modifiers " ++ showModifiers totalities ++
+          ", resulting in the default totality of " ++ showModifiers [def]
+
   -- Given a high level declaration, return a list of TTImp declarations
   -- which process it, and update any necessary state on the way.
   export
@@ -1044,6 +1078,8 @@ mutual
                 List Name -> PDecl -> Core (List ImpDecl)
   desugarDecl ps (PClaim (MkFCVal fc (MkPClaim rig vis fnopts ty)))
       = do opts <- traverse (desugarFnOpt ps) fnopts
+           verifyTotalityModifiers fc opts
+
            types <- desugarType ps ty
            pure $ flip (map {f = List, b = ImpDecl}) types $ \ty' =>
                       IClaim (MkFCVal fc $ MkIClaimData rig vis opts ty')
@@ -1136,6 +1172,8 @@ mutual
 
   desugarDecl ps (PImplementation fc vis fnopts pass is cons tn params impln nusing body)
       = do opts <- traverse (desugarFnOpt ps) fnopts
+           verifyTotalityModifiers fc opts
+
            is' <- for is $ \ (fc, c, n, pi, tm) =>
                      do tm' <- desugar AnyExpr ps tm
                         pi' <- mapDesugarPiInfo ps pi

src/Idris/Elab/Implementation.idr

@@ -466,8 +466,10 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
 
     mkTopMethDecl : (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> ImpDecl
     mkTopMethDecl (mn, n, upds, c, treq, mty)
-        = let opts = maybe opts_in (\t => Totality t :: opts_in) treq in
-              IClaim (MkFCVal vfc (MkIClaimData c vis opts (MkImpTy EmptyFC (NoFC n) mty)))
+        = do let opts = if isJust $ findTotality opts_in
+                          then opts_in
+                          else maybe opts_in (\t => Totality t :: opts_in) treq
+             IClaim $ MkFCVal vfc $ MkIClaimData c vis opts $ MkImpTy EmptyFC (NoFC n) mty
 
     -- Given the method type (result of topMethType) return the mapping from
     -- top level method name to current implementation's method name

src/Idris/Elab/Interface.idr

@@ -303,14 +303,9 @@ updateIfaceSyn iname cn impps ps cs ms ds
          update Syn { ifaces     $= addName iname info,
                       saveIFaces $= (iname :: ) }
  where
-    findSetTotal : List FnOpt -> Maybe TotalReq
-    findSetTotal [] = Nothing
-    findSetTotal (Totality t :: _) = Just t
-    findSetTotal (_ :: xs) = findSetTotal xs
-
     totMeth : Declaration -> Core Method
     totMeth decl
-        = do let treq = findSetTotal decl.flags
+        = do let treq = findTotality decl.flags
              pure $ MkMethod { name = decl.name
                              , count = decl.count
                              , totalReq = treq

src/TTImp/ProcessData.idr

@@ -441,6 +441,10 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw)
                       addHashWithNames fullty
                       log "module.hash" 15 "Adding hash for data declaration with name \{show n}"
 
+         whenJust mbtot $ \ tot => do
+             log "declare.data" 5 $ "setting totality flag for data declaration with name \{show n}"
+             setFlag fc n (SetTotal tot)
+
 processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw opts cons_raw)
     = do n <- inCurrentNS n_in
 
@@ -464,14 +468,15 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o
          let mfullty = map snd mmetasfullty
 
          -- If n exists, check it's the same type as we have here, is
-         -- a type constructor, and has either the same visibility or we don't define one.
+         -- a type constructor, and has either the same visibility and totality
+         -- or we don't define them.
          -- When looking up, note the data types which were undefined at the
          -- point of declaration.
          ndefm <- lookupCtxtExact n (gamma defs)
-         (mw, vis, fullty) <- the (Core (List Name, Visibility, ClosedTerm)) $ case ndefm of
+         (mw, vis, tot, fullty) <- the (Core (List Name, Visibility, Maybe TotalReq, ClosedTerm)) $ case ndefm of
                   Nothing => case mfullty of
                     Nothing => throw (GenericMsg fc "Missing telescope for data definition \{show n_in}")
-                    Just fullty => pure ([], collapseDefault def_vis, fullty)
+                    Just fullty => pure ([], collapseDefault def_vis, mbtot, fullty)
                   Just ndef => do
                     vis <- the (Core Visibility) $ case collapseDefaults ndef.visibility def_vis of
                       Right finalVis => pure finalVis
@@ -480,12 +485,25 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o
                         recordWarning (IncompatibleVisibility fc oldVis newVis n)
                         pure (max oldVis newVis)
 
+                    let declTot = findSetTotal $ ndef.flags
+                    tot <- case (mbtot, declTot) of
+                      (Just oldTot, Just newTot) => do
+                        when (oldTot /= newTot) $ throw $ GenericMsgSol fc
+                          "Data \{show n_in} has been forward-declared with totality `\{show oldTot}`, cannot change to `\{show newTot}`"
+                          "Possible solutions"
+                          [ "Use the same totality modifiers"
+                          , "Remove the totality modifier from the declaration"
+                          , "Remove the totality modifier from the definition"
+                          ]
+                        pure mbtot
+                      _ => pure $ mbtot <|> declTot
+
                     case definition ndef of
                       TCon _ _ _ _ _ mw [] _ => case mfullty of
-                        Nothing => pure (mw, vis, type ndef)
+                        Nothing => pure (mw, vis, tot, type ndef)
                         Just fullty =>
                             do ok <- convert defs [] fullty (type ndef)
-                               if ok then pure (mw, vis, fullty)
+                               if ok then pure (mw, vis, tot, fullty)
                                      else do logTermNF "declare.data" 1 "Previous" [] (type ndef)
                                              logTermNF "declare.data" 1 "Now" [] fullty
                                              throw (AlreadyDefined fc n)
@@ -545,6 +563,6 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o
          traverse_ updateErasable (Resolved tidx :: connames)
 
          -- #1404
-         whenJust mbtot $ \ tot => do
-             log "declare.data" 5 $ "setting totality flag for " ++ show n ++ " and its constructors"
+         whenJust tot $ \ tot => do
+             log "declare.data" 5 $ "setting totality flag for \{show n} and its constructors"
              for_ (n :: map name cons) $ \ n => setFlag fc n (SetTotal tot)

src/TTImp/ProcessFnOpt.idr

@@ -18,9 +18,17 @@ getRetTy defs ty
     = throw (GenericMsg (getLoc ty)
              "Can only add hints for concrete return types")
 
+%inline
+throwIf : {auto c : Ref Ctxt Defs} -> FC -> Bool -> String -> Core ()
+throwIf fc cond msg = when cond $ throw (GenericMsg fc msg)
+
+%inline
 throwIfHasFlag : {auto c : Ref Ctxt Defs} -> FC -> Name -> DefFlag -> String -> Core ()
-throwIfHasFlag fc ndef fl msg
-    = when !(hasFlag fc ndef fl) $ throw (GenericMsg fc msg)
+throwIfHasFlag fc ndef fl msg = throwIf fc !(hasFlag fc ndef fl) msg
+
+%inline
+throwIfHasTotality : {auto c : Ref Ctxt Defs} -> FC -> Name -> String -> Core ()
+throwIfHasTotality fc ndef msg = throwIf fc !(hasSetTotal fc ndef) msg
 
 export
 processFnOpt : {auto c : Ref Ctxt Defs} ->
@@ -35,7 +43,7 @@ processFnOpt fc _ ndef NoInline
     = do throwIfHasFlag fc ndef Inline "%inline and %noinline are mutually exclusive"
          setFlag fc ndef NoInline
 processFnOpt fc _ ndef Deprecate
-    =  setFlag fc ndef Deprecate
+    = setFlag fc ndef Deprecate
 processFnOpt fc _ ndef TCInline
     = setFlag fc ndef TCInline
 processFnOpt fc True ndef (Hint d)
@@ -62,7 +70,8 @@ processFnOpt fc _ ndef (ForeignExport _)
 processFnOpt fc _ ndef Invertible
     = setFlag fc ndef Invertible
 processFnOpt fc _ ndef (Totality tot)
-    = setFlag fc ndef (SetTotal tot)
+    = do throwIfHasTotality fc ndef "Multiple totality modifiers"
+         setFlag fc ndef (SetTotal tot)
 processFnOpt fc _ ndef Macro
     = setFlag fc ndef Macro
 processFnOpt fc _ ndef (SpecArgs ns)

src/TTImp/TTImp.idr

@@ -257,6 +257,15 @@ mutual
   isTotalityReq (Totality _) = True
   isTotalityReq _ = False
 
+  export
+  extractTotality : FnOpt' nm -> Maybe TotalReq
+  extractTotality (Totality t) = Just t
+  extractTotality _ = Nothing
+
+  export
+  findTotality : List (FnOpt' nm) -> Maybe TotalReq
+  findTotality = foldr (\elem, acc => extractTotality elem <|> acc) empty
+
   export
   covering
   Show nm => Show (FnOpt' nm) where

tests/idris2/total/total026/compilerOption.idr

@@ -0,0 +1,3 @@
+covering
+f : Int -> Int
+f i = f i

tests/idris2/total/total026/doubleTotal.idr

@@ -0,0 +1,4 @@
+total
+total
+f : ()
+f = ()

tests/idris2/total/total026/duplicates.idr

@@ -0,0 +1,7 @@
+total
+partial
+covering
+total
+partial
+f : ()
+f = ()

tests/idris2/total/total026/expected

@@ -0,0 +1,83 @@
+1/1: Building overrideDefault (overrideDefault.idr)
+------
+1/1: Building compilerOption (compilerOption.idr)
+------
+1/1: Building sameAsDefault (sameAsDefault.idr)
+------
+1/1: Building implementationOverride (implementationOverride.idr)
+------
+1/1: Building issue3437 (issue3437.idr)
+Error: Multiple totality modifiers
+
+issue3437:1:1--3:15
+ 1 | total
+ 2 | covering
+ 3 | f : Int -> Int
+
+Possible solutions:
+ - Leave only one modifier out of `covering`, `total`
+ - Remove modifiers `covering`, `total`, resulting in the default totality of `covering`
+------
+1/1: Building doubleTotal (doubleTotal.idr)
+Error: Multiple totality modifiers
+
+doubleTotal:1:1--3:7
+ 1 | total
+ 2 | total
+ 3 | f : ()
+
+Possible solutions:
+ - Remove duplicates of `total`
+------
+1/1: Building implementation (implementation.idr)
+Error: Multiple totality modifiers
+
+implementation:3:1--6:21
+ 3 | total
+ 4 | covering
+ 5 | partial
+ 6 | implementation Iface
+
+Possible solutions:
+ - Leave only one modifier out of `partial`, `covering`, `total`
+ - Remove modifiers `partial`, `covering`, `total`, resulting in the default totality of `covering`
+------
+1/1: Building interface (interface.idr)
+Error: Multiple totality modifiers
+
+interface:2:3--5:14
+ 2 |   total
+ 3 |   covering
+ 4 |   partial
+ 5 |   method : ()
+
+Possible solutions:
+ - Leave only one modifier out of `partial`, `covering`, `total`
+ - Remove modifiers `partial`, `covering`, `total`, resulting in the default totality of `covering`
+------
+1/1: Building noOverrideDefault (noOverrideDefault.idr)
+Error: Multiple totality modifiers
+
+noOverrideDefault:1:1--3:15
+ 1 | total
+ 2 | partial
+ 3 | f : Int -> Int
+
+Possible solutions:
+ - Leave only one modifier out of `partial`, `total`
+------
+1/1: Building duplicates (duplicates.idr)
+Error: Multiple totality modifiers
+
+duplicates:1:1--6:7
+ 1 | total
+ 2 | partial
+ 3 | covering
+ 4 | total
+ 5 | partial
+ 6 | f : ()
+
+Possible solutions:
+ - Remove duplicates of `partial`, `total`
+ - Leave only one modifier out of `partial`, `covering`, `total`
+ - Remove modifiers `partial`, `covering`, `total`, resulting in the default totality of `covering`

tests/idris2/total/total026/implementation.idr

@@ -0,0 +1,6 @@
+interface Iface where
+
+total
+covering
+partial
+implementation Iface

tests/idris2/total/total026/implementationOverride.idr

@@ -0,0 +1,7 @@
+interface Iface where
+  total
+  method : ()
+
+covering
+implementation Iface where
+  method = ()

tests/idris2/total/total026/interface.idr

@@ -0,0 +1,5 @@
+interface Iface where
+  total
+  covering
+  partial
+  method : ()

tests/idris2/total/total026/issue3437.idr

@@ -0,0 +1,4 @@
+total
+covering
+f : Int -> Int
+f i = f i

tests/idris2/total/total026/noOverrideDefault.idr

@@ -0,0 +1,4 @@
+total
+partial
+f : Int -> Int
+f i = f i

tests/idris2/total/total026/overrideDefault.idr

@@ -0,0 +1,5 @@
+%default total
+
+covering
+f : Int -> Int
+f i = f i

tests/idris2/total/total026/run

@@ -0,0 +1,21 @@
+. ../../../testutils.sh
+
+check overrideDefault.idr
+echo "------"
+idris2 --check --total compilerOption.idr
+echo "------"
+check sameAsDefault.idr
+echo "------"
+check implementationOverride.idr
+echo "------"
+check issue3437.idr
+echo "------"
+check doubleTotal.idr
+echo "------"
+check implementation.idr
+echo "------"
+check interface.idr
+echo "------"
+check noOverrideDefault.idr
+echo "------"
+check duplicates.idr

tests/idris2/total/total026/sameAsDefault.idr

@@ -0,0 +1,5 @@
+%default total
+
+total
+f : ()
+f = ()

tests/idris2/total/total027/dataDifferentTotality.idr

@@ -0,0 +1,6 @@
+total
+data X : Type
+
+partial
+data X where
+  MkX : (X -> X) -> X