[GHC] #15245: Data family promotion is possible

[GHC]

#15245: Data family promotion is possible
-------------------------------------+-------------------------------------
           Reporter:  int-index      |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Documentation  |           Version:  8.4.3
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The User's Guide states that data families cannot be promoted, even with
 `-XTypeInType`:

 > We promote data types and newtypes; type synonyms and type/data families
 are not promoted.
 >
 > The flag TypeInType (which implies DataKinds) relaxes some of these
 restrictions, allowing:
 >
 >    Promotion of type synonyms and type families, but not data families.
 GHC’s type theory just isn’t up to the task of promoting data families,
 which requires full dependent types.

 And yet the following code typechecks and runs:

 {{{#!hs
 {-# LANGUAGE TypeFamilies, TypeInType, TypeApplications #-}

 import Type.Reflection

 data family K
 data instance K = MkK

 main = print (typeRep @'MkK)
 }}}

 Is this a GHC bug or a documentation bug? I asked in IRC but I'm still
 confused:

 {{{
 <int-index> The user guide states that data families aren't promoted even
 when -XTypeInType is enabled. Where's the logic that ensures this? I
 checked with `data family K; data instance K = MkK` and I can use `'MkK`
 with no errors/warnings.
 <int-index>
 https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview
 "Promotion of type synonyms and type families, but not data families.
 GHC’s type theory just isn’t up to the task of promoting data families,
 which requires full dependent types."
 <int-index> Is this info outdated?
 <RyanGlScott> int-index: Is this in GHCi?
 <RyanGlScott> It certainly fails in GHC
 <RyanGlScott> But I think I understand why the former works
 <int-index> RyanGlScott, yes, I'm checking this in GHCi
 <RyanGlScott> int-index: So here's my understanding of how this works
 <RyanGlScott> GHC kind-checks top-level declarations using a rather
 primitive SCC analysis
 <RyanGlScott> In particular, it's primitive in the sense that data family
 instances give it a lot of trouble
 <RyanGlScott> If you tried taking your code and putting it into a
 standalone .hs file and compiling that, then it would definitely complain
 about a promoted use of MkT
 <RyanGlScott> As luck would have it, though, you were trying things out in
 GHCi
 <RyanGlScott> Which essentially checks each line of input as its own
 strongly connected group of declarations
 <RyanGlScott> So you can define MkT on one line and promote it in
 subsequent lines, since they're separate in the sense
 <RyanGlScott> *that sense
 <int-index> this sounds related to Trac #12088, and then I could work
 around it in GHC by using `$(return [])`, so data families are actually
 promoted anyway and this has nothing to do with GHC needing more powerful
 type theory
 <RyanGlScott> Well, it does need more powerful type theory in the sense
 that that's a prerequisite for making the SCC analysis for kind-checking
 sophisticated enough to handle this
 <RyanGlScott> But yes, it's quite simple to work around by using Template
 Haskell to explicitly split up groups.
 <int-index> https://gist.github.com/int-
 index/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell
 involved
 <int-index> The reason I'm asking is that I'm touching this part of the
 User's Guide and I don't know what to write there.
 <RyanGlScott> Huh, now that's interesting
 <int-index> RyanGlScott, the only check I could find that controls what's
 promoted and what's not is 'isLegacyPromotableDataCon' - and enabling
 -XTypeInType disables this check.
 <RyanGlScott> int-index: Right, that's baffling me
 <RyanGlScott> Since that's supposed to be checked every time you promote a
 data constructor (I think)
 <RyanGlScott> int-index: File a bug about that, I suppose
 <RyanGlScott> Richard (who's sitting next to me right now) seems to think
 that that shouldn't be possible
 <int-index> RyanGlScott, the thing is, I happily removed this check
 completely in D4748. Does this mean I have to restore a weaker version of
 it that only checks for data families? Why?
 <int-index> Is it bad that -XDataKinds promotes data family constructors?
 Looks like I can just remove the "restrictions" part of the user guide and
 be done with it
 <RyanGlScott> int-index: In theory, that shouldn't be possible
 <int-index> OK, then what the check should be? No data families, any other
 restrictions?
 <RyanGlScott> I might qualify that with "no data family instances defined
 in the same module"
 <RyanGlScott> (Or to be precise, in the same SCC, but that's probably too
 technical for the users' guide)
 <int-index> Well, this sounds hard to check. I was thinking along the
 lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the
 check...
 <RyanGlScott> Oh, I thought you were only changing the users' guide :)
 <int-index> Well, at this point I'm confused if I should change only the
 user guide or the check as well. If data families shouldn't be promoted
 ever, then I'll change GHC. If the limitation is about the current SCC
 group, I can just mention Trac #12088 as a known infelicity in the User's
 Guide
 }}}

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