[GHC] #4361: Typechecker regression

[GHC]

#4361: Typechecker regression
----------------------------------------+-----------------------------------
    Reporter:  igloo                    |        Owner:  simonpj    
        Type:  bug                      |       Status:  new        
    Priority:  high                     |    Milestone:  7.0.1      
   Component:  Compiler (Type checker)  |      Version:  7.1        
    Keywords:                           |     Testcase:              
   Blockedby:                           |   Difficulty:              
          Os:  Unknown/Multiple         |     Blocking:              
Architecture:  Unknown/Multiple         |      Failure:  None/Unknown
----------------------------------------+-----------------------------------
 Here's the essence of the regression DoCon showed up, reported here:
 http://www.haskell.org/pipermail/glasgow-haskell-
 bugs/2010-September/025511.html

 {{{
 {-# LANGUAGE FlexibleContexts #-}

 module Pol3_ (moduloBasisx) where

 class CommutativeRing a
 class CommutativeRing a => LinSolvRing a
 class LinSolvRing a => EuclideanRing a

 instance EuclideanRing a => LinSolvRing (Pol a)
 instance CommutativeRing a => CommutativeRing (Pol a)

 data Pol a = MkPol

 upLinSolvRing :: LinSolvRing a => a -> ()
 upLinSolvRing = undefined

 moduloBasisx :: (LinSolvRing (Pol a), CommutativeRing a) => Pol a -> ()
 moduloBasisx p = let x = upLinSolvRing p
                  in ()
 }}}

 {{{
 $ ghc --version
 The Glorious Glasgow Haskell Compilation System, version 6.12.2
 $ ghc --make Pol3_
 [1 of 1] Compiling Pol3_            ( Pol3_.hs, Pol3_.o )
 $
 }}}

 {{{
 $ ghc --version
 The Glorious Glasgow Haskell Compilation System, version 7.0.0.20100924
 $ ghc --make Pol3_
 [1 of 1] Compiling Pol3_            ( Pol3_.hs, Pol3_.o )

 Pol3_.hs:19:26:
     Could not deduce (EuclideanRing a)
       from the context (LinSolvRing (Pol a), CommutativeRing a)
       arising from a use of `upLinSolvRing'
     Possible fix:
       add (EuclideanRing a) to the context of
         the type signature for `moduloBasisx'
     In the expression: upLinSolvRing p
     In an equation for `x': x = upLinSolvRing p
     In the expression: let x = upLinSolvRing p in ()
 $
 }}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4361>
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]

#4361: Typechecker regression
---------------------------------------------+------------------------------
  Reporter:  igloo                           |          Owner:  simonpj        
      Type:  bug                             |         Status:  closed          
  Priority:  high                            |      Milestone:  7.0.1          
 Component:  Compiler (Type checker)         |        Version:  7.1            
Resolution:  fixed                           |       Keywords:                  
  Testcase:  typecheck/should_compile/T4361  |      Blockedby:                  
Difficulty:                                  |             Os:  Unknown/Multiple
  Blocking:                                  |   Architecture:  Unknown/Multiple
   Failure:  None/Unknown                    |  
---------------------------------------------+------------------------------
Changes (by simonpj):

  * status:  new => closed
  * testcase:  => typecheck/should_compile/T4361
  * resolution:  => fixed


Comment:

 Aha. It turns out that Sergei is pushing the boundaries here.  It's not at
 all clear that this program should be accepted.  Still I've beefed up
 `simplifyInfer` so that it does the job.  I had to take two bites at this
 particular cherry:
 {{{
 Fri Oct  8 04:12:27 PDT 2010  [hidden email]
   * Fix Trac #4361: be more discerning when inferring types

   Note [Avoid unecessary constraint simplification] in TcSimplify

     M ./compiler/typecheck/TcSimplify.lhs -3 +41
 }}}
 and
 {{{
 Fri Oct  8 06:35:42 PDT 2010  [hidden email]
   * Do less simplification when doing let-generalisation

   This fixes Trac #4361.  In a rather delicate way, but
   no more delicate than before.  A more remoseless typechecker
   would reject #4361 altogether.

   See Note [Avoid unecessary constraint simplification]

     M ./compiler/typecheck/TcSimplify.lhs -22 +32
 }}}
 Simon

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

#4361: Typechecker regression
---------------------------------------------+------------------------------
  Reporter:  igloo                           |          Owner:  simonpj        
      Type:  bug                             |         Status:  closed          
  Priority:  high                            |      Milestone:  7.0.1          
 Component:  Compiler (Type checker)         |        Version:  7.1            
Resolution:  fixed                           |       Keywords:                  
        Os:  Unknown/Multiple                |   Architecture:  Unknown/Multiple
   Failure:  None/Unknown                    |     Difficulty:  Unknown        
  Testcase:  typecheck/should_compile/T4361  |      Blockedby:                  
  Blocking:                                  |        Related:                  
---------------------------------------------+------------------------------
Changes (by simonpj):

  * difficulty:  => Unknown


Comment:

 For completeness, `Note [Avoid unecessary constraint simplification]` is
 this:
 {{{
 Note [Avoid unecessary constraint simplification]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When inferring the type of a let-binding, with simplifyInfer,
 try to avoid unnecessarily simplifying class constraints.
 Doing so aids sharing, but it also helps with delicate
 situations like

    instance C t => C [t] where ..

    f :: C [t] => ....
    f x = let g y = ...(constraint C [t])...
          in ...
 When inferring a type for 'g', we don't want to apply the
 instance decl, because then we can't satisfy (C t).  So we
 just notice that g isn't quantified over 't' and partition
 the contraints before simplifying.

 This only half-works, but then let-generalisation only half-works.
 }}}

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

#4361: Typechecker regression
---------------------------------------------+------------------------------
  Reporter:  igloo                           |          Owner:  simonpj        
      Type:  bug                             |         Status:  closed          
  Priority:  high                            |      Milestone:  7.0.1          
 Component:  Compiler (Type checker)         |        Version:  7.1            
Resolution:  fixed                           |       Keywords:                  
        Os:  Unknown/Multiple                |   Architecture:  Unknown/Multiple
   Failure:  None/Unknown                    |     Difficulty:  Unknown        
  Testcase:  typecheck/should_compile/T4361  |      Blockedby:                  
  Blocking:                                  |        Related:                  
---------------------------------------------+------------------------------
Changes (by simonpj):

 * cc: mechvel@… (added)


Comment:

 With all the changes to type inference engine, it has become apparent that
 the hack I put in to solve Serge's problem is indeed a GROSSLY UNSAVOURY
 HACK.
  * It is extremely fragile.  It only solves the problem in a special case,
 so the very same problem will arise again in a somewhat more complicated
 program.
  * It takes quite a bit of code.
  * It has increasingly unpleasant knock-on effects.  Eg `IPRun` has
 started failing because a special case for implicit parameters has been
 removed. But the special case itself was only needed because of the
 GROSSLY UNSAVOURY HACK.

 The hack is described in `Note [Avoid unecessary constraint
 simplification]` above. I'm taking it out, which will make !DoCon fail to
 compile. The culprit is local let generalisation (see
 [http://hackage.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7 my blog
 post]).  Happily, it's extremely easy to fix your source code in either of
 these two ways:

  * If you use `-XMonoLocalBinds` (which is in any case implied by
 `-XGADTs` and `-XTypeFamilies`), then GHC won't generalise the definition
 of `x` in the example, and all will be well.

  * Alterantively, give a type signature for `x`, thus (in this case)
 {{{
 moduloBasisx p = let x :: ()
                      x = upLinSolvRing p
                  in ()
 }}}
  Doing so means that generalisation does not happen, and the constraints
 are solved outside-in, as is really desired.

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

[Serge D. Mechveliani]

On Wed, Jun 20, 2012 at 04:55:59PM -0000, GHC wrote:

> #4361: Typechecker regression
> ---------------------------------------------+------------------------------
>   Reporter:  igloo                           |          Owner:  simonpj        
>       Type:  bug                             |         Status:  closed          
>   Priority:  high                            |      Milestone:  7.0.1          
>  Component:  Compiler (Type checker)         |        Version:  7.1            
> Resolution:  fixed                           |       Keywords:                  
>         Os:  Unknown/Multiple                |   Architecture:  Unknown/Multiple
>    Failure:  None/Unknown                    |     Difficulty:  Unknown        
>   Testcase:  typecheck/should_compile/T4361  |      Blockedby:                  
>   Blocking:                                  |        Related:                  
> ---------------------------------------------+------------------------------
> Changes (by simonpj):
>
>  * cc: mechvel@??? (added)
>
>
> Comment:
>
>  With all the changes to type inference engine, it has become apparent that
>  the hack I put in to solve Serge's problem is indeed a GROSSLY UNSAVOURY
>  HACK.
>   * It is extremely fragile.  It only solves the problem in a special case,
>  so the very same problem will arise again in a somewhat more complicated
>  program.
>   * It takes quite a bit of code.
>   * It has increasingly unpleasant knock-on effects.  Eg `IPRun` has
>  started failing because a special case for implicit parameters has been
>  removed. But the special case itself was only needed because of the
>  GROSSLY UNSAVOURY HACK.
>
>  The hack is described in `Note [Avoid unecessary constraint
>  simplification]` above. I'm taking it out, which will make !DoCon fail to
>  compile. The culprit is local let generalisation (see
>  [http://hackage.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7 my blog
>  post]).  Happily, it's extremely easy to fix your source code in either of
>  these two ways:
>
>   * If you use `-XMonoLocalBinds` (which is in any case implied by
>  `-XGADTs` and `-XTypeFamilies`), then GHC won't generalise the definition
>  of `x` in the example, and all will be well.
>
>   * Alterantively, give a type signature for `x`, thus (in this case)
>  {{{
>  moduloBasisx p = let x :: ()
>                       x = upLinSolvRing p
>                   in ()
>  }}}
>   Doing so means that generalisation does not happen, and the constraints
>  are solved outside-in, as is really desired.
>

All right.
Later, I shall try your two way outs for DoCon and report the result.

Regards,
Sergei

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

[GHC]

#4361: Typechecker regression
---------------------------------------------+------------------------------
  Reporter:  igloo                           |          Owner:  simonpj        
      Type:  bug                             |         Status:  closed          
  Priority:  high                            |      Milestone:  7.0.1          
 Component:  Compiler (Type checker)         |        Version:  7.1            
Resolution:  fixed                           |       Keywords:                  
        Os:  Unknown/Multiple                |   Architecture:  Unknown/Multiple
   Failure:  None/Unknown                    |     Difficulty:  Unknown        
  Testcase:  typecheck/should_compile/T4361  |      Blockedby:                  
  Blocking:                                  |        Related:                  
---------------------------------------------+------------------------------

Comment(by simonpj@…):

 commit f450d36a31d6687f338cb6a9590f8c2f689d79fe
 {{{
 Author: Simon Peyton Jones <[hidden email]>
 Date:   Thu Jun 21 08:47:33 2012 +0100

     Remove the USAVOURY HACK in simplifyInfer

     See the discussion in Trac #4361.  The change fixes
     a regression in test IPRun.

  compiler/typecheck/TcSimplify.lhs |  104
 +++++++++++--------------------------
  1 files changed, 30 insertions(+), 74 deletions(-)
 }}}

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

#4361: Typechecker regression
---------------------------------------------+------------------------------
  Reporter:  igloo                           |          Owner:  simonpj        
      Type:  bug                             |         Status:  closed          
  Priority:  high                            |      Milestone:  7.0.1          
 Component:  Compiler (Type checker)         |        Version:  7.1            
Resolution:  fixed                           |       Keywords:                  
        Os:  Unknown/Multiple                |   Architecture:  Unknown/Multiple
   Failure:  None/Unknown                    |     Difficulty:  Unknown        
  Testcase:  typecheck/should_compile/T4361  |      Blockedby:                  
  Blocking:                                  |        Related:                  
---------------------------------------------+------------------------------

Comment(by pcapriotti):

 I ran into this while building the `morfette` package (see #6082) with GHC
 HEAD.

 Here's a very simple example which fails to type check without
 `-XMonoLocalBinds`:

 {{{
 {-# LANGUAGE FlexibleContexts #-}

 foo :: Eq (a,b) => (a,b) -> Bool
 foo x = let r = x == x in r
 }}}

 Is this expected?

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

#4361: Typechecker regression
---------------------------------------------+------------------------------
  Reporter:  igloo                           |          Owner:  simonpj        
      Type:  bug                             |         Status:  closed          
  Priority:  high                            |      Milestone:  7.0.1          
 Component:  Compiler (Type checker)         |        Version:  7.1            
Resolution:  fixed                           |       Keywords:                  
        Os:  Unknown/Multiple                |   Architecture:  Unknown/Multiple
   Failure:  None/Unknown                    |     Difficulty:  Unknown        
  Testcase:  typecheck/should_compile/T4361  |      Blockedby:                  
  Blocking:                                  |        Related:                  
---------------------------------------------+------------------------------

Comment(by simonpj):

 Yes, that's expected.  When inferring a type for 'r' we simplify (Eq
 (a,b)) to (Eq a, Eq b); and those can't be deduced from (Eq (a,b)).

 Again `-XMonoLocalBinds` or a type signature solves it.  I'm not inclined
 to worry here.

 Simon

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