Result type signatures and lexically scoped type variables
|Reported by:||nobody||Owned by:||nobody|
|Component:||Compiler (Type checker)||Version:||None|
|Type of failure:||Difficulty:|
|Test Case:||Blocked By:|
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
Note: See TracTickets for help on using tickets.