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

[GHC]

#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