Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,248
    • Issues 5,248
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 564
    • Merge requests 564
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #9633
Closed
Open
Issue created Sep 25, 2014 by Eric Crockett@crockeeaReporter

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:

  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 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.
Edited Mar 09, 2019 by Eric Crockett
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking