#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]