Opened 4 years ago

Closed 4 years ago

#10924 closed bug (fixed)

Template variable unbound in rewrite rule

Reported by: crockeea Owned by:
Priority: normal Milestone: 7.10.3
Component: Compiler Version: 7.10.2
Keywords: singletons, templatehaskell Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by crockeea)

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.

Change History (4)

comment:1 Changed 4 years ago by crockeea

Description: modified (diff)

comment:2 Changed 4 years ago by thomie

Milestone: 7.10.3

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.

comment:3 Changed 4 years ago 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.

comment:4 Changed 4 years ago by bgamari

Resolution: fixed
Status: newclosed

The fix for #10689 will be present in 7.10.3. Closing.

Note: See TracTickets for help on using tickets.