#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------ Reporter: goldfire | Owner: jstolarek Type: bug | Status: new Priority: normal | 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: -------------------------------------+------------------------------------ Comment (by simonpj): Richard, re (1), here's my analysis * For ordinary GADTs we first figure out the kind of the type constructor, and only then typecheck the constructor types. So this works fine: {{{ data SingDF (a :: (Bool, Bool -> *)) where SFalse :: SingDF '(False, Ctor) }}} We figure out the kind `SingDF :: (Bool, Bool -> *) -> *`, and only then typecheck the type of `SFalse`. So the use of `SingDF` in the type of the data constructor is fine. * But for a data family, the kind of the type constructor is polymorphic, in this case `SingDF :: forall k1,k1. (k1, k2 -> *) -> *`. When we use this kind in type-checking the type of `SFalse` we don't get any info from the `data instance` header. * And indeed if `SingDF` was used in a constructor ''argument'' we would want the polymorphic version: {{{ data instance SingDF (a :: (Bool, Bool) -> *) where SFalse :: SingDF (...blah...) -> SingDF '(False, Ctor) }}} Here the `(...blah...)` need not have kind `(Bool,Bool) -> *`. * So if we are to use the `data instance` header to inform the kind of the quantified type variables in the data constructor(s), we must treat the result type specially (`TcTyClsDecls.tcConRes`). * Currently we simply use `tcHsLiftedType`. I think to do the Right Thing we would need a special version of `TcHsType.tc_lhs_type`, expecially for data constructor result types. And this might be a Good Thing. Although it would mean a little code duplication, it might eliminate much of the delicacy in `Note [Checking GADT return types]` This is a bit of code you know quite well. Happy to discuss. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler