Template variable unbound in rewrite rule

[guest]

I was trying to compile the latest darcs source (darcs get --lazy  http://darcs.net) using ghc7. I had to modify darcs.cabal to add NoMonoLocalBinds to 3 places (just search for extensions, and add it to the END of the lists).

When I do a build I get this:

[ 65 of 154] Compiling Darcs.Patch.V1.Commute ( src/Darcs/Patch/V1/Commute.lhs, dist/build/Darcs/Patch/V1/Commute.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 7.0.1 for i386-unknown-linux):
	Template variable unbound in rewrite rule
    sg_s2vkQ{tv} [co]
    [x{tv a2uFt} [sk], y{tv a2uFu} [sk], sg_s2vkQ{tv} [co],
     sc_s2vkR{v} [lid], sc_s2vkS{v} [lid]]
    [x{tv X2uJc} [sk], y{tv X2uJe} [sk], sg_s2vkQ{tv} [co],
     sc_s2vkR{v} [lid], sc_s2vkS{v} [lid]]
    [TYPE y{tv a2uFu} [sk], TYPE y{tv a2uFu} [sk],
     TYPE x{tv a2uFt} [sk], TYPE x{tv a2uFt} [sk],
     TYPE x{tv a2uFt} [sk], sc_s2vkS{v} [lid], sc_s2vkR{v} [lid],
     darcs-2.5:Darcs.Witnesses.Ordered.NilRL{v ruI5} [gid[DataCon]]
       @ darcs-2.5:Darcs.Patch.V1.Core.Patch{tc r1EYF}
       @ x{tv a2uFt} [sk]
       @ x{tv a2uFt} [sk]
       @ x{tv a2uFt} [sk]]
    [TYPE y{tv a2uFu} [sk], TYPE y{tv a2uFu} [sk],
     TYPE x{tv a2uFt} [sk], TYPE x{tv a2uFt} [sk],
     TYPE x{tv a2uFt} [sk], wild_s2vhT{v} [lid], sc_s2vke{v} [lid],
     darcs-2.5:Darcs.Witnesses.Ordered.NilRL{v ruI5} [gid[DataCon]]
       @ darcs-2.5:Darcs.Patch.V1.Core.Patch{tc r1EYF}
       @ x{tv a2uFt} [sk]
       @ x{tv a2uFt} [sk]
       @ x{tv a2uFt} [sk]]

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

As an additional data point, this module builds correctly without NoMonoLocalBinds. The reason I was adding NoMonoLocalBinds to the .cabal file is because I can't use #if __GLASGOW_HASKELL >= 700 to conditionally add in this language flag. The reason is because ghc6 will not correctly understand the language flag appearing inside a CPP #if/#endif block and I want this code to compile on ghc6 and 7.

Please let me know if I can provide additional information to help reproduce this bug. My email address is dagitj on gmail, also on CC of this ticket.

[guest]

After about 6 hours of trying to boil this down to a minimal test case I have some new information. Initially I thought this was a type error so I reported it as affecting the type checker. I now think this is an optimization bug. Below is a standalone program that triggers the bug:

{-# LANGUAGE 
        GADTs,
        TypeOperators,
        ScopedTypeVariables,
        RankNTypes,
        NoMonoLocalBinds
 #-}
{-# OPTIONS_GHC -O2 #-}
{-
  Copyright (C) 2002-2003 David Roundy

  This program is free software; you can redistribute it and/or modify
  it under the terms of the GNU General Public License as published by
  the Free Software Foundation; either version 2, or (at your option)
  any later version.

  This program is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  GNU General Public License for more details.

  You should have received a copy of the GNU General Public License
  along with this program; see the file COPYING.  If not, write to
  the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
  Boston, MA 02110-1301, USA.
-}

module Foo where

import Data.Maybe ( mapMaybe )
import Control.Monad ( MonadPlus, mplus, msum, mzero )
import Unsafe.Coerce (unsafeCoerce)

newtype FileName = FN FilePath deriving ( Eq, Ord )

data FL a x z where
    (:>:) :: a x y -> FL a y z -> FL a x z
    NilFL :: FL a x x
data RL a x z where
    (:<:) :: a y z -> RL a x y -> RL a x z
    NilRL :: RL a x x
data (a1 :> a2) x y = forall z. (a1 x z) :> (a2 z y)
infixr 1 :>
data (a1 :< a2) x y = forall z. (a1 z y) :< (a2 x z)
infix 1 :<
infixr 5 :>:, :<:

data EqCheck a b where
    IsEq :: EqCheck a a
    NotEq :: EqCheck a b

class MyEq p => Invert p where
    invert :: p x y -> p y x
    identity :: p x x

class MyEq p where
    unsafeCompare :: p a b -> p c d -> Bool
    unsafeCompare a b = IsEq == (a =/\= unsafeCoerceP b)

    (=\/=) :: p a b -> p a c -> EqCheck b c
    a =\/= b | unsafeCompare a b = unsafeCoerceP IsEq
             | otherwise = NotEq

    (=/\=) :: p a c -> p b c -> EqCheck a b
    a =/\= b | IsEq == (a =\/= unsafeCoerceP b) = unsafeCoerceP IsEq
             | otherwise = NotEq

infix 4 =\/=, =/\=

class Commute p where
    commute :: (p :> p) x y -> Maybe ((p :> p) x y)

instance (MyEq p, Commute p) => MyEq (FL p) where
instance (MyEq p, Commute p) => MyEq (RL p) where
instance Commute p => Commute (RL p) where
instance (Commute p, Invert p) => Invert (RL p) where
instance (Invert p, Commute p) => Invert (FL p) where
instance Eq (EqCheck a b) where
instance MyEq FilePatchType where
instance Invert Patch where

instance MyEq Patch where
    unsafeCompare = eqPatches

eqPatches :: Patch x y -> Patch w z -> Bool
eqPatches (PP p1) (PP p2) = undefined
eqPatches (Merger _ _ p1a p1b) (Merger _ _ p2a p2b)
 = eqPatches p1a p2a &&
   eqPatches p1b p2b
eqPatches (Regrem _ _ p1a p1b) (Regrem _ _ p2a p2b)
 = eqPatches p1a p2a &&
   eqPatches p1b p2b
eqPatches _ _ = False

data Prim x y where
    FP :: !FileName -> !(FilePatchType x y) -> Prim x y

data FilePatchType x y = FilePatchType
                            deriving (Eq,Ord)

data Patch x y where
    PP :: Prim x y -> Patch x y
    Merger :: FL Patch x y
           -> RL Patch x b
           -> Patch c b
           -> Patch c d
           -> Patch x y
    Regrem :: FL Patch x y
           -> RL Patch x b
           -> Patch c b
           -> Patch c a
           -> Patch y x

data Sealed a where
    Sealed :: a x -> Sealed a
data FlippedSeal a y where
    FlippedSeal :: !(a x y) -> FlippedSeal a y

mapFlipped :: (forall x. a x y -> b x z) -> FlippedSeal a y -> FlippedSeal b z
mapFlipped f (FlippedSeal x) = FlippedSeal (f x)

headPermutationsRL :: Commute p => RL p x y -> [RL p x y]
headPermutationsRL NilRL = []
headPermutationsRL (p:<:ps) =
    (p:<:ps) : mapMaybe (swapfirstRL.(p:<:)) (headPermutationsRL ps)
        where swapfirstRL (p1:<:p2:<:xs) = do p1':>p2' <- commute (p2:>p1)
                                              Just $ p2':<:p1':<:xs
              swapfirstRL _ = Nothing

is_filepatch :: Prim x y -> Maybe FileName
is_filepatch (FP f _) = Just f
is_filepatch _ = Nothing

toFwdCommute :: (Commute p, Commute q, Monad m)
             => ((p :< q) x y -> m ((q :< p) x y))
             -> (q :> p) x y -> m ((p :> q) x y)
toFwdCommute c (x :> y) = do x' :< y' <- c (y :< x)
                             return (y' :> x')

unsafeUnseal :: Sealed a -> a x
unsafeUnseal (Sealed a) = unsafeCoerceP1 a

unsafeUnsealFlipped :: FlippedSeal a y -> a x y
unsafeUnsealFlipped (FlippedSeal a) = unsafeCoerceP a

unsafeCoerceP :: a x y -> a b c
unsafeCoerceP = unsafeCoerce

unsafeCoercePStart :: a x1 y -> a x2 y
unsafeCoercePStart = unsafeCoerce

unsafeCoercePEnd :: a x y1 -> a x y2
unsafeCoercePEnd = unsafeCoerce

unsafeCoerceP1 :: a x -> a y
unsafeCoerceP1 = unsafeCoerce

data Perhaps a = Unknown | Failed | Succeeded a

instance  Monad Perhaps where
    (Succeeded x) >>= k =  k x
    Failed   >>= _      =  Failed
    Unknown  >>= _      =  Unknown
    Failed   >> _       =  Failed
    (Succeeded _) >> k  =  k
    Unknown  >> k       =  k
    return              =  Succeeded
    fail _              =  Unknown

instance  MonadPlus Perhaps where
    mzero                 = Unknown
    Unknown `mplus` ys    = ys
    Failed  `mplus` _     = Failed
    (Succeeded x) `mplus` _ = Succeeded x

toMaybe :: Perhaps a -> Maybe a
toMaybe (Succeeded x) = Just x
toMaybe _ = Nothing

cleverCommute :: CommuteFunction -> CommuteFunction
cleverCommute c (p1:<p2) =
    case c (p1 :< p2) of
    Succeeded x -> Succeeded x
    Failed -> Failed

speedyCommute :: CommuteFunction
speedyCommute (p1 :< p2) -- Deal with common case quickly!
    | p1_modifies /= Nothing && p2_modifies /= Nothing &&
      p1_modifies /= p2_modifies = undefined
    | otherwise = Unknown
    where p1_modifies = isFilepatchMerger p1
          p2_modifies = isFilepatchMerger p2

everythingElseCommute :: MaybeCommute -> CommuteFunction
everythingElseCommute _ x = undefined

unsafeMerger :: String -> Patch x y -> Patch x z -> Patch a b
unsafeMerger x p1 p2 = unsafeCoercePStart $ unsafeUnseal $ merger x p1 p2

mergerCommute :: (Patch :< Patch) x y -> Perhaps ((Patch :< Patch) x y)
mergerCommute (Merger _ _ p1 p2 :< pA)
    | unsafeCompare pA p1 = Succeeded (unsafeMerger "0.0" p2 p1 :< unsafeCoercePStart p2)
    | unsafeCompare pA (invert (unsafeMerger "0.0" p2 p1)) = Failed
mergerCommute (Merger _ _
                (Merger _ _ c b)
                (Merger _ _ c' a) :<
                Merger _ _ b' c'')
    | unsafeCompare b' b && unsafeCompare c c' && unsafeCompare c c'' = undefined
mergerCommute _ = Unknown

instance Commute Patch where
    commute x = toMaybe $ msum
                  [toFwdCommute speedyCommute x,
                   toFwdCommute (cleverCommute mergerCommute) x,
                   toFwdCommute (everythingElseCommute undefined) x
                  ]

isFilepatchMerger :: Patch x y -> Maybe FileName
isFilepatchMerger (PP p) = is_filepatch p
isFilepatchMerger (Regrem und unw p1 p2)
    = isFilepatchMerger (Merger und unw p1 p2)

type CommuteFunction = forall x y. (Patch :< Patch) x y -> Perhaps ((Patch :< Patch) x y)
type MaybeCommute = forall x y. (Patch :< Patch) x y -> Maybe ((Patch :< Patch) x y)

{- unwind, trueUnwind, reconcleUnwindings, and merger are most likely
 where the problem lies.  Everything above is just brought in to bring
 in enough context so that those four will compile. -}
unwind :: Patch x y -> Sealed (RL Patch x) -- Recreates a patch history in reverse.
unwind (Merger _ unwindings _ _) = Sealed unwindings
unwind p = Sealed (p :<: NilRL)

trueUnwind :: Patch x y -> Sealed (RL Patch x) -- Recreates a patch history in reverse.
trueUnwind p@(Merger _ _ p1 p2) =
    case (unwind p1, unwind p2) of
    (Sealed (_:<:p1s),Sealed (_:<:p2s)) ->
         Sealed (p :<: unsafeCoerceP p1 :<: unsafeUnsealFlipped (reconcileUnwindings p1s (unsafeCoercePEnd p2s)))

reconcileUnwindings :: RL Patch x z -> RL Patch y z -> FlippedSeal (RL Patch) z
reconcileUnwindings p1s NilRL = FlippedSeal p1s
reconcileUnwindings (p1:<:_) (p2:<:_) =
    case [undefined | p1s'@(_:<:_) <- headPermutationsRL (p1:<:undefined)] of
    ((_:<:p1s', _:<:p2s'):_) ->
        mapFlipped (undefined :<:) $ reconcileUnwindings p1s' (unsafeCoercePEnd p2s')

merger :: String -> Patch x y -> Patch x z -> Sealed (Patch y)
merger "0.0" p1 p2 = Sealed $ Merger undoit unwindings p1 p2
    where fake_p = Merger identity NilRL p1 p2
          unwindings = unsafeUnseal (trueUnwind fake_p)
          p = undefined
          undoit = undefined

If you save this to Foo.hs then you should be able to reproduce my crash with:

ghc --make Foo.hs

When I run it, I get this:

$ ghc Foo.hs --make
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 7.0.1 for i386-unknown-linux):
	Template variable unbound in rewrite rule
    sg_sVX{tv} [co]
    [c{tv aBJ} [sk], sg_sVX{tv} [co], sc_sVY{v} [lid]]
    [c{tv aBJ} [sk], sg_sVX{tv} [co], sc_sVY{v} [lid]]
    [TYPE c{tv aBJ} [sk], TYPE c{tv aBJ} [sk], TYPE c{tv aBJ} [sk],
     sc_sVY{v} [lid],
     main:Foo.NilRL{v rI} [gid[DataCon]]
       @ main:Foo.Patch{tc r2R}
       @ c{tv aBJ} [sk]
       @ c{tv aBJ} [sk]
       @ c{tv aBJ} [sk]]
    [TYPE x{tv aC4} [sk], TYPE x{tv aC4} [sk], TYPE x{tv aC4} [sk],
     sc_sWe{v} [lid],
     main:Foo.NilRL{v rI} [gid[DataCon]]
       @ main:Foo.Patch{tc r2R}
       @ x{tv aC4} [sk]
       @ x{tv aC4} [sk]
       @ x{tv aC4} [sk]]

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

I apologize for the size of the program (it's not very minimal), but I spent several hours trying to trim it down and this was the best I could manage. I left the copyright notice in there because it is pulled directly from the darcs source, and hence technically it's a derivative work.

Some important points:

• The crash only appears at -O2 and -O3, specifically not at -O1
• The crash only happens with -XNoMonoLocalBinds
• The source of the problem is most likely within the last 4 definitions in the file, everything else just seems to need to be there so the compilation gets far enough to fail. Try replacing things with undefined to see what I mean.

My hunch is that the problem lies in reconcileUnwindings. Again, sorry for such a large test case, but hopefully someone can take it from here.

Thanks!

[simonpj]

Great. I see it. Fixed by

Thu Nov 25 09:23:56 PST 2010  simonpj@microsoft.com
  * Substitution should just substitute, not optimise
  
  This was causing Trac #4524, by optimising
       (e |> co)  to   e
  on the LHS of a rule.  Result, the template variable
  'co' wasn't bound any more.
  
  Now that substition doesn't optimise, it seems sensible to call
  simpleOptExpr rather than substExpr when substituting in the
  RHS of rules.  Not a big deal either way.

    M ./compiler/coreSyn/CoreSubst.lhs -10 +14

Please merge.

Simon

[igloo]

Merged.