Re: [GHC] #13882: Template variable unbound in rewrite rule

28 Jun 2017


      #13882: Template variable unbound in rewrite rule
-------------------------------------+-------------------------------------
        Reporter:  achirkin          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1-rc2
      Resolution:                    |             Keywords:
Operating System:  Linux             |         Architecture:  x86_64
 Type of failure:  Compile-time      |  (amd64)
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

@@ -149,0 +149,23 @@
+
+ UPDATE 28.06.2017:
+ Interestingly, the two variants below compile fine with `-O2`:
+ {{{#!hs
+ concatDim :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim
+ (xs ++ ys)
+ concatDim D ys         = ys
+ concatDim xs D         = xs
+ concatDim (x :* xs) ys = case unsafeCoerce Refl :: (xs ++ ys) :~: (Head xs
+ ': (Tail xs ++ ys)) of
+       Refl -> x :* concatDim xs ys
+ {-# NOINLINE concatDim #-}
+ }}}
+
+ {{{#!hs
+ concatDim :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim
+ (xs ++ ys)
+ concatDim D ys         = ys
+ concatDim xs D         = xs
+ concatDim (x :* xs) ys = case unsafeCoerce Refl :: (xs ++ ys) :~: (Head xs
+ ': (Tail xs ++ ys)) of
+       Refl -> x :* concatDim (undefined :: Dim (Tail xs)) ys
+ }}}

New description:

 I'm getting GHC panic on `GHC 8.0.1`, `GHC 8.2.1-rc1`, and `GHC
 8.2.1-rc2`.
 I think this error can somehow be related to
 https://ghc.haskell.org/trac/ghc/ticket/10924 or
 https://ghc.haskell.org/trac/ghc/ticket/13410 .

 On all three versions of compiler it builds fine with `-O1` or `-O0`.
 With `-O2` it crashes with the following error:

 {{{
 [1 of 1] Compiling Numeric.Dimensions.Dim ( Dim.hs, Dim.o )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.2.0.20170507 for x86_64-unknown-linux):
         Template variable unbound in rewrite rule
   Variable: ipv_s1e7
   Rule "SC:concatDim0"
   Rule bndrs: [ipv_s1ee, ipv_s1ed, ipv_s1ef, ys_a19R, ipv_s1e4,
                ipv_s1e6, sc_s1fF, sc_s1fG, sc_s1fH, sc_s1fI, sc_s1fE,
 ipv_s1e7]
   LHS args: [TYPE: (ipv1_s1e6 |> ([Nth:0 (Sym ipv2)])_N),
              TYPE: ys_a19R, sc_s1fE,
              :*
                @ [Nat]
                @ ys_a19R
                @ ipv_s1ed
                @ ipv_s1ee
                @ ipv1_s1ef
                @~ (sc_s1fF :: ([Nat] :: *) ~# ([ipv_s1ed] :: *))
                @~ (sc_s1fG
                    :: (ys_a19R :: [Nat])
                       ~#
                       (ConsDim ipv_s1ee ipv2_s1ef :: [ipv1_s1ed]))
                sc_s1fH
                sc_s1fI]
   Actual args: [TYPE: (ipv1_X1eZ |> ([Nth:0 (Sym ipv2)])_N),
                 TYPE: ys_a19R,
                 ipv_s1ea
                 `cast` ((Dim
                            ([Nth:0 (Sym ipv)])_N (Sym (Coh <ipv>_N ([Nth:0
 (Sym ipv)])_N)))_R
                         :: (Dim ipv1_X1eZ :: *)
                            ~R#
                            (Dim (ipv1_X1eZ |> ([Nth:0 (Sym ipv2)])_N) ::
 *)),
                 :*
                   @ [Nat]
                   @ ys_a19R
                   @ ipv_s1ed
                   @ ipv_s1ee
                   @ ipv1_s1ef
                   @~ (sc_s1fF :: ([Nat] :: *) ~# ([ipv_s1ed] :: *))
                   @~ (sc_s1fG
                       :: (ys_a19R :: [Nat])
                          ~#
                          (ConsDim ipv_s1ee ipv2_s1ef :: [ipv1_s1ed]))
                   sc_s1fH
                   sc_s1fI]
   Call stack:
       CallStack (from HasCallStack):
         prettyCurrentCallStack, called at
 compiler/utils/Outputable.hs:1134:58 in ghc:Outputable
         callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in
 ghc:Outputable
         pprPanic, called at compiler/specialise/Rules.hs:584:19 in
 ghc:Rules

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

 }}}


 Here is a minimal example I could come up with.
 Function `concatDim` is what causes the panic.

 {{{#!hs
 {-# LANGUAGE DataKinds                 #-}
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE KindSignatures            #-}
 {-# LANGUAGE PolyKinds                 #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
 {-# LANGUAGE TypeFamilyDependencies    #-}
 {-# LANGUAGE TypeOperators             #-}
 {-# LANGUAGE UndecidableInstances      #-}

 module Numeric.Dimensions.Dim (Dim (..), concatDim) where

 import           Data.Type.Equality      ((:~:)(..))
 import           GHC.TypeLits  (Nat, TypeError, ErrorMessage (..))
 import           Unsafe.Coerce (unsafeCoerce)


 -- | Type-level dimensionality
 data Dim (ns :: k) where
   D   :: Dim '[]
   (:*) :: forall (n::Nat) (ns::[k]) . Dim n -> Dim ns -> Dim (ConsDim n
 ns)
   Dn :: forall (n :: Nat) . Dim (n :: Nat)
 infixr 5 :*

 -- | Either known or unknown at compile-time natural number
 data XNat = XN Nat | N Nat
 -- | Unknown natural number, known to be not smaller than the given Nat
 type XN (n::Nat) = 'XN n
 -- | Known natural number
 type N (n::Nat) = 'N n

 -- | List concatenation
 type family (as :: [k]) ++ (bs :: [k]) :: [k] where
     (++) '[] bs = bs
     (++) as '[] = as
     (++) (a ': as) bs = a ': (as ++ bs)
 infixr 5 ++

 type family Head (xs :: [k]) :: k where
     Head (x ': xs) = x
     Head '[]       = TypeError ( 'Text
       "Head -- empty type-level list."
      )

 type family Tail (xs :: [k]) :: [k] where
     Tail (x ': xs) = xs
     Tail '[]       = TypeError ( 'Text
       "Tail -- empty type-level list."
      )

 -- | Unify usage of XNat and Nat.
 --   This is useful in function and type definitions.
 --   Mainly used in the definition of Dim.
 type family ConsDim (x :: l) (xs :: [k]) = (ys :: [k]) | ys -> x xs l
 where
     ConsDim (x :: Nat) (xs :: [Nat])  = x    ': xs
     ConsDim (x :: Nat) (xs :: [XNat]) = N x  ': xs
     ConsDim (XN m)     (xs :: [XNat]) = XN m ': xs

 concatDim :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim
 (xs ++ ys)
 concatDim D ys         = ys
 concatDim xs D         = xs
 concatDim (x :* xs) ys = case unsafeCoerce Refl :: (xs ++ ys) :~: (Head xs
 ': (Tail xs ++ ys)) of
       Refl -> x :* concatDim xs ys

 }}}

 I am a little bit suspicious about `unsafeCoerce Refl`, but it worked in
 all other places so far.
 So if you find it not a bug but my incorrect usage of `unsafeCoerce`,
 please explain me why :)

 UPDATE 28.06.2017:
 Interestingly, the two variants below compile fine with `-O2`:
 {{{#!hs
 concatDim :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim
 (xs ++ ys)
 concatDim D ys         = ys
 concatDim xs D         = xs
 concatDim (x :* xs) ys = case unsafeCoerce Refl :: (xs ++ ys) :~: (Head xs
 ': (Tail xs ++ ys)) of
       Refl -> x :* concatDim xs ys
 {-# NOINLINE concatDim #-}
 }}}

 {{{#!hs
 concatDim :: forall (xs :: [Nat]) (ys :: [Nat]) . Dim xs -> Dim ys -> Dim
 (xs ++ ys)
 concatDim D ys         = ys
 concatDim xs D         = xs
 concatDim (x :* xs) ys = case unsafeCoerce Refl :: (xs ++ ys) :~: (Head xs
 ': (Tail xs ++ ys)) of
       Refl -> x :* concatDim (undefined :: Dim (Tail xs)) ys
 }}}

--

Comment (by achirkin):

 After some experimenting added two examples illustrating the strange
 optimizer behaviour.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13882#comment:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

    