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#l130... 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@cs.kuleuven.be] Sent: 05 February 2015 10:51 To: Simon Peyton Jones Cc: ghc-devs@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 #10045http://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/d108a19cf6cd802c30ff1fa2758dd6aa8c... * 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/28299d6827b334f5337bf5931124abc1e5... 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#l130... 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.

Oh gosh you are absolutely right. Ordinary, lexically scoped type variables only scope over the RHS of the relevant binding, not the body of the let. I was completely wrong about that. In which case my objection is much milder: - the inconsistency of treatment wrt ordinary type variables (which require a forall; and yes, you can't give a forall for wildcards) - the lack of documentation The system would be simpler without this. So, is it really important? If so, we could add it later. Sorry to make such a misleading post. Simon | -----Original Message----- | From: dominique.devriese@gmail.com [mailto:dominique.devriese@gmail.com] | On Behalf Of Dominique Devriese | Sent: 05 February 2015 20:13 | To: Simon Peyton Jones | Cc: Thomas Winant; ghc-devs@haskell.org; Frank Piessens | Subject: Re: Partial type sigs | | Simon, | | 2015-02-05 17:44 GMT+01:00 Simon Peyton Jones : | > 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’) | | Isn't this a different case than Thomas' example? As I understand it, | an equivalent of his example would have the wildcard in scope in the | body of f, not in the body of the let. Something like this: | | let f :: _a -> _a | f xs = reverse (xs :: _a) | in (f [True], f "x") | | or | | let f :: _a -> _a | f xs = let ys :: _a | ys = tail xs | in reverse ys | in (f [True], f "x") | | I agree with what you say about _a being in scope in the body of the | if, but I don't see a problem with _a being in scope in the body of f. | Do you? | | Note also that I haven't yet checked which of both is actually | implemented. | | Regards, | Dominique

| avoid breaking existing programs. We might as well make named | wildcards lexically scoped by default, not even opt-out (as was the | case in my initial proposal). I don't object strongly, so long as the user manual is very clear on the question, and mentions the inconsistency with ordinary type variables. | About using a Maybe for sig_id to fix 10045: I tried it out, and your | solution does indeed fix it. In order for TcSigInfo to still implement | NamedThing, I used an 'Either Name TcId' instead of a 'Maybe TcId'. Do | you prefer a separate data type for this instead of an Either? (Please | come up with a good name for it in that case :) Better: * Remove instance NamedThing TcSigInfo * Add a field sig_name :: Name, and use it instead of getName in tcTySigs Comment that if sig_id = Just f, then sig_name = idName f * Leave the sig_id field as (Maybe TcId). It needs a pretty big comment. Actually sig_poly_id would be a better name for the field. | Unfortunately, some of my tests started failing, so I'll post | something on Phabricator as soon as I have worked out the kinks. OK thank you. Ping me when ready Simon | | | Cheers, | Thomas | | | | > Sorry to make such a misleading post. | > | > Simon | > | > | -----Original Message----- | > | From: dominique.devriese@gmail.com | > [mailto:dominique.devriese@gmail.com] | > | On Behalf Of Dominique Devriese | > | Sent: 05 February 2015 20:13 | > | To: Simon Peyton Jones | > | Cc: Thomas Winant; ghc-devs@haskell.org; Frank Piessens | > | Subject: Re: Partial type sigs | > | | > | Simon, | > | | > | 2015-02-05 17:44 GMT+01:00 Simon Peyton Jones | > : | > | > 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’) | > | | > | Isn't this a different case than Thomas' example? As I understand | > | it, an equivalent of his example would have the wildcard in scope | in | > | the body of f, not in the body of the let. Something like this: | > | | > | let f :: _a -> _a | > | f xs = reverse (xs :: _a) | > | in (f [True], f "x") | > | | > | or | > | | > | let f :: _a -> _a | > | f xs = let ys :: _a | > | ys = tail xs | > | in reverse ys | > | in (f [True], f "x") | > | | > | I agree with what you say about _a being in scope in the body of | the | > | if, but I don't see a problem with _a being in scope in the body | of | > f. | > | Do you? | > | | > | Note also that I haven't yet checked which of both is actually | > | implemented. | > | | > | Regards, | > | Dominique | | Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm