[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
       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:
-------------------------------------+-------------------------------------
 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 Control.Monad.Primitive

 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, PolyKinds #-}
 module Bar where

 import Control.Monad.Primitive

 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9633
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler