[GHC] #2418: desugaring type function application to constraint makes bug disappear

[GHC-2]

#2418: desugaring type function application to constraint makes bug disappear
------------------------------+---------------------------------------------
    Reporter:  claus          |       Owner:                        
        Type:  bug            |      Status:  new                    
    Priority:  normal         |   Component:  Compiler (Type checker)
     Version:  6.9            |    Severity:  normal                
    Keywords:  type families  |    Testcase:                        
Architecture:  Unknown        |          Os:  Unknown                
------------------------------+---------------------------------------------
 When considering type functions, I find it helpful to desugar their
 applications into additional constraints (`tf a` becomes `tf a~tfa=>tfa`).
 But consider this example from a recent [http://www.haskell.org/pipermail
 /haskell-cafe/2008-July/044911.html haskell-cafe thread]:
 {{{
 {-# OPTIONS_GHC -fglasgow-exts #-}

 class Blah f a where blah :: a -> T f f a
 class A f where type T f :: (* -> *) -> * -> *

 -- wrapper :: forall a f tf . (Blah f a,T f~tf) => a -> tf f a
 wrapper :: forall a f . (Blah f a) => a -> T f f a
 wrapper x = blah x
 }}}
 for which `GHCi, version 6.9.20080514` yields:
 {{{
 C:\Documents and Settings\cr3\Desktop\TF.hs:8:12:
     Could not deduce (Blah f a) from the context (Blah f1 a)
       arising from a use of `blah'
                    at C:\Documents and Settings\cr3\Desktop\TF.hs:8:12-17
     Possible fix:
       add (Blah f a) to the context of the type signature for `wrapper'
     In the expression: blah x
     In the definition of `wrapper': wrapper x = blah x

 C:\Documents and Settings\cr3\Desktop\TF.hs:8:12:
     Couldn't match expected type `T f1 f1 a'
            against inferred type `T f f a'
     In the expression: blah x
     In the definition of `wrapper': wrapper x = blah x
 Failed, modules loaded: none.
 }}}
 Switching to the desugared version of the `wrapper` signature makes the
 error go away, so the "desugared" and original version are not equivalent
 in the current implementation of type families! See also
 [http://www.haskell.org/pipermail/haskell-cafe/2008-July/044914.html].

 For added fun, GHCi reports the sugared type when using the desugared one:
 {{{
 *Main> :t wrapper
 wrapper :: (Blah f a) => a -> T f f a
 }}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2418>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

[GHC-2]

#2418: desugaring type function application to constraint makes bug disappear
-------------------------------------+--------------------------------------
 Reporter:  claus                    |          Owner:        
     Type:  bug                      |         Status:  new    
 Priority:  normal                   |      Milestone:        
Component:  Compiler (Type checker)  |        Version:  6.9    
 Severity:  normal                   |     Resolution:        
 Keywords:  type families            |     Difficulty:  Unknown
 Testcase:                           |   Architecture:  Unknown
       Os:  Unknown                  |  
-------------------------------------+--------------------------------------
Changes (by simonpj):

  * difficulty:  => Unknown

Comment:

 Thanks.  We're collecting type-function-related bugs here
 http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsStatus.  Manuel is
 on the job, now that his exam season is nearly over.

 Simon

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2418#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

[GHC-2]

#2418: desugaring type function application to constraint makes bug disappear
-------------------------------------+--------------------------------------
 Reporter:  claus                    |          Owner:        
     Type:  bug                      |         Status:  new    
 Priority:  normal                   |      Milestone:  6.10.1
Component:  Compiler (Type checker)  |        Version:  6.9    
 Severity:  normal                   |     Resolution:        
 Keywords:  type families            |     Difficulty:  Unknown
 Testcase:                           |   Architecture:  Unknown
       Os:  Unknown                  |  
-------------------------------------+--------------------------------------
Changes (by igloo):

  * milestone:  => 6.10.1

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2418#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

[GHC-2]

#2418: desugaring type function application to constraint makes bug disappear
-------------------------------------+--------------------------------------
 Reporter:  claus                    |          Owner:          
     Type:  bug                      |         Status:  closed  
 Priority:  normal                   |      Milestone:  6.10.1  
Component:  Compiler (Type checker)  |        Version:  6.9      
 Severity:  normal                   |     Resolution:  duplicate
 Keywords:  type families            |     Difficulty:  Unknown  
 Testcase:                           |   Architecture:  Unknown  
       Os:  Unknown                  |  
-------------------------------------+--------------------------------------
Changes (by chak):

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

Comment:

 This is actually a duplicate of #2146 (which more accurately pinpoints the
 underlying problem).

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2418#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

[GHC-2]

#2418: desugaring type function application to constraint makes bug disappear
-------------------------------------+--------------------------------------
 Reporter:  claus                    |          Owner:          
     Type:  bug                      |         Status:  closed  
 Priority:  normal                   |      Milestone:  6.10.1  
Component:  Compiler (Type checker)  |        Version:  6.9      
 Severity:  normal                   |     Resolution:  duplicate
 Keywords:  type families            |     Difficulty:  Unknown  
 Testcase:                           |   Architecture:  Unknown  
       Os:  Unknown                  |  
-------------------------------------+--------------------------------------
Comment (by claus):

 Replying to [comment:3 chak]:
 > This is actually a duplicate of #2146 (which more accurately pinpoints
 the underlying problem).

 How so? I had some trouble reconstructing the intended example in #2146,
 but given the implicit constraints (higher-kinded & ignores first
 parameter), I assume it is something like:
 {{{
 {-# LANGUAGE TypeFamilies #-}
 type family F a :: * -> *
 type instance F a = (,) String

 foo :: (F Int a ~ F Int [a]) => a -> [a]
 foo = undefined

 foo' :: (F Int a ~ F Bool [a]) => a -> [a]
 foo' = undefined
 }}}
 for which `GHCi, version 6.9.20080514` (a version that fails the
 desugaring test) gives the expected errors
 {{{
 C:\Documents and Settings\cr3\Desktop\F.hs:6:0:
     Occurs check: cannot construct the infinite type: a = [a]
     When generalising the type(s) for `foo'

 C:\Documents and Settings\cr3\Desktop\F.hs:9:0:
     Occurs check: cannot construct the infinite type: a = [a]
     When generalising the type(s) for `foo''
 Failed, modules loaded: none.
 }}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2418#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

[GHC-2]

#2418: desugaring type function application to constraint makes bug disappear
-------------------------------------+--------------------------------------
 Reporter:  claus                    |          Owner:          
     Type:  bug                      |         Status:  closed  
 Priority:  normal                   |      Milestone:  6.10.1  
Component:  Compiler (Type checker)  |        Version:  6.9      
 Severity:  normal                   |     Resolution:  duplicate
 Keywords:  type families            |     Difficulty:  Unknown  
 Testcase:                           |   Architecture:  Unknown  
       Os:  Unknown                  |  
-------------------------------------+--------------------------------------
Comment (by chak):

 Replying to [comment:4 claus]:
 > Replying to [comment:3 chak]:
 > > This is actually a duplicate of #2146 (which more accurately pinpoints
 the underlying problem).
 >
 > How so?

 `T` is a unary type synonym family, so in
 {{{
 wrapper :: forall a f . (Blah f a) => a -> T f f a
 }}}
 you should read the result type as `(T f) f a`, where `T f` is the
 ''family application,'' whereas the application of `(T f)` to the second
 `f` and to `a` are vanilla type applications.  The bug is that GHC
 mistakenly takes the whole of `T f f a` as tertiary family application.
 (If it ''were'' a tertiary family application, the signature would be
 ambiguous and the error message would be correct - but it's unary, so GHC
 is wrong in rejecting the program.)

 This also explains why what you call the desugared variant works:
 {{{
 wrapper :: forall a f tf . (Blah f a,T f~tf) => a -> tf f a
 }}}
 Here `tf f a` syntactically contains no type family.  So, GHC correctly
 takes this to be vanilla type applications.

 The place in the type checker where things go wrong is in the
 implementation of what we call the ''decomposition rule'' (see our
 forthcoming ICFP'08 paper for details on the type checking algorithm).
 That's exactly what #2146 is about.  (In any case, I will also add the
 example of the present ticket to the testsuite when I fix the bug.)

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2418#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs