[ ghc-Bugs-1248208 ] Result type signatures and lexically scoped type variables

Bugs item #1248208, was opened at 2005-07-30 20:03
Message generated for change (Tracker Item Submitted) made by Item Submitter
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=108032&aid=1248208&group_id=8032

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: Compiler (Type checker)
Group: None
Status: Open
Resolution: None
Priority: 5
Submitted By: Nobody/Anonymous (nobody)
Assigned to: Nobody/Anonymous (nobody)
Summary: Result type signatures and lexically scoped type variables

Initial Comment:
Dear ghc developers,

The ghc documentation (7.4.10.) states that
  "A lexically scoped type variable can be bound by: 
  [...] A result type signature"

However, actually trying to use them causes some
unexpected behavior:

import Data.Typeable

foo :: Typeable b => b
foo :: a = typeOf (undefined :: a) `seq` (undefined :: a)

bar :: forall b. Typeable b => b
bar :: a = typeOf (undefined :: a) `seq` (undefined :: a)
         
baz :: forall a. Typeable a => a
baz :: a = typeOf (undefined :: a) `seq` (undefined :: a)

All three examples give rise to basically the same
error message, namely

    Inferred type is less polymorphic than expected
      Quantified type variable `b' is mentioned in the
environment:
        Scoped type variable `a' = b (bound at:
test135.hs:4:7)
    When trying to generalise the type inferred for `foo'
      Signature type:     forall b. (Typeable b) => b
      Type to generalise: b
    In the type signature for `foo'
    When generalising the type(s) for `foo'

If I understand the documentation correctly, they
should all compile. An especially interesting case is
'baz', where the 'a' from the result type annotation
seems to shadow the a from the type signature (that
doesn't happen with pattern type annotations).

Another curiosity happens if we alpha-rename foo:

qux :: Typeable a => a
qux :: a = typeOf (undefined :: a) `seq` (undefined :: a)

The error message becomes

    All of the type variables in the constraint
`Typeable a' are already in scope
        (at least one must be universally quantified here)
    In the type signature: qux :: (Typeable a) => a

This is just my wild speculation, but does this really
mean that the 'a' in qux's signature is bound by "qux
:: a"?

ghc6.2 gives the same error messages, where of course
'bar' behaves like 'foo' and 'baz' like 'qux'.

Thanks you,

-- Thomas Jäger

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=108032&aid=1248208&group_id=8032