#10924: Template variable unbound in rewrite rule -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: singletons, | templatehaskell Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): -------------------------------------+------------------------------------- Description changed by crockeea: Old description:
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
_N _N) ; (Apply (Sym (TFCo:R:Apply(->)kTuple2Sym0l0[0] <Nat>_N <Nat>_N _N)) _N)_N) :: R:Sing(,)z (Tuple2Sym2 n0_aeyH n1_aeyI) ~R# Sing (Apply (Apply Tuple2Sym0 n0_aeyH) n1_aeyI)))) `cast` (Sub (Sym TFCo:R:SingPrimePowerz[0]) (Sym (TFCo:R:ApplyPrimePower(,)PPSym0l0[0] <(Tuple2Sym0 @@ n0_aeyH) @@ n1_aeyI>_N)) :: R:SingPrimePowerz (PPSym1 ((Tuple2Sym0 @@ n0_aeyH) @@ n1_aeyI)) ~R# Sing (Apply PPSym0 ((Tuple2Sym0 @@ n0_aeyH) @@ n1_aeyI))), ipv_sfxW] }}}
New description:
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