GHC 6.10.1 type puzzler

[Daniil Elovkov]

Dave Bayer wrote:
> Here is an example illustrating a type problem I've having with GHC 6.10.1:
> 
>> module Main where
>>
>> newtype Box a = B a
>>
>> make :: a -> Box a
>> make x = B x
>>
>> val :: Box a -> a
>> val (B x) = x
>>
>> test1 :: Box a -> a -> [a]
>> test1 box x = go box x
>>  where
>>    go :: Box a -> a -> [a]
>>    go b y = [(val b), y]
>>
>> test2 :: Box a -> a -> [a]
>> test2 box x = go x
>>  where
>> --  go :: a -> [a]
>>    go y = [(val box), y]

If you really want to specify the type for a local declaration, you'll have to turn on ScopedTypeVariables. Otherwise 'a' is test2 type signature and 'a' in go type signature mean different unrelated things.

In test2 box remains with the first 'a', while go is with the second. There is need for unification. In the case of test1 go has all the variables.

In other words, you get

test1 :: forall p. Box p -> p -> [p]
  go :: forall q. Box q -> q -> [q]

and you perfectly can call go with test1 arguments.

On the other hand,
test2 :: forall p. Box p -> p -> [p]
  go :: forall q. q -> [q]

and obviously there's a problem.

Do this

{-# LANGUAGE ScopedTypeVariables, PatternSignatures #-}

test2 :: Box a -> a -> [a]
test2 box (x::a) = go x    -- here you say, that x :: a
  where
    go :: a -> [a]         -- here you mention the same a
    go y = [(val box), y]


PatternSignatures appears to be needed for pattern x::a

> 
> If I uncomment the commented type declaration, I get the familiar error
> 
>> Couldn't match expected type `a1' against inferred type `a'
> 
> On the other hand, the earlier code is identical except that it passes 
> an extra argument, and GHC matches the types without complaint.
> 
> This is a toy example to isolate the issue; in the actual code one wants 
> a machine-checkable type declaration to help understand the function, 
> which is local to save passing an argument. To the best of my 
> understanding, I've given the correct type, but GHC won't make the 
> inference to unify the type variables.
> 
> I wonder if I found a GHC blind spot. However, it is far more likely 
> that my understanding is faulty here. Any thoughts?
> 
> Thanks,
> Dave
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users