Opened 4 years ago

Closed 19 months ago

Last modified 19 months ago

#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 compile-time Test Case:
Blocked By: Blocking:
Related Tickets: #8128, #8740 Differential Rev(s): Phab:D1454, Phab:D4744
Wiki Page:

Description (last modified by rrnewton)

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,..."

Attachments (1)

SimpleInaccessible.hs (487 bytes) - added by rrnewton 4 years ago.
Example program that will error with "inaccessible code"

Download all attachments as: .zip

Change History (51)

Changed 4 years ago by rrnewton

Attachment: SimpleInaccessible.hs added

Example program that will error with "inaccessible code"

comment:1 Changed 4 years ago by rrnewton

Description: modified (diff)

comment:2 Changed 4 years ago by jstolarek

Cc: jstolarek added

comment:3 Changed 4 years ago by osa1

Cc: osa1 added

comment:4 Changed 4 years ago by simonpj

I'm ok with making it a warning instead of an error.

Simon

comment:5 Changed 4 years ago by osa1

Differential Rev(s): Phab:D1454

comment:6 Changed 4 years ago by bgamari

Milestone: 7.10.3

I'm going to try to get this into 7.10.3

comment:7 Changed 4 years ago 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

comment:8 Changed 4 years ago by bgamari

Milestone: 7.10.38.0.1

comment:9 Changed 4 years ago by jstolarek

comment:10 Changed 4 years ago by adamgundry

Cc: adamgundry added

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 thomie

Type of failure: GHC rejects valid programIncorrect warning at compile-time

comment:12 Changed 4 years ago by bgamari

Milestone: 8.0.18.2.1

Unfortunately it doesn't look like this will happen for 8.0.1.

comment:13 Changed 3 years ago by heisenbug

Cc: heisenbug added

comment:14 Changed 3 years ago by RyanGlScott

Cc: RyanGlScott added

comment:15 Changed 3 years ago 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:

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

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:

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 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.

comment:17 Changed 3 years ago by bgamari

Milestone: 8.2.18.4.1

It doesn't look like this will get finished up for 8.2.

comment:18 Changed 3 years ago by ekmett

Cc: ekmett added

comment:19 Changed 3 years ago 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.

{-# 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 ekmett

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 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.

comment:22 in reply to:  19 Changed 2 years ago by dfeuer

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 dfeuer

Cc: dfeuer added

comment:24 Changed 2 years ago by dfeuer

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 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.

comment:26 Changed 2 years ago 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.

comment:27 Changed 2 years ago 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 unsafeCoerceful code. It's up to you whether you find his argument compelling.

comment:28 Changed 2 years ago 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).

comment:29 Changed 2 years ago 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.

comment:30 Changed 2 years ago by ekmett

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 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.

comment:32 Changed 2 years ago 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.

comment:33 in reply to:  30 Changed 2 years ago by adamgundry

Replying to ekmett:

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.

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:34 Changed 23 months ago by bgamari

Milestone: 8.4.18.6.1

This won't be resolved for 8.4.

comment:35 Changed 20 months ago 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.

comment:36 Changed 20 months ago by simonpj

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

Makes sense to me.

comment:37 Changed 19 months ago 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.

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.

Last edited 19 months ago by tdammers (previous) (diff)

comment:38 Changed 19 months ago 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.

comment:39 Changed 19 months ago 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)

comment:40 Changed 19 months ago by tdammers

Core lint error may actually be an orthogonal issue; moved that part to #15152.

comment:41 Changed 19 months ago 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.

comment:42 Changed 19 months ago 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?

comment:43 Changed 19 months ago by simonpj

I fixed #15152, so that may unblock progress here.

comment:44 in reply to:  43 Changed 19 months ago by tdammers

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  
    11
    2 T3651.hs:11:11: error:
    3     • Couldn't match type ‘Bool’ with ‘()
    4       Inaccessible code in
    5         a pattern with constructor: U :: Z (), in an equation for ‘unsafe1’
    6     • In the pattern: U
     2T3651.hs:11:15: error:
     3    • Couldn't match type ‘()’ with ‘Bool
     4      Expected type: a
     5        Actual type: ()
     6    • In the expression: ()
    77      In an equation for ‘unsafe1’: unsafe1 B U = ()
    88
    9 T3651.hs:14:11: error:
    10     • Couldn't match type ‘Bool’ with ‘()
    11       Inaccessible code in
    12         a pattern with constructor: U :: Z (), in an equation for ‘unsafe2’
    13     • In the pattern: U
     9T3651.hs:14:15: error:
     10    • Couldn't match type ‘()’ with ‘Bool
     11      Expected type: a
     12        Actual type: ()
     13    • In the expression: ()
    1414      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 in
    19         a pattern with constructor: U :: Z (), in an equation for ‘unsafe3’
    20     • In the pattern: U
    21       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 Changed 19 months ago 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.

comment:46 in reply to:  45 Changed 19 months ago by tdammers

Replying to 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.

comment:47 Changed 19 months ago by tdammers

Differential Rev(s): Phab:D1454Phab:D1454, Phab:D4744
Status: newpatch

comment:48 Changed 19 months ago by Ben Gamari <ben@…>

In 08073e16/ghc:

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

comment:49 Changed 19 months ago by bgamari

Resolution: fixed
Status: patchclosed

comment:50 Changed 19 months ago by Ryan Scott <ryan.gl.scott@…>

In 90e99c4c/ghc:

Add tests for #8128 and #8740

Commit 08073e16cf672d8009309e4e55d4566af1ecaff4 (#11066) ended up
fixing these, fortunately enough.
Note: See TracTickets for help on using tickets.