[GHC] #10924: Template variable unbound in rewrite rule

[GHC]

#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
 <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]
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10924>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler