[GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

[GHC]

#11066: Inacessible branch should be warning - otherwise breaks type soundness?
-------------------------------------+-------------------------------------
        Reporter:  rrnewton          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #8128, #8740      |  Differential Rev(s):  Phab:D1454
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by tdammers):

 Replying to [comment:43 simonpj]:
 > I fixed #15152, so that may unblock progress here.

 I noticed that, very nice.

 I've rebased my patch onto this fixed version, and it seems that the lint
 errors indeed disappear. I'm also seeing the expected failures (provided I
 change the relevant tests to compile with `-Werror`), however the exact
 error messages differ slightly, e.g. for T3651:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}

 module T3651 where

 data Z a where
   U :: Z ()
   B :: Z Bool

 unsafe1 :: Z a -> Z a -> a
 unsafe1 B U = ()

 unsafe2 :: a ~ b => Z b -> Z a -> a
 unsafe2 B U = ()

 unsafe3 :: a ~ b => Z a -> Z b -> a
 unsafe3 B U = True

 }}}

 {{{#!diff
 commit 89b64708fa2928978c0822b0540977663a4b087d
 Author: Tobias Dammers <tdammers at gmail.com>
 Date:   Wed May 16 08:49:48 2018 +0200

     Make gadt/T3651 pass

 diff --git a/testsuite/tests/gadt/T3651.stderr
 b/testsuite/tests/gadt/T3651.stderr
 index 14216eb149..62e3bf16d7 100644
 --- a/testsuite/tests/gadt/T3651.stderr
 +++ b/testsuite/tests/gadt/T3651.stderr
 @@ -1,21 +1,14 @@

 -T3651.hs:11:11: error:
 -    • Couldn't match type ‘Bool’ with ‘()’
 -      Inaccessible code in
 -        a pattern with constructor: U :: Z (), in an equation for
 ‘unsafe1’
 -    • In the pattern: U
 +T3651.hs:11:15: error:
 +    • Couldn't match type ‘()’ with ‘Bool’
 +      Expected type: a
 +        Actual type: ()
 +    • In the expression: ()
        In an equation for ‘unsafe1’: unsafe1 B U = ()

 -T3651.hs:14:11: error:
 -    • Couldn't match type ‘Bool’ with ‘()’
 -      Inaccessible code in
 -        a pattern with constructor: U :: Z (), in an equation for
 ‘unsafe2’
 -    • In the pattern: U
 +T3651.hs:14:15: error:
 +    • Couldn't match type ‘()’ with ‘Bool’
 +      Expected type: a
 +        Actual type: ()
 +    • In the expression: ()
        In an equation for ‘unsafe2’: unsafe2 B U = ()
 -
 -T3651.hs:17:11: error:
 -    • Couldn't match type ‘Bool’ with ‘()’
 -      Inaccessible code in
 -        a pattern with constructor: U :: Z (), in an equation for
 ‘unsafe3’
 -    • In the pattern: U
 -      In an equation for ‘unsafe3’: unsafe3 B U = True
 }}}

 So this means that `unsafe1` and `unsafe2` keep getting rejected, but for
 a different reason (plain old type mismatch, rather than the "Inaccessible
 code" warning), and `unsafe3` is now accepted. But that doesn't seem
 right.

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