Proposal: Partial Type Signatures - Status update

[Dominique Devriese]

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 <eir at cis.upenn.edu>:
> 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