#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 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 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 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 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 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 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): 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, #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 Ben Gamari ): 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,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