Confusing Typing Problem
Simon PeytonJones
simonpj at microsoft.com
Fri Nov 18 08:41:04 EST 2005
Tricky!
It certainly is confusing, but that's the way HindleyMilner type
inference for mutually recursive functions works.
The localdefn 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 throwaway 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: glasgowhaskellusersbounces at haskell.org
[mailto:glasgowhaskellusers
 bounces at haskell.org] On Behalf Of Bernd Brassel
 Sent: 18 November 2005 10:16
 To: glasgowhaskellusers at haskell.org
 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 toplevel, 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 throwaway 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
 _______________________________________________
 Glasgowhaskellusers mailing list
 Glasgowhaskellusers at haskell.org
 http://www.haskell.org/mailman/listinfo/glasgowhask
More information about the Glasgowhaskellusers
mailing list