Wot? with `PartialTypeSignatures`, `NamedWildCards` aka `ScopedTypeVariables` is evil

#1

(Adam might be surprised at this, but I won’t burden that discussion any further.) Consider:

{-#  LANGUAGE  PartialTypeSignatures, NamedWildCards, ExplicitForAll   #-}
               --  ScopedTypeVariables, 
               
module NamedWildCards where

    f2 :: [a] -> [a]                  -- forall a. 
    f2 xs = ys ++ ys          ::  _aa
        where ys              :: [_aa]
              ys = reverse xs ::  _aa

I was expecting GHC to reject this: NamedWildCard _aa used at inconsistent types (occurs check), but no. If I switch on ScopedTypeVariables, then it warns me – even without the ExplicitForAll on f2, or indeed without any signature at all for f2.

Is this behaviour what anybody out there expects?

But! But! I was using the NamedWildCard mechanism precisely to avoid the scope pollution from ScopedTypeVariables and yet annotate my types. (I can’t declare a fresh tyvar within the body of the where: rigid type variable rejections.)

The term-level names declared on RHS of the where scope also ‘backwards’ to its left – that is the RHS of f2's equation. That is the precise purpose of where. Then I expect tyvars to have the same scoping.

(Yes I know I’ll soon be able to accomplish this with TypeAbstractions. No that doesn’t persuade me one jot. The way I’d prefer to do this is with a tyvar annotation on f2's LHS where other names get bound: parameter xs – but needs bl…y ScopedTypeVariables, and/or ResultTypeSignatures – still in bl…y development pipeline.)

#2

I would expect that without ScopedTypeVariables (or a future extension), nothing (wildcards or quantified variables) bound inside a type annotation escapes that annotation.

You can even write

foo :: Int -> Bool -> Int
foo (a :: _a) (b :: _a) = a

and it’ll check because each annotation is a new scope, if you haven’t enabled something that defines a larger scope for type variables.

1 Like
#3

Thanks but Hah! [at 8.10 if that’s relevant]

   Illegal type signature: `_a'
     Type signatures are only allowed in patterns with ScopedTypeVariables

And if you enable the evil ScopedTypeVariables, it’ll then insist all those _as be at the same type.

I’m not seeing the benefit of that. Unless the annotation is no more than _, in effect asking GHC to tell you the inferred type. Using the same _a in two places would be asking GHC to make sure they’re unifiable/the same type (or reject if not)(?)

#4

Ah thanks, the snippet I offered started working in 9.2, it seems.

Per the documentation for NamedWildCards (emphasis mine),

It’s just what it’s spec’d to do. I’d think that if you dislike the action-at-a-distance of ScopedTypeVariables, you’d appreciate that wildcards also don’t leak into other signatures.

1 Like
#5

An annotation isn’t a signature, it’s a usage site/part of the declaration syntactic construct. The LHS of a function equation is a binding site. If foo (a :: _a) (b :: _a) = ... is binding a, it’s also binding _a. If a body of a where is declaring ys, and the LHS of where is using ys, then why when the body is declaring ys :: [_aa] can’t I use that _aa on the LHS?

#6

Ok, let me rationalise what I don’t like about ScopedTypeVariables (chiefly to explain it to myself). Yes it’s the leaking of scope.

Term variables are ‘dummy’ in the sense they’re merely position-holders. No leakage between the xs's (or ys's) here:

foo xs = ys ++ ys where ys = reverse xs

bar xs = ys ++ ys where ys = take (length xs `div` 2) xs

Not even leakage between equations for the same function/same varname doesn’t mean the same/is not even necessarily the same type:

baz [Maybe x] = ...
baz (x:xs)    = ...       -- I don't like this re-use of x at different types
baz  xs       = ...       -- but you do see it in the wild

At the type level, is there ‘conceptually’ leakage? Not to my mind, even with this ‘sharing’ syntax

foo, bar :: [a] -> [a]

(Does anybody write signatures that way any more?)

The explicit forall in signatures is partly stylistic variation/personal preference (I’m fine with that); partly to make explicit the type-level argument position. So these should be distinguishable at the type level:

quuxai :: forall a i. Integral i => [a] -> i -> [a]
quuxia :: forall i a. Integral i => [a] -> i -> [a]

quuxai xs n = genericTake n xs   -- } same equation although different type
quuxia xs n = genericTake n xs   -- }

Then the ‘proper’ way to use that distinction is with the (almost arrived) explicit binding TypeAbstractions, which must follow the order of the explicit forall's:

quuxai @a @i xs n = ...       -- i is Integral

Then I’m happy to take the Pattern Signatures as a ‘shorthand’ eliding the explicit forall/explicit binding – for coders who don’t want the bureaucracy/don’t care about ordering of type bindings:

quux (xs :: [a]) (n :: i) :: [a] = genericTake ...

Means “please, oh-so-clever compiler, figure out the explicit foralls and the type position-binding for me, because nothing relies on it.” And that works whether or not there’s a standalone signature for quux; and whether or not it uses explicit forall.

I can’t specify the Integral i => i on that LHS, but I think that’s a ‘fair cop’ if you’re writing shorthand. Although I could specify that on RHS, what I can’t do is introduce i out of the blue without a binding site on LHS:

        quux (xs :: [a]) n :: [a] = genericTake (n :: Integral i => i) xs
        --                              can't introduce i here ^^
#7

A mysterious emanation asks: What happens if you use a local forall?

quux (xs :: [a]) n :: [a] = genericTake (n :: forall i . Integral i => i) xs

===> You get (what I would expect) rigid type variable rejection (in GHC 8.10, equivalent rejection in Hugs).

The parallel to f2 perhaps easier to see in this form

    quux (xs :: [a]) n = genericTake ni xs
        where ni :: Integral i => i
              ni = n