Regression: panic! on inaccessible code with constraint
Running the following program with ghci-8.0.1:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Prove where
data Nat = Zero | Succ Nat
data SNat (n :: Nat) where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
type family (:+:) (a :: Nat) (b :: Nat) :: Nat where
m :+: Zero = m
m :+: (Succ n) = Succ (m :+: n)
sadd :: ((Succ n1 :+: n) ~ Succ (n1 :+: n), (Succ n1) ~ m) => SNat m -> SNat n -> SNat (m :+: n)
sadd SZero n = n
-ddump-tc-trace shows:
...
dischargeFmv
s_a9qV[fuv:4] = t_a9qW[tau:5]
(1 kicked out)
doTopReactFunEq (occurs)
old_ev: [D] _ :: ((n1_a9qu[sk] :+: 'Succ s_a9qV[fuv:4]) :: Nat)
GHC.Prim.~#
(s_a9qV[fuv:4] :: Nat)ghc: panic! (the 'impossible' happened)
(GHC version 8.0.1 for x86_64-unknown-linux):
ctEvCoercion
[D] _ :: (t_a9qW[tau:5] :: Nat)
~#
('Succ (n1_a9qu[sk] :+: s_a9qV[fuv:4]) :: Nat)
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
It is rightly rejected by ghci-7.10.2:
Prove.hs:42:6:
Couldn't match type ‘'Succ n1’ with ‘'Zero’
Inaccessible code in
a pattern with constructor
SZero :: SNat 'Zero,
in an equation for ‘sadd’
In the pattern: SZero
In an equation for ‘sadd’: sadd SZero n = n
Failed, modules loaded: none.
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |