Kind inference fails in data instance definition
Consider the following shenanigans:
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs #-}
data family SingDF (a :: (k, k2 -> *))
data Ctor :: k -> *
data instance SingDF (a :: (Bool, Bool -> *)) where
SFalse :: SingDF '(False, Ctor)
HEAD reports (with -fprint-explicit-kinds
)
Data constructor ‛SFalse’ returns type ‛SingDF
Bool k '('False, Ctor k)’
instead of an instance of its parent type ‛SingDF Bool Bool a’
In the definition of data constructor ‛SFalse’
In the data instance declaration for ‛SingDF’
I see two problems here:
-
Kind inference should fix the problem. If I add a kind annotation to
Ctor
, the code works. GHC should be able to infer this kind annotation for me. -
The error message is not particularly helpful. GHC 7.6.3 had a more verbose, but more helpful message.
Trac metadata
Trac field | Value |
---|---|
Version | 7.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |