Confusing Typing Problem

Simon Peyton-Jones simonpj at microsoft.com
Fri Nov 18 08:41:04 EST 2005

```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-----
| bounces at haskell.org] On Behalf Of Bernd Brassel
| Sent: 18 November 2005 10:16
| 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:
|
| 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:
|
| 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
|
| > 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
| _______________________________________________