I think rewriting involving SSet was never implemented (check the blame):

• 2ltt: Ported cubical primitives to use strict universes, and other fixes. #4781

Okay, so I shouldn't expect it to work? That's fair, although it might be helpful to raise an error like "Rewriting with 2LTT not implemented" as soon as the user tries to combine the flags --rewriting and --two-level. Are there significant difficulties in implementing it?

FWIW, I haven't gotten any errors with it until now. And it's easy to modify the example in other ways to remove the error while keeping the SSets around, e.g.:

{-# OPTIONS --type-in-type --rewriting --two-level #-}

module Test where

open import Agda.Primitive public

postulate
  Tel : SSet
  ε : Tel
  _≡_ : {A : SSet} (a : A) → A → SSet
  el : Tel → SSet
  coe← : {A B : Tel} → (A ≡ B) → el B → el A
  [] : el ε
  ID : (Δ : Tel) → Tel
  ID′ : {Δ : Tel} (Θ : el Δ → Tel) → Tel
  ID′ε : {Δ : Tel} → ID′ {Δ} (λ _ → ε) ≡ ε

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE ID′ε #-}

postulate
  ID′-CONST : {Θ : Tel} (Δ : Tel) →
    ID′ {Θ} (λ _ → Δ) ≡ ID Δ
  ID′-CONST-ε : {Θ : Tel} (δ₂ : el (ID ε)) →
    coe← (ID′-CONST {Θ} ε) δ₂ ≡ []

{-# REWRITE ID′-CONST-ε #-}

I see on that line you linked to that an error is raised whenever SSet is encountered while doing something involving rewriting, but without knowing anything about the internals of rewriting I can't tell exactly what that is. Evidently whatever this something is, it's possible to do a good deal of rewriting that "involves" SSet without it, at least for an intuitive meaning of "involves".

@mikeshulman :
So I made some arguments explicit until I could see why Agda wants to match against SSet in a rewrite rule:

{-# OPTIONS --type-in-type --rewriting --two-level #-}

open import Agda.Primitive public

postulate
  Tel   : SSet
  ε     : Tel
  _≡_   : {A : SSet} (a : A) → A → SSet
  cong  : (A B : SSet) (f : A → B) {x y : A} (p : x ≡ y) → f x ≡ f y
  coe←  : (A B : SSet) → (A ≡ B) → B → A
  el    : Tel → SSet
  []    : el ε
  ID    : (Δ : Tel) → Tel
  ID′   : (Δ : Tel) (Θ : el Δ → Tel) → Tel
  ID′ε  : (Δ : Tel) → ID′ Δ (λ _ → ε) ≡ ε

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE ID′ε #-}

postulate
  ID′-CONST   : (Θ : Tel) (Δ : Tel)

              → ID′ Θ (λ _ → Δ) ≡ ID Δ

  ID′-CONST-ε : (Θ : Tel) (δ₂ : el (ID ε))

              → coe← (el (ID′ Θ (λ _ → ε))) (el (ID ε)) (cong Tel (SSet lzero) el (ID′-CONST Θ ε)) δ₂ ≡ []

{-# REWRITE ID′-CONST-ε #-}

As you can see, you are asking Agda to rewrite anything of the form coe← (el (ID′ Θ (λ _ → ε))) (el (ID ε)) (cong Tel (SSet lzero) el (ID′-CONST Θ ε)) δ₂ to []. Agda, trying to turn the lhs into a pattern crashes because there is no case for SSet:

Just why the author(s) of rewriting with 2ltt thought such a case would be impossible I cannot tell. It would have been reasonable to leave a comment there explaining why they think it is impossible, or a TODO. But most coders seem to have commentophobia...

What you can try is to extend the type of NLPSort by a case for SSet in analogy to PType and then let the GHC type checker take you all the functions where something has to be done about the new PSSet case.
If you get it to work, please submit a PR!

@andreasabel let me try to explain the presence of __IMPOSSIBLE__ here. I have implemented rewriting, which has existed for longer than 2ltt. I also did the prototype implementation of 2ltt during one of the Agda meetings, where I might have written an __IMPOSSIBLE__ since it was just a prototype and I didn't yet want to think about the interaction between the two features. Later, an updated version of --2ltt got merged into master by @Saizan to fix a certain issue with --cubical (I am not sure what exactly), he also fixed a number of things in my prototype implementation including the interaction between --2ltt and --cubical. However, I guess that he does not know the implementation of --rewriting so the __IMPOSSIBLE__ was left in the code (and there was no test case using --2ltt and --rewriting anyway). Which bring us to the current situation.

The good news is that there is no reason to believe there are any difficulties with supporting the combination of --2ltt and --rewriting, it is really just not yet implemented. I don't expect it to be very difficult to support either.

Ah, I see; the problem arises with rewrite rules whose LHS actually includes SSet as an argument to be matched against. Trying to implement it sounds like a fun way to learn more about Agda internals, but unfortunately I don't think it'd be a good use of my time right now. Maybe I'll come back to it later. Thanks!

As long as this remains unimplemented, I do still think it would be nice to give a more informative error message.

Ok I give it a shot...

Thanks!!