#10924: Template variable unbound in rewrite rule
-------------------------------------+-------------------------------------
Reporter: crockeea | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.10.2
Keywords: singletons, | Operating System: Unknown/Multiple
templatehaskell |
Architecture: | Type of failure: Compile-time
Unknown/Multiple | crash
Test Case: | Blocked By:
Blocking: | Related Tickets:
Differential Rev(s): |
-------------------------------------+-------------------------------------
The only ticket I see with this issues that *isn't* resolved in 7.10.2 is
#10689. Might be a dup.
Compiling with -O1 succeeds, but `ghc -O2` fails:
{{{
{-# LANGUAGE DataKinds, GADTs, PolyKinds, ScopedTypeVariables,
TemplateHaskell, TypeFamilies, UndecidableInstances #-}
module Bug where
-- needed to use Nat's Num instance for +
import qualified GHC.Num as Num
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Type.Natural
import Data.Typeable
-- | Copied from Data.Type.Natural because the data-level version
-- is not exported there.
(<<=) :: Nat -> Nat -> Bool
Z <<= _ = True
S _ <<= Z = False
S n <<= S m = n <<= m
singletons [d|
newtype PrimePower = PP (Nat,Nat) deriving (Eq,Show,Typeable)
|]
singletons [d|
ppMul :: PrimePower -> [PrimePower] -> [PrimePower]
ppMul x [] = [x]
ppMul x@(PP(p,e)) pps@(PP (p',e'):pps')
| p == p' = PP(p,e Num.+ e'):pps'
| p <<= p' = x:pps
| otherwise = (PP(p',e')):ppMul x pps'
|]
}}}
{{{
ghc: panic! (the 'impossible' happened)
(GHC version 7.10.2 for x86_64-unknown-linux):
Template variable unbound in rewrite rule
t_XexU
[t_aev4, t_aev5, n0_aeyH, n1_aeyI, n0_aeyV, n1_aeyW, ipv_sfxT,
sc_sg53, sc_sg54, sg_sg55, sg_sg56, sc_sg57]
[t_XexU, t_XexW, n0_XeBz, n1_XeBB, n0_XeBP, n1_XeBR, ipv_XfAP,
sc_Xg80, sc_Xg82, sg_Xg84, sg_Xg86, sc_Xg88]
[TYPE Let1627437970XSym7
n0_aeyH n1_aeyI n0_aeyV n1_aeyW ipv_sfxT t_aev4 t_aev5,
TYPE ipv_sfxT,
(SPP
@ ('PP ((Tuple2Sym0 @@ n0_aeyH) @@ n1_aeyI))
@ ((Tuple2Sym0 @@ n0_aeyH) @@ n1_aeyI)
@~ <'PP ((Tuple2Sym0 @@ n0_aeyH) @@ n1_aeyI)>_N
((STuple2
@ Nat
@ Nat
@ '(n0_aeyH, n1_aeyI)
@ n0_aeyH
@ n1_aeyI
@~ <'(n0_aeyH, n1_aeyI)>_N
sc_sg53
sc_sg54)
`cast` (sg_sg55
:: R:Sing(,)z '(n0_aeyH, n1_aeyI)
~R# Sing (Apply (Apply Tuple2Sym0 n0_aeyH) n1_aeyI))))
`cast` (sg_sg56
:: R:SingPrimePowerz
('PP (Apply (Apply Tuple2Sym0 n0_aeyH) n1_aeyI))
~R# Sing
(Apply PPSym0 (Apply (Apply Tuple2Sym0 n0_aeyH)
n1_aeyI))),
sc_sg57]
[TYPE Let1627437970XSym7
n0_aeyH
n1_aeyI
n0_XeB0
n1_XeB2
ipv_XfzF
(Let1627437970XSym7
n0_aeyH n1_aeyI n0_aeyV n1_aeyW ipv_sfxT t_aev4 t_aev5)
ipv_sfxT,
TYPE ipv_XfzF,
(SPP
@ ('PP ((Tuple2Sym0 @@ n0_aeyH) @@ n1_aeyI))
@ ((Tuple2Sym0 @@ n0_aeyH) @@ n1_aeyI)
@~ <'PP ((Tuple2Sym0 @@ n0_aeyH) @@ n1_aeyI)>_N
((STuple2
@ Nat
@ Nat
@ '(n0_aeyH, n1_aeyI)
@ n0_aeyH
@ n1_aeyI
@~ <'(n0_aeyH, n1_aeyI)>_N
sc_sg53
sc_sg54)
`cast` (Sub (Sym (TFCo:R:Sing(,)z[0] <Nat>_N <Nat>_N)) (Sym
(TFCo:R:Apply(,)kTuple2Sym1l0[0]
<Nat>_N
<Nat>_N