[ Issue 1428 ] Parametrized size postulates considered harmful.

src/full/Agda/TypeChecking/Rules/Decl.hs

@@ -363,7 +363,14 @@ checkAxiom funSig i info0 x e = do
   reportSDoc "tc.decl.ax" 10 $ sep
     [ text $ "checked type signature"
     , nest 2 $ prettyTCM rel <> prettyTCM x <+> text ":" <+> prettyTCM t
+    , nest 2 $ text "of sort " <+> prettyTCM (getSort t)
     ]
+  -- Andreas, 2015-03-17 Issue 1428: Do not postulate sizes in parametrized
+  -- modules!
+  when (funSig == A.NoFunSig) $ do
+    whenM ((== SizeUniv) <$> do reduce $ getSort t) $ do
+      whenM ((> 0) <$> getContextSize) $ do
+        typeError $ GenericError $ "We don't like postulated sizes in parametrized modules."
   -- Not safe. See Issue 330
   -- t <- addForcingAnnotations t
   addConstant x =<< do

test/fail/Issue1428c.agda

@@ -0,0 +1,23 @@
+-- Andreas, 2015-03-17
+
+open import Common.Size
+
+data ⊥ : Set where
+
+data D (i : Size) : Set where
+  c : Size< i → D i
+
+-- This definition of size predecessor should be forbidden...
+module _ (i : Size) where
+  postulate
+    pred : Size< i
+
+-- ...otherwise the injectivity test loops here.
+iter : ∀ i → D i → ⊥
+iter i (c j) = iter j (c (pred j))
+
+loop : Size → ⊥
+loop i = iter i (c (pred i))
+
+absurd : ⊥
+absurd = loop ∞

test/fail/Issue1428c.err

@@ -0,0 +1,2 @@
+Issue1428c.agda:8,5-19
+We don't like postulated sizes in parametrized modules.