diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index 3215555b34..528780510d 100644
--- a/src/Core/Context.idr
+++ b/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 ()
diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index 54423d1816..8fb8b74e49 100644
--- a/src/Idris/Desugar.idr
+++ b/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
diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr
index 2f69486833..727a3c1067 100644
--- a/src/Idris/Elab/Implementation.idr
+++ b/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
diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr
index f0835b4247..35c2d9dc98 100644
--- a/src/Idris/Elab/Interface.idr
+++ b/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
diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr
index 5b045c2cd8..f2c0942b13 100644
--- a/src/TTImp/ProcessData.idr
+++ b/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)
diff --git a/src/TTImp/ProcessFnOpt.idr b/src/TTImp/ProcessFnOpt.idr
index a2db835821..818687fee6 100644
--- a/src/TTImp/ProcessFnOpt.idr
+++ b/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)
diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr
index 1a716264a3..f2f718f7f8 100644
--- a/src/TTImp/TTImp.idr
+++ b/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
diff --git a/tests/idris2/total/total026/compilerOption.idr b/tests/idris2/total/total026/compilerOption.idr
new file mode 100644
index 0000000000..09adb9877f
--- /dev/null
+++ b/tests/idris2/total/total026/compilerOption.idr
@@ -0,0 +1,3 @@
+covering
+f : Int -> Int
+f i = f i
diff --git a/tests/idris2/total/total026/doubleTotal.idr b/tests/idris2/total/total026/doubleTotal.idr
new file mode 100644
index 0000000000..26296e5522
--- /dev/null
+++ b/tests/idris2/total/total026/doubleTotal.idr
@@ -0,0 +1,4 @@
+total
+total
+f : ()
+f = ()
diff --git a/tests/idris2/total/total026/duplicates.idr b/tests/idris2/total/total026/duplicates.idr
new file mode 100644
index 0000000000..0ef10caecc
--- /dev/null
+++ b/tests/idris2/total/total026/duplicates.idr
@@ -0,0 +1,7 @@
+total
+partial
+covering
+total
+partial
+f : ()
+f = ()
diff --git a/tests/idris2/total/total026/expected b/tests/idris2/total/total026/expected
new file mode 100644
index 0000000000..467b68aeae
--- /dev/null
+++ b/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`
diff --git a/tests/idris2/total/total026/implementation.idr b/tests/idris2/total/total026/implementation.idr
new file mode 100644
index 0000000000..89a0fa3f66
--- /dev/null
+++ b/tests/idris2/total/total026/implementation.idr
@@ -0,0 +1,6 @@
+interface Iface where
+
+total
+covering
+partial
+implementation Iface
diff --git a/tests/idris2/total/total026/implementationOverride.idr b/tests/idris2/total/total026/implementationOverride.idr
new file mode 100644
index 0000000000..055678ab54
--- /dev/null
+++ b/tests/idris2/total/total026/implementationOverride.idr
@@ -0,0 +1,7 @@
+interface Iface where
+  total
+  method : ()
+
+covering
+implementation Iface where
+  method = ()
diff --git a/tests/idris2/total/total026/interface.idr b/tests/idris2/total/total026/interface.idr
new file mode 100644
index 0000000000..a9fd049f82
--- /dev/null
+++ b/tests/idris2/total/total026/interface.idr
@@ -0,0 +1,5 @@
+interface Iface where
+  total
+  covering
+  partial
+  method : ()
diff --git a/tests/idris2/total/total026/issue3437.idr b/tests/idris2/total/total026/issue3437.idr
new file mode 100644
index 0000000000..06cb40d450
--- /dev/null
+++ b/tests/idris2/total/total026/issue3437.idr
@@ -0,0 +1,4 @@
+total
+covering
+f : Int -> Int
+f i = f i
diff --git a/tests/idris2/total/total026/noOverrideDefault.idr b/tests/idris2/total/total026/noOverrideDefault.idr
new file mode 100644
index 0000000000..7938c3ceb4
--- /dev/null
+++ b/tests/idris2/total/total026/noOverrideDefault.idr
@@ -0,0 +1,4 @@
+total
+partial
+f : Int -> Int
+f i = f i
diff --git a/tests/idris2/total/total026/overrideDefault.idr b/tests/idris2/total/total026/overrideDefault.idr
new file mode 100644
index 0000000000..5d6bbd78fa
--- /dev/null
+++ b/tests/idris2/total/total026/overrideDefault.idr
@@ -0,0 +1,5 @@
+%default total
+
+covering
+f : Int -> Int
+f i = f i
diff --git a/tests/idris2/total/total026/run b/tests/idris2/total/total026/run
new file mode 100755
index 0000000000..b9a1ec0a28
--- /dev/null
+++ b/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
diff --git a/tests/idris2/total/total026/sameAsDefault.idr b/tests/idris2/total/total026/sameAsDefault.idr
new file mode 100644
index 0000000000..c13c6d34ac
--- /dev/null
+++ b/tests/idris2/total/total026/sameAsDefault.idr
@@ -0,0 +1,5 @@
+%default total
+
+total
+f : ()
+f = ()
diff --git a/tests/idris2/total/total027/dataDifferentTotality.idr b/tests/idris2/total/total027/dataDifferentTotality.idr
new file mode 100644
index 0000000000..8e47f6ee67
--- /dev/null
+++ b/tests/idris2/total/total027/dataDifferentTotality.idr
@@ -0,0 +1,6 @@
+total
+data X : Type
+
+partial
+data X where
+  MkX : (X -> X) -> X
diff --git a/tests/idris2/total/total027/dataSameTotality.idr b/tests/idris2/total/total027/dataSameTotality.idr
new file mode 100644
index 0000000000..797e61fe6d
--- /dev/null
+++ b/tests/idris2/total/total027/dataSameTotality.idr
@@ -0,0 +1,6 @@
+total
+data X : Type
+
+total
+data X where
+  MkX : (X -> X) -> X
diff --git a/tests/idris2/total/total027/dataTotalityOnlyDeclaration.idr b/tests/idris2/total/total027/dataTotalityOnlyDeclaration.idr
new file mode 100644
index 0000000000..30152cfde1
--- /dev/null
+++ b/tests/idris2/total/total027/dataTotalityOnlyDeclaration.idr
@@ -0,0 +1,5 @@
+total
+data X : Type
+
+data X where
+  MkX : (X -> X) -> X
diff --git a/tests/idris2/total/total027/dataTotalityOnlyDefinition.idr b/tests/idris2/total/total027/dataTotalityOnlyDefinition.idr
new file mode 100644
index 0000000000..ca96ae8e44
--- /dev/null
+++ b/tests/idris2/total/total027/dataTotalityOnlyDefinition.idr
@@ -0,0 +1,5 @@
+data X : Type
+
+total
+data X where
+  MkX : (X -> X) -> X
diff --git a/tests/idris2/total/total027/expected b/tests/idris2/total/total027/expected
new file mode 100644
index 0000000000..dc49de1165
--- /dev/null
+++ b/tests/idris2/total/total027/expected
@@ -0,0 +1,79 @@
+1/1: Building dataSameTotality (dataSameTotality.idr)
+Error: X is not total, not strictly positive
+
+dataSameTotality:5:1--6:22
+ 5 | data X where
+ 6 |   MkX : (X -> X) -> X
+
+------
+1/1: Building recordSameTotality (recordSameTotality.idr)
+Error: X is not total, not strictly positive
+
+recordSameTotality:4:1--7:13
+ 4 | total
+ 5 | record X where
+ 6 |   constructor MkX
+ 7 |   f : X -> X
+
+------
+1/1: Building dataDifferentTotality (dataDifferentTotality.idr)
+Error: Data X has been forward-declared with totality `partial`, cannot change to `total`
+
+dataDifferentTotality:4:1--6:22
+ 4 | partial
+ 5 | data X where
+ 6 |   MkX : (X -> X) -> X
+
+Possible solutions:
+ - Use the same totality modifiers
+ - Remove the totality modifier from the declaration
+ - Remove the totality modifier from the definition
+------
+1/1: Building recordDifferentTotality (recordDifferentTotality.idr)
+Error: Data Main.X has been forward-declared with totality `partial`, cannot change to `total`
+
+recordDifferentTotality:4:1--7:13
+ 4 | partial
+ 5 | record X where
+ 6 |   constructor MkX
+ 7 |   f : X -> X
+
+Possible solutions:
+ - Use the same totality modifiers
+ - Remove the totality modifier from the declaration
+ - Remove the totality modifier from the definition
+------
+1/1: Building dataTotalityOnlyDeclaration (dataTotalityOnlyDeclaration.idr)
+Error: X is not total, not strictly positive
+
+dataTotalityOnlyDeclaration:4:1--5:22
+ 4 | data X where
+ 5 |   MkX : (X -> X) -> X
+
+------
+1/1: Building recordTotalityOnlyDeclaration (recordTotalityOnlyDeclaration.idr)
+Error: X is not total, not strictly positive
+
+recordTotalityOnlyDeclaration:4:1--6:13
+ 4 | record X where
+ 5 |   constructor MkX
+ 6 |   f : X -> X
+
+------
+1/1: Building dataTotalityOnlyDefinition (dataTotalityOnlyDefinition.idr)
+Error: X is not total, not strictly positive
+
+dataTotalityOnlyDefinition:4:1--5:22
+ 4 | data X where
+ 5 |   MkX : (X -> X) -> X
+
+------
+1/1: Building recordTotalityOnlyDefinition (recordTotalityOnlyDefinition.idr)
+Error: X is not total, not strictly positive
+
+recordTotalityOnlyDefinition:3:1--6:13
+ 3 | total
+ 4 | record X where
+ 5 |   constructor MkX
+ 6 |   f : X -> X
+
diff --git a/tests/idris2/total/total027/recordDifferentTotality.idr b/tests/idris2/total/total027/recordDifferentTotality.idr
new file mode 100644
index 0000000000..19abd56e0d
--- /dev/null
+++ b/tests/idris2/total/total027/recordDifferentTotality.idr
@@ -0,0 +1,7 @@
+total
+record X
+
+partial
+record X where
+  constructor MkX
+  f : X -> X
diff --git a/tests/idris2/total/total027/recordSameTotality.idr b/tests/idris2/total/total027/recordSameTotality.idr
new file mode 100644
index 0000000000..94c2559fcb
--- /dev/null
+++ b/tests/idris2/total/total027/recordSameTotality.idr
@@ -0,0 +1,7 @@
+total
+record X
+
+total
+record X where
+  constructor MkX
+  f : X -> X
diff --git a/tests/idris2/total/total027/recordTotalityOnlyDeclaration.idr b/tests/idris2/total/total027/recordTotalityOnlyDeclaration.idr
new file mode 100644
index 0000000000..de84e407be
--- /dev/null
+++ b/tests/idris2/total/total027/recordTotalityOnlyDeclaration.idr
@@ -0,0 +1,6 @@
+total
+record X
+
+record X where
+  constructor MkX
+  f : X -> X
diff --git a/tests/idris2/total/total027/recordTotalityOnlyDefinition.idr b/tests/idris2/total/total027/recordTotalityOnlyDefinition.idr
new file mode 100644
index 0000000000..ebc98379a0
--- /dev/null
+++ b/tests/idris2/total/total027/recordTotalityOnlyDefinition.idr
@@ -0,0 +1,6 @@
+record X
+
+total
+record X where
+  constructor MkX
+  f : X -> X
diff --git a/tests/idris2/total/total027/run b/tests/idris2/total/total027/run
new file mode 100755
index 0000000000..6eb3c4e04c
--- /dev/null
+++ b/tests/idris2/total/total027/run
@@ -0,0 +1,17 @@
+. ../../../testutils.sh
+
+check dataSameTotality.idr
+echo "------"
+check recordSameTotality.idr
+echo "------"
+check dataDifferentTotality.idr
+echo "------"
+check recordDifferentTotality.idr
+echo "------"
+check dataTotalityOnlyDeclaration.idr
+echo "------"
+check recordTotalityOnlyDeclaration.idr
+echo "------"
+check dataTotalityOnlyDefinition.idr
+echo "------"
+check recordTotalityOnlyDefinition.idr
diff --git a/tests/ttimp/total004/expected b/tests/ttimp/total004/expected
new file mode 100644
index 0000000000..809a5afac3
--- /dev/null
+++ b/tests/ttimp/total004/expected
@@ -0,0 +1,3 @@
+Processing as TTImp
+issue3437:1:1--4:1:Multiple totality modifiers
+Yaffle> Bye for now!
diff --git a/tests/ttimp/total004/input b/tests/ttimp/total004/input
new file mode 100644
index 0000000000..d325550eb0
--- /dev/null
+++ b/tests/ttimp/total004/input
@@ -0,0 +1 @@
+:q
diff --git a/tests/ttimp/total004/issue3437.yaff b/tests/ttimp/total004/issue3437.yaff
new file mode 100644
index 0000000000..06cb40d450
--- /dev/null
+++ b/tests/ttimp/total004/issue3437.yaff
@@ -0,0 +1,4 @@
+total
+covering
+f : Int -> Int
+f i = f i
diff --git a/tests/ttimp/total004/run b/tests/ttimp/total004/run
new file mode 100755
index 0000000000..30a3b5576e
--- /dev/null
+++ b/tests/ttimp/total004/run
@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+idris2 --check --yaffle issue3437.yaff < input