I suppose this is just a start, as you note. I like the general direction, but I think some more attention needs to be paid around the distinction between tyvars in the tycon and in the equations.

This looks much more plausible to me.

This fix looks very suspicious.

Bah. The Q/no Q distinction makes me want to yell obscenities.

Why does DsMeta differentiate between types and kinds? In other words, does anything go wrong if we replace repLKind with repLTy?

As for all those tickets: Trac #9196 is not related. Perhaps it once was, but the error message is now quite different.

I'm satisfied with this, then.

I just took a look here to see what I thought... and it's hard to know where to begin. I took a look at HsExpr.hs and TcExpr.hs and didn't see much interesting. Also saw HsExtension.hs, which was more interesting. But I still don't know where to focus.

Simon's last round of comments. I agree the change in the
zonker is now unnecessary.

Updates as per feedback from Simon

Looks plausible to me. If it validates. commit.

Ah. Yes, I was mistaken. (And I missed the notification from last week. Sorry.)

Fix testsuite wibble. Rebase. Validating again.

Yet another stab at fixing this the right way. But I think
I have it now. There is a good deal of commentary in this
patch that explains it. Good starting places for reading
are Note [Flattening] in TcFlatten and
Note [Rewriting with Refl] in TcCanonical.

I think this fixes the ticket. Thanks!

Correct me if I'm wrong, but these semantics say that let rec x = 3 in x steps to itself, no? And you can do this with proper (co-)recursion: let rec ones = 1 : ones in ones is quite useful, yet this, too, seems to step to itself.

This is a new approach to Trac #13333, summarized by
Note [Zonking in canonicalization] in TcCanonical.

The thread this task has been assigned to has a high priority. But threads that serve my classes that meet daily have higher. This thread has been starving of late. It should get cycles on Friday.

In D3424#98126, @simonpj wrote:

Zonking when you build the implication is obviously bogus, because a subsequent unification will invalidate it.

OK. I now know what's going on. Not sure how best to fix (though it is easy to fix).

While this patch fixed Trac #13333, it's surely the wrong approach.

I see a few other uses of splitTyConApp_maybe in the unifier. These should probably be changed to tcSplitTyConApp_maybe. Ditto with repSplitAppTy_maybe.... but perhaps the "rep" version of these functions are the same between tc and core.

Not only is it not useful, but the warning is utterly wrong. Ben said he was looking into this.

I have merged this.

Pushed to master.

Fix error message wibbles

This attempt removes the tcView/coreView (D3316) part, as there
are some design issues to discuss, as I will post to Trac #11715.

Rebase

Rebase

Simon's feedback

Thanks for the feedback. New version forthcoming.

Remove debug output. Include Haddock update.

Apply Simon's comments

Thanks!

Otherwise, looks good.

Yes, coreViewOneStarKind is your friend. It is a view on the world with only one * kind -- that is, it changes Constraint to Type. It's hard for me to be sure whether D3218 is correct or not. Adding some coreViewOneStarKinds as I have described might be an improvement.

If this works, hooray!

In D3123#93264, @ezyang wrote:

Actually this is sound!

This doesn't look right in here. eqType Constraint Type returns True. So, I recommend using coreViewOneStarKind on a and b to "unwrap" the Constraint and reveal the TYPE LiftedRep underneath. Then this all becomes much simpler.

Looks good to me. Thanks!

Ah. Just read the ticket. Thanks for doing this!

It looks like you're just removing a check. I don't think it's safe to simply remove it. Simon and I have discussed this at some length.... and, if memory serves, we did agree that because of a long series of delicate invariants, this indeed might be safe. But a long Note is in order, at the minimum.

Yes, I recommended this course of action on Trac. I would add another sentence to the Note saying that alternatives are debated on the ticket, as this design choice is indeed strange. It's just that it's better than the alternatives! Thanks, Ryan!

In D2038#89360, @simonpj wrote:

To avoid being able to extract ContraintRep ~R LiftedPtrRep we decided to weaken one of the coercion constructors, the one that gets a kind coercion from a type coercion. We don't need it, and it's awkward here.

This is looking great, Ben, other than my comment below including the text "major disaster". The disaster is in the theory, not this implementation, though!

Look great. Thanks!

Having another parameter to TYPE also solves another small wrinkle in this patch. The noinline function is used in interface files to provide loop-breakers when hs-boot files are involved. See Note [Inlining and hs-boot files] in ToIface. However, we sometimes need to apply noinline to dictionaries. If Constraint /= Type, then noinline needs to be levity polymorphic. Except that it really shouldn't be -- it should be coherency-polymorphic. Note also that coherency doesn't affect the code generator at all, so I could define

In thinking about this, I think adding the Coherency argument to TYPE might be the only solution. As it stands we're in a strange space: If I have forall (r :: RuntimeRep) (a :: TYPE r). a -> a, then any choice of r is OK except ConstraintRep -- because ConstraintRep requires a => (and can't be returned from a function, besides). This bump in the surface tells me we have the wrong design. The "obvious" way forward is to add another parameter to TYPE. Then it's all easy. And tuples can be made to infer their kind more naturally.

Add HsConLikeOut to get cleaner pretty-printing of typechecked
ConLikes. More tests and such. Still need to update manual.

This looks good. I agree about not backporting. But I wonder how TH clients would react to this change -- the new version presents clients of TH with less information than we did previously. Is it worth making a ImplicitForallT or some such that still includes the quantified variables? I guess if we did, then we'd be back to needing splitting.

Somehow I'm not getting emails from this diff. Perhaps this will help.

Some cleaning up. Some testsuite. There are still
some failing tests, including a nasty one about
printing type-checked unlifted pattern synonyms occurrences
without the void# argument. Any ideas of how to do this
would be greatly appreciated!

More bugfixing and straightening out of checkStrictBinds,
which was rather broken before.

This looks great to me. Ship it!

As you can see above, I ran into some technical trouble. This
is a test.

This patch now contains the work originally in D2852. They are
merged because that patch is easier in the context of this one,
and they're so related anyway.

This patch now contains the work originally in D2852. They are
merged because that patch is easier in the context of this one,
and they're so related anyway.

This patch now contains the work originally in D2852. They are
merged because that patch is easier in the context of this one,
and they're so related anyway.

Update: I was able to remove hsExprType and friends. I had written these because of the fixM in desugaring arrows, but it turns out that the knot-tied stuff is surely not levity polymorphic already. No need for hsExprType. However, the performance implications of LP checking are still very present, and so the idea behind the optimized version must remain. This has been integrated into a new isExprLevPoly function. However, for this function to actually be correct, it either must be rather complicated, or we need UnboxedTupleRep not to be a lie. (c.f. checkForLevPolyX and its complications)

This patch solves the problem well and fits with existing code in the area. Thanks, @sjorn3 !

Simon's feedback was delivered by voice, and I will have to incorporate changes into this patch:

• hsExprTypeForLPCheck should just become hsIsLevPoly and return a Bool instead of a Maybe Type.
• Some calls to newSysLocalDs can really be newSysLocalDsNoCheck. And with the latter being much more common than the former, I should make the latter's name shorter.
• Further thought makes me wonder if we can just do the levity polymorphism check on the desugared expression after all: perhaps the interaction with DsArrows is simpler than I thought and that there is a way to finesse the whole matter. I will explore.
• Simon has signed off on the new bit of IdInfo. But I will refactor it slightly to make my new IdInfo functions stylistically closer to existing ones. It's unclear to me whether serializing the new IdInfo is better than just recalculating it upon deserialization.

• More bugfixing. Much of base compiles.

NB: Validation successful. Still waiting for feedback from Simon, as this patch is a good deal more complicated than we hoped it would be.

Remove a debugging statement and fix some comments.

Well spotted, @facundominguez !

Oh, and yes about the name change. Simon convinced me while writing the paper that we should call it the more conspicuous "levity polymorphism".

Add several optimizations to hsExprType in order to get
T5631 to pass. There are three main optimizations:

This resolves the challenges above as well as I could.

Rebase against master