[GHC] #9633: PolyKinds in 7.8.2 vs 7.8.3
GHC
ghc-devs at haskell.org
Fri Sep 26 00:13:28 UTC 2014
#9633: PolyKinds in 7.8.2 vs 7.8.3
-------------------------------------+-------------------------------------
Reporter: crockeea | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.3
Resolution: | Keywords: PolyKinds
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: GHC | Blocked By:
rejects valid program | Related Tickets:
Test Case: |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Description changed by crockeea:
Old description:
> The following code '''compiles''' with GHC 7.8.2.
>
>
> This code has been distilled down from a larger example where I needed
> `-XPolyKinds` in Bar.hs but not in Foo.hs. In addition, the `modify`
> function is supposed to modify a mutable `Data.Vector`, hence the inner
> `go` function has the intended type of `Int -> m ()`, though strictly
> speaking it could return any value since everything is discarded by the
> `forM_`.
>
> {{{
> -- {-# LANGUAGE PolyKinds #-}
>
> module Foo where
>
> import Control.Monad (forM_)
> import Bar
>
> -- Vector signatures
> unsafeRead :: (PrimMonad m) => v (PrimState m) a -> Int -> m a
> unsafeRead = error "type only"
> unsafeWrite :: (PrimMonad m) => v (PrimState m) a -> Int -> a -> m ()
> unsafeWrite = error "type only"
>
> modify :: Int -> Bar v r
> modify p = Bar (p-1) $ \y -> do
> let go i = do
> a <- unsafeRead y i
> unsafeWrite y i a
> --return a
> forM_ [0..(p-1)] go
> }}}
>
> {{{
> {-# LANGUAGE RankNTypes, KindSignatures, TypeFamilies, PolyKinds #-}
> module Bar where
>
> class Monad m => PrimMonad (m :: * -> *) where
> type family PrimState (m :: * -> *) :: *
>
> data Bar v r = Bar Int (forall s . (PrimMonad s) => v (PrimState s) r ->
> s ())
> }}}
>
> In 7.8.3, this above code results in the error (with `-fprint-explicit-
> kinds`)
>
> {{{
> Foo.hs:19:23:
> Couldn't match type ‘a0’ with ‘r’
> ‘a0’ is untouchable
> inside the constraints (PrimMonad m,
> (~) * (PrimState m) (PrimState s))
> bound by the inferred type of
> go :: (PrimMonad m, (~) * (PrimState m) (PrimState s))
> =>
> Int -> m ()
> at Foo.hs:(18,7)-(20,23)
> ‘r’ is a rigid type variable bound by
> the type signature for modify :: Int -> Bar * v r at
> Foo.hs:16:11
> Expected type: v0 (PrimState m) a0
> Actual type: v (PrimState s) r
> ...
> In the first argument of ‘unsafeRead’, namely ‘y’
> In a stmt of a 'do' block: a <- unsafeRead y i
>
> Foo.hs:20:19:
> Couldn't match type ‘v1’ with ‘v’
> ‘v1’ is untouchable
> inside the constraints (PrimMonad m,
> (~) * (PrimState m) (PrimState s))
> bound by the inferred type of
> go :: (PrimMonad m, (~) * (PrimState m) (PrimState s))
> =>
> Int -> m ()
> at Foo.hs:(18,7)-(20,23)
> ‘v’ is a rigid type variable bound by
> the type signature for modify :: Int -> Bar * v r at
> Foo.hs:16:11
> Expected type: v1 (PrimState m) a0
> Actual type: v (PrimState s) r
> ...
> In the first argument of ‘unsafeWrite’, namely ‘y’
> ...
> Failed, modules loaded: Bar.
> }}}
>
> After much digging, I found that enabling `-XPolyKinds` in Foo.hs gives a
> more meaningful error:
>
> {{{
> Foo.hs:19:23:
> Could not deduce ((~) (* -> k -> *) v v0)
> ...
> Expected type: v0 (PrimState m) a0
> Actual type: v (PrimState s) r
> ...
> In the first argument of ‘unsafeRead’, namely ‘y’
> In a stmt of a 'do' block: a <- unsafeRead y i
>
> Foo.hs:20:19:
> Could not deduce ((~) (* -> k -> *) v v1)
> ...
> Expected type: v1 (PrimState m) a0
> Actual type: v (PrimState s) r
> ...
> In the first argument of ‘unsafeWrite’, namely ‘y’
> In a stmt of a 'do' block: unsafeWrite y i a
> Failed, modules loaded: Bar.
> }}}
>
> Adding `PolyKinds` to Foo.hs ''and'' uncommenting `return a` results in
> the error:
>
> {{{
> Foo.hs:17:12:
> Couldn't match kind ‘k’ with ‘k1’
> because type variable ‘k1’ would escape its scope
> This (rigid, skolem) type variable is bound by
> the type signature for modify :: Int -> Bar k1 v r
> at Foo.hs:16:11-24
> Expected type: Bar k1 v r
> Actual type: Bar k v0 r0
> ...
> In the expression:
> Bar (p - 1)
> $ \ y
> -> do { let ...;
> forM_ [0 .. (p - 1)] go }
> ...
>
> Foo.hs:18:7:
> Kind incompatibility when matching types:
> v0 :: * -> k -> *
> v1 :: * -> * -> *
> ...
> When checking that ‘go’
> has the inferred type ‘forall (k :: BOX)
> (m :: * -> *)
> b
> (v :: * -> * -> *)
> (v1 :: * -> * -> *).
> ((~) (* -> k -> *) v0 v, (~) k r0 b, (~) (*
> -> k -> *) v0 v1,
> PrimMonad m, (~) * (PrimState m) (PrimState
> s)) =>
> Int -> m b’
> Probable cause: the inferred type is ambiguous
> In the expression:
> do { let go i = ...;
> forM_ [0 .. (p - 1)] go }
> ...
> Failed, modules loaded: Bar.
>
> }}}
>
> These errors can be resolved by modifying the original code above in any
> of the following ways:
>
> 1. Remove `-XPolyKinds` from Bar.hs
> 2. Add an explicit kind signature to the `v :: * -> * -> *` parameter of
> type `Bar`
> 3. With `PolyKinds` in Bar but *not* Foo, uncommenting `return a` make
> GHC 7.8.3. compile
>
> What I'm trying to understand is
> 1. Why there is different behavior from 7.8.2 to 7.8.3. There doesn't
> seem to be anything addressing `PolyKinds` in the
> [http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/release-7-8-3.html
> release notes vs 7.8.2] .
> 2. In the event the above code should not compile with 7.8.3, there
> error message could be much clearer. The first error message above didn't
> help me understand that `PolyKinds` was to blame, while the second error
> did a better job, and the third was very clearly a `PolyKinds` issue
> (i.e. `kind mismatch`)
> 3. For the third resolution option above, I can't see any reason that
> adding `return a` to the inner `go` function should make the code compile
> while leaving it out makes the code somehow ambiguous. This, if nothing
> else, seems like a bug.
New description:
The following code '''compiles''' with GHC 7.8.2.
This code has been distilled down from a larger example where I needed
`-XPolyKinds` in Bar.hs but not in Foo.hs. In addition, the `modify`
function is supposed to modify a mutable `Data.Vector`, hence the inner
`go` function has the intended type of `Int -> m ()`, though strictly
speaking it could return any value since everything is discarded by the
`forM_`.
{{{
-- {-# LANGUAGE PolyKinds #-}
module Foo where
import Control.Monad (forM_)
import Bar
-- Vector signatures
unsafeRead :: (Monad m) => v (PrimState m) a -> Int -> m a
unsafeRead = error "type only"
unsafeWrite :: (Monad m) => v (PrimState m) a -> Int -> a -> m ()
unsafeWrite = error "type only"
modify :: Int -> Bar v r
modify p = Bar (p-1) $ \y -> do
let go i = do
a <- unsafeRead y i
unsafeWrite y i a
--return a
forM_ [0..(p-1)] go
}}}
{{{
{-# LANGUAGE RankNTypes, KindSignatures, TypeFamilies, PolyKinds #-}
module Bar where
type family PrimState (m :: * -> *) :: *
data Bar v r = Bar Int (forall s . (Monad s) => v (PrimState s) r -> s ())
}}}
In 7.8.3, this above code results in the error (with `-fprint-explicit-
kinds`)
{{{
Foo.hs:19:23:
Couldn't match type ‘a0’ with ‘r’
‘a0’ is untouchable
inside the constraints (Monad m,
(~) * (PrimState m) (PrimState s))
bound by the inferred type of
go :: (Monad m, (~) * (PrimState m) (PrimState s)) =>
Int -> m ()
at Foo.hs:(18,7)-(20,23)
‘r’ is a rigid type variable bound by
the type signature for modify :: Int -> Bar * v r at
Foo.hs:16:11
Expected type: v0 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeRead’, namely ‘y’
In a stmt of a 'do' block: a <- unsafeRead y i
Foo.hs:20:19:
Couldn't match type ‘v1’ with ‘v’
‘v1’ is untouchable
inside the constraints (Monad m,
(~) * (PrimState m) (PrimState s))
bound by the inferred type of
go :: (Monad m, (~) * (PrimState m) (PrimState s)) =>
Int -> m ()
at Foo.hs:(18,7)-(20,23)
‘v’ is a rigid type variable bound by
the type signature for modify :: Int -> Bar * v r at
Foo.hs:16:11
Expected type: v1 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeWrite’, namely ‘y’
...
Failed, modules loaded: Bar.
}}}
After much digging, I found that enabling `-XPolyKinds` in Foo.hs gives a
more meaningful error:
{{{
Foo.hs:19:23:
Could not deduce ((~) (* -> k -> *) v v0)
...
Expected type: v0 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeRead’, namely ‘y’
In a stmt of a 'do' block: a <- unsafeRead y i
Foo.hs:20:19:
Could not deduce ((~) (* -> k -> *) v v1)
...
Expected type: v1 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeWrite’, namely ‘y’
In a stmt of a 'do' block: unsafeWrite y i a
Failed, modules loaded: Bar.
}}}
Adding `PolyKinds` to Foo.hs ''and'' uncommenting `return a` results in
the error:
{{{
Foo.hs:17:12:
Couldn't match kind ‘k’ with ‘k1’
because type variable ‘k1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for modify :: Int -> Bar k1 v r
at Foo.hs:16:11-24
Expected type: Bar k1 v r
Actual type: Bar k v0 r0
...
In the expression:
Bar (p - 1)
$ \ y
-> do { let ...;
forM_ [0 .. (p - 1)] go }
...
Foo.hs:18:7:
Kind incompatibility when matching types:
v0 :: * -> k -> *
v1 :: * -> * -> *
...
When checking that ‘go’
has the inferred type ‘forall (k :: BOX)
(m :: * -> *)
b
(v :: * -> * -> *)
(v1 :: * -> * -> *).
((~) (* -> k -> *) v0 v, (~) k r0 b, (~) (*
-> k -> *) v0 v1,
PrimMonad m, (~) * (PrimState m) (PrimState
s)) =>
Int -> m b’
Probable cause: the inferred type is ambiguous
In the expression:
do { let go i = ...;
forM_ [0 .. (p - 1)] go }
...
Failed, modules loaded: Bar.
}}}
These errors can be resolved by modifying the original code above in any
of the following ways:
1. Remove `-XPolyKinds` from Bar.hs
2. Add an explicit kind signature to the `v :: * -> * -> *` parameter of
type `Bar`
3. With `PolyKinds` in Bar but *not* Foo, uncommenting `return a` make
GHC 7.8.3. compile
What I'm trying to understand is
1. Why there is different behavior from 7.8.2 to 7.8.3. There doesn't
seem to be anything addressing `PolyKinds` in the
[http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/release-7-8-3.html
release notes vs 7.8.2] .
2. In the event the above code should not compile with 7.8.3, there error
message could be much clearer. The first error message above didn't help
me understand that `PolyKinds` was to blame, while the second error did a
better job, and the third was very clearly a `PolyKinds` issue (i.e. `kind
mismatch`)
3. For the third resolution option above, I can't see any reason that
adding `return a` to the inner `go` function should make the code compile
while leaving it out makes the code somehow ambiguous. This, if nothing
else, seems like a bug.
--
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9633#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list