[Bug] Deriving a Show instance for Pointwise

[ana-pantilie]

The following code throws an error when compiling:

module Issue where

open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
open import Data.List.Base
open import Agda.Builtin.Sigma

open import Tactic.Derive.Show
open import Tactic.Defaults

unquoteDecl Show-Pointwise = derive-Show ((quote Pointwise , Show-Pointwise) ∷ [])

The error is:

/path/to/Issue.agda:10,1-83
specializeType should never fail! This is a bug!
Error:
TC doesn't provide which error to catch

As discussed in person, I have a recursive type which depends on Pointwise, and defining the Pointwise instance manually doesn't help with deriving the Show instance for the original type. I tried to minimise the code as much as I could, but the example is still a bit complicated:

module Issue where

open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
open import Data.List.Base
open import Agda.Builtin.Sigma
open import Relation.Binary.Core using (REL)
open import Agda.Primitive using (Level)

open import Tactic.Derive.Show
open import Tactic.Defaults

open import Class.Show.Core

data AST (X : Set) : Set where
    constr : (xs : List (AST X)) → AST X

Relation = { X : Set } → AST X → AST X → Set₁

data Translation (R : Relation) { X : Set } : AST X → AST X → Set₁ where
    pointwiseCase
        : {xs xs' : List (AST X)}
        → Pointwise (Translation R) xs xs'
        → Translation R (constr xs) (constr xs')

instance
  Show-Pointwise
    : {a : Level} {A : Set a} {b : Level} {B : Set b} {l : Level}
      {xs : List A} {ys : List B} {r : REL A B l}
    → Show (Pointwise r xs ys)
  Show-Pointwise = mkShow (λ x → "TODO")

unquoteDecl Show-Translation = derive-Show ((quote Translation , Show-Translation) ∷ [])

This throws the same error:

/path/to/Issue.agda:32,1-89
specializeType should never fail! This is a bug!
Error:
TC doesn't provide which error to catch