This wasn't as bad as I was worried about, but I'm curious for Simon's thoughts on the design.

In D4777#151674, @andrewthad wrote:

The user deserves a better error message here. I had thought that unifyKind would fail if you tried to unify TYPE 'LiftedRep and TYPE 'IntRep (with an error message along the lines on "Could not unify actual kind X with expected kind Y"). But this doesn't happen.

One last suggestion below. Then I think we're ready to merge! :)

For data family instances, there are potentially three kinds that all get unified:

No, I don't think the new implementation of unravelFamInstPats is good: throwing away the cast might cause trouble later on. I still say we shouldn't ever see the case with the coercion, because kcConDecl won't let us. My guess is that you didn't see my earlier comment before posting yours.

Let's take a step back:

In D4777#151457, @andrewthad wrote:

That is, the data constructor has type Int# -> Foo and not type Int# -> Foo 'Red. I don't understand why this is the case, but I'm guessing there are good reasons for it.

Yes, -ddump-tc-trace sometimes hangs. My approach there is to add a bunch more traces (printing out strings only) to learn where the hang is. Then, you'll find some knot-tied something being printed out. Remove the printing. This is a bug that you have the opportunity to find and fix. :)

The Typeable related panic shouldn't be hard to stop. I'm not sure offhand where the fix is (there already have to be a slew of checks before generating Typeable instances), but it sounds like Ryan knows. If you can't find it, ask and I'll take a closer look.

I have done a thorough review. While I'm not surprised that this mostly works (the code is indeed pretty close), there are some corner cases worth investigating before merging.

I've actually (locally) taken care of the line comments I've made here (which I wrote weeks ago but never posted -- sorry). This patch is ready to land. But I'm holding off because @bgamari said to wait until after the GitLab migration is complete. There is a lingering user-facing design and internal design issue: Trac #16082. We'll fix that in a separate patch.

Looks good to me.

In its current form, does it validate? If so, let's merge it. 8.8 is nigh, and it's best to get this out the door. However, even after merging, we should continue to press forward with some of the tweaks suggested in this thread. My and I will discuss in person later this week. In the meantime, My, report if it validates; when it does, let's just pull the trigger.

We can get a precise answer by looking at the intersection of what checkPattern and checkExpr accept.

With commands, we need to look at the intersection of what checkPattern, checkExpr, and checkCommand accept. And when I get to unifying term/type parsers, also checkType (not currently defined).

👍

OK. I've exhausted my time budget for this today, but I'll keep this in my queue. Sad to say, but I likely won't get to it for a few days.

I've taken my pass, but I skipped the following:

• TH (Thanks, @RyanGlScott)
• Parser (Thanks, @int-index)
• Test output in partial-sigs, thinking that my suggested change to addTypeCtxt will take care of it.

I'm late to this conversation, and I haven't looked at the code -- only the conversation. Here are my thoughts:

I do intend to take a close look at this, but it likely won't happen until after classes end, in about 2 weeks.

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

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.

We might want to update this approach if/when Trac #12363 ever gets implemented.

Sharing comments for call Simon and I are having.

More from SPJ.

More later!

More updates from Simon.

LGTM.

In D5282#146871, @simonpj wrote:

make all binders in a representation TyCon into Specified, at birth

More commits from Simon:

This looks like it works, but I think it can be refactored to be simpler. Thanks!

Out of time now; more later. (Note to self: I read through files before TcHsType, kcImplicitTKBndrs but not kcLHsQTyVars; also read through TcMType)

LGTM.

Not from me. Ship it!

Yes!

I've commented on the ticket, as that seems a better place than here.

I have a hunch that this might also fix Trac #15852.

Committed: 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3

Committed: 4427315a65b25db22e1754d41b43dd4b782b022f

Thanks for the quick action here!

I may not get a chance to cycle back to this one. If it validates, please merge. Thanks.

Get quantification right, for once.

Thanks!