| 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? Yes I think it can, although you are right to point out that I said nothing about type inference. One minor thing is that you've misunderstood the proposal a bit. It ONLY springs into action when there's a dot. So you'd have to write bar1 x = x.foo bar2 x = x.foo OK so now it works rather like type functions. Suppose, the types with which foo was in scope were foo :: Int -> Int foo :: Bool -> Char Now imagine that we had a weird kind of type function type instance TDNR_foo Int = Int -> Int type instance TDNR_foo Bool = Bool -> Char Each 'foo' gives a type instance for TDNR_foo, mapping the type of the first argument to the type of that foo. So when we see (x.foo) we produce the following constraints TDNR_foo tx ~ tx -> tr where x:tx and the result type is tr. Then we can solve at our leisure. We can't make progress until we know 'tx', but when we do we can choose which foo is used. Of course, there'd be some modest built-in machinery rather than a forest of Now you rightly ask what if foo :: F Int -> Int Now under my "type function" analogy, we'd get type instance TDNR_foo (F Int) = F Int -> Int and now we may be in trouble because type functions can't have a type function call in an argument pattern. I hadn't thought of that. The obvious thing to do is to *refrain* from adding a "type instance" for such a 'foo'. But that would be a bit odd, because it would silently mean that some 'foo's (the ones whose first argument involved type functions) just didn't participate in TDNR at all. But we can hardly emit a warning message for every function with a type function in the first argument! I suppose that if you use x.foo, we could warn if any in-scope foo's have this property, saying "you might have meant one of these, but I can't even consider them". GADTs, on the other hand, are no problem. | 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. You mean x.foo and x.foo, right? Then yes, certainly. Of course that's already true of type classes: data T a where T1 :: Show a => T a T2 :: Sow a => T a bar :: a -> T a -> String bar x y = case y of T1 -> show x T2 -> show x Then I get different show's. Simon