[GHC] #12468: GADTs don't refine hole types

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

[GHC] #12468: GADTs don't refine hole types

GHC - devs mailing list
#12468: GADTs don't refine hole types
-------------------------------------+-------------------------------------
           Reporter:                 |             Owner:
  benjamin.hodgson                   |
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  MacOS X
       Architecture:                 |   Type of failure:  Incorrect
  Unknown/Multiple                   |  warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Apologies if this is a dupe. I did look!

 {{{
 #!haskell
 {-# LANGUAGE GADTs #-}

 data T a where
     I :: T Int

 f :: T a -> a
 f I = _
 }}}

 This gives the type error:

 {{{
     • Found hole: _ :: a
       Where: ‘a’ is a rigid type variable bound by
                the type signature for:
                  f :: forall a. T a -> a
                at test.hs:6:6
     • In the expression: _
       In an equation for ‘f’: f I = _
     • Relevant bindings include f :: T a -> a (bound at test.hs:7:1)
 }}}

 It should say something about `a` being `Int` in this branch.

 I'm using GHC 8.0.1 on OSX El Capitan. I think this may be a regression; I
 have a vague memory of it working with GHC 7.10.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468>
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] #12468: GADTs don't refine hole types

GHC - devs mailing list
#12468: GADTs don't refine hole types
-------------------------------------+-------------------------------------
        Reporter:  benjamin.hodgson  |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  MacOS X           |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I don't think this is a bug.  Yes we have an equality in scope; but a
 value of type `a` and one of type `Int` are both equally valid things to
 fill the hole with.  E.g.
 {{{
 f :: T a -> a -> a
 f I x = _
 }}}
 I could fill the hole with `(3::Int)` or with `x`.  Neitehr is better than
 the other.

 Another way to say this is that type equalities are not normalising; they
 are equalities, not left-to-right rewrite rules.   Suppose we had `a ~ b`
 in scope.  Should report the hole as having type `a` or `b`?  What if it
 was `a ~ [b]`?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#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] #12468: GADTs don't refine hole types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#12468: GADTs don't refine hole types
-------------------------------------+-------------------------------------
        Reporter:  benjamin.hodgson  |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  MacOS X           |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by benjamin.hodgson):

 Thanks for the reply! I see what you mean about `a` and `Int` both being
 good options to show for the hole type. However, I do think it would still
 be helpful to have ''some'' indicator in the error message of the fact
 that the context gives us a useful equality. Something along the lines of:

 {{{
     • Found hole: _ :: a
       ...
     • NB: a ~ [b]
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#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] #12468: GADTs don't refine hole types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#12468: GADTs don't refine hole types
-------------------------------------+-------------------------------------
        Reporter:  benjamin.hodgson  |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  MacOS X           |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 > However, I do think it would still be helpful to have some indicator in
 the error message of the fact that the context gives us an equality. After
 all, such information can be very useful when you're trying to fill in a
 hole.  Something along the lines of:

 Yes, that's plausible and do-able; along the lines of displaying the
 "relevant bindings".  Does anyone want to have a go?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#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] #12468: GADTs don't refine hole types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#12468: GADTs don't refine hole types
-------------------------------------+-------------------------------------
        Reporter:  benjamin.hodgson  |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  MacOS X           |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by bgamari):

 * type:  bug => feature request


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#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] #12468: GADTs don't refine hole types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#12468: GADTs don't refine hole types
-------------------------------------+-------------------------------------
        Reporter:  benjamin.hodgson  |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11325            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * os:  MacOS X => Unknown/Multiple
 * related:   => #11325


Comment:

 As noted in #11325, this is actually a regression from GHC 7.10 to 8.0. In
 GHC 7.10.3, you get the behavior that you seek:

 {{{
 $ /opt/ghc/7.10.3/bin/ghci Bug.hs
 GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 Bug.hs:7:7:
     Found hole ‘_’ with type: Int
     Relevant bindings include f :: T a -> a (bound at Bug.hs:7:1)
     In the expression: _
     In an equation for ‘f’: f I = _
 Failed, modules loaded: none.
 }}}

 As opposed to the current behavior:

 {{{
 $ /opt/ghc/8.0.1/bin/ghci Bug.hs
 GHCi, version 8.0.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:7:7: error:
     • Found hole: _ :: a
       Where: ‘a’ is a rigid type variable bound by
                the type signature for:
                  f :: forall a. T a -> a
                at Bug.hs:6:6
     • In the expression: _
       In an equation for ‘f’: f I = _
     • Relevant bindings include f :: T a -> a (bound at Bug.hs:7:1)
 Failed, modules loaded: none.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#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] #12468: GADTs don't refine hole types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#12468: GADTs don't refine hole types
-------------------------------------+-------------------------------------
        Reporter:  benjamin.hodgson  |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11325            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 On second thoughts, I don't think I'd fully realised that there was a type
 signature to guide the type checker.  Yes, it probably does make sense to
 "normalise" the hole with all the "givens". And it's very easy to do, a
 2-line change.  Patch coming

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#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] #12468: GADTs don't refine hole types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#12468: GADTs don't refine hole types
-------------------------------------+-------------------------------------
        Reporter:  benjamin.hodgson  |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11325            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Simon Peyton Jones <simonpj@…>):

 In [changeset:"433b80dec1cfef787fc1327a9eada1791b11c12e/ghc" 433b80d/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="433b80dec1cfef787fc1327a9eada1791b11c12e"
 Ensure that insolubles are fully rewritten

 I was alerted to this by Trac #12468 and #11325.  We were treating
 insolubles (and "hole" constraints are treated as insoluble)
 inconsistently.  In some places we were carefully rewriting them
 e.g. Note [Make sure that insolubles are fully rewritten] in
 TcCanonical.  But in TcSimplify we weren't feeding them into
 the solver.

 As a result, "hole" constraints were not being rewritten, which
 some users found confusing, and I think rightly so.

 This patch also fixes a bug in TcSMonad.emitInsoluble, in which two
 different "hole" constriants could be treated (bogusly) as duplicates,
 thereby losing one.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12468#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] #12468: GADTs don't refine hole types

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#12468: GADTs don't refine hole types
-------------------------------------+-------------------------------------
        Reporter:  benjamin.hodgson  |                Owner:  (none)
            Type:  feature request   |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:  gadt/T12468
      Blocked By:                    |             Blocking:
 Related Tickets:  #11325            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  new => closed
 * testcase:   => gadt/T12468
 * resolution:   => fixed


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