[GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?
#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 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: -------------------------------------+------------------------------------- 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> 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 rrnewton): * Attachment "SimpleInaccessible.hs" added. Example program that will error with "inaccessible code" -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066> 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: | -------------------------------------+------------------------------------- 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 jstolarek): * cc: jstolarek (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:2> 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): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm ok with making it a warning instead of an error. Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:4> 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: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: => 7.10.3 Comment: I'm going to try to get this into 7.10.3 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:6> 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: | Differential Rev(s): Phab:D1454 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 7.10.3 => 8.0.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:8> 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.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, #8740 | Differential Rev(s): Phab:D1454 Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) * related: #8128 => #8128, #8740 Comment: I'd like to see this: it would be particularly useful for code generated by standalone deriving (see related tickets). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:10> 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 heisenbug): * cc: heisenbug (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:13> 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 jstolarek): I've been bitten by this bug just now. With GHC 8.0.1 this simple program will not compile because of inaccessible branches: {{{#!hs {-# LANGUAGE GADTs, StandaloneDeriving #-} module T11066 where data Foo a where A :: Foo Int B :: Foo Bool C :: Foo a -> Foo a deriving instance Eq (Foo a) deriving instance Ord (Foo a) }}} GHC complains with five identical error messages, one for each derived function of `Ord` type class (this error is for `compare`): {{{ T11066.hs:11:1: Couldn't match type ‘Bool’ with ‘Int’ Inaccessible code in a pattern with constructor A :: Foo Int, in a case alternative In the pattern: A {} In a case alternative: A {} -> GT In the expression: case b of { A {} -> GT B -> EQ _ -> LT } When typechecking the code for ‘compare’ in a derived instance for ‘Ord (Foo a)’: To see the code I am typechecking, use -ddump-deriv }}} Here's the derived code of `compare` (after some cleanup): {{{#!hs instance Ord (Foo a) where compare a b = case a of A -> case b of A -> EQ _ -> LT B -> case b of A {} -> GT B -> EQ _ -> LT C c -> case b of C d -> (c `compare` d) _ -> GT }}} It is of course possible to write a well-typed instance of `Ord`: {{{#!hs instance Ord (Foo a) where compare A A = EQ compare A _ = LT compare _ A = GT compare B B = EQ compare B (C _) = LT compare (C _) B = GT compare (C a) (C b) = compare a b }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:15> 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: 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 bgamari): * milestone: 8.2.1 => 8.4.1 Comment: It doesn't look like this will get finished up for 8.2. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:17> 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): I just had a user reach out to me with this error being caused by an open type family that couldn't be reduced in a local setting, but which could be reduced elsewhere in the program where the extra type instance information was available. The irony here is the 'inaccessible' code was matching on a `Refl` to prove the existence of this type instance existed to the local context. Without this being reduced to a merely overly-enthusiastic warning that he can opt out of there is no way to fix the problem at present. A concrete example of code this currently cripples is the use of `Data.Constraint.Nat`. http://hackage.haskell.org/package/constraints-0.9.1/docs/Data-Constraint- Nat.html The user can't use the machinery provided therein to prove in a local context that, say `Gcd 3 6` is `3`. {{{#!hs {-# LANGUAGE GADTs, TypeApplications, DataKinds #-} import Data.Constraint import Data.Constraint.Nat import Data.Proxy import Data.Type.Equality import GHC.TypeLits foo = case sameNat (Proxy @3) (Proxy @(Gcd 3 6)) \\ gcdNat @3 @6 of Just Refl -> () }}} The `Refl` match there is being rejected as "Inaccessible code" despite the fact that if it was allowed to compile, it'd darn well get accessed! (This happens even if we weaken the closed type families in that module to open type families.) There isn't anything special about `Gcd` here. The same issue arises trying to write "userspace" proof terms about the (+) provided by GHC.TypeLits as if it were an uninterpreted function. This may be a case of this being a closely related error where GHC is being too eager to claim code inaccessible when it can't reduce a type family further in a local context, but its made into a crippling problem rather than a useless warning when combined with this issue. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:19> 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 simonpj): It certainly sounds wrong for GHC to reject a branch as inaccessible (i.e. definitely cannot be executed) when it actually ''can'' be executed. Can you make an example that doesn't depend on relatively sophisticated package? I tried {{{ {-# LANGUAGE FlexibleContexts, TypeFamilies, TypeApplications #-} module T11066 where import Data.Typeable type family F a foo:: Typeable (F Bool) => () foo = case eqT @Int @(F Bool) of Just Refl -> () _ -> () }}} thinking that GHC might claim that `F Bool ~ Int` is inaccesible; but it's accepted just fine. You do not say which version of the compiler you are using. A milder version of the problem is if the branch really is inaccessible, but you want to accept it anyway for some reason -- e.g. it's produced by `deriving`. But that is not what you are bothered about here. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:21> 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: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:23> 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 dfeuer): Actually, I take that last bit back. Does Ed need the original version of `Gcd`, or will the more legitimate version work in this context? I don't see how he can really take advantage of the former, but I could be missing something; it's late. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:25> 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): I'm not saying that it's wrong for GHC to complain. Ed seems to be saying that he doesn't want GHC to consider this an error, because that breaks his `unsafeCoerce`ful code. It's up to you whether you find his argument compelling. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:27> 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 simonpj): But `foo (unsafeCoerce Refl)` asks GHC to come up with a proof of `1 :~: Gcd 3 4` and pass it as an implicit argument. Which it cannot do. (Remember this isn't the usual `Gcd`; it's a hypothetical nullary function.) So in fact I can't call `foo`. Rather than speculate about Ed let's see if he wants to say anything himself. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:29> 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 ekmett): 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, then I think I see where you're coming from. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:31> 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.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 adamgundry): Replying to [comment:30 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.
Doesn't an empty closed type family serve the same purpose? The first encoding seems simply wrong, because it implies that `Gcd` is injective. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:33> 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 tdammers): I've been looking at this for a little while, and AFAICT, we have two actionable points at hand here: 1. "Inaccessible code" is currently an error, but it would be more reasonable to make it a warning. 2. Programs exist that the type checker currently rejects, even though we would like them to be accepted. It seems that there is no consensus on the exact conditions for this though. I believe that #1 is easy to solve, and would produce immediate benefit, while #2 needs better understanding of the actual problem. So I would suggest we tackle #1 now, and continue the discussion on #2. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:35> 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): Turning the error into a warning causes a few regressions, e.g. T3651: {{{ {-# 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 }}} This program previously failed with this exact error, and of course changing it into a warning makes it compile. Other regressions are: - {{{concurrent/prog001/concprog001.run concprog001 [bad exit code] (threaded2)}}} - {{{gadt/T3651.run T3651 [stderr mismatch] (normal)}}} - {{{gadt/T7293.run T7293 [exit code 0] (normal)}}} - {{{gadt/T7294.run T7294 [stderr mismatch] (normal)}}} - {{{gadt/T7558.run T7558 [stderr mismatch] (normal)}}} - {{{ghci/scripts/Defer02.run Defer02 [bad stderr] (ghci)}}} - {{{typecheck/should_fail/tcfail167.run tcfail167 [exit code 0] (normal)}}} - {{{typecheck/should_fail/FrozenErrorTests.run FrozenErrorTests [stderr mismatch] (normal)}}} - {{{typecheck/should_run/Typeable1.run Typeable1 [exit code 0] (normal)}}} I will look into these, but I suspect that most of them are exactly what we'd expect. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:37> 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): The following patch turns the "Inaccessible" error into a warning: {{{ commit f4f9c0fc9564f17339718378e9fea3bd186fff96 Author: Tobias Dammers <tdammers@gmail.com> Date: Tue May 8 13:54:28 2018 +0200 [WIP] turn "inaccessible code" error into a warning (#11066) diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index dde7c3c75a..2d3af68008 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -708,7 +708,7 @@ mkGivenErrorReporter implic ctxt cts Nothing ty1 ty2 ; traceTc "mkGivenErrorReporter" (ppr ct) - ; maybeReportError ctxt err } + ; reportWarning NoReason err } where (ct : _ ) = cts -- Never empty (ty1, ty2) = getEqPredTys (ctPred ct) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:39> 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 adamgundry): @tdammers I don't think this is as straightforward as simply switching the error into a warning. Have you looked at Phab:D1454 and the associated discussion? Indeed GHC doesn't currently produce correct Core under inaccessible branches, and doing so would probably require extending Core. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:41> 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 simonpj): I fixed #15152, so that may unblock progress here. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:43> 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: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
#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):
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. It's not worth losing sleep over this. BTW, if it's now a warning do we have a flag to control whether the warning is enabled? We should. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:45> 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 -------------------------------------+------------------------------------- Changes (by tdammers): * status: new => patch * differential: Phab:D1454 => Phab:D1454, Phab:D4744 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:47> 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 <ben@…>): 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 -------------------------------------+------------------------------------- Changes (by bgamari): * status: patch => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066#comment:49> 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 <ryan.gl.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
participants (1)
-
GHC