#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... "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