#6049: Kind variable generalization error in GADTs
----------------------------------------+-----------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.5
Keywords: PolyKinds | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid
program
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
----------------------------------------+-----------------------------------
Changes (by simonpj):
* cc: dimitris@…, dreixel, sweirich@… (added)
* difficulty: => Unknown
Comment:
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?
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6049#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
