Add tests for issues #7269, #7270, #7271 with dummy error msgs

test/Fail/TypeBasedTermination/Issue7269.agda

@@ -0,0 +1,14 @@
+-- Andreas, 2024-05-16, issue #7269
+-- --no-syntax-based-termination should not turn on --type-based-termination
+
+{-# OPTIONS --no-type-based-termination #-}
+{-# OPTIONS --no-syntax-based-termination #-}  -- Turns on TBT, but should not
+
+record U : Set where
+  coinductive
+  field force : U
+open U
+
+-- This should not pass since no termination checker is on.
+u : U
+u .force = u

test/Fail/TypeBasedTermination/Issue7269.err

@@ -0,0 +1 @@
+AGDA_FAIL

test/Fail/TypeBasedTermination/Issue7270.agda

@@ -0,0 +1,21 @@
+-- Andreas, 2024-05-16, issue #7270
+
+{-# OPTIONS --type-based-termination #-}
+
+record U : Set where
+  coinductive
+  field force : U
+open U
+
+postulate d : U → U
+
+-- f is classified as size preserving, but is not, since d is unknown
+-- Counterexamples: d = id; d u = u .force
+--
+f : U → U
+f u = d u .force
+
+-- This should not pass:
+--
+u : U
+u .force = f u

test/Fail/TypeBasedTermination/Issue7270.err

@@ -0,0 +1 @@
+AGDA_FAIL

test/Fail/TypeBasedTermination/Issue7271.agda

@@ -0,0 +1,32 @@
+-- Andreas, 2024-05-16, issue #7271.
+-- Bug in size-preservation checker.
+
+{-# OPTIONS --type-based-termination #-}
+
+data ⊥ : Set where
+
+record _×_ (A B : Set) : Set where
+  field
+    fst : A
+    snd : B
+open _×_
+
+-- Empty stream type.
+--
+record S : Set where
+  coinductive; constructor delay
+  field force : ⊥ × S
+open S
+
+-- This is not size-preserving:
+--
+f : S → ⊥ × S
+f s = s' .force where s' = s
+
+-- This should not be accepted:
+--
+s : S
+s .force = f s
+
+absurd : ⊥
+absurd = s .force .fst

test/Fail/TypeBasedTermination/Issue7271.err

@@ -0,0 +1 @@
+AGDA_FAIL

test/Fail/TypeBasedTermination/Issue7271With.agda

@@ -0,0 +1,33 @@
+-- Andreas, 2024-05-16, issue #7271.
+-- Bug in size-preservation checker.
+
+{-# OPTIONS --type-based-termination #-}
+
+data ⊥ : Set where
+
+record _×_ (A B : Set) : Set where
+  field
+    fst : A
+    snd : B
+open _×_
+
+-- Empty stream type.
+--
+record S : Set where
+  coinductive; constructor delay
+  field force : ⊥ × S
+open S
+
+-- This is not size-preserving:
+--
+f : S → ⊥ × S
+f s with s
+... | s' = s' .force
+
+-- This should not be accepted:
+--
+s : S
+s .force = f s
+
+absurd : ⊥
+absurd = s .force .fst

test/Fail/TypeBasedTermination/Issue7271With.err

@@ -0,0 +1 @@
+AGDA_FAIL