Opened 13 days ago

Last modified 5 days ago

#15245 merge bug

Data family promotion is possible

Reported by: int-index Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.4.3
Keywords: TypeInType Cc: RyanGlScott, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case: dependent/should_fail/T15245.hs
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4748
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:

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

Change History (3)

comment:1 Changed 8 days ago by goldfire

According to these mutterings, we need to abstract over a coercion to promote data family instances properly. I haven't paged it all back in, but this is an implementation error, not a documentation one.

comment:2 Changed 5 days ago by int-index

Component: DocumentationCompiler (Type checker)
Differential Rev(s): D4748
Status: newmerge
Test Case: dependent/should_fail/T15245.hs
Type of failure: None/UnknownGHC accepts invalid program

This is now fixed in HEAD by disallowing promotion of data families. If anyone needs this feature, it would be appropriate to create a feature request.

comment:3 Changed 5 days ago by RyanGlScott

Differential Rev(s): D4748Phab:D4748
Note: See TracTickets for help on using tickets.