[GHC] #14845: TypeInType, index by GADT witnessing constraint
#14845: TypeInType, index by GADT witnessing constraint -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.5 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: -------------------------------------+------------------------------------- Just wondering if it would ever make sense to allow or use constraints like this {{{#!hs {-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-} import Data.Kind data Struct :: (k -> Constraint) -> (k -> Type) where S :: cls a => Struct cls a data Foo a where F :: Foo (S::Struct Eq a) }}} {{{ $ ghci -ignore-dot-ghci /tmp/test.hs GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/test.hs, interpreted ) /tmp/test.hs:9:13: error: • Illegal constraint in a type: cls0 a0 • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’ In the type ‘Foo (S :: Struct Eq a)’ In the definition of data constructor ‘F’ | 9 | F :: Foo (S::Struct Eq a) | ^ Failed, no modules loaded. Prelude> }}} Please close the ticket if it doesn't -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #13895 Comment: I too have hit this limitation—or rather, I have hit this error message—in #13895. But in the case of #13895, the root of the issue is impredicativity, whereas here I'm not sure that's the case. I'd be curious to hear goldfire's reasoning for why this restriction is in place, since the [http://git.haskell.org/ghc.git/blob/34834234fff4a9dd0408d3b29e001cd132665327... source code] doesn't have much in the way of an explanation. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I think it's this. `S` is a data constructor with an evidence argument. At the term level we pass evidence to `S`. But if we promote `S` we don't have a type-level version of evidence. So I was going to say "we don't promote `S`". But then I remembered that `TypeInType` is supposed to allow GADTs at the type level. So now I'm confused. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Technically, we do promote `S`, but the promoted `S` can't ever be applied, because we can't produce evidence. Perhaps a better error message is warranted, but until we have real dependent types (and can promote dictionaries), I think we're stuck on this one. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Technically, we do promote S, but the promoted S can't ever be applied
Would it not be better (for now anyway) not to promote S? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I suppose the difference in promoting and not promoting is in the error message, no? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:6 goldfire]:
I suppose the difference in promoting and not promoting is in the error message, no?
Indeed. If a tree is promoted in a forest but no one can see it, is it ever really promoted? :) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
I suppose the difference in promoting and not promoting is in the error message, no?
Indeed! You'll get "Data constructor S can't be used in a type because it's a GADT" or something like tat, rather than the current mysterious one. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): OK. Then we can just reword the error message. :) Note that problem isn't that it's a GADT constructor. The problem is that it's a constrained constructor and constraints don't promote. Ryan, you find it far easier than I to actually get patches sent off -- would you mind tweaking this message? Thanks! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): But there's a significant wrinkle here. You're proposing that we change the error message to something like `Data constructor has a constraint 'cls0 a0', and thus cannot be promoted`, yes? But the place where this error message is thrown is `tcInstBinders`, which is not in any way data- constructor–specific. Indeed, as I mentioned in comment:2, this error message also occurs in the program in #13895, but that doesn't promote any data constructors whatsoever. So if we change this error message _carte blanche_, all of a sudden GHC is going to be complaining about data constructors which don't exist. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I don't agree with comment:2. This ticket doesn't seem to have anything to do with impredicativity. It just has to do with a constructor that's promoted, but shouldn't be. Doesn't it? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): This is the test case from #13895: {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeInType #-} module Foo where import Data.Data (Data, Typeable) import Data.Kind dataCast1 :: forall (a :: Type). Data a => forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a) dataCast1 _ = undefined }}} {{{ $ /opt/ghc/8.4.1/bin/ghci Bug.hs GHCi, version 8.4.0.20180224: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Foo ( Bug.hs, interpreted ) Bug.hs:11:23: error: • Illegal constraint in a type: Typeable k0 • In the first argument of ‘Typeable’, namely ‘t’ In the type signature: dataCast1 :: forall (a :: Type). Data a => forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a) | 11 | Typeable t | ^ Bug.hs:12:38: error: • Illegal constraint in a type: Typeable k0 • In the first argument of ‘c’, namely ‘(t d)’ In the type signature: dataCast1 :: forall (a :: Type). Data a => forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a) | 12 | => (forall d. Data d => c (t d)) | ^^^ }}} Note that there are no promoted constructors in this program! But changing the error message as per the suggestion in comment:9 means that the new error message for this program would (incorrectly) be: {{{ Data constructor has a constraint `Typeable k0`, and thus cannot be promoted }}} Since the [http://git.haskell.org/ghc.git/blob/ffdb110a7f71b29f30adab7fea794b9f070a8e75... place where this error message arises], `tcInstBinder`, has no knowledge of where the constraint comes from (in particular, whether it comes from a promoted constructor or not). I just want to make sure that if we do change this error message, that we don't degrade the quality of the error message in this program. But I have no idea how `tcInstBinder` works, so knowing how to propagate the relevant information down into `tcInstBinder` to make it aware of the provenance of the error message is far above my pay grade. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Hmph. You're right. You could always just add a `NB: Constrained data constructors cannot be promoted` or `Have you tried promoting a constrained data constructor?`. I don't think people will often trip over this. The other place to check is in the `AGlobal (AConLike (RealDataCon dc))` case in `TcHsType.tcTyVar`. I don't suppose it would be hard to check if the datacon had constraints. The only access seems to be in the fourth component of a `dataConFullSig`, but the comments there refer to a `dataConDictTheta` (now extinct) that could be revived to return this nugget. That might be a better route. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): OK so there are two things * A data constructor should not be promoted if it has a constrained type. This should not be hard to arrange. * As comment:12 shows, a kind signature should hove no constraints in it. Surely `checkValidType` is the place for that check. By the time we get to `tcInstBinder` the crime is well past! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): But ''equality'' constraints are OK. Even user-written ones. What about ones hidden behind type synonyms? I think they should be, too. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:15> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Actually, come to think of it, the check I suggested around `dataConFullSig` will snag user-written equality constraints, which it shouldn't. For example {{{ data G a where MkG :: a ~ Int => G a }}} should be just fine to promote. So something more delicate will be needed. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:16> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895 | Differential Rev(s): Phab:D4728 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D4728 Comment: Phab:D4728 attempts to provide a better error message when promoting a data constructor with an unpromotable context. Note that I didn't attempt to change `checkValidType` in this patch, since that would require a significant amount of plumbing to check whether `checkValidType` was being called on a type or a kind. I felt that the existing error message from `tcInstBinder` (which I tweaked slightly in this Diff to say "kind" instead of "type") was sufficient. This patch also doesn't check for type synonyms, as suggested in comment:15, since that would require changing the checks in `tcInstBinder` accordingly, and I don't know how to do that. But in any case, this is a solid improvement over the status quo. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:17> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895, #15215 | Differential Rev(s): Phab:D4728 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * related: #13895 => #13895, #15215 Comment: #15215 (after fixing the bug in that ticket) is another example of the horrible error message reported in the Description. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:18> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895, #15215 | Differential Rev(s): Phab:D4728 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"2f6069ccf21d7be0e09016896238f417d2492ffa/ghc" 2f6069c/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="2f6069ccf21d7be0e09016896238f417d2492ffa" Make better "fake tycons" in error recovery Consider (Trac #15215) data T a = MkT ... data S a = ...T...MkT.... If there is an error in the definition of 'T' we add a "fake type constructor" to the type environment, so that we can continue to typecheck 'S'. But we /were not/ adding a fake anything for 'MkT' and so there was an internal error when we met 'MkT' in the body of 'S'. The fix is to add fake tycons for all the 'implicits' of 'T'. This is done by mk_fake_tc in TcTyClsDecls.checkValidTyCl, which now returns a /list/ of TyCons rather than just one. On the way I did some refactoring: * Rename TcTyDecls.tcAddImplicits to tcAddTyConsToGblEnv and make it /include/ the TyCons themeselves as well as their implicits * Some incidental refactoring about tcRecSelBinds. The main thing is that I've avoided creating a HsValBinds that we immediately decompose. That meant moving some deck chairs around. NB: The new error message for the regression test T15215 has the opaque error "Illegal constraint in a type:", flagged in Trac #14845. But that's the fault of the latter ticket. The fix here not to blame. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:19> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13895, #15215 | Differential Rev(s): Phab:D4728 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari <ben@…>): In [changeset:"c63754118cf6c3d0947d0c611f1db39c78acf1b7/ghc" c637541/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="c63754118cf6c3d0947d0c611f1db39c78acf1b7" Provide a better error message for unpromotable data constructor contexts Trac #14845 brought to light a corner case where a data constructor could not be promoted (even with `-XTypeInType`) due to an unpromotable constraint in its context. However, the error message was less than helpful, so this patch adds an additional check to `tcTyVar` catch unpromotable data constructors like these //before// they're promoted, and to give a sensible error message in such cases. Test Plan: make test TEST="T13895 T14845" Reviewers: simonpj, goldfire, bgamari Reviewed By: bgamari Subscribers: rwbarton, thomie, carter GHC Trac Issues: #13895, #14845 Differential Revision: https://phabricator.haskell.org/D4728 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:20> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T14845_fail1, | dependent/should_fail/T14845_fail2 Blocked By: | Blocking: Related Tickets: #13895, #15215, | Differential Rev(s): Phab:D4728 #15282 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * testcase: => dependent/should_fail/T14845_fail1, dependent/should_fail/T14845_fail2 * resolution: => fixed * related: #13895, #15215 => #13895, #15215, #15282 * milestone: => 8.6.1 Comment: Commit c63754118cf6c3d0947d0c611f1db39c78acf1b7 improves the error message substantially. As mentioned in comment:4, we can't actually allow this program until dependent types are available. The remaining task from this ticket is to document how a program like the one in comment:16 desugars into coercions at the Core Level. I've opened #15282 for this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:21> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14845: TypeInType, index GADT by constraint witness -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T14845_fail1,T14845_fail2 Blocked By: | Blocking: Related Tickets: #13895, #15215, | Differential Rev(s): Phab:D4728 #15282 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: dependent/should_fail/T14845_fail1, dependent/should_fail/T14845_fail2 => dependent/should_fail/T14845_fail1,T14845_fail2 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14845#comment:22> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC