Opened 3 years ago

Closed 3 years ago

#10427 closed bug (duplicate)

Template variable unbound in rewrite rule

Reported by: crockeea Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.1
Keywords: 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

This may be due to a bug in [singletons](https://hackage.haskell.org/package/singletons), but GHC requested I post a bug here, so I am dutifully complying.

The following code fails with -O2 (but succeeds with -O1):

{-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds,
             ScopedTypeVariables, TemplateHaskell, 
             TypeFamilies, UndecidableInstances #-}

module Error where

import qualified GHC.Num as Num

import Data.Singletons.Prelude hiding (sMin, sMax, MinSym0, MaxSym0)
import Data.Singletons.TH
import Data.Type.Natural         as N hiding ((:-))

singletons [d|
            newtype Foo = Bar Nat deriving (Eq,Show)
            |]

singletons [d|
            ppMul :: Foo -> [Foo] -> [Foo]
            ppMul x@(Bar p) pps@((Bar p'):pps') = (Bar p'):ppMul x pps'
            |]

with the message

ghc: panic! (the 'impossible' happened)
  (GHC version 7.10.1 for x86_64-unknown-linux):
	Template variable unbound in rewrite rule
  n_Xdkc
  [n_adis, n1_adix, n_adiA, sc_se5w, sg_se5x, sc_se5y]
  [n_Xdk2, n1_Xdk8, n_Xdkc, sc_Xe79, sg_Xe7b, sc_Xe7d]
  [TYPE Let_1627437169XSym3 n_adis n_adiA n1_adix, TYPE n1_adix,
   (SBar @ ('Bar n_adis) @ n_adis @~ <'Bar n_adis>_N sc_se5w)
   `cast` (sg_se5x
           :: R:SingFooz (BarSym1 n_adis) ~R# Sing (Apply BarSym0 n_adis)),
   sc_se5y]
  [TYPE Let_1627437169XSym3 n_adis n_XdjP n1_XdjH, TYPE n1_XdjH,
   (SBar @ ('Bar n_adis) @ n_adis @~ <'Bar n_adis>_N sc_se5w)
   `cast` (Sub (Sym TFCo:R:SingFooz[0]) (Sym
                                           (TFCo:R:ApplyFooNatBarSym0l0[0] <n_adis>_N))
           :: R:SingFooz (BarSym1 n_adis) ~R# Sing (Apply BarSym0 n_adis)),
   sPps'_aciK]

I found that if I rewrite ppmul as

ppMul x pps@((Bar p'):pps') = (Bar p'):ppMul x pps'

(i.e. remove the pattern match on x), then ghc -02 succeeds.

Change History (1)

comment:1 Changed 3 years ago by goldfire

Resolution: duplicate
Status: newclosed

Appears to be a duplicate of #10251, which appears to be fixed for 7.10.2.

Note: See TracTickets for help on using tickets.