Re: [GHC] #9633: PolyKinds in 7.8.2 vs 7.8.3

25 Sep 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