Partial type sigs

[Simon Peyton Jones]

Named wildcards follow the scoping behaviour of ScopedTypeVariables but
without the forall. See the following example:


{-# LANGUAGE PartialTypeSignatures, NamedWildCards #-}
{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}
module Scope where

f :: _a -> _b -> _a
f x y = x :: _b
I really don't like this behaviour!

1.      It is entirely undocumented, in the manual or the wiki page, I think.

2.      it is inconsistent with the lexical scoping rules for ordinary scoped type variables.

3.      It interferes with generalisation.
For (3), consider

     let f :: _a -> _a

         f xs = reverse xs

     in (f True, f 'x')
Here, f gets the type f :: forall b. [b] -> [b], and _a is unifed with [b].
So it simply doesn't make sense for _a to appear in the body.  What would it mean to say

     let f :: _a -> _a

         f xs = reverse xs

     in (f (True :: _a), f 'x')
Does this mean we *shouldn't* generalise as we usually would?  I think of a partial signature as perhaps constraining the shape of the type a bit, but not affecting generalisation.  It would be hard to predict exactly how it was supposed to affect generalisation.... e.g. .what if _a in the above example did not, after all, appear in the body of the let?
I urge (strongly) that we back off from this and say that named wildcards scope only over the type signature in which they appear.
OK?   The implementation gets simpler too.   RSVP.

What you say makes sense, but don't we already do something with the
same effect (see link)? We only add monomorphic Ids of non-partial type
signatures. Or am I missing something?
http://git.haskell.org/ghc.git/blob/HEAD:/compiler/typecheck/TcBinds.hs#l1306

That's true, but we also (wrongly) bring the polymorphic Id into scope (TcBinds line 313).  We should only do that for full (not partial) type sigs.
But my point is that the sig_id field never makes sense of sig_partial is true. (Correct?) So we should rule it out structurally (via the Maybe) rather than rely on an unstated invariant.
Simon


From: Thomas Winant [mailto:thomas.winant at cs.kuleuven.be]
Sent: 05 February 2015 10:51
To: Simon Peyton Jones
Cc: ghc-devs at haskell.org; Dominique Devriese; Frank Piessens
Subject: Re: Partial type sigs


On 02/04/2015 09:24 PM, Simon Peyton Jones wrote:
Thomas
I was looking at Trac #10045<http://ghc.haskell.org/trac/ghc/ticket/10045>.   I know exactly what is going on, but my investigation triggered several questions.
I'll have a look too, but first my answers to your questions:




1.      What is the state of the ToDos on https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures?
I've updated the TODOs on the wiki page, but I'll summarise the changes:

* I've updated the user manual.
* I have fixed a TODO in the code, see:
  http://ghc.haskell.org/trac/ghc/changeset/d108a19cf6cd802c30ff1fa2758dd6aa8c049ad0/ghc
* You fixed the panic for TODO 1 (see link below), but we still don't
  get the error messages we (or I would) want when we change the type of
  the local binding to `_`.

  http://ghc.haskell.org/trac/ghc/changeset/28299d6827b334f5337bf5931124abc1e534f33f/ghc





2.      Is a named wildcard supposed to have any scope?  For example:

f :: _a -> b -> _a

f x y = x :: _a
The _a in the signature is not supposed to have any lexical scope over the binding is it?  That would be entirely inconsistent with the treatment of ordinary type variables (such as 'b' in the example) which only scope if you have an explicit 'forall b'.
Assuming the answer is "no" (and I really think it should be no), what is the call to tcExtendTyVarEnv2 tvsAndNcs doing in TcBinds.tcRhs?  I'm pretty certain it bring into scope only the sig_tvs, and NOT the sig_nwcs.

3.      If that is true, I think we may not need the sig_nwcs field of TcSigInfo at all.
Named wildcards follow the scoping behaviour of ScopedTypeVariables but
without the forall. See the following example:


{-# LANGUAGE PartialTypeSignatures, NamedWildCards #-}
{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}
module Scope where

f :: _a -> _b -> _a
f x y = x :: _b
-- Note that this is not your example


$ ghc -ddump-types
> TYPE SIGNATURES
>   f :: forall w_a w_b. w_a -> w_b -> w_a
> ...

$ ghc -ddump-types -XScopedTypeVariables
> TYPE SIGNATURES
>   f :: forall w_a. w_a -> w_a -> w_a
> ..

With scoped named wildcards, the second _b (with type _a) must be the
same as the first _b and thus _b ~ _a, hence no w_b.

That's why there is a call to tcExpandTyVarEnv2 in TcBinds.tcRhs and why
we need the sig_nwcs field of TcSigInfo.




4.      A TcSigInfo has a sig_id field, which is intended to give the fixed, fully-known polymorphic type of the function.  This is used:

*        for polymorphic recursion

*        as the type of the function to use in the body of the let, even if typechecking the function itself fails.
Neither of these makes sense for partial type sigs.  (And in fact, using sig_id for a partial type sig is what gives rise to #10045.)  So I'm pretty convinced that we should replace sig_id and sig_partial with a single field sig_id :: Maybe Id, which is Nothing for partial sigs, and (Just ty) for total sigs.

What you say makes sense, but don't we already do something with the
same effect (see link)? We only add monomorphic Ids of non-partial type
signatures. Or am I missing something?
http://git.haskell.org/ghc.git/blob/HEAD:/compiler/typecheck/TcBinds.hs#l1306



I wanted to check with you before blundering in and doing this.  Or you could.
RSVP
Thanks
Simon


Cheers,
Thomas

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm for more information.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20150205/71af812b/attachment-0001.html>