[GHC] #8707: Kind inference fails in data instance definition

[GHC]

#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