#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@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