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 |