[GHC] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

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

[GHC] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Inspired by adamse's comment at
 https://ghc.haskell.org/trac/ghc/ticket/14317#comment:3, I've discovered
 some programs which behave differently on GHC 8.0.2, 8.2.1, and HEAD.

 -----

 First, there's this program:

 {{{#!hs
 {-# LANGUAGE GADTs #-}

 hm1 :: b ~ f b => b -> f b
 hm1 x = x
 }}}

 On GHC 8.0.2, this compiles (with a warning):

 {{{
 GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 Bug.hs:4:1: warning: [-Woverlapping-patterns]
     Pattern match is redundant
     In an equation for ‘hm1’: hm1 x = ...
 }}}

 But on GHC 8.2.1, it errors:

 {{{
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 Bug.hs:4:9: error:
     • Could not deduce: b ~ f b
       from the context: b ~ f b
         bound by the type signature for:
                    hm1 :: forall b (f :: * -> *). b ~ f b => b -> f b
         at Bug.hs:3:1-26
       ‘b’ is a rigid type variable bound by
         the type signature for:
           hm1 :: forall b (f :: * -> *). b ~ f b => b -> f b
         at Bug.hs:3:1-26
     • In the expression: x
       In an equation for ‘hm1’: hm1 x = x
     • Relevant bindings include
         x :: b (bound at Bug.hs:4:5)
         hm1 :: b -> f b (bound at Bug.hs:4:1)
   |
 4 | hm1 x = x
   |         ^
 }}}

 And on GHC HEAD, it fails with a different error!

 {{{
 GHCi, version 8.3.20171004: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 Bug.hs:4:9: error:
     • Occurs check: cannot construct the infinite type: b ~ f b
     • In the expression: x
       In an equation for ‘hm1’: hm1 x = x
     • Relevant bindings include
         x :: b (bound at Bug.hs:4:5)
         hm1 :: b -> f b (bound at Bug.hs:4:1)
   |
 4 | hm1 x = x
   |         ^
 }}}

 The same errors occur if you give `hm1` the type `hm1 :: b ~ f b => f b ->
 b`.

 -----

 What happens if you try `Coercible` instead of `(~)`? Consider this
 variant of the program above:

 {{{#!hs
 {-# LANGUAGE GADTs #-}

 import Data.Coerce

 hm2 :: Coercible b (f b) => b -> f b
 hm2 = coerce
 }}}

 On GHC 8.0.2, 8.2.1, and HEAD, this compiles (without warnings). Good. But
 if you change the type to use the symmetric version of that constraint:

 {{{#!hs
 {-# LANGUAGE GADTs #-}

 import Data.Coerce

 hm3 :: Coercible (f b) b => b -> f b
 hm3 = coerce
 }}}

 Then on GHC 8.0.2, it compiles without warnings, but on 8.2.1 and HEAD it
 fails!

 Here is the error with 8.2.1:

 {{{
 Bug3.hs:6:7: error:
     • Could not deduce: Coercible b (f b)
         arising from a use of ‘coerce’
       from the context: Coercible (f b) b
         bound by the type signature for:
                    hm3 :: forall (f :: * -> *) b. Coercible (f b) b => b
 -> f b
         at Bug3.hs:5:1-36
       ‘b’ is a rigid type variable bound by
         the type signature for:
           hm3 :: forall (f :: * -> *) b. Coercible (f b) b => b -> f b
         at Bug3.hs:5:1-36
     • In the expression: coerce
       In an equation for ‘hm3’: hm3 = coerce
     • Relevant bindings include hm3 :: b -> f b (bound at Bug3.hs:6:1)
   |
 6 | hm3 = coerce
   |       ^^^^^^
 }}}

 And on HEAD:

 {{{
 Bug3.hs:6:7: error:
     • Occurs check: cannot construct the infinite type: b ~ f b
         arising from a use of ‘coerce’
     • In the expression: coerce
       In an equation for ‘hm3’: hm3 = coerce
     • Relevant bindings include hm3 :: b -> f b (bound at Bug3.hs:6:1)
   |
 6 | hm3 = coerce
   |       ^^^^^^
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323>
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] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Here's what is happening

 * The given `b ~ f b` has an occurs check, so it's insoluble. It's a bit
 like saying
 {{{
 f :: (Int ~ Bool) => blah
 }}}

 * In the long discussion on #12466 (see `Note [Given errors]` in
 `TcErrors` we decided not to complain about insoluble givens.

 * So the given `b ~ f b` is just parked.

 * Now we try to solve `b ~ f b`.  Lo, it has an occurs-check error.  Which
 we report.

 Seems reasonable to me, except for the lack of a complaint about the
 insoluble given; better ideas welcome (but look at #12466).

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323#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] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 And what of the second and third programs (with `Coercible` instead of
 `(~)`)? Those constraints aren't insoluble.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323#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] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Well, this is annoying.  The definition of `Coercible` is roughly this
 {{{
 class (a ~R# b) => Coercible a b
 }}}
 So then

 * When we have `[G] Coercible b (f b)` we put that into the inert set, and
 add its superclasses `[G] b ~R# f b`.

 * The given `[G] b ~R# f b`  has an occurs check, so we "park" it in the
 insolubles.

 * Now we try `[W] Coercible b (f b)`.  Aha!  We have precisely that inert
 in the inert set, so we solve it.

 If we switch te type sig to `Coercible (f b) b` then something slightly
 different happens:

 * `[G] Coercible (f b) b` is put into the inert set; then add its
 superclasses `[G] f b ~R# b`.

 * The given `[G] f b ~R# b` normalised to `b ~R# f b` but has an occurs
 check, so we "park" it in the insolubles.

 * Now we try `[W] Coercible b (f b)`.  Alas!  No matching dictionary
 exists, so is reported as "can't solve".

 The inconsistency here is that when the givens are insoluble we may not
 (indeed cannot) fully normalise them and use them to solve the wanteds.
 But it's hard to spot that the `Coercible` dictionary (just another class
 to the solver) is insoluble because its superclass is.

 I'm not sure what to do here.  Since it's all to do with a wrong program
 anyhow, maybe it does not matter too much.

 Incidentally the same thing can happen with nominal equality:
 {{{
 class (a~b) => C a b

 foo :: C a b => a -> b
 foo x = x

 hm2 :: C b (f b) => b -> f b
 hm2 x = foo x

 hm3 :: C (f b) b => b -> f b
 hm3 x = foo x
 }}}
 Here `hm2` typechecks because of the exactly-matching given `C b (f b)`
 dictionary, but `hm3` does not.

 (Actually `hm3` fails to typecheck but regrettably does not emit an error
 message. That's a separate bug which I'm fixing.)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323#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] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I'm quite confused. Why should an occurs check ever fire in the first
 place for `b ~R# f b`? This is a perfectly legitimate constraint that can
 be witnessed, for instance, by letting `f` be `Identity` (since `b` is
 representationally equal to `Identity b`). Thus, I'd argue that `hm2` and
 `hm3` are //not// wrong programs.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323#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] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 > Thus, I'd argue that hm2 and hm3 are not wrong programs.

 Hmm.  That's a good point.  But we solve constraints, both `~#` and `~R#`
 by normalising and then rewriteing.  So if we have
 {{{
 [G] b ~R# f b
 [W] b ~R# blah
 }}}
 then we can use the given to rewrite the wanted to
 {{{
 [W] b ~R# blah
 ==> [W] f b ~R# blah
 ==> [W] f (f b) ~R# blah
 ..etc...
 }}}
 We don't want to do that.  So we park the given and don't use it for
 rewriting.

 So maybe the point is not that the code is inaccessible, but rather that
 we don't have a complete solver.  Hmm.

 I wonder what Richard and Stephanie think?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323#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] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Some reactions to all this:

 * comment:3 talks about parking `Coercible` constraints in the insolubles.
 I hope we don't -- they're not insoluble. I imagine you mean that they're
 parked in the "irreducibles", which is more sensible.

 * The representational equality solver is known to be incomplete. I
 believe the problem is simply undecidable. Perhaps this could be better
 documented, but its incompleteness is precisely in recursive situations.

 * I agree that the reason for occurs-checks isn't about solubility, but
 rather about keeping the solver from going into gratuitous loops.

 Bottom line: I don't have any better ideas. I doubt we can make the
 `Coercible` solver more complete without gross hacks. And, absent a Real
 Use Case, I'm not keen on trying.

 I have not digested all of #12466 about nominal equalities, which I tend
 to think are more worrisome.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323#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] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Given that the incompleteness of the representational equality solver has
 spawned at least a couple of Track tickets (this one and #14247, off the
 top of my head), it would be nice to document all of this somewhere.
 (Perhaps `Data.Coerce`?)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323#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] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 > comment:3 talks about parking Coercible constraints in the insolubles

 Actually the `Coercible b (f b)` constraint is parked in the inert dicts.
 But the `b ~R# f b` constraint is parked in insolubles.  It probably
 shouldn't be.

 But in fact I want to kill off the insolubles altogether, and combine then
 with tie irreducibles.  I don't think the distinction pays its way.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323#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] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 comment:8 done in
 {{{
 commit f20cf982f126aea968ed6a482551550ffb6650cf
 Author: Simon Peyton Jones <[hidden email]>
 Date:   Mon Oct 9 13:16:59 2017 +0100

     Remove wc_insol from WantedConstraints

     This patch is a pure refactoring, which I've wanted to do for
     some time.  The main payload is

     * Remove the wc_insol field from WantedConstraints;
       instead put all the insolubles in wc_simple

     * Remove inert_insols from InertCans
       Instead put all the insolubles in inert_irreds

     * Add a cc_insol flag to CIrredCan, to record that
       the constraint is definitely insoluble

     Reasons

     * Quite a bit of code gets slightly simpler
     * Fewer concepts to keep separate
     * Insolubles don't happen at all in production code that is
       just being recompiled, so previously there was a lot of
       moving-about of empty sets

     A couple of error messages acutally improved.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323#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] #14323: Occurs check regressions in GHC 8.2.1 (and HEAD)

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14323: Occurs check regressions in GHC 8.2.1 (and HEAD)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14333            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * status:  new => closed
 * resolution:   => fixed
 * related:   => #14333
 * milestone:   => 8.4.1


Comment:

 Thanks to commit 5a66d574890ed09859ca912c9e0969dba72f4a23 (`Better solving
 for representational equalities`), both `hm2` and `hm3` from the original
 description now typecheck. See `typecheck/should_compile/T14333` from the
 testsuite.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14323#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