As of #118, termination checking no longer allows proving that parameterised Acc enjoys the induction principle of indexed Acc.
Problematic call:
go y (w y y<x)
(at NonUniformTermination.agda:18.36-38)
This is a breaking change, but it's sort-of expected if we imagine writing out the induction principle for parameterised Acc:
Acc-elim:∀{x}(P:Accx→Type)→(∀(w:∀y→y<x→Accy)→{! ∀ y y<x → P (w y y<x) !}-- ^~~~~~~~~~~~~~~~~~~~~~~~~~~-- this is the inductive hypothesis that would justify a recursive call-- go x (acc w) → go y (w ...)-- but we can't apply P : Acc x → ... to (w y y<x) : Acc y→P(accw))→∀x→Accx
However, the termination checking change only forbids uses recursion on arguments where the parameter change was caused by matching on a separate indexed-inductive type, or because that constructor argument is a dependent function returning an instance of the data type at a parameter that was introduced in the argument's own telescope. This means that a lot of non-uniformly parameterised types can still be declared and shown equivalent to their indexed versions, like this silly example:
dataParityList(A:Type)(b:Bool):Typewherenil:b≡true→ParityListAb_∷_:A→ParityListA(notb)→ParityListAbpattern[]=nilreflelim:∀{A:Type}(P:∀b→ParityListAb→Type)→Ptrue[]→(∀{b}axs→P(notb)xs→Pb(a∷xs))→∀{b}xs→PbxselimPpnilpconsxs=goxswherego:∀{b}xs→Pbxsgo[]=pnilgo(x∷xs)=pconsxxs(goxs)
So we should decide on a fate for non-uniformly recursive types. If we still want to support them, 88addd3f95 could be rolled back while still patching the incompatibility between untyped size-change termination and impredicativity by having (e.g.) the positivity checker mark the forbidden positions. If we don't want to support them, we should have the positivity checker raise error-warnings when it runs into one of the datatypes in the mutual block applied to the wrong parameters.
As of #118, termination checking no longer allows proving that *parameterised* `Acc` enjoys the induction principle of *indexed* `Acc`.
https://codeberg.org/1lab/mikan/src/commit/88addd3f9572bbd2d0f426cffa244a97ab988dfc/test/Fail/NonUniformTermination.err#L3-L5
This is a breaking change, but it's sort-of expected if we imagine writing out the induction principle for *parameterised* `Acc`:
```agda
Acc-elim
: ∀ {x} (P : Acc x → Type)
→ (∀ (w : ∀ y → y < x → Acc y)
→ {! ∀ y y<x → P (w y y<x) !}
-- ^~~~~~~~~~~~~~~~~~~~~~~~~~~
-- this is the inductive hypothesis that would justify a recursive call
-- go x (acc w) → go y (w ...)
-- but we can't apply P : Acc x → ... to (w y y<x) : Acc y
→ P (acc w))
→ ∀ x → Acc x
```
However, the termination checking change only forbids uses recursion on arguments where the parameter change was caused by matching on a separate indexed-inductive type, or because that constructor argument is a dependent function returning an instance of the data type at a parameter that was introduced in the argument's own telescope. This means that a lot of non-uniformly parameterised types can still be declared and shown equivalent to their indexed versions, like this silly example:
```agda
data ParityList (A : Type) (b : Bool) : Type where
nil : b ≡ true → ParityList A b
_∷_ : A → ParityList A (not b) → ParityList A b
pattern [] = nil refl
elim
: ∀ {A : Type} (P : ∀ b → ParityList A b → Type)
→ P true []
→ (∀ {b} a xs → P (not b) xs → P b (a ∷ xs))
→ ∀ {b} xs → P b xs
elim P pnil pcons xs = go xs where
go : ∀ {b} xs → P b xs
go [] = pnil
go (x ∷ xs) = pcons x xs (go xs)
```
So we should decide on a fate for non-uniformly recursive types. If we still want to support them, 88addd3f9572bbd2d0f426cffa244a97ab988dfc could be rolled back while still patching the incompatibility between untyped size-change termination and impredicativity by having (e.g.) the positivity checker mark the forbidden positions. If we don't want to support them, we should have the positivity checker raise error-warnings when it runs into one of the datatypes in the mutual block applied to the wrong parameters.