#11066 closed bug (fixed)
Inacessible branch should be warning  otherwise breaks type soundness?
Reported by:  rrnewton  Owned by:  

Priority:  high  Milestone:  8.6.1 
Component:  Compiler  Version:  7.10.2 
Keywords:  Cc:  ekmett, jstolarek, osa1, adamgundry, heisenbug, RyanGlScott, dfeuer  
Operating System:  Unknown/Multiple  Architecture:  Unknown/Multiple 
Type of failure:  Incorrect warning at compiletime  Test Case:  
Blocked By:  Blocking:  
Related Tickets:  #8128, #8740  Differential Rev(s):  Phab:D1454, Phab:D4744 
Wiki Page: 
Description (last modified by )
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 humanwritten 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 righthand side of a nonredundant clause is inaccessible,..."
Attachments (1)
Change History (51)
Changed 4 years ago by
Attachment:  SimpleInaccessible.hs added 

comment:1 Changed 4 years ago by
Description:  modified (diff) 

comment:2 Changed 4 years ago by
Cc:  jstolarek added 

comment:3 Changed 4 years ago by
Cc:  osa1 added 

comment:5 Changed 4 years ago by
Differential Rev(s):  → Phab:D1454 

comment:7 Changed 4 years ago by
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
comment:8 Changed 4 years ago by
Milestone:  7.10.3 → 8.0.1 

comment:9 Changed 4 years ago by
Related Tickets:  → #8128 

comment:10 Changed 4 years ago by
Cc:  adamgundry added 

Related Tickets:  #8128 → #8128, #8740 
I'd like to see this: it would be particularly useful for code generated by standalone deriving (see related tickets).
comment:11 Changed 4 years ago by
Type of failure:  GHC rejects valid program → Incorrect warning at compiletime 

comment:12 Changed 4 years ago by
Milestone:  8.0.1 → 8.2.1 

Unfortunately it doesn't look like this will happen for 8.0.1.
comment:13 Changed 3 years ago by
Cc:  heisenbug added 

comment:14 Changed 3 years ago by
Cc:  RyanGlScott added 

comment:15 Changed 3 years ago by
I've been bitten by this bug just now. With GHC 8.0.1 this simple program will not compile because of inaccessible branches:
{# 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 ddumpderiv
Here's the derived code of compare
(after some cleanup):
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 welltyped instance of Ord
:
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
comment:16 Changed 3 years ago by
 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 betastep it is rejected. (I'm not sure I'd call it typeunsound, 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.
comment:17 Changed 3 years ago by
Milestone:  8.2.1 → 8.4.1 

It doesn't look like this will get finished up for 8.2.
comment:18 Changed 3 years ago by
Cc:  ekmett added 

comment:19 followup: 22 Changed 3 years ago by
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 overlyenthusiastic 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/constraints0.9.1/docs/DataConstraintNat.html
The user can't use the machinery provided therein to prove in a local context that, say Gcd 3 6
is 3
.
{# 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.
comment:20 Changed 3 years ago by
Note,
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 (:~:).
comment:21 Changed 3 years ago by
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.
comment:22 Changed 2 years ago by
I wonder if ekmett's problem lies in the somewhat bogus type family definition:
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.
comment:23 Changed 2 years ago by
Cc:  dfeuer added 

comment:24 Changed 2 years ago by
Here's a much smaller reproduction of what I suspect is going on in Edward's code:
{# 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
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
.
comment:25 Changed 2 years ago by
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.
comment:26 Changed 2 years ago by
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.
comment:27 Changed 2 years ago by
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.
comment:28 Changed 2 years ago by
To put it a bit differently, I believe that whereas you write "foo
cannot be called", Ed is effectively calling foo (unsafeCoerce Refl)
.
comment:29 Changed 2 years ago by
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.
comment:30 followup: 33 Changed 2 years ago by
I'm not particularly wedded to whether I use
type family Gcd :: Nat > Nat > Nat
or
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:
module Foo where type family Gcd (x :: Nat) (y :: Nat) :: Nat
but refine it later in another:
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.
comment:31 Changed 2 years ago by
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.
comment:32 Changed 2 years ago by
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
.
comment:33 Changed 2 years ago by
Replying to ekmett:
I'm not particularly wedded to whether I use
type family Gcd :: Nat > Nat > Nator
type family Gcd (n:: Nat) (m::Nat) :: Nathere.
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.
comment:35 Changed 18 months ago by
I've been looking at this for a little while, and AFAICT, we have two actionable points at hand here:
 "Inaccessible code" is currently an error, but it would be more reasonable to make it a warning.
 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.
comment:36 Changed 18 months ago by
comment:37 Changed 17 months ago by
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.
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.
comment:38 Changed 17 months ago by
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 dcorelint
) does produce the desired behavior.
comment:39 Changed 17 months ago by
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)
comment:40 Changed 17 months ago by
Core lint error may actually be an orthogonal issue; moved that part to #15152.
comment:41 Changed 17 months ago by
@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.
comment:42 Changed 17 months ago by
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?
comment:43 followup: 44 Changed 17 months ago by
I fixed #15152, so that may unblock progress here.
comment:44 Changed 17 months ago by
Replying to 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:
{# 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

testsuite/tests/gadt/T3651.stderr
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 b 1 1 2 T3651.hs:11:1 1: error:3 • Couldn't match type ‘ Bool’ with ‘()’4 Inaccessible code in5 a pattern with constructor: U :: Z (), in an equation for ‘unsafe1’6 • In the pattern: U2 T3651.hs:11:15: error: 3 • Couldn't match type ‘()’ with ‘Bool’ 4 Expected type: a 5 Actual type: () 6 • In the expression: () 7 7 In an equation for ‘unsafe1’: unsafe1 B U = () 8 8 9 T3651.hs:14:1 1: error:10 • Couldn't match type ‘ Bool’ with ‘()’11 Inaccessible code in12 a pattern with constructor: U :: Z (), in an equation for ‘unsafe2’13 • In the pattern: U9 T3651.hs:14:15: error: 10 • Couldn't match type ‘()’ with ‘Bool’ 11 Expected type: a 12 Actual type: () 13 • In the expression: () 14 14 In an equation for ‘unsafe2’: unsafe2 B U = () 15 16 T3651.hs:17:11: error:17 • Couldn't match type ‘Bool’ with ‘()’18 Inaccessible code in19 a pattern with constructor: U :: Z (), in an equation for ‘unsafe3’20 • In the pattern: U21 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.
comment:45 followup: 46 Changed 17 months ago by
But that doesn't seem right.
It seems fine to me, arguably. The equality a~b
is not needed; running unsafe3
will never segfault.
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.
comment:46 Changed 17 months ago by
Replying to simonpj:
But that doesn't seem right.
It seems fine to me, arguably. The equality
a~b
is not needed; runningunsafe3
will never segfault.
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.
comment:47 Changed 17 months ago by
Differential Rev(s):  Phab:D1454 → Phab:D1454, Phab:D4744 

Status:  new → patch 
comment:49 Changed 17 months ago by
Resolution:  → fixed 

Status:  patch → closed 
Example program that will error with "inaccessible code"