Confusing Typing Problem

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

Confusing Typing Problem

Bernd Brassel
I am a bit confused by GHC behaviour for the following variants of a
program:

data A = A (Int -> A)

f = A g

g _ = f

h = g 'c'

ghc:
 > Error:
 > Couldn't match `Int' against `Char'

The problem is that a small change ommits the error:
data A = A (Int -> A)

f = A g
   where
   g _ = f

   h = g 'c'

ghc:
 > Ok, modules loaded

But I really need the functions to be top-level, thus I added type
signatures:
data A = A (Int -> A)

f :: A
f = A g

g :: a -> A
g _ = f

h :: A
h = g 'c'

ghc:
 > Ok, modules loaded

Fine, but what I really need, is this:

data A = A (Int -> A)

f :: A
f = A g

g :: Ord a => a -> A
g _ = f

h :: A
h = g 'c'

 > Contexts differ in length
 > The signature contexts in a mutually recursive group should all be
 > identical
 > ...
 > Couldn't match `Int' against `Char'

Again the problem does not occur for local functions:

data A = A (Int -> A)

f :: A
f = A g
   where
     g :: Ord a => a -> A
     g _ = f

     h :: A
     h = g 'c'

Why is ghc treating local and global functions differently? Is there
really a difference in decidability of the Polymorphic Type Inference?
And regarding the "contexts differ in length", I read a comment in
"Typing Haskell in Haskell":

> a throw-away comment specifying that all explicit type signatures
 > in a binding group must have the same context up to renaming of
variables
 > [10,Section 4.5.2]. This is a syntactic restriction that can easily
 > be checked prior to type checking. Our comments here, however, suggest
 > that it is unnecessarily restrictive.

Why does ghc still use that unnecessary restriction?

Cheers
Bernd
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

RE: Confusing Typing Problem

Simon Peyton Jones
Tricky!  

It certainly is confusing, but that's the way Hindley-Milner type
inference for mutually recursive functions works.

The local-defn version works differently because it
        - assumes a monomorphic type for f
        - completely typechecks g, including generalisation
        - finishes typechecking f

That could be done if one typechecked the original defns in the "right"
order, but it's not clear what the right order is.   You specified the
order by choosing which defn to nest. The other way round won't work
        g _ = f where f = A g

Specifying a type sig should fix the problem, and does.

| > a throw-away comment specifying that all explicit type signatures
|  > in a binding group must have the same context up to renaming of
| variables
|  > [10,Section 4.5.2]. This is a syntactic restriction that can easily
|  > be checked prior to type checking. Our comments here, however,
suggest
|  > that it is unnecessarily restrictive.
|
| Why does ghc still use that unnecessary restriction?

It doesn't any more.  The HEAD lifts the restriction; that'll be in GHC
6.6.  Meanwhile you could try a snapshot build from the download site.

Simon


| -----Original Message-----
| From: [hidden email]
[mailto:glasgow-haskell-users-
| [hidden email]] On Behalf Of Bernd Brassel
| Sent: 18 November 2005 10:16
| To: [hidden email]
| Subject: Confusing Typing Problem
|
| I am a bit confused by GHC behaviour for the following variants of a
| program:
|
| data A = A (Int -> A)
|
| f = A g
|
| g _ = f
|
| h = g 'c'
|
| ghc:
|  > Error:
|  > Couldn't match `Int' against `Char'
|
| The problem is that a small change ommits the error:
| data A = A (Int -> A)
|
| f = A g
|    where
|    g _ = f
|
|    h = g 'c'
|
| ghc:
|  > Ok, modules loaded
|
| But I really need the functions to be top-level, thus I added type
| signatures:
| data A = A (Int -> A)
|
| f :: A
| f = A g
|
| g :: a -> A
| g _ = f
|
| h :: A
| h = g 'c'
|
| ghc:
|  > Ok, modules loaded
|
| Fine, but what I really need, is this:
|
| data A = A (Int -> A)
|
| f :: A
| f = A g
|
| g :: Ord a => a -> A
| g _ = f
|
| h :: A
| h = g 'c'
|
|  > Contexts differ in length
|  > The signature contexts in a mutually recursive group should all be
|  > identical
|  > ...
|  > Couldn't match `Int' against `Char'
|
| Again the problem does not occur for local functions:
|
| data A = A (Int -> A)
|
| f :: A
| f = A g
|    where
|      g :: Ord a => a -> A
|      g _ = f
|
|      h :: A
|      h = g 'c'
|
| Why is ghc treating local and global functions differently? Is there
| really a difference in decidability of the Polymorphic Type Inference?
| And regarding the "contexts differ in length", I read a comment in
| "Typing Haskell in Haskell":
|
| > a throw-away comment specifying that all explicit type signatures
|  > in a binding group must have the same context up to renaming of
| variables
|  > [10,Section 4.5.2]. This is a syntactic restriction that can easily
|  > be checked prior to type checking. Our comments here, however,
suggest
|  > that it is unnecessarily restrictive.
|
| Why does ghc still use that unnecessary restriction?
|
| Cheers
| Bernd
| _______________________________________________
| Glasgow-haskell-users mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/glasgow-hask
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users