Quantcast

[GHC] #6065: Suggested type signature causes a type error (even though it appears correct)

classic Classic list List threaded Threaded
8 messages Options
GHC
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

[GHC] #6065: Suggested type signature causes a type error (even though it appears correct)

GHC
#6065: Suggested type signature causes a type error (even though it appears
correct)
---------------------------------------+------------------------------------
 Reporter:  tvynr                      |          Owner:                                          
     Type:  bug                        |         Status:  new                                    
 Priority:  normal                     |      Component:  Compiler (Type checker)                
  Version:  7.4.1                      |       Keywords:  type signature typeclass instance forall
       Os:  Linux                      |   Architecture:  x86_64 (amd64)                          
  Failure:  GHC rejects valid program  |       Testcase:                                          
Blockedby:                             |       Blocking:                                          
  Related:                             |  
---------------------------------------+------------------------------------
 The attached file, MWE.hs, contains an experiment attempting a rudimentary
 encoding of extensible ASTs in Haskell (without using compdata or a
 similar package relying upon OverlappingInstances and so forth).  The
 definition of the upcast function appears to be correct.  Compiling
 without a type signature produces a warning and the suggestion to include
 a type signature.  Including the suggested type signature (which appears
 to be the correct one) causes a type error.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6065>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
GHC
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6065: Suggested type signature causes a type error (even though it appears correct)

GHC
#6065: Suggested type signature causes a type error (even though it appears
correct)
---------------------------------------+------------------------------------
 Reporter:  tvynr                      |          Owner:                                          
     Type:  bug                        |         Status:  new                                    
 Priority:  normal                     |      Component:  Compiler (Type checker)                
  Version:  7.4.1                      |       Keywords:  type signature typeclass instance forall
       Os:  Linux                      |   Architecture:  x86_64 (amd64)                          
  Failure:  GHC rejects valid program  |       Testcase:                                          
Blockedby:                             |       Blocking:                                          
  Related:                             |  
---------------------------------------+------------------------------------
Changes (by rpglover64):

 * cc: rpglover64 (added)


--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6065#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
GHC
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6065: Suggested type signature causes a type error (even though it appears correct)

GHC
In reply to this post by GHC
#6065: Suggested type signature causes a type error (even though it appears
correct)
---------------------------------------+------------------------------------
 Reporter:  tvynr                      |          Owner:                                          
     Type:  bug                        |         Status:  new                                    
 Priority:  normal                     |      Component:  Compiler (Type checker)                
  Version:  7.4.1                      |       Keywords:  type signature typeclass instance forall
       Os:  Linux                      |   Architecture:  x86_64 (amd64)                          
  Failure:  GHC rejects valid program  |       Testcase:                                          
Blockedby:                             |       Blocking:                                          
  Related:                             |  
---------------------------------------+------------------------------------

Comment(by guest):

 I reduced your test case. The following file compiles, but if inferred
 type signature to "upcast" is added, it doesn't.

 {{{
 {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances
 #-}

 class AstOp ast result where
   astop :: ast -> result

 -- upcast :: AstOp ast ((ast -> t) -> t) => ast -> t
 upcast ast = astop ast upcast
 }}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6065#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
GHC
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6065: Suggested type signature causes a type error (even though it appears correct)

GHC
In reply to this post by GHC
#6065: Suggested type signature causes a type error (even though it appears
correct)
---------------------------------------------------------+------------------
    Reporter:  tvynr                                     |       Owner:                          
        Type:  bug                                       |      Status:  new                      
    Priority:  normal                                    |   Milestone:                          
   Component:  Compiler (Type checker)                   |     Version:  7.4.1                    
    Keywords:  type signature typeclass instance forall  |          Os:  Linux                    
Architecture:  x86_64 (amd64)                            |     Failure:  GHC rejects valid program
  Difficulty:  Unknown                                   |    Testcase:                          
   Blockedby:                                            |    Blocking:                          
     Related:                                            |  
---------------------------------------------------------+------------------
Changes (by simonpj):

  * difficulty:  => Unknown


Comment:

 Generally speaking GHC is now much better about ''not'' suggesting a type
 signature that then doesn't work. But it's not perfect and there's a good
 reason for that.  Here's why, if you care, but partly just to record the
 thinking in the ticket.

 I'll use a yet-simpler example that demonstrates the problem
 {{{
 {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances
 #-}

 module T6065 where

 class AstOp a b where
   astop :: a -> b -> Int

 -- upcast :: AstOp a (a -> Int) => a -> Int
 upcast ast = astop ast upcast
 }}}

 When GHC typechecks the RHS of `upcast` it provisionally gives `upcast`
 the (monomorphic) type `upcast :: alpha -> beta`, where `alpha` and `beta`
 are fresh unification variables. Then it typechecks the RHS of `upcast`,
 getting
 {{{
   (\ast -> astop ast upcast)
   Type :: alpha -> Int
   Constraint :: AstOp alpha (alpha -> Int)
                    (arising from the call to 'astop')
 }}}
 (`beta` gets unified to `Int`.)  Now it generalises that type to get
 {{{
   upcast :: forall c. AstOp c (c -> Int) => c -> Int
 }}}
 And that is the type GHE suggests:
 {{{
 T6065.hs:9:1: Warning:
     Top-level binding with no type signature:
       upcast :: forall a. AstOp a (a -> Int) => a -> Int
 }}}


 BUT if we ''provide'' this type signature, and then re-type-check the
 entire definition, we typecheck it with `upcast` having the above
 ''polymorphic'' type, NOT the old ''monomorphic'' type.  So the recursive
 call to `upcast` is instantiated by instantiating `c` with a fresh unknown
 type, say `gamma`.
 So we get this:
 {{{
   (\ast -> astop ast upcast)
   Type :: alpha -> beta
   Constraint :: AstOp alpha (gamma -> Int)
                    (arising from the call to 'astop')
                 AstOp gamma (gamma -> Int)
                    (arising from the recursive call to 'upcast')
 }}}
 And we can't solve these from the given constraint `(AstOp alpha (alpha ->
 Int))`, because nothing forces `gamma` and `alpha` to be unified.

 The problem is that when the recursive call is polymorphic, we get more
 unknown types (arising from instantiating the type variables of the
 recursive call to `upcast`). We can fix that with a type signature such as
 {{{
 upcast :: forall a. AstOp a (a -> Int) => a -> Int
 upcast ast = astop ast (upcast :: a -> Int)
 }}}
 where the type signature on the RHS fixes `gamma`.  (Needs
 `ScopedTypeVariables`.)

 But that is not the point.  The point is that it's very unhelpful for GHC
 to suggest a type that doesn't work. But
  * Even realising that the suggested type doesn't work requires re-
 generating the constraints from scratch, which is a major (and non-linear)
 pain.
  * Even if we knew that the suggested type didn't work, it's not clear
 what complaint to give.

 So I'm a bit stuck here, and for now I propose to do nothing. Nice bug
 report though!

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6065#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
GHC
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6065: Suggested type signature causes a type error (even though it appears correct)

GHC
In reply to this post by GHC
#6065: Suggested type signature causes a type error (even though it appears
correct)
---------------------------------------------------------+------------------
    Reporter:  tvynr                                     |       Owner:                          
        Type:  bug                                       |      Status:  new                      
    Priority:  normal                                    |   Milestone:  _|_                      
   Component:  Compiler (Type checker)                   |     Version:  7.4.1                    
    Keywords:  type signature typeclass instance forall  |          Os:  Linux                    
Architecture:  x86_64 (amd64)                            |     Failure:  GHC rejects valid program
  Difficulty:  Unknown                                   |    Testcase:                          
   Blockedby:                                            |    Blocking:                          
     Related:                                            |  
---------------------------------------------------------+------------------
Changes (by simonpj):

  * milestone:  => _|_


--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6065#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
GHC
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6065: Suggested type signature causes a type error (even though it appears correct)

GHC
In reply to this post by GHC
#6065: Suggested type signature causes a type error (even though it appears
correct)
---------------------------------------------------------+------------------
    Reporter:  tvynr                                     |       Owner:                          
        Type:  bug                                       |      Status:  new                      
    Priority:  normal                                    |   Milestone:  _|_                      
   Component:  Compiler (Type checker)                   |     Version:  7.4.1                    
    Keywords:  type signature typeclass instance forall  |          Os:  Linux                    
Architecture:  x86_64 (amd64)                            |     Failure:  GHC rejects valid program
  Difficulty:  Unknown                                   |    Testcase:                          
   Blockedby:                                            |    Blocking:                          
     Related:                                            |  
---------------------------------------------------------+------------------

Comment(by tvynr):

 Unfortunately, it seems that the reduced example has lost something;
 applying the typecast to the upcast function in the original MWE.hs (as
 shown in the newly-attached MWE2.hs) does not work; the same type error is
 raised.  Does MWE2.hs have the appropriate typecast or did I do something
 wrong?

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6065#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
GHC
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6065: Suggested type signature causes a type error (even though it appears correct)

GHC
In reply to this post by GHC
#6065: Suggested type signature causes a type error (even though it appears
correct)
---------------------------------------------------------+------------------
    Reporter:  tvynr                                     |       Owner:                          
        Type:  bug                                       |      Status:  new                      
    Priority:  normal                                    |   Milestone:  _|_                      
   Component:  Compiler (Type checker)                   |     Version:  7.4.1                    
    Keywords:  type signature typeclass instance forall  |          Os:  Linux                    
Architecture:  x86_64 (amd64)                            |     Failure:  GHC rejects valid program
  Difficulty:  Unknown                                   |    Testcase:                          
   Blockedby:                                            |    Blocking:                          
     Related:                                            |  
---------------------------------------------------------+------------------

Comment(by simonpj):

 Type variables only scope if you have an explicit `forall`.  So you need
 {{{
 upcast :: forall ast1 ast2. (AstOp HomOp ast1 ((ast1 -> ast2) -> ast2)) =>
 ast1 -> ast2
 }}}
 That compiles fine.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6065#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
GHC
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6065: Suggested type signature causes a type error (even though it appears correct)

GHC
In reply to this post by GHC
#6065: Suggested type signature causes a type error (even though it appears
correct)
---------------------------------------------------------+------------------
    Reporter:  tvynr                                     |       Owner:                          
        Type:  bug                                       |      Status:  new                      
    Priority:  normal                                    |   Milestone:  _|_                      
   Component:  Compiler (Type checker)                   |     Version:  7.4.1                    
    Keywords:  type signature typeclass instance forall  |          Os:  Linux                    
Architecture:  x86_64 (amd64)                            |     Failure:  GHC rejects valid program
  Difficulty:  Unknown                                   |    Testcase:                          
   Blockedby:                                            |    Blocking:                          
     Related:                                            |  
---------------------------------------------------------+------------------

Comment(by tvynr):

 Fair point; sorry about that.  :)  It compiles fine on my machine as well.
 Thanks for the workaround!

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6065#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Loading...