Opened 3 years ago
Closed 3 years ago
#6049 closed bug (fixed)
Kind variable generalization error in GADTs
Reported by: | goldfire | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.5 |
Keywords: | PolyKinds | Cc: | dimitris@…, dreixel, sweirich@… |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | polykinds/T6049 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
The following code fails to compile with 7.5.20120426:
{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, GADTs, ExistentialQuantification #-} data SMaybe :: (k -> *) -> Maybe k -> * where SNothing :: forall (s :: k -> *). SMaybe s Nothing SJust :: forall (s :: k -> *) (a :: k). s a -> SMaybe s (Just a)
The reported error is
Kind mis-match The first argument of `SMaybe' should have kind `k1 -> *', but `s' has kind `k -> *' In the type `SMaybe s (Just a)' In the definition of data constructor `SJust' In the data declaration for `SMaybe'
The code compiles fine without the explicit forall annotations, but other, more involved code I'm working on (involving Proxy) requires the annotations, so simply omitting the explicit kind annotations is not always a viable workaround.
Change History (6)
comment:1 Changed 3 years ago by simonpj
- Cc dimitris@… dreixel sweirich@… added
- difficulty set to Unknown
comment:2 Changed 3 years ago by goldfire
Actually, I think you've over-generalized the problem. As I see it, the kinds for SMaybe in both constructors are the same (modulo kind variables --- but maybe that's the issue). In any case, the error still comes up when I omit the SJust constructor. Fortunately, in both this case and in my original, larger case, the problem goes away when I avoid GADT syntax, so this isn't holding me up any longer.
As for your description above, I don't fully understand why the treatment of the two syntax forms have to be different. In the original SMaybe case, I propose this: Read SMaybe's kind from the user-supplied signature, and then infer SMaybe's kind from the constructor definitions. Notice that all three kinds are the same, modulo names of kind variables, so we unify the variables and are done. Is there some detail I'm missing here? Does kind variable unification in that way not exist yet? I recognize that the case above is very simple, in that the kinds to be compared are all structurally identical and that the general case may require matching one kind variable against some structural component, possibly containing other variables, in another kind. However, my intuition is that this manner of unification must already exist somewhere. Am I wrong?
comment:3 Changed 3 years ago by simonpj
I was wrong in detail but I think right in principle. Consider
data Maybe a where Nothing :: Maybe a
The two a's have nothing to do with each other. We could equally well write
data Maybe a where Nothing :: Maybe b or data Maybe a where Nothing :: forall b. Maybe b or data Maybe :: * -> * where Nothing :: Maybe a
Now consider your exmaple:
data SMaybe :: (k -> *) -> Maybe k -> * where SNothing :: forall (s :: k -> *). SMaybe s Nothing
The k in the SNothing is nothing to do with the k in the header, just like the Maybe case above. So we could also write
data SMaybe :: (k -> *) -> Maybe k -> * where SNothing :: forall (s :: kk -> *). SMaybe s Nothing or data SMaybe :: (k -> *) -> Maybe k -> * where SNothing :: forall kk. forall (s :: kk -> *). SMaybe s Nothing
Actually we can't write the latter because we don't yet support explicit kind foralls, but morally we could.
When kind-checking SMaybe, if we initially give it the monomorphic kind
SMaybe :: (kappa -> *) -> Maybe kappa -> *
where kappa is a kind unification variable, then if we kind-check the type of SNothing we'll have a problem because SMaybe is insufficiently polymorphic to kind-check the type
forall kk. forall (s::kk -> *). SMaybe s Nothing
We could hack our way round this, perhpas by (in effect) not kind-genrealising the type of SNothing. But it seems smelly. I'd be interested in what Stephanie and Dimitrios think.
comment:4 Changed 3 years ago by simonpj
Actually I think it's harder than I thought to "hack around". Suppose we had
data SMaybe :: (k -> *) -> Maybe k -> * where SNothing :: Int -> (forall kk. forall (ss :: kk -> *). SMaybe ss Nothing) -> SMaybe s a
I have used a nested forall, so now really impossible (without lots of hackery) to make this work with a kind-monomorphic SMaybe.
This can't really happen unless we have explicit kind-foralls, but sooner or later we will.
I think the simplest path is to say that for GADT-style syntax you must give the kind of the type constructor in the header; and if you don't you'll get * -> * -> *, ie not even higher kinds. This would mean that some existing programs would need a kind signature.
data T a b where MkT :: a b -> T a b
would need signatures, thus
data T (a : * -> *) b where MkT :: a b -> T a b or data T :: (* -> *) -> * -> * where MkT :: a b -> T a b or data T :: (k -> *) -> k -> * where MkT :: a b -> T a b
But it would enforce good practice (put those kind signatures in! And I suppose that this new behaviour could be enabled by -XPolyKinds.
comment:5 Changed 3 years ago by simonpj@…
commit c91172004f2a5a6bf201b418c32c2d640ee34049
Author: Simon Peyton Jones <[email protected]> Date: Thu Jun 7 12:09:22 2012 +0100 Support polymorphic kind recursion This is (I hope) the last major patch for kind polymorphism. The big new feature is polymorphic kind recursion when you supply a complete kind signature for a type constructor. (I've documented it in the user manual too.) This fixes Trac #6137, #6093, #6049. The patch also makes type/data families less polymorphic by default. data family T a now defaults to T :: * -> * If you want T :: forall k. k -> *, use data family T (a :: k) This defaulting to * is done whenever there is a "complete, user-specified kind signature", something that is carefully defined in the user manual. Hurrah! compiler/typecheck/TcBinds.lhs | 3 +- compiler/typecheck/TcClassDcl.lhs | 49 -------- compiler/typecheck/TcHsType.lhs | 50 ++++++-- compiler/typecheck/TcInstDcls.lhs | 106 +++++------------ compiler/typecheck/TcRnDriver.lhs | 66 ++++++++--- compiler/typecheck/TcRnTypes.lhs | 31 ++---- compiler/typecheck/TcSplice.lhs | 3 +- compiler/typecheck/TcTyClsDecls.lhs | 204 ++++++++++++++++++------------- docs/users_guide/flags.xml | 5 +- docs/users_guide/glasgow_exts.xml | 228 ++++++++++++++++++++++------------- 10 files changed, 400 insertions(+), 345 deletions(-)
comment:6 Changed 3 years ago by simonpj
- Resolution set to fixed
- Status changed from new to closed
- Test Case set to polykinds/T6049
Interesting. The issue turns out to be this. Consider
Then we expect to infer the kind T :: (* -> *) -> * for T. How did we do this? We gave T a kind unification variable, and kind-checked the MkT signature. All good.
Just like for polymorphic functions, we can infer polymorphic kinds too:
We give T a kind unification variable, kind-check, and generalise, to get
BUT if T is used at different kinds in its definition, as in the return types of SMaybe and SNothing above, then we are hosed. This is really polymorphic recursion.
The solution for polymorphic recursion is to give a type signature -- and you have done just that for SMaybe. So when there is a kind signature we want to ignore the data constructor definitions, and instead take the kind signature as giving the kind of the tycon.
Annoyingly at the moment GHC allows a mixed economy. You can say
so there is "half a kind signature", as it were. I don't think anyone uses this though.
Alternatively, and I think I like this more, we could say that for kind inference we look at the constructors only in H98-style definitions. So, consider
For S1 we look at the constructor. For for S2, we look only at the data S2 a b where..., and ignore the constructors. So we infer these kinds:
Then when we later type-check the constructors for S2 we'll get a kind error.
I like this because it is simple: if you use GADT syntax, and you want a higher kind, you must give a signature. Does that seem OK?