#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by rrnewton: Old description:

GHC 7.10.2 reports inaccessible branches as a type error, and I think this is really a bug.

First, the implicit thinking seems to be "why would a user want to write inaccessible cases, they'd be crazy!". But that only applies to human-written code. Program generators can have a great deal of trouble avoiding this error, unless they replicate the GHC type checker to predict the problem and prune branches. (That's why we are hitting this error and are stuck.)

Second, it seems like this is a problem for type soundness. See the attached program where "step1" typechecks but "step2" does not. And yet, the operational semantics should allow step1 to reduce to step2.

Indeed, in the "GADTs meet their match" paper it seems like the intent was to warn for these inaccessible cases, not error. For example, the paper contains the language:

"If we warn that a right-hand side of a non-redundant clause is inaccessible,"

New description: GHC 7.10.2 reports inaccessible branches as a type error, and I think this is really a bug. First, the implicit thinking seems to be "why would a user want to write inaccessible cases, they'd be crazy!". But that only applies to human-written code. Program generators can have a great deal of trouble avoiding this error, unless they replicate the GHC type checker to predict the problem and prune branches. (That's why we are hitting this error and are stuck.) Second, it seems like this is a problem for type soundness. See the attached program where "step1" typechecks but "step2" does not. And yet, the operational semantics should allow step1 to reduce to step2. Indeed, in the "GADTs meet their match" paper it seems like the intent was to warn for these inaccessible cases, not error. For example, the paper contains the language: "If we warn that a right-hand side of a non-redundant clause is inaccessible,..." -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by osa1): * cc: osa1 (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1454 Wiki Page: | -------------------------------------+------------------------------------- Changes (by osa1): * differential: => Phab:D1454 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: high | Milestone: 7.10.3 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1454 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): There was muttering on the Phab trail about details. Not sure it's converged enough to commit. I trust Richard's judgement on this. Sadly I have ~zero time this week or next. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #8128 | Differential Rev(s): Phab:D1454 Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * related: => #8128 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: high | Milestone: 8.2.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: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.0.1 => 8.2.1 Comment: Unfortunately it doesn't look like this will happen for 8.0.1. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: high | Milestone: 8.2.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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: high | Milestone: 8.2.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 simonpj): * Concerning the original ticket: I'd be perfectly happy if it became a warning. I agree that it's a bit odd if a program is accepted, but then after one beta-step it is rejected. (I'm not sure I'd call it type- unsound, which to me means that it's not rejected at all, but crashes at runtime.) * Concerning comment:15, good point. I think it might be quite tricky to make the 'deriving' mechanism predict which branches would be inaccessible; but perhaps possible. A significant advantage of making the error into a warning is that we could then ignore the warning in deriving code (we already ignore others). Happy to advise if someone would like to take this up. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.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: | -------------------------------------+------------------------------------- Changes (by ekmett): * cc: ekmett (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.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 ekmett): Note, {{{#!hs foo :: forall n m. (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Maybe (Dict (Divides n m)) foo = case sameNat (Proxy @n) (Proxy @(Gcd n m)) \\ gcdNat @n @m of Just Refl -> ... }}} works just fine. I'm guessing GHC is more willing to claim the case is inaccessible because there aren't any type variables in it, despite the fact that `Gcd` is a type family and the local context might not know all of the instances elsewhere in the program that could be used to construct such a (:~:). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.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 dfeuer): I wonder if ekmett's problem lies in the somewhat bogus type family definition: {{{#!hs type family Gcd :: Nat -> Nat -> Nat }}} An instance of the family would have to be a ''constructor'' of kind `Nat -> Nat -> Nat`. There is no such thing, so GHC may reject the notion under some circumstances. This is just speculation, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.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 dfeuer): Here's a much smaller reproduction of what I suspect is going on in Edward's code: {{{#!hs {-# language DataKinds #-} {-# language TypeFamilies #-} {-# language TypeOperators #-} module T11066 where import Data.Type.Equality import GHC.TypeLits (Nat) type family Gcd :: Nat -> Nat -> Nat foo :: 1 :~: Gcd 3 4 -> () foo Refl = () }}} This produces {{{ T11066.hs:11:5: error: • Couldn't match type ‘Gcd 3 4’ with ‘1’ Inaccessible code in a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in an equation for ‘foo’ • In the pattern: Refl In an equation for ‘foo’: foo Refl = () | 11 | foo Refl = () | }}} even though someone could easily `unsafeCoerce` their way into `1 :~: Gcd 3 4`. My hypothesis about the type family is supported by the fact that changing `Gcd` to {{{#!hs type family Gcd (a :: Nat) (b :: Nat) :: Nat }}} makes the problem go away. But I suspect ekmett needs the original version to be able to perform symbolic calculations on `Gcd`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.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 simonpj):

Here's a much smaller reproduction of what I suspect is going on in Edward's code

I don't see the problem here. As stated, `Gcd` is a nullary type function, so it's definitely the case that `1 :~: Gcd 3 4` is unsatisfiable, so `foo` cannot be called. Why is it wrong for GHC to complain. I'm really lost in this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.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 dfeuer): To put it a bit differently, I believe that whereas you write "`foo` cannot be called", Ed is effectively calling `foo (unsafeCoerce Refl)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.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 ekmett): I'm not particularly wedded to whether I use {{{#!hs type family Gcd :: Nat -> Nat -> Nat }}} or {{{#!hs type family Gcd (n:: Nat) (m::Nat) :: Nat }}} here. The one thing I have in favor (or against, depending on your perspective) of the Nat -> Nat -> Nat encoding is that it allows me to preclude the user actually defining any ad hoc base cases. Switching to the other address the "eta" concern to some extent. The main usecase I have sort of mirrors this situation: In the module we're in Gcd 3 4 doesn't have a type instance, but that doesn't mean that in another context it might not be reducible. Say you define the type family in one module: {{{#!hs module Foo where type family Gcd (x :: Nat) (y :: Nat) :: Nat }}} but refine it later in another: {{{#!hs module Bar where type instance Gcd 3 4 = 1 }}} In Bar, we can perform the reduction, but in Foo we'd get stuck. The machinery in Data.Constraint.Nat acts much the same way. We later on get into a situation that lets us discharge a stuck constraint. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:30 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.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 simonpj):

If what you're saying is that the fact that its type family Gcd :: Nat -> Nat -> Nat, rather than that other form, that is causing the problem

Precisely. If `Gcd` is nullary, then `Gcd a b` can never be equal to `1`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.4.1 => 8.6.1 Comment: This won't be resolved for 8.4. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:34 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj):

So I would suggest we tackle #1 now, and continue the discussion on #2#

Makes sense to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:36 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): It turns out that `T3651` doesn't fail the right way if we turn this error into a warning and then compile with `-Werror`, because the core linter errors out first, so instead of the errorized warning, we see the core linter failure. Manually compiling with just `-Werror` (but not `-dcore- lint`) does produce the desired behavior. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:38 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Core lint error may actually be an orthogonal issue; moved that part to #15152. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:40 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): Hmm. I don't think I agree, Adam. GHC currently simply doesn't use insoluble inert constraints, so it won't make use of `Int ~ Bool`. Would you like to offer an example where we don't produce correct Core under inaccessible branches? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:42 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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:45 simonpj]:

...

But that doesn't seem right.

It seems fine to me, arguably. The equality `a~b` is not needed; running `unsafe3` will never seg-fault.

Right, of course... it's nonsensical code, but it won't blow up. I just found it peculiar that the "Inaccessible code" warning doesn't fire at all anymore.

BTW, if it's now a warning do we have a flag to control whether the warning is enabled? We should.

Not yet, but I was going to add one. Just didn't want to put in that effort while it was still unclear whether we go through with this. I would suggest that we turn it on by default though; it's generally a useful warning to have, and disabling it is probably something you'd only want to do when you know what you're doing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:46 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: (none) Type: bug | Status: patch 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: | Phab:D4744 -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"08073e16cf672d8009309e4e55d4566af1ecaff4/ghc" 08073e16/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="08073e16cf672d8009309e4e55d4566af1ecaff4" Turn "inaccessible code" error into a warning With GADTs, it is possible to write programs such that the type constraints make some code branches inaccessible. Take, for example, the following program :: {-# LANGUAGE GADTs #-} data Foo a where Foo1 :: Foo Char Foo2 :: Foo Int data TyEquality a b where Refl :: TyEquality a a checkTEQ :: Foo t -> Foo u -> Maybe (TyEquality t u) checkTEQ x y = error "unimportant" step2 :: Bool step2 = case checkTEQ Foo1 Foo2 of Just Refl -> True -- Inaccessible code Nothing -> False Clearly, the `Just Refl` case cannot ever be reached, because the `Foo1` and `Foo2` constructors say `t ~ Char` and `u ~ Int`, while the `Refl` constructor essentially mandates `t ~ u`, and thus `Char ~ Int`. Previously, GHC would reject such programs entirely; however, in practice this is too harsh. Accepting such code does little harm, since attempting to use the "impossible" code will still produce errors down the chain, while rejecting it means we cannot legally write or generate such code at all. Hence, we turn the error into a warning, and provide `-Winaccessible-code` to control GHC's behavior upon encountering this situation. Test Plan: ./validate Reviewers: bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie, carter GHC Trac Issues: #11066 Differential Revision: https://phabricator.haskell.org/D4744 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:48 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: (none) Type: bug | Status: closed Priority: high | Milestone: 8.6.1 Component: Compiler | Version: 7.10.2 Resolution: fixed | 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: | Phab:D4744 -------------------------------------+------------------------------------- Comment (by Ryan Scott ): In [changeset:"90e99c4cfd601601e56fc6041186ca3e070408d9/ghc" 90e99c4c/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="90e99c4cfd601601e56fc6041186ca3e070408d9" Add tests for #8128 and #8740 Commit 08073e16cf672d8009309e4e55d4566af1ecaff4 (#11066) ended up fixing these, fortunately enough. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11066#comment:50 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler