Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#6159 closed bug (invalid)

unexpected GADT kind error

Reported by: kosmikus Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.5
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

I am surprised that the following two declarations are treated differently in HEAD (7.5.20120607):

{-# LANGUAGE GADTs, KindSignatures #-}

-- ok
data X f ix where
  X :: f ix -> X f ix

-- not ok
data Y f :: * -> * where
  Y :: f ix -> Y f ix

The second version causes an error:

/home/andres/trans/BugTest.hs:7:18:
    Expecting one more argument to `f'
    In the type `Y f ix'
    In the definition of data constructor `Y'
    In the data declaration for `Y'

I'd expect both to work.

Change History (3)

comment:1 Changed 3 years ago by simonpj

  • difficulty set to Unknown
  • Resolution set to invalid
  • Status changed from new to closed

This is by (current) design. It's even documented: see Polymorphic kind recursion and complete kind signatures

Simon

comment:2 Changed 3 years ago by kosmikus

Thanks for the quick reply.

The documentation makes it clear, but it isn't the place I'd have looked at. I'm not using kind polymorphism, nor am I using recursion.

The documentation also says: "you get kind * -- if you want to get polymorphism, use an explicit annotation". But I don't want polymorphism. I want the type checker to infer "* -> *" for f.

So all in all, the current system seems more restrictive than the value-level inference, as I don't get even monomorphic types inferred anymore.

comment:3 Changed 3 years ago by simonpj

Ah yes, that's a good point. The difficult is this. For polymorphic recursion we need to know when you have supplied a complete kind signature for a type contructor. When (and only when) you supply a complete kind signature, you can use polymorphic recursion.

At the value level this is obvious enough: you have supplied a type signature for f if you write f :: blah. But at the kind level it's not so obvious. In your definition for Y you have supplied part, but not all, of a kind signature.

Currently I've said that you have supplied "a complete kind signature" when you give a "::" in the definition. That is,

  • with "::" the kind is declared;
  • without "::" it is inferred.

That certainly is a change but it seems one that is easy to explain. I'd welcome suggestions for what changes I should make elsewhere in the user manual; where did you look when you were seeking information?

Note: See TracTickets for help on using tickets.