GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:39:44Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/9633PolyKinds in 7.8.2 vs 7.8.32019-07-07T18:39:44ZEric CrockettPolyKinds in 7.8.2 vs 7.8.3The 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,
Monad 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
1. Add an explicit kind signature to the `v :: * -> * -> *` parameter of type `Bar`
1. 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 [release notes vs 7.8.2](http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/release-7-8-3.html) .
1. 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`)
1. 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.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,
Monad 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
1. Add an explicit kind signature to the `v :: * -> * -> *` parameter of type `Bar`
1. 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 [release notes vs 7.8.2](http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/release-7-8-3.html) .
1. 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`)
1. 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.7.10.1