Fix #12102/#15872 by removing outdated users' guide prose
ClosedPublic

Authored by RyanGlScott on Nov 30 2018, 9:03 AM.

Details

Summary

In the beginning, Trac #12102 (and Trac #15872, which is of a similar
ilk) were caused by a poor, confused user trying to use code that
looks like this (with a constraint in the kind of a data type):

type family IsTypeLit a where
  IsTypeLit Nat    = 'True
  IsTypeLit Symbol = 'True
  IsTypeLit a      = 'False

data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
  MkNat    :: T 42
  MkSymbol :: T "Don't panic!"

Many bizarre GHC quirks (documented in those tickets) arose from
this sort of construction. Ultimately, the use of constraints in
data type kinds like this has made a lot of people very confused and
been widely regarded as a bad move.

Commit 2257a86daa72db382eb927df12a718669d5491f8 finally put this
feature out of its misery, so now the code above simply errors with
Illegal constraint in a kind. As a result, the aforementioned
tickets are moot, so this patch wraps a bow on the whole thing by:

  1. Removing the (now outdated) section on constraints in data type kinds from the users' guide, and
  2. Adding a test case to test this code path.
Test Plan

make test TEST=T12102

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
RyanGlScott created this revision.Nov 30 2018, 9:03 AM

Great! I had quite forgotten that bit of the monster-patch. I hope Richard agrees!?

Looking at the relevant bits of the Monster Patch, it looks like these constraints are eliminated simply in the validity checker. That is, equality constraints in kinds still work, but now the user can't write them. By "work", I mean that tcInstTyBinders does the right thing. It looks like this from the code, but I'm just double-checking my understanding.

Yes, I think this is the right way to deal with these constraints, at least until we can deal with them properly.

That is, equality constraints in kinds still work, but now the user can't write them. By "work", I mean that tcInstTyBinders does the right thing. It looks like this from the code, but I'm just double-checking my understanding.

I think that's right.

But if they can't show up in user types, when _can_ they show up? Id' like to add a note to tcInstTyBInders to say.

They can appear in the kinds of promoted data constructors, say from GADTs with hand-written equality constraints.

They can appear in the kinds of promoted data constructors, say from GADTs with hand-written equality constraints.

But promoted data constructors could have _arbitrary_ constraints, including class constraints. What is supposed to happen to them?

tdammers accepted this revision.Dec 3 2018, 6:40 AM
tdammers added a subscriber: tdammers.

If I could, I'd give you extra points for the HHGTTG references.

This revision is now accepted and ready to land.Dec 3 2018, 6:40 AM
data T a = Eq a => MkT
> :k MkT

<interactive>:1:1: error:
    • Data constructor ‘MkT’ cannot be used here
        (it has an unpromotable context ‘Eq a’)
    • In the type ‘MkT’

Looks reasonable to me.

In that case, is this patch ready to be merged?

Let's land this!

This revision was automatically updated to reflect the committed changes.