Quantcast

[GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

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

[GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

GHC - devs mailing list
#11325: Type of hole does not get refined after pattern matching on [GADT]
constructors
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.11
  (Type checker)                     |
           Keywords:  GADTs          |  Operating System:  Linux
       Architecture:  x86            |   Type of failure:  Incorrect
                                     |  warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 From [https://www.youtube.com/watch?v=6snteFntvjM A Practical Introduction
 to Haskell GADTs] from LambdaConf 2015, example from attachment Hole.hs:

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

 data STy ty where
   SInt   :: STy Int
   SBool  :: STy Bool
   SMaybe :: STy a -> STy (Maybe a)

 zero :: STy ty -> ty
 zero ty = case ty of
   SInt     -> 5
   SBool    -> False
   SMaybe a -> _
 }}}

 When running with "GHCi, version 7.11.20151226":

 {{{
 % ghci -ignore-dot-ghci /tmp/Hole.hs
 GHCi, version 7.11.20151226: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( /tmp/Hole.hs, interpreted )

 /tmp/Hole.hs:12:15: error:
     • Found hole: _ :: ty
       Where: ‘ty’ is a rigid type variable bound by
                the type signature for:
                  zero :: forall ty. STy ty -> ty
                at /tmp/Hole.hs:8:9
     • In the expression: _
       In a case alternative: SMaybe a -> _
       In the expression:
         case ty of {
           SInt -> 5
           SBool -> False
           SMaybe a -> _ }
     • Relevant bindings include
         a :: STy a (bound at /tmp/Hole.hs:12:10)
         ty :: STy ty (bound at /tmp/Hole.hs:9:6)
         zero :: STy ty -> ty (bound at /tmp/Hole.hs:9:1)
 Failed, modules loaded: none.
 Prelude>
 }}}

 when older versions (GHCi version 7.10.2) refine the type of `_` to `Maybe
 a`:

 {{{
 % ghci-7.10.2 -ignore-dot-ghci /tmp/Hole.hs
 GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( /tmp/Hole.hs, interpreted )

 /tmp/Hole.hs:12:15:
     Found hole ‘_’ with type: Maybe a
     Where: ‘a’ is a rigid type variable bound by
                a pattern with constructor
                  SMaybe :: forall a. STy a -> STy (Maybe a),
                in a case alternative
                at /tmp/Hole.hs:12:3
     Relevant bindings include
       a :: STy a (bound at /tmp/Hole.hs:12:10)
       ty :: STy ty (bound at /tmp/Hole.hs:9:6)
       zero :: STy ty -> ty (bound at /tmp/Hole.hs:9:1)
     In the expression: _
     In a case alternative: SMaybe a -> _
     In the expression:
       case ty of {
         SInt -> 5
         SBool -> False
         SMaybe a -> _ }
 Failed, modules loaded: none.
 Prelude>
 }}}

 Regression?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325>
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
|  
Report Content as Inappropriate

Re: [GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

GHC - devs mailing list
#11325: Type of hole does not get refined after pattern matching on [GADT]
constructors
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Linux             |         Architecture:  x86
 Type of failure:  Incorrect         |            Test Case:
  warning at compile-time            |
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by Iceland_jack):

 * Attachment "Hole.hs" added.

 GHC 7.11 does not refine the typed hole

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325>
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
|  
Report Content as Inappropriate

Re: [GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#11325: Type of hole does not get refined after pattern matching on [GADT]
constructors
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Linux             |         Architecture:  x86
 Type of failure:  Incorrect         |            Test Case:
  warning at compile-time            |
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by Iceland_jack):

 * Attachment "Hole.log" added.

 ghci-7.11.20151226 -v -ignore-dot-ghci /tmp/Hole.hs &> /tmp/Hole.log

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325>
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
|  
Report Content as Inappropriate

Re: [GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#11325: Type of hole does not get refined after pattern matching on [GADT]
constructors
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Linux             |         Architecture:  x86
 Type of failure:  Incorrect         |            Test Case:
  warning at compile-time            |
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * owner:   => goldfire


Comment:

 I'm sure this is from the visible type application stuff. Will take a
 look.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325#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
|  
Report Content as Inappropriate

Re: [GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#11325: Type of hole does not get refined after pattern matching on [GADT]
constructors
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Linux             |         Architecture:  x86
 Type of failure:  Incorrect         |            Test Case:
  warning at compile-time            |
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * cc: RyanGlScott (added)


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325#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
|  
Report Content as Inappropriate

Re: [GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#11325: Type of hole does not get refined after pattern matching on [GADT]
constructors
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Linux             |         Architecture:  x86
 Type of failure:  Incorrect         |            Test Case:
  warning at compile-time            |
      Blocked By:                    |             Blocking:
 Related Tickets:  #12468            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * related:   => #12468


Comment:

 See #12468, where SPJ argues that the current behavior is not necessarily
 wrong, and proposes that we should instead report something to the effect
 of:

 {{{
     • Found hole: _ :: ty
       ...
     • NB: ty ~ Maybe a
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325#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
|  
Report Content as Inappropriate

Re: [GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#11325: Type of hole does not get refined after pattern matching on [GADT]
constructors
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Linux             |         Architecture:  x86
 Type of failure:  Incorrect         |            Test Case:
  warning at compile-time            |
      Blocked By:                    |             Blocking:
 Related Tickets:  #12468            |  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/11325#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
|  
Report Content as Inappropriate

Re: [GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#11325: Type of hole does not get refined after pattern matching on [GADT]
constructors
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |
      Resolution:                    |             Keywords:  GADTs
Operating System:  Linux             |         Architecture:  x86
 Type of failure:  Incorrect         |            Test Case:
  warning at compile-time            |
      Blocked By:                    |             Blocking:
 Related Tickets:  #12468            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I've confirmed that the 7.10 behaviour is restored, but I didn't add a
 second test ... the test for #12468 seems sufficient.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11325#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
|  
Report Content as Inappropriate

Re: [GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#11325: Type of hole does not get refined after pattern matching on [GADT]
constructors
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  goldfire
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |
      Resolution:  fixed             |             Keywords:  GADTs
Operating System:  Linux             |         Architecture:  x86
 Type of failure:  Incorrect         |            Test Case:
  warning at compile-time            |
      Blocked By:                    |             Blocking:
 Related Tickets:  #12468            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  new => closed
 * resolution:   => fixed


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