Scoped type variables

[Marcin 'Qrczak' Kowalczyk]

Tue, 8 May 2001 00:47:58 -0700, Simon Peyton-Jones <simonpj@microsoft.com> pisze:

> 	g = \x::(Int,Bool) -> let-type (a,b) = (Int,Bool) in e
> 
> But notice that the RHS of a pattern-matching let-type is statically
> guaranteed to have the right shape.  So I don't allow
> 
> 	let-type (a,b) = c in ...
> 
> (where c is  a type variable).

Really? I disagree. Making pattern type sygnatures perform unification
of the variable with the supplied signature is useful for resolving
ambiguities, and backward-compatible (valid programs will remain
valid), and doesn't allow "unwanted generality" to cause trouble
(when an expression has a more general type than needed).

Currently ghc does not accept:
    (\(x::a) -> x) :: Int->Int
but accepts this:
    (let f = \(x::a) -> x in f) :: Int->Int

Hugs accepts both! But it doesn't like
    (\(x::a) -> (x::Int))

I would make all three legal.


Unfortunately it doesn't help for my example:

f:: (IArray a e, Ix i) => a i e -> a i e
f arr = runST (do
    (marr :: STArray s i e) <- thaw arr
    do some stateful operations on marr
    freeze marr)

unless the type inference could deduce that the constraint
    MArray (STArray s') e (ST s)
in the presence of instance
    MArray (STArray s) e (ST s)
unifies s' with s.

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^                      SYGNATURA ZASTĘPCZA
QRCZAK