[GHC] #10924: Template variable unbound in rewrite rule
GHC
ghc-devs at haskell.org
Thu Oct 1 21:15:34 UTC 2015
#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
More information about the ghc-tickets
mailing list