[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 goldfire):

 Jan asked me a few months ago for a "simple" bug to fix in the type-
 checker, and I recommended this one, thinking it to be much simpler than
 it is -- that's why I haven't tackled it myself.

 He and I just spent a some time going through the details, and we hit upon
 a much simpler solution than what you proposed.

 Right now, `tcConRes` looks like this:

 {{{
 tcConRes (ResTyGADT res_ty) = do { res_ty' <- tcHsLiftedType res_ty
                                  ; return (ResTyGADT res_ty') }
 }}}

 I propose changing it to:

 {{{
 tcConRes (ResTyGADT res_ty) = do { res_ty' <- tcHsLiftedType res_ty
                                  ; _ <- unifyType type_in_head res_ty'
                                  ; return (ResTyGADT res_ty') }
 }}}

 where `type_in_head` is the desugared type that appears in the declaration
 (either normal datatype or data instance) head. Getting that data here
 will take some plumbing, but it shouldn't be too bad. We also will need to
 freshen any type variables (with `tcInstTyVars` for the type from the
 declaration head and `tcInstSkolTyVars` for the return type, I imagine) to
 get everything to work.

 This approach seems to solve the case in point, and it would also fix the
 complications in `Note [Checking GADT return types]`. I do see some
 potential trouble with getting error messages to be right, but I still
 think this is a better approach than repeating much of `tc_hs_type`.

 Thoughts?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8707#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler