Opened 5 years ago

Last modified 5 years ago

#10114 new bug

Kind mismatches with AnyK in rank-2 types

Reported by: cam Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.4
Keywords: Cc: sweirich@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The following module:

{-# LANGUAGE Rank2Types #-}
module KindBug where

type T = forall f a. f a

foo :: T
foo = undefined

bar :: forall f a. f a
bar = foo

...produces the following error:

[1 of 1] Compiling KindBug          ( KindBug.hs, KindBug.o )

KindBug.hs:10:7:
    Kind incompatibility when matching types:
      f0 :: AnyK -> *
      f :: * -> *
    Expected type: f a
      Actual type: f0 a0
    Relevant bindings include bar :: f a (bound at KindBug.hs:10:1)
    In the expression: foo
    In an equation for ‘bar’: bar = foo

Note that no extensions are enabled other than rank-2 types.

Enabling and using kind annotations fixes the error, as does replacing the type synonym with its definition in the type signature of foo.

Similar errors can also be generated with PolyKinds enabled and less plausible code, e.g. (return undefined :: forall f a. f a) :: f a . The non-PolyKinds example is simplified from some actual code, where the type synonym was similar to the ones used in lens, and is the simplest example I could find (with help from Shachaf on IRC) that resembled real code.

I searched for existing tickets and the closest I could find are #7916 and #5935, both of which are already fixed.

Also, according to glguy (Eric Mertens) just now in #haskell-lens, the same error occurs in the 7.10 branch and in 7.11.20150120.

Change History (10)

comment:1 Changed 5 years ago by simonpj

Some notes for myself (work in progress). Consider first the non-poly-kinded case. At the moment, for type T above we get

-- Without PolyKinds
type T = forall (f :: AnyK -> *) (a :: AnyK). f a
bar :: forall (f :: * -> *) (a :: *). f a

Remark: note that defaulting is done inconsistently! And this is stupid.

Defaulting to * is the the most useful thing (and is explicitly specified in Haskell 98). C.f.

data D f a = MkD (f a)  -- Here we want D :: (*->*) -> * -> *

(and in fact we do). It would be stupid to get D :: (AnyK -> *) -> AnyK -> * because then D would be unusable.

Conclusion: in the non-poly-kinded case, the inner foralls of T should default to *:

type T = forall (f :: * -> *) (a :: *). f a

Now the poly-kinded case. Currently we get

-- With PolyKinds
type T k = forall (f :: AnyK -> k) (a :: AnyK). f a-- Without PolyKinds

But maybe we want:

-- With PolyKinds
type T k1 k2 = forall (f :: k1 -> k2) (a :: k1). f a

But note the strange kind of T in PolyKinds case: T :: forall k1 k2. k2.

I'm pretty sure we do NOT want to kind-generalise "inside", thus:

type T = forall k1 k2 (f :: k1->k2) (a::k1). f a

Reasons:

  • see Note [Kind generalisation] in TcHsType
  • what kind would T have? T :: k2 ???
  • more operationally, kind foralls must be implicitly instantiated, during kind inference using only T's kind. (Subsequently recognised as bogus: see comment:5.)
Last edited 5 years ago by simonpj (previous) (diff)

comment:2 Changed 5 years ago by goldfire

What about

type T k2 = forall k1 (f :: k1 -> k2) (a :: k1). f a

That makes T :: forall k2. k2. That's a well-formed kind, but it looks awfully like the type of undefined... but I don't know if that's a problem.

comment:3 Changed 5 years ago by simonpj

Re comment:2, I don't think so: how does k1 get instantiated when you have occurrences of T?

comment:4 Changed 5 years ago by goldfire

I'm not sure I understand comment:3. What are you worried about?

I will also say that it's possible the right answer is

type T = forall k1. (f :: k1 -> *) (a :: k1). f a

so that T :: *. My understanding is that it's generally more common to restrict the body of a forall to have kind *. GHC doesn't do this, but all the papers about System FC do.

In other work, I changed the typing rule for forall accordingly, and something broke horribly (eta-reducing newtypes, maybe?), but perhaps we don't have to infer a type that has a non-* kind as the body of a forall.

comment:5 Changed 5 years ago by simonpj

In comment:3 I think I was confusing these two things:

  T = forall k. blah
  T :: forall k. blah   -- Uses of T must be applied to a kind 

So I think I retract my claim in comment:1. Perhaps we do want to generalise "inside".

Can anyone say why it is "generally more common to restrict the body of a forall to have kind *"? I can't articulate a clear argument.

In GHC's case, a good reason not to do this was types like forall a. a -> (# a, a #), but levity polymorpism will help here.

Simon

comment:6 in reply to:  5 Changed 5 years ago by goldfire

Cc: sweirich@… added

Replying to simonpj:

So I think I retract my claim in comment:1. Perhaps we do want to generalise "inside".

I agree with your (now retracted) claim.

If T = forall k1 k2 (f :: k1 -> k2) (a :: k1). f a, then I think T's type would have to be k2, which is nonsense. As I understand it, the kind of a forall-type is the kind of the body of the forall-type.

Can anyone say why it is "generally more common to restrict the body of a forall to have kind *"? I can't articulate a clear argument.

This claim of mine is direct from Stephanie. Stephanie, do you know why this is?

In GHC's case, a good reason not to do this was types like forall a. a -> (# a, a #), but levity polymorpism will help here.

I don't think that's quite what you want to say, because the kind of the body of that forall is *! Maybe forall a. (# a, a #)?

I don't see how levity polymorphism fixes this problem. Even with levity polymorphism, the kind of the body of that last forall is still #.

comment:7 Changed 5 years ago by simonpj

It's amazing how easily I can be confused by this stuff!

To the question of why restricting foralls to have result of kind *, maybe I can attempt to answer my own question, thus: in what context could you could use such a type? Obviously not in a type signature, since that must have kind *. Where else? Would it make sense to say T (forall a. Either a)? But if T expected an arg of kind * -> *, does it make sense to instantiate it with (forall a. Either a)? Does the type (forall a. Either a) Int make sense? Maybe not.

Also if the body of a forall must have kind *, it avoids the awkward question of what is the kind of forall k. forall (a:k). a

Re unboxed tuples, maybe you are right. Perhaps it only matters in very special cases like forall a. (# a, a #) which may not be very important.

In short, maybe we should explore

  • forall always has kind *
  • Kind-generalise the RHS of type synonyms, so we get the kind in comment:4
Last edited 5 years ago by simonpj (previous) (diff)

comment:8 Changed 5 years ago by goldfire

When someone (possibly me, but not before April) explores this, a good way forward is to just change CoreLint around this issue and then to recompile GHC, the libraries, and the test suite, all with -dcore-lint enabled. I'm 99% sure that the usage of forall with a non-* body will show up.

comment:9 Changed 5 years ago by simonpj

NB the rule for kind generalisation in 7.8.2 of the user manual.

f1 :: (forall a.      Proxy a) -> Int    -- Means  f :: forall k. (forall (a:k). Proxy k a) -> Int
f2 :: (forall (a::k). Proxy a) -> Int    -- Means  f :: (forall k. forall (a:k). Proxy k a) -> Int

(Richard's new branch, which collapses types and kinds, allows explicit kind quantification, so we can then control this more explicitly.)

The forall k on the RHS of the type synonym, is in effect rank-N kinds.

So maybe the same should be true for T:

type T = forall f a. f a       -- Means type T k = forall (f::k->*) (a::k). f a
type T = forall f (a::k). f a  -- Means type T = forall k (f::k->*) (a::k). f a
Last edited 5 years ago by simonpj (previous) (diff)

comment:10 Changed 5 years ago by simonpj

Current BUG (HEAD, 7.10)

type T = forall (f :: k -> k2) (a::k). f a

Compile with -fprint-explicit-kinds -ddump-types -XRankNTypes -XPolyKinds

TYPE CONSTRUCTORS
  type T (k2 :: BOX) =
    forall (k :: BOX) (k1 :: BOX) (f :: k -> k1) (a :: k). f a

But this elaborated T simply doesn't have a sensible kind.

Note: See TracTickets for help on using tickets.