[GHC] #10427: Template variable unbound in rewrite rule

[GHC]

#10427: Template variable unbound in rewrite rule
-------------------------------------+-------------------------------------
              Reporter:  crockeea    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.1
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 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):

 {{{#!hs
 {-# 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10427>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler