Template variable unbound in rewrite rule

This may be due to a bug in [singletons](https://hackage.haskell.org/package/singletons), but GHC requested I post a bug here, so I am dutifully complying.

The following code fails with -O2 (but succeeds with -O1):

{-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds,
             ScopedTypeVariables, TemplateHaskell, 
             TypeFamilies, UndecidableInstances #-}

module Error where

import qualified GHC.Num as Num

import Data.Singletons.Prelude hiding (sMin, sMax, MinSym0, MaxSym0)
import Data.Singletons.TH
import Data.Type.Natural         as N hiding ((:-))

singletons [d|
            newtype Foo = Bar Nat deriving (Eq,Show)
            |]

singletons [d|
            ppMul :: Foo -> [Foo] -> [Foo]
            ppMul x@(Bar p) pps@((Bar p'):pps') = (Bar p'):ppMul x pps'
            |]

with the message

ghc: panic! (the 'impossible' happened)
  (GHC version 7.10.1 for x86_64-unknown-linux):
	Template variable unbound in rewrite rule
  n_Xdkc
  [n_adis, n1_adix, n_adiA, sc_se5w, sg_se5x, sc_se5y]
  [n_Xdk2, n1_Xdk8, n_Xdkc, sc_Xe79, sg_Xe7b, sc_Xe7d]
  [TYPE Let_1627437169XSym3 n_adis n_adiA n1_adix, TYPE n1_adix,
   (SBar @ ('Bar n_adis) @ n_adis @~ <'Bar n_adis>_N sc_se5w)
   `cast` (sg_se5x
           :: R:SingFooz (BarSym1 n_adis) ~R# Sing (Apply BarSym0 n_adis)),
   sc_se5y]
  [TYPE Let_1627437169XSym3 n_adis n_XdjP n1_XdjH, TYPE n1_XdjH,
   (SBar @ ('Bar n_adis) @ n_adis @~ <'Bar n_adis>_N sc_se5w)
   `cast` (Sub (Sym TFCo:R:SingFooz[0]) (Sym
                                           (TFCo:R:ApplyFooNatBarSym0l0[0] <n_adis>_N))
           :: R:SingFooz (BarSym1 n_adis) ~R# Sing (Apply BarSym0 n_adis)),
   sPps'_aciK]

I found that if I rewrite ppmul as

ppMul x pps@((Bar p'):pps') = (Bar p'):ppMul x pps'

(i.e. remove the pattern match on x), then ghc -02 succeeds.

Trac metadata

Trac field	Value
Version	7.10.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture