Skip to content

Template variable unbound in rewrite rule

The only ticket I see with this issues that *isn't* resolved in 7.10.2 is #10689 (closed). 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.

Edited by Eric Crockett
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information