[GHC] #12444: Regression: panic! on inaccessible code with constraint

[GHC]

#12444: Regression: panic! on inaccessible code with constraint
-------------------------------------+-------------------------------------
           Reporter:  zilinc         |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Running the following program with ghci-8.0.1:
 {{{#!hs

 {-# 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.

 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12444>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler