#7961: Remove restrictions on promoting GADT's ---------------------------------+------------------------------------------ Reporter: danharaj | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: #6204 | ---------------------------------+------------------------------------------ Comment(by thoughtpolice): Related: Richard Eisenberg's recent paper, "Towards dependently typed Haskell: System FC with kind equality" attacks almost exactly these problems I think. Or at least, it addresses the notion of promoting GADTs and indexing them by e.g. kinds (and the usual kin: kind families, etc.) http://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds-extended.pdf (Section 2, "Shallow Embedding" followed by "Deep embedding" gives an example of promoting GADTs.) I don't know what the status of this work is, but at the least you can use this paper as a basis to discuss precisely what you do/do not want? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7961#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler