GHC 6.10.1 type puzzler
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]
main :: IO () main = do print $ test1 (make 1) 2
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
test2 :: Box a -> a -> [a] test2 box x = go x where -- go :: a -> [a] go y = [(val box), y]
Couldn't match expected type `a1' against inferred type `a'
You need to turn on {-# ScopedTypedVariables #-}. See http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extension... Your first example works without this extension, because the local definition 'go' is fully polymorphic. However, in the second example, the type variable 'a' in the signature of 'go' is not fully polymorphic - it must be exactly the _same_ 'a' as in the top-level signature. Regards, Malcolm
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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Dave Bayer
test1 :: Box a -> a -> [a] test1 box x = go box x where go :: Box a -> a -> [a] go b y = [(val b), y]
The type signature "go :: Box a -> a -> [a]" is equivalent to "go :: Box b -> b -> [b]" or "go :: forall a. Box a -> a -> [a]" or "go :: forall b. Box b -> b -> [b]" because the type variable "a" in the type signature for "test1" does not scope over the type signature for "go". Fortunately, "go" here does have that type.
test2 :: Box a -> a -> [a] test2 box x = go x where -- go :: a -> [a] go y = [(val box), y]
Here "go" does not have the type "forall a. a -> [a]"; it is not polymorphic enough. To write the signature for "go" inside "test2", you need lexically scoped type variables: http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extension... -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig 2008-11-20 Universal Children's Day http://unicef.org/ 1948-12-10 Universal Declaration of Human Rights http://everyhumanhasrights.org
Thanks all. Sorting this out for my actual code was a bit harder, but it worked. The manual sure wasn't kidding when it said "Read this section carefully!" Dave On Nov 19, 2008, at 12:12 PM, Malcolm Wallace wrote:
You need to turn on {-# ScopedTypedVariables #-}.
On Nov 19, 2008, at 12:15 PM, Daniil Elovkov wrote:
If you really want to specify the type for a local declaration, you'll have to turn on ScopedTypeVariables.
On Nov 19, 2008, at 12:29 PM, Chung-chieh Shan wrote:
To write the signature for "go" inside "test2", you need lexically scoped type variables: http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extension...
participants (4)
-
Chung-chieh Shan -
Daniil Elovkov -
Dave Bayer -
Malcolm Wallace