Simon, have you given any thought to how this interacts with type system extensions, in particular with GADTs and type families? The proposal relies on being able to "find the type" of a term but it's not entirely clear to me what that means. Here is an example: foo :: F Int -> Int foo :: Int -> Int bar1 :: Int -> Int bar1 = foo bar2 :: Int ~ F Int => Int -> Int bar2 = foo IIUC, bar1 is ok but bar2 isn't. Do we realy want to have such a strong dependency between name lookup and type inference? Can name lookup be specified properly without also having to specify the entire inference algorithm? Another example: suppose we have data T a where TInt :: T Int TBool :: T Bool foo :: T Int -> u foo :: T Bool -> u bar :: T a -> u bar x = case x of TInt -> foo x TBool -> foo x Here, (foo x) calls different functions in the two alternatives, right? To be honest, that's not something I'd like to see in Haskell. Roman