#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 <n1_aeyI>_N <n0_aeyH>_N) ; (Apply (Sym (TFCo:R:Apply(->)kTuple2Sym0l0[0] <Nat>_N <Nat>_N <n0_aeyH>_N)) <n1_aeyI>_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 <n1_aeyI>_N <n0_aeyH>_N) ; (Apply (Sym (TFCo:R:Apply(->)kTuple2Sym0l0[0] <Nat>_N <Nat>_N <n0_aeyH>_N)) <n1_aeyI>_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] }}} I'd love a workaround if possible; I've been unable to find one. -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10924#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler