RE: infered type does not typecheck

Duncan

Oleg's recent message to Haskell-Café tackles your real problem, but I thought 
I'd just say what is going on with your apparent bug below.  Here's a much 
simpler example:

        class Foo a b where
           to :: a -> b
           fro :: b -> a

        -- foo :: forall b1 b a. (Foo a b, Foo a b1) => b -> b1
        foo x = to (fro x) 

Without the type signature, the program typechecks "fine", and GHCi reports the 
type in the comment.  But if you uncomment the type signature, typechecking 
fails.  Why?

It's because the type is really ambiguous.  'fro' converts from b to a, and 
'to' converts back... but the 'a' is entirely lost in the process.  It's very 
like the classic (show (read x)) example.  So the type
        foo :: forall b1 b a. (Foo a b, Foo a b1) => b -> b1

is really unusable, because there is nothing to constrain 'a'.  When you add 
the type signature, GHC can't establish the connection between the 'a' needed 
as the intermediate type in the (to (fro x)) composition and the 'a' in the 
type signature.

You might argue that GHC should reject foo in the first place, and you'd be 
right, really.  But it's hard in general to reject exactly and only the 
ambiguous cases (given functional dependencies and all that jazz), and I have 
not worked hard on that.

But I grant that it's rather counter-intuitive that adding a type signature 
that GHC itself deduces goes wrong!  You're right to count it a bug.

Simon

| This was posted to the Haskell list earlier,
| http://www.haskell.org//pipermail/haskell/2004-June/014286.html
| but just to record what appears to be a typechecker bug.
| 
| I have a function with this type:
| buildUArray' :: (Ix i, MArray (array s) a (ST s)) =>
|               (i,i) -> (i -> a) -> ST s (array s i a)
| 
| Then I ask ghci (6.2.1 and 6.3 recent cvs) the type of the following
| function:
| 
| buildUArray bounds f = do arr <- buildUArray' bounds f
|                           unsafeFreeze arr
| 
| ghci says:
| buildUArray :: forall a i b s array.
|              (MArray (array s) a (ST s), Ix i, IArray b a) =>
|              (i, i) -> (i -> a) -> ST s (b i a)
| 
| However if I add this annotation back in the script, ghc complains:
| 
| Could not deduce (MArray (array1 s) a (ST s))
|       from the context (MArray (array s) a (ST s), Ix i, IArray b a)
|       arising from use of `unsafeFreeze' at BuildArray.hs:25
|     Probable fix:
|       Add (MArray (array1 s) a (ST s))
|       to the type signature(s) for `buildUArray'
|       Or add an instance declaration for (MArray (array1 s) a (ST s))
|     In the result of a 'do' expression: unsafeFreeze arr
|     In the definition of `buildUArray':
|       buildUArray bounds f
|                     = do
|                         arr <- buildUArray' bounds f
|                         unsafeFreeze arr