Opened 2 years ago

Closed 23 months 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 Difficulty: Unknown
Test Case: polykinds/T6049 Blocked By:
Blocking: Related Tickets:

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 2 years ago by simonpj

  • Cc dimitris@… dreixel sweirich@… added
  • Difficulty set to Unknown

Interesting. The issue turns out to be this. Consider

data T a where
   MkT :: forall b. (b Int) -> T b

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:

data T a b where
   MkT :: forall a b. a b -> T a b

We give T a kind unification variable, kind-check, and generalise, to get

T :: forall k. (k->*) -> k -> *

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

data T a :: * -> * where ...

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

data S1 a = MkS1 (a b)

data S2 a b where
   MkS2 :: forall a b. a b -> S a b

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:

S1 :: forall k. (k->*) -> k -> *
S2 :: * -> * -> *

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?

comment:2 Changed 2 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 2 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 2 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 23 months ago by simonpj@…

commit c91172004f2a5a6bf201b418c32c2d640ee34049

Author: Simon Peyton Jones <simonpj@microsoft.com>
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 23 months ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to polykinds/T6049
Note: See TracTickets for help on using tickets.