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: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Bernd Brassel | Sent: 18 November 2005 10:16 | To: glasgow-haskell-users@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 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 | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-hask