[GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
47 messages Options
123
Reply | Threaded
Open this post in threaded view
|

[GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
123