From 57f69c03110b50f5b58e9fcf80bf8e9a1e530bb9 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Mon, 26 Oct 2020 15:28:42 +0100
Subject: [PATCH] [ #5000 ] testcases cosmetics #1428 #1292

We now have Agda.Builtin.Size !
---
 test/Fail/Issue1428a.agda    | 33 +++++++++++++++++++++------------
 test/Fail/Issue1428a.err     |  4 ++--
 test/Fail/Issue1428c.agda    | 23 +++++++++++++----------
 test/Fail/Issue1428c.err     |  5 +++--
 test/Succeed/Issue1292b.agda |  4 +++-
 5 files changed, 42 insertions(+), 27 deletions(-)

diff --git a/test/Fail/Issue1428a.agda b/test/Fail/Issue1428a.agda
index c3fe6549c95..53e83c384ee 100644
--- a/test/Fail/Issue1428a.agda
+++ b/test/Fail/Issue1428a.agda
@@ -1,32 +1,41 @@
 -- Andreas, 2015-03-16
+-- Andreas, 2020-10-26 removed loop during injectivity check
 
-open import Common.Size
-open import Common.Prelude
+open import Agda.Builtin.Size
 
 -- Note: the assumption of pred is absurd,
 -- but still should not make Agda loop.
 
 module _ (pred : ∀ i → Size< i) where
 
-data D (i : Size) : Set where
-  wrap : (j : Size< i) → D i
+data ⊥ : Set where
 
-loop : ∀ i → D i → ⊥
-loop i (wrap j) = loop j (wrap (pred j))
--- Loops during injectivity check
+data SizeLt (i : Size) : Set where
+  wrap : (j : Size< i) → SizeLt i
 
-d : ∀ i → D i
+loop : (d : ∀ i → SizeLt i) → ∀ i → SizeLt i → ⊥
+loop d i (wrap j) = loop d j (d j)
+
+-- -- Loops during injectivity check:
+-- loop : ∀ i → SizeLt i → ⊥
+-- loop i (wrap j) = loop j (wrap (pred j))
+
+d : ∀ i → SizeLt i
 d i = wrap (pred i)
 
 absurd : ⊥
-absurd = FIXME loop ∞ (d ∞)
+absurd = loop d ∞ (d ∞)
+
+_ = FIXME
 
 -- Testcase temporarily mutilated, original error:
--- -Issue1428a.agda:9,20-31
+--
+-- -Issue1428a.agda:..
 -- -Functions may not return sizes, thus, function type
 -- -(i : Size) → Size< i is illegal
 -- -when checking that the expression ∀ i → Size< i is a type
--- +Issue1428a.agda:22,10-15
+--
+-- +Issue1428a.agda:...
 -- +Not in scope:
--- +  FIXME at Issue1428a.agda:22,10-15
+-- +  FIXME at Issue1428a.agda:...
 -- +when scope checking FIXME
diff --git a/test/Fail/Issue1428a.err b/test/Fail/Issue1428a.err
index eb7d837c3f6..1907bb51123 100644
--- a/test/Fail/Issue1428a.err
+++ b/test/Fail/Issue1428a.err
@@ -1,4 +1,4 @@
-Issue1428a.agda:22,10-15
+Issue1428a.agda:29,5-10
 Not in scope:
-  FIXME at Issue1428a.agda:22,10-15
+  FIXME at Issue1428a.agda:29,5-10
 when scope checking FIXME
diff --git a/test/Fail/Issue1428c.agda b/test/Fail/Issue1428c.agda
index 88ac3f4549a..8a5a573d330 100644
--- a/test/Fail/Issue1428c.agda
+++ b/test/Fail/Issue1428c.agda
@@ -1,11 +1,12 @@
 -- Andreas, 2015-03-17
+-- Andreas, 2020-10-26 conform to Issue1428a
 
-open import Common.Size
+open import Agda.Builtin.Size
 
 data ⊥ : Set where
 
-data D (i : Size) : Set where
-  c : Size< i → D i
+data SizeLt (i : Size) : Set where
+  wrap : Size< i → SizeLt i
 
 -- This definition of size predecessor should be forbidden...
 module _ (i : Size) where
@@ -13,19 +14,21 @@ module _ (i : Size) where
     pred : Size< i
 
 -- ...otherwise the injectivity test loops here.
-iter : ∀ i → D i → ⊥
-iter i (c j) = iter j (c (pred j))
+iter : ∀ i → SizeLt i → ⊥
+iter i (wrap j) = iter j (wrap (pred j))
 
 loop : Size → ⊥
-loop i = iter i (c (pred i))
+loop i = iter i (wrap (pred i))
 
 absurd : ⊥
 absurd = FIXME loop ∞
 
--- Testcase temporarily mutilated, original error
--- -Issue1428c.agda:13,5-19
+-- Testcase temporarily mutilated, original error:
+--
+-- -Issue1428c.agda:...
 -- -We don't like postulated sizes in parametrized modules.
--- +Issue1428c.agda:23,10-15
+--
+-- +Issue1428c.agda:...
 -- +Not in scope:
--- +  FIXME at Issue1428c.agda:23,10-15
+-- +  FIXME at Issue1428c.agda:...
 -- +when scope checking FIXME
diff --git a/test/Fail/Issue1428c.err b/test/Fail/Issue1428c.err
index fff5c9aef00..33ec8080cbe 100644
--- a/test/Fail/Issue1428c.err
+++ b/test/Fail/Issue1428c.err
@@ -1,4 +1,5 @@
-Issue1428c.agda:23,10-15
+Issue1428c.agda:24,10-15
 Not in scope:
-  FIXME at Issue1428c.agda:23,10-15
+  FIXME
+  at Issue1428c.agda:24,10-15
 when scope checking FIXME
diff --git a/test/Succeed/Issue1292b.agda b/test/Succeed/Issue1292b.agda
index e06fca82213..86f0d54dedb 100644
--- a/test/Succeed/Issue1292b.agda
+++ b/test/Succeed/Issue1292b.agda
@@ -4,7 +4,7 @@
 
 -- {-# OPTIONS -v tc.size:20  #-}
 
-open import Common.Size
+open import Agda.Builtin.Size
 
 data Nat : {size : Size} -> Set where
   zero : {size : Size} -> Nat {↑ size}
@@ -22,3 +22,5 @@ div' zero    n = zero
 div' (suc m) n = suc (div' (sub m n) n)
 
 -- should termination check even --without-K
+
+-- -}