diff --git a/src/Core/Core.idr b/src/Core/Core.idr
index d6eee7edf..28a7510ee 100644
--- a/src/Core/Core.idr
+++ b/src/Core/Core.idr
@@ -438,6 +438,10 @@ export %inline
 (<$>) : (a -> b) -> Core a -> Core b
 (<$>) f (MkCore a) = MkCore (map (map f) a)
 
+export %inline
+ignore : Core a -> Core ()
+ignore = map (\ _ => ())
+
 -- Monad (specialised)
 export %inline
 (>>=) : Core a -> (a -> Core b) -> Core b
diff --git a/src/Core/Termination.idr b/src/Core/Termination.idr
index 1d3e8b1fa..a2f422f19 100644
--- a/src/Core/Termination.idr
+++ b/src/Core/Termination.idr
@@ -25,8 +25,10 @@ totRefs defs (n :: ns)
               | Nothing => pure rest
          case isTerminating (totality d) of
               IsTerminating => pure rest
-              Unchecked => pure rest
-              bad => case rest of
+              Unchecked => do
+                log "totality" 20 $ "Totality unchecked for " ++ show !(toFullNames n)
+                pure rest
+              _ => case rest of
                           NotTerminating (BadCall ns)
                              => toFullNames $ NotTerminating (BadCall (n :: ns))
                           _ => toFullNames $ NotTerminating (BadCall [n])
@@ -43,7 +45,7 @@ export
 checkIfGuarded : {auto c : Ref Ctxt Defs} ->
                  FC -> Name -> Core ()
 checkIfGuarded fc n
-    = do log "totality.termination.guarded" 6 $ "Check if Guarded: " ++ show n
+    = do log "totality.termination.guarded" 6 $ "Check if Guarded: " ++ show !(toFullNames n)
          defs <- get Ctxt
          Just (PMDef _ _ _ _ pats) <- lookupDefExact n (gamma defs)
               | _ => pure ()
@@ -363,7 +365,7 @@ mutual
       = do Just gdef <- lookupCtxtExact fn_in (gamma defs)
                 | Nothing => throw (UndefinedName fc fn_in)
            let fn = fullname gdef
-           log "totality.termination.sizechange" 10 $ "Looking under " ++ show fn
+           log "totality.termination.sizechange" 10 $ "Looking under " ++ show !(toFullNames fn)
            aSmaller <- resolved (gamma defs) (NS builtinNS (UN "assert_smaller"))
            cond [(fn == NS builtinNS (UN "assert_total"), pure []),
               (caseFn fn,
@@ -410,7 +412,7 @@ export
 calculateSizeChange : {auto c : Ref Ctxt Defs} ->
                       FC -> Name -> Core (List SCCall)
 calculateSizeChange loc n
-    = do log "totality.termination.sizechange" 5 $ "Calculating Size Change: " ++ show n
+    = do log "totality.termination.sizechange" 5 $ "Calculating Size Change: " ++ show !(toFullNames n)
          defs <- get Ctxt
          Just def <- lookupCtxtExact n (gamma defs)
               | Nothing => throw (UndefinedName loc n)
@@ -447,15 +449,15 @@ checkSC : {auto a : Ref APos Arg} ->
           List (Name, List (Maybe Arg)) -> -- calls we've seen so far
           Core Terminating
 checkSC defs f args path
-   = do log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show f
+   = do log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show !(toFullNames f)
         let pos = (f, map (map Builtin.fst) args)
         if pos `elem` path
-           then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show f
+           then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show !(toFullNames f)
                    toFullNames $ checkDesc (mapMaybe (map Builtin.snd) args) path
            else case !(lookupCtxtExact f (gamma defs)) of
-                     Nothing => do log "totality.termination.sizechange.isTerminating" 8 $ "Size Change Graph is Terminating for: " ++ show f
+                     Nothing => do log "totality.termination.sizechange.isTerminating" 8 $ "Size Change Graph is Terminating for: " ++ show !(toFullNames f)
                                    pure IsTerminating
-                     Just def => do log "totality.termination.sizechange.needsChecking" 8 $ "Size Change Graph needs traversing: " ++ show f
+                     Just def => do log "totality.termination.sizechange.needsChecking" 8 $ "Size Change Graph needs traversing: " ++ show !(toFullNames f)
                                     continue (sizeChange def) (pos :: path)
   where
     -- Look for something descending in the list of size changes
@@ -492,7 +494,7 @@ checkSC defs f args path
              let Unchecked = isTerminating (totality gdef)
                   | IsTerminating => pure IsTerminating
                   | _ => pure (NotTerminating (BadCall [fnCall sc]))
-             log "totality.termination.sizechange.checkCall" 8 $ "CheckCall Size Change Graph: " ++ show (fnCall sc)
+             log "totality.termination.sizechange.checkCall" 8 $ "CheckCall Size Change Graph: " ++ show !(toFullNames (fnCall sc))
              term <- checkSC defs (fnCall sc) (mkArgs (fnArgs sc)) path
              if not inpath
                 then case term of
@@ -501,12 +503,12 @@ checkSC defs f args path
                           -- was mutually recursive, so start again with new
                           -- arguments (that is, where we'd start if the
                           -- function was the top level thing we were checking)
-                          do log "totality.termination.sizechange.checkCall.inPathNot.restart" 9 $ "ReChecking Size Change Graph: " ++ show (fnCall sc)
+                          do log "totality.termination.sizechange.checkCall.inPathNot.restart" 9 $ "ReChecking Size Change Graph: " ++ show !(toFullNames (fnCall sc))
                              args' <- initArgs (length (fnArgs sc))
                              checkSC defs (fnCall sc) args' path
-                       t => do log "totality.termination.sizechange.checkCall.inPathNot.return" 9 $ "Have result: " ++ show (fnCall sc)
+                       t => do log "totality.termination.sizechange.checkCall.inPathNot.return" 9 $ "Have result: " ++ show !(toFullNames (fnCall sc))
                                pure t
-                else do log "totality.termination.sizechange.checkCall.inPath" 9 $ "Have Result: " ++ show (fnCall sc)
+                else do log "totality.termination.sizechange.checkCall.inPath" 9 $ "Have Result: " ++ show !(toFullNames (fnCall sc))
                         pure term
 
     getWorst : Terminating -> List Terminating -> Terminating
@@ -524,7 +526,7 @@ calcTerminating : {auto c : Ref Ctxt Defs} ->
                   FC -> Name -> Core Terminating
 calcTerminating loc n
     = do defs <- get Ctxt
-         log "totality.termination.calc" 7 $ "Calculating termination: " ++ show n
+         log "totality.termination.calc" 7 $ "Calculating termination: " ++ show !(toFullNames n)
          case !(lookupCtxtExact n (gamma defs)) of
               Nothing => throw (UndefinedName loc n)
               Just def =>
@@ -558,7 +560,7 @@ checkTerminating : {auto c : Ref Ctxt Defs} ->
                    FC -> Name -> Core Terminating
 checkTerminating loc n
     = do tot <- getTotality loc n
-         log "totality.termination" 6 $ "Checking termination: " ++ show n
+         log "totality.termination" 6 $ "Checking termination: " ++ show !(toFullNames n)
          case isTerminating tot of
               Unchecked =>
                  do tot' <- calcTerminating loc n
@@ -651,7 +653,7 @@ calcPositive : {auto c : Ref Ctxt Defs} ->
                FC -> Name -> Core (Terminating, List Name)
 calcPositive loc n
     = do defs <- get Ctxt
-         log "totality.positivity" 6 $ "Calculating positivity: " ++ show n
+         log "totality.positivity" 6 $ "Calculating positivity: " ++ show !(toFullNames n)
          case !(lookupDefTyExact n (gamma defs)) of
               Just (TCon _ _ _ _ _ tns dcons _, ty) =>
                   case !(totRefsIn defs ty) of
@@ -670,7 +672,7 @@ checkPositive : {auto c : Ref Ctxt Defs} ->
 checkPositive loc n_in
     = do n <- toResolvedNames n_in
          tot <- getTotality loc n
-         log "totality.positivity" 6 $ "Checking positivity: " ++ show n
+         log "totality.positivity" 6 $ "Checking positivity: " ++ show !(toFullNames n)
          case isTerminating tot of
               Unchecked =>
                   do (tot', cons) <- calcPositive loc n
@@ -679,6 +681,7 @@ checkPositive loc n_in
                      pure tot'
               t => pure t
 
+
 -- Check and record totality of the given name; positivity if it's a data
 -- type, termination if it's a function
 export
@@ -690,7 +693,7 @@ checkTotal loc n_in
              | Nothing => throw (UndefinedName loc n_in)
          let n = Resolved nidx
          tot <- getTotality loc n
-         log "totality" 5 $ "Checking totality: " ++ show n
+         log "totality" 5 $ "Checking totality: " ++ show !(toFullNames n)
          defs <- get Ctxt
          case isTerminating tot of
               Unchecked =>
diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr
index 6569e3a13..810dc7c0c 100644
--- a/src/TTImp/ProcessDecls.idr
+++ b/src/TTImp/ProcessDecls.idr
@@ -72,14 +72,22 @@ checkTotalityOK n
     = do defs <- get Ctxt
          Just gdef <- lookupCtxtExact n (gamma defs)
               | Nothing => pure Nothing
+         let fc = location gdef
+
+         -- #524: need to check positivity even if we're not in a total context
+         -- because a definition coming later may need to know it is positive
+         case definition gdef of
+           (TCon _ _ _ _ _ _ _ _) => ignore $ checkPositive fc n
+           _ => pure ()
+
+         -- Once that is done, we build up errors if necessary
          let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
          let tot = totality gdef
-         let fc = location gdef
          log "totality" 3 $ show n ++ " must be: " ++ show treq
          case treq of
-              PartialOK => pure Nothing
-              CoveringOnly => checkCovering fc (isCovering tot)
-              Total => checkTotality fc
+            PartialOK => pure Nothing
+            CoveringOnly => checkCovering fc (isCovering tot)
+            Total => checkTotality fc
   where
     checkCovering : FC -> Covering -> Core (Maybe Error)
     checkCovering fc IsCovering = pure Nothing