Intuition behind nested positivity and counterexamples
Here is an example exploiting positivity of an index to prove false:
module Whatever where

open import Level using (Level)
open import Relation.Binary.PropositionalEquality
open import Data.Empty

variable
  ℓ : Level
  A B : Set ℓ

data _≅_ (A : Set ℓ) : Set ℓ → Set ℓ where
  trefl : A ≅ A

Subst : (P : Set ℓ → Set ℓ) → A ≅ B → P A → P B
Subst P trefl PA = PA

data U : Set where
  d : U

El : U → Set
data D : Set

El d = D

{-# NO_POSITIVITY_CHECK #-}
data D where
  neg : ∀(c : U) → El c ≅ D → (El c → ⊥) → D

¬D : D → ⊥
¬D v@(neg c eq f) = Subst (λ D → D → ⊥) eq f v

spin : ⊥
spin = ¬D (neg d trefl ¬D)

Technically it also makes use of the fact that induction-recursion can create small universes, and that type equality can be smaller than general equality applied to the universe, but those are otherwise not really problematic to my knowledge (Coq has impredicative equality anyway, I believe). It's possible the simultaneous definition could be eliminated, too, but it's not straight forward, at least.

Edit: I asked around about your first bullet point. It was pointed out to me that there is essentially nothing special about a nested type that is nested in itself. This article shows how to use a non-native translation of nested types into indexed types of equivalent size. When you do that, as long as nesting is strictly positive, it's not difficult to apply the translation to a strictly positive indexed type.
Or for instance, the example translation I was shown uses a nested $ℕ$ parameter instead of self-nesting:
data D' (A : Set) (n : ℕ) : Set where
  c : D' A (suc n) → D' A n
  t : (case n of λ where
         zero → A
         (suc m) → D' A m
      ) → D' A n

Where I added the t constructor to make something actually use A, and D A is meant to be equivalent to D' A 0. I think another way to write this would be:
data D' (A : Set) : ℕ → Set where
  c : D' A (suc n) → D' A n
  t : D' A n → D' A (suc n)
  t' : A → D' A zero

Essentially, the $ℕ$ is a tree tracking how much nesting we need to unfold.