Richard,
Since Thomas is attending a summer school for the moment, I'll
try to provide a response and Thomas can correct me later if needed...
2014-06-19 17:57 GMT+02:00 Richard Eisenberg
Vigorous debate on #9200 (https://ghc.haskell.org/trac/ghc/ticket/9200) has led me to think about polymorphic recursion in the presence of a partial type signature. For example, take the following silly but well-typed function:
foo :: (a -> Bool) -> a -> () foo _ _ = foo not True
GHC reasonably requires the type signature here, because the recursive call to foo is called with *different* type parameters than the original call -- this is exactly polymorphic recursion. But, what about this?
bar :: _ -> a -> () bar _ _ = bar not True
I see several possible outcomes of type-checking bar: 1) Failure. Categorically disallow polymorphic recursion in the presence of a partial type signature. 2) bar :: (Bool -> Bool) -> a -> () 3) bar :: (a -> Bool) -> a -> () 4) bar :: (a -> a ) -> a -> () 5) bar :: (Bool -> a ) -> a -> ()
None of (2-5) is more general than another. So, I advocate for (1), which is essentially what we have decided to do at the kind level. The other approach is to say that wildcards refine to types that never mention user-written type variables. This would select (2) as the correct type. But, it is generally useful to allow wildcards to unify with user-written type variables! We could, I suppose, notice that polymorphic recursion is happening and then impose the restriction, but that seems very unpredictable to a user.
What do you think? Have you pondered this particular corner case?
Interesting question. In general, we definitely unify wildcards with user-written type variables. This is implied by a guiding design principle that we have used: a function with a trivial partial signature ":: _ => _" should be treated the same as one with no signature at all. We even share most of the code that does inference for definitions with partial type signatures with the code for definitions with no signature. Note: this sharing is something Thomas has worked on recently, after discussion with SPJ. As for your concrete example, I have tried it on our current branch and here's an overview of what we get for the function definition "bar _ _ = bar not True", depending on the provided signature: signature result inferred type/error no signature works (Bool -> Bool) -> Bool -> t _ -> _ -> () works (Bool -> Bool) -> Bool -> () _ works (Bool -> Bool) -> Bool -> t _ -> a -> () doesn't work Couldn't match type ‘a’ with ‘Bool’ (a -> _) -> a -> () doesn't work Couldn't match type ‘a’ with ‘Bool’ So in general, if there is a partial type signature, the compiler tries to infer a type under the assumption that there is no polymorphic recursion, similar to what it does when there is no signature. Regards, Dominique