PolyKinds in 7.8.2 vs 7.8.3
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:
- Remove
-XPolyKinds
from Bar.hs - Add an explicit kind signature to the
v :: * -> * -> *
parameter of typeBar
- With
PolyKinds
in Bar but *not* Foo, uncommentingreturn a
make GHC 7.8.3. compile
What I'm trying to understand is
- 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 . - 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 aPolyKinds
issue (i.e.kind mismatch
) - For the third resolution option above, I can't see any reason that adding
return a
to the innergo
function should make the code compile while leaving it out makes the code somehow ambiguous. This, if nothing else, seems like a bug.