[GHC] #10924: Template variable unbound in rewrite rule
#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
#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
#10924: Template variable unbound in rewrite rule -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.10.3 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): -------------------------------------+------------------------------------- Changes (by thomie): * milestone: => 7.10.3 Comment: I can reproduce this issue with ghc-7.10.2.20150906 (commit 108e35ff67586ffd570ca18d84a4f5fbf79727cc), which doesn't include the fix for #10689 yet. Run `cabal install --with-ghc=/opt/ghc/7.10.3/bin/ghc type-natural singletons` first. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10924#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10924: Template variable unbound in rewrite rule -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.10.3 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): -------------------------------------+------------------------------------- Comment (by crockeea): I did figure out a workaround: don't use "as-patterns" at all. The following definition of `ppMul` compiles: {{{ ppMul :: PrimePower -> [PrimePower] -> [PrimePower] ppMul x [] = [x] ppMul (PP(p,e)) (PP (p',e'):pps') | p == p' = PP(p,e Num.+ e'):pps' | p <<= p' = (PP(p,e)):(PP (p',e'):pps') | otherwise = (PP(p',e')):ppMul (PP(p,e)) pps' }}} Since the point of using singletons is to get type-level functions, it's not clear that there is any performance overhead (except perhaps in the compiler) by rebuilding `PP(p,e)` and `PP(p,e')`, but it would be nice to be able to write this in a more idiomatic manner. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10924#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10924: Template variable unbound in rewrite rule -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: 7.10.3 Component: Compiler | Version: 7.10.2 Resolution: fixed | 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): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => closed * resolution: => fixed Comment: The fix for #10689 will be present in 7.10.3. Closing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10924#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC