[GHC] #13882: Template variable unbound in rewrite rule
GHC
ghc-devs at haskell.org
Wed Jun 28 08:38:35 UTC 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
More information about the ghc-tickets
mailing list