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