Fixed issue #2477.

src/full/Agda/TypeChecking/Monad/SizedTypes.hs

@@ -163,6 +163,7 @@ sizeMax vs = case vs of
 -- | A useful view on sizes.
 data SizeView = SizeInf | SizeSuc Term | OtherSize Term
 
+-- | Expects argument to be 'reduce'd.
 sizeView :: Term -> TCM SizeView
 sizeView v = do
   Def inf [] <- ignoreSharing <$> primSizeInf

src/full/Agda/TypeChecking/Polarity.hs

@@ -16,6 +16,7 @@ import Agda.Syntax.Internal.Pattern
 
 import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Pretty
+import Agda.TypeChecking.SizedTypes
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope
 import Agda.TypeChecking.Reduce
@@ -136,7 +137,7 @@ computePolarity x = inConcreteOrAbstractMode x $ \ def -> do
   -- Andreas, 2015-07-01: I thought one should do this for
   -- abstract local definitions in @where@ blocks to fix Issue 1366b,
   -- but it is not necessary.
-  -- t <- if (defAbstract def == AbsxtractDef) && not (isAnonymousModuleName $ qnameModule x)
+  -- t <- if (defAbstract def == AbstractDef) && not (isAnonymousModuleName $ qnameModule x)
   -- Andreas, 2017-01-27: Leave definition alone if there is nothing to update.
   when (defAbstract def /= AbstractDef && any (Nonvariant ==) pol) $ do
     reportSDoc "tc.polarity.set" 15 $
@@ -346,9 +347,9 @@ checkSizeIndex d np i a = do
   case ignoreSharing $ unEl a of
     Def d0 es -> do
       whenNothingM (sameDef d d0) __IMPOSSIBLE__
-      s <- sizeView $ unArg ix
+      s <- deepSizeView $ unArg ix
       case s of
-        SizeSuc v | Var j [] <- ignoreSharing v, i == j
+        DSizeVar j 1 | i == j
           -> return $ not $ freeIn i (pars ++ ixs)
         _ -> return False
       where

test/Succeed/Issue2477.agda

@@ -0,0 +1,22 @@
+-- Andreas, 2017-02-27, issue #2477
+
+{-# OPTIONS --show-irrelevant #-}
+
+open import Agda.Builtin.Size
+open import Agda.Builtin.Nat using (suc) renaming (Nat to ℕ)
+
+_+_ : Size → ℕ → Size
+s + 0 = s
+s + suc n = ↑ (s + n)
+
+data Nat : Size → Set where
+  zero  :  ∀ i → Nat (i + 1)
+  suc   :  ∀ i → Nat i → Nat (i + 1)
+  -- i + 1 should be reduced to ↑ i
+  -- to make Nat monotone in its size argument
+
+pred : ∀ i → Nat i → Nat i
+pred .(i + 1) (zero i)   =  zero i
+pred .(i + 1) (suc i x)  =  x
+
+-- Should succeed