Errors involving rigid skolem types
The following code is intended as a first step towards creating a cyclical enumerable type, such that: (e.g.) [Cyc Friday .. Cyc Tuesday] would yield [Friday, Saturday, Sunday, Monday, Tuesday] module Cycle where newtype Cyc a = Cyc a deriving (Eq, Ord, Bounded, Show, Read) fromCyc :: Cyc a -> a fromCyc (Cyc a) = a instance (Enum a, Bounded a) => Enum (Cyc a) where fromEnum = fromEnum . fromCyc toEnum n = Cyc x where (x, max) = (x', maxBound) :: (a, a) x' = toEnum $ n `mod` ((fromEnum max) - 1) This yields a kind of error message that I've often bashed my head against in other code I've written, without ever really understanding what the problem is exactly: Couldn't match type `a0' with `a1' because type variable `a1' would escape its scope This (rigid, skolem) type variable is bound by an expression type signature: (a1, a1) The following variables have types that mention a0 x' :: a0 (bound at Cycle.hs:12:15) In the expression: (x', maxBound) :: (a, a) In a pattern binding: (x, max) = (x', maxBound) :: (a, a) In an equation for `toEnum': toEnum n = Cyc x where (x, max) = (x', maxBound) :: (a, a) x' = toEnum $ n `mod` ((fromEnum max) - 1) The problem comes up when I'm trying to give hints to the compiler about the type that a particular expression should have. My questions are: (1) what exactly is going on here, and (2) is there any general technique for specifying types in situations like this that gets around this problem?
A couple of clarifications regarding my previous post:
It should be ((fromEnum max) + 1) rather than ((fromEnum max) - 1); and
Perhaps question (2) should be: are there any lessons to be learnt about
how to avoid this problem in future?
On Mon, Aug 27, 2012 at 11:21 PM, Matthew Moppett
The following code is intended as a first step towards creating a cyclical enumerable type, such that: (e.g.) [Cyc Friday .. Cyc Tuesday] would yield [Friday, Saturday, Sunday, Monday, Tuesday]
module Cycle where
newtype Cyc a = Cyc a deriving (Eq, Ord, Bounded, Show, Read)
fromCyc :: Cyc a -> a fromCyc (Cyc a) = a
instance (Enum a, Bounded a) => Enum (Cyc a) where fromEnum = fromEnum . fromCyc toEnum n = Cyc x where (x, max) = (x', maxBound) :: (a, a) x' = toEnum $ n `mod` ((fromEnum max) - 1)
This yields a kind of error message that I've often bashed my head against in other code I've written, without ever really understanding what the problem is exactly:
Couldn't match type `a0' with `a1' because type variable `a1' would escape its scope This (rigid, skolem) type variable is bound by an expression type signature: (a1, a1) The following variables have types that mention a0 x' :: a0 (bound at Cycle.hs:12:15) In the expression: (x', maxBound) :: (a, a) In a pattern binding: (x, max) = (x', maxBound) :: (a, a) In an equation for `toEnum': toEnum n = Cyc x where (x, max) = (x', maxBound) :: (a, a) x' = toEnum $ n `mod` ((fromEnum max) - 1)
The problem comes up when I'm trying to give hints to the compiler about the type that a particular expression should have.
My questions are: (1) what exactly is going on here, and (2) is there any general technique for specifying types in situations like this that gets around this problem?
On Mon, Aug 27, 2012 at 11:21:55PM +1000, Matthew Moppett wrote:
This yields a kind of error message that I've often bashed my head against in other code I've written, without ever really understanding what the problem is exactly:
Couldn't match type `a0' with `a1' because type variable `a1' would escape its scope This (rigid, skolem) type variable is bound by an expression type signature: (a1, a1) The following variables have types that mention a0 x' :: a0 (bound at Cycle.hs:12:15) In the expression: (x', maxBound) :: (a, a) In a pattern binding: (x, max) = (x', maxBound) :: (a, a) In an equation for `toEnum': toEnum n = Cyc x where (x, max) = (x', maxBound) :: (a, a) x' = toEnum $ n `mod` ((fromEnum max) - 1)
The problem comes up when I'm trying to give hints to the compiler about the type that a particular expression should have.
My questions are: (1) what exactly is going on here, and (2) is there any general technique for specifying types in situations like this that gets around this problem?
What is going on here is that the occurrences of 'a' in (x', maxBound) :: (a,a) are not the same as the occurrences of 'a' in the instance head. You might as well have written (x', maxBound) :: (b,b) or :: (foo,foo). The idea is that by default, any type with type variables is generalized to a forall type, so what you really have is (x', maxBound) :: forall a. (a,a) which makes it easier to see why those a's have nothing to do with those in the instance head. You don't want x' and maxBound to have *any* type, you want them to have whatever *particular* type corresponds to the chosen instance. The solution is to use an extension called ScopedTypeVariables which lets you connect type variables across different signatures in exactly this way. In this case, simply turning on the extension by putting {-# LANGUAGE ScopedTypeVariables #-} at the top of your file is enough to get the program to compile. Now the 'a's in your local type annotation really do refer back to the 'a' in the instance head. In general, if you want to have a local type variable refer to a top-level type signature (as opposed to an instance head) you also have to put an explicit 'forall' on the variables you want to be scoped in this way, like {-# LANGUAGE ScopedTypeVariables #-} foo :: forall a. a -> a -> a foo = ... where bar = ... :: a -> Int note the 'forall a' in the top-level signature for foo. -Brent
participants (2)
-
Brent Yorgey -
Matthew Moppett