Opened 4 years ago
Last modified 4 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:2 Changed 4 years ago by
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 4 years ago by
Re comment:2, I don't think so: how does k1
get instantiated when you have occurrences of T
?
comment:4 Changed 4 years ago by
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 follow-up: 6 Changed 4 years ago by
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 Changed 4 years ago by
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 4 years ago by
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
comment:8 Changed 4 years ago by
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 4 years ago by
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
comment:10 Changed 4 years ago by
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.
Some notes for myself (work in progress). Consider first the non-poly-kinded case. At the moment, for type
T
above we getRemark: 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.(and in fact we do). It would be stupid to get
D :: (AnyK -> *) -> AnyK -> *
because thenD
would be unusable.Conclusion: in the non-poly-kinded case, the inner foralls of
T
should default to*
:Now the poly-kinded case. Currently we get
But maybe we want:
But note the strange kind of
T
inPolyKinds
case:T :: forall k1 k2. k2
.I'm pretty sure we do NOT want to kind-generalise "inside", thus:
Reasons:
Note [Kind generalisation]
inTcHsType
T
have?T :: k2
???T
's kind. (Subsequently recognised as bogus: see comment:5.)