#16263: GHC accepts illegal constraint in kind -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeInType, | newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: TypeInType => TypeInType, newcomer * milestone: => 8.8.1 Comment: Luckily, commit 2257a86daa72db382eb927df12a718669d5491f8 (`Taming the Kind Inference Monster`) has already fixed this in GHC HEAD: {{{ $ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive -XPolyKinds -XDataKinds GHCi, version 8.7.20190128: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci λ> import Data.Kind λ> data Q :: Eq a => Type <interactive>:2:1: error: Illegal constraint in a kind: Eq a => * }}} We just need a regression test. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16263#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16263: GHC accepts illegal constraint in kind -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeInType, | newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Why should equality constraints be accepted? In fact, we moved in the opposite direction in https://phabricator.haskell.org/D5397#149402. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16263#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16263: GHC accepts illegal constraint in kind -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeInType, | newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): OK, and that's all well and good, but surely that ought to be the subject of a separate ticket? This one is just about GHC blindly accepting a (non- equality) constraint in a kind, which is something that we ought to just reject. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16263#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16263: GHC accepts illegal constraint in kind -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeInType, | newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Thanks for the ping. Fixing this will fit right into my work on #16185 (see `wip/T16185`) where I have already written new Notes on constraints in kinds. I'll adjust `TcValidity` to reject this kind up-front, as you suggest. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16263#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16263: Rework GHC's treatment of constraints in kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeInType, | newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/128 -------------------------------------+------------------------------------- Comment (by simonpj):

By "this kind", I assume you mean Eq a => Type from the original example? If so, yes, rejecting that (and adding a test case for it) would be wonderful.

Yes, exactly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16263#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16263: Rework GHC's treatment of constraints in kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: simonpj Type: bug | Status: patch Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeInType, | newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/128 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * owner: (none) => simonpj Comment: Assigning to simonpj to take care of the remaining work in comment:10. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16263#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16263: Rework GHC's treatment of constraints in kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: simonpj Type: bug | Status: patch Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeInType, | newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12102, #15872 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/128 -------------------------------------+------------------------------------- Comment (by Marge Bot ): In [changeset:"6cce36f83aec33d33545e0ef2135894d22dff5ca/ghc" 6cce36f8/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="6cce36f83aec33d33545e0ef2135894d22dff5ca" Add AnonArgFlag to FunTy The big payload of this patch is: Add an AnonArgFlag to the FunTy constructor of Type, so that (FunTy VisArg t1 t2) means (t1 -> t2) (FunTy InvisArg t1 t2) means (t1 => t2) The big payoff is that we have a simple, local test to make when decomposing a type, leading to many fewer calls to isPredTy. To me the code seems a lot tidier, and probably more efficient (isPredTy has to take the kind of the type). See Note [Function types] in TyCoRep. There are lots of consequences * I made FunTy into a record, so that it'll be easier when we add a linearity field, something that is coming down the road. * Lots of code gets touched in a routine way, simply because it pattern matches on FunTy. * I wanted to make a pattern synonym for (FunTy2 arg res), which picks out just the argument and result type from the record. But alas the pattern-match overlap checker has a heart attack, and either reports false positives, or takes too long. In the end I gave up on pattern synonyms. There's some commented-out code in TyCoRep that shows what I wanted to do. * Much more clarity about predicate types, constraint types and (in particular) equality constraints in kinds. See TyCoRep Note [Types for coercions, predicates, and evidence] and Note [Constraints in kinds]. This made me realise that we need an AnonArgFlag on AnonTCB in a TyConBinder, something that was really plain wrong before. See TyCon Note [AnonTCB InivsArg] * When building function types we must know whether we need VisArg (mkVisFunTy) or InvisArg (mkInvisFunTy). This turned out to be pretty easy in practice. * Pretty-printing of types, esp in IfaceType, gets tidier, because we were already recording the (->) vs (=>) distinction in an ad-hoc way. Death to IfaceFunTy. * mkLamType needs to keep track of whether it is building (t1 -> t2) or (t1 => t2). See Type Note [mkLamType: dictionary arguments] Other minor stuff * Some tidy-up in validity checking involving constraints; Trac #16263 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16263#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#16263: Rework GHC's treatment of constraints in kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: simonpj Type: bug | Status: closed Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 Resolution: fixed | Keywords: TypeInType, | newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T16263 Blocked By: | Blocking: Related Tickets: #12102, #15872 | Differential Rev(s): | https://gitlab.haskell.org/ghc/ghc/merge_requests/128, Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/499 -------------------------------------+------------------------------------- Changes (by simonpj): * status: patch => closed * testcase: => polykinds/T16263 * resolution: => fixed Comment: Landed as {{{ commit 25c3dd39f7d446f66b5c967be81f80cd7facb509 Author: Simon Peyton Jones Date: Wed Mar 6 10:17:12 2019 +0000 Test Trac #16263 testsuite/tests/polykinds/T16263.hs | 7 +++++++ testsuite/tests/polykinds/T16263.stderr | 2 ++ testsuite/tests/polykinds/all.T | 1 + 3 files changed, 10 insertions(+) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16263#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler