Opened 8 months ago

Closed 7 months ago

Last modified 7 months ago

#16263 closed bug (fixed)

Rework GHC's treatment of constraints in kinds

Reported by: goldfire Owned by: simonpj
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.6.3
Keywords: TypeInType, newcomer Cc:
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, https://gitlab.haskell.org/ghc/ghc/merge_requests/499
Wiki Page:

Description

GHC 8.6 accepts

data Q :: Eq a => Type

It shouldn't, as we can't have Eq a as a constraint in kinds. Note that writing a constructor for Q is rejected.

Change History (16)

comment:1 Changed 8 months ago by RyanGlScott

Keywords: newcomer added
Milestone: 8.8.1

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.

comment:2 Changed 8 months ago by simonpj

Terrific. But note that is should work for equality constraints like (a ~ b), and I bet it does not.

comment:3 Changed 8 months ago by RyanGlScott

Why should equality constraints be accepted? In fact, we moved in the opposite direction in https://phabricator.haskell.org/D5397#149402.

comment:4 Changed 8 months ago by simonpj

Good spot!

But there is code in GHC that specifically deals with equality constraints (only) in kinds: see

  • Inst.tcInstTyBinder.
  • dc_theta_illegal_constraint in TcHsType.tcTyVar (which deals with promoting data constructors)

I talked with Richard about this last night. I think we agreed that we can systematically and consistently support equality constraints in types. If so, we should un-do the commit you reference.

comment:5 Changed 8 months ago 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.

comment:6 Changed 7 months ago by RyanGlScott

Thoughts on comment:5, simonpj?

comment:7 Changed 7 months ago 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.

comment:8 in reply to:  7 Changed 7 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/128
Milestone: 8.8.18.10.1
Status: newpatch
Summary: GHC accepts illegal constraint in kindRework GHC's treatment of constraints in kinds

Replying to 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.

OK, I didn't realize that you were directly working on fixing this. In that case, I'll retitle this ticket to reflect your more ambitious goals.

I'll adjust TcValidity to reject this kind up-front, as you suggest.

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.

comment:9 Changed 7 months ago 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.

comment:10 Changed 7 months ago by mpickering

The test files weren't included in the patch for #16185 so this test still needs to be added separately.

comment:11 Changed 7 months ago by RyanGlScott

Owner: set to simonpj

Assigning to simonpj to take care of the remaining work in comment:10.

comment:12 Changed 7 months ago by RyanGlScott

Equality constraints in kinds are quite broken currently, as demonstrated in #12102 and #15872.

comment:13 Changed 7 months ago by Marge Bot <ben+marge-bot@…>

In 6cce36f8/ghc:

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

comment:14 Changed 7 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/128https://gitlab.haskell.org/ghc/ghc/merge_requests/128, https://gitlab.haskell.org/ghc/ghc/merge_requests/499

comment:15 Changed 7 months ago by simonpj

Resolution: fixed
Status: patchclosed
Test Case: polykinds/T16263

Landed as

commit 25c3dd39f7d446f66b5c967be81f80cd7facb509
Author: Simon Peyton Jones <simonpj@microsoft.com>
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(+)

comment:16 Changed 7 months ago by Marge Bot <ben+marge-bot@…>

In 25c3dd3/ghc:

Test Trac #16263
Note: See TracTickets for help on using tickets.