#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------ Reporter: goldfire | Owner: jstolarek Type: feature request | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * priority: normal => low * type: bug => feature request Comment: I've thought about this some more. My conclusion: we should do nothing. * Whatever we do will make things more complicated * Arguably what is happening now is right anyway For the second point, consider {{{ data family T a data instance T [a] where MkT :: b -> T b }}} We rightly reject this because `(T b)` is not an instance of `T [a]`. We do not say "oh, that b must be [c]", using information from the header. No, we treat the type signature for `MkT` as a perfectly ordinary type signature, and check that it has the right shape. Similarly when you write {{{ data instance SingDF (a :: (Bool, Bool -> *)) where SFalse :: SingDF '(False, Ctor) }}} the type signature for `SFalse` is perfectly ordinary type signature, and means what it means. We then check that it is an instance of the header, and it isn't. It's less obvious, because the kinds are hidden, but it's the same thing really. Moreover, if/when we have kind equalities, the kind arguments in the result type may be an instance of (not equal to) the kind arguments of the header. I can see a way to hack it up (along the lines I suggested) but it feels like a hack. Perhaps convenient in certain cases, but imagine trying to write the typing rules that says exactly which programs are accepted and which are rejected! I don't think the `kcConDecl` thing will work. Look at `TcHsType.tcTyVar` and the local definition `get_loopy_tc`; plus `Note [Type checking recursive type and class declarations]` in `TcTyClsDecls` which describes how a `TyCon` can have a definition in both the local and global environments. It's not a bug; it's a feature request, and one that I'm dubious about. On reflection I think we probably have better uses for our cycles. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler