Partial type sigs

[Thomas Winant]

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 
> <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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20150205/b5237181/attachment.html>