[Agda] guardedness-preserving-type-constructors failing termination checker

[Twan van Laarhoven]

I was playing around with guardedness-preserving-type-constructors and ΠΣ style 
definitions; and some of the original examples no longer work. For instance the 
code at the bottom of https://lists.chalmers.se/pipermail/agda/2010/001720.html 
fails the termination checker.

Here is a simpler example that shows the same problem:

     open import Coinduction
     open import Data.Unit
     open import Data.Product
     open import Data.Sum
     open import Data.Bool

     --accepted:
     ℕ₁ : Set
     ℕ₁ = ⊤ ⊎ Rec (♯ ℕ₁)

     --accepted:
     ℕ₂ : Set
     ℕ₂ = Rec (♯ Σ Bool \{true → ⊤; false → ℕ₂})

     --rejected:
     ℕ₃ : Set
     ℕ₃ = Rec (♯ Σ Bool \x → if x then ⊤ else ℕ₃)

     --rejected:
     ℕ₄ : Set
     ℕ₄ = Rec (♯ ∃ ℕ₄′)
       where
       ℕ₄′ : Bool → Set
       ℕ₄′ true = ⊤
       ℕ₄′ false = ℕ₄

ℕ₂ is accepted, while ℕ₃ is rejected by the termination checker, the only 
difference is that one uses a pattern matching lambda, while the other uses 
another function to do the pattern matching.

What could be going on here? Is this a bug? I am using Agda 2.3.2.1, and also 
tested it in 2.3.3 (HEAD as of today).



Twan