Be pickier about unsaturated synonyms in :kind

Authored by RyanGlScott on Dec 21 2018, 8:39 PM.



We currently permit any and all uses of unsaturated type
synonyms and type families in GHCi's :kind command, which allows
strange interactions like this one:

> :set -XTypeFamilies -XPolyKinds
> type family Id (a :: k)
> type instance Id a = a
> type Foo x = Maybe
> :kind! Id Foo

This is probably a stretch too far, so this patch moves to disallow
unsaturated synonyms that aren't at the top level (we still want to
allow :kind Id, for instance). We do this by augmenting GhciCtxt
with an additional Bool field to indicate if we are at the
outermost level of the type being passed to :kind or not. See
Note [Unsaturated type synonyms in GHCi] in TcValidity for the
full story.

Test Plan

make test TEST=T16013

RyanGlScott created this revision.Dec 21 2018, 8:39 PM
goldfire accepted this revision.Dec 21 2018, 8:52 PM

Looks good to me.

This revision is now accepted and ready to land.Dec 21 2018, 8:52 PM

One suggestion. Somewhat a matter of taste I suppose.


I wonder if this is really needed? You switch from GhciCtxt True to GhciCtxt False at certain points. Could you not just switch from GhciCtxt to SigmaCtxt? GHCi has no special behaviour after top-level; and SigmaCtxt is a kind of generic context.

We do this elsewhere. E.g. check_type uses SigmaCtxt for the body of a forall-type, regardless of incoming context (see line 493 of TcValidity.

RyanGlScott added inline comments.Dec 24 2018, 3:02 PM

SigmaCtxt is a kind of generic context.

It is? Its documentation suggests otherwise:

| SigmaCtxt           -- Theta part of a normal for-all type
                      --      f :: <S> => a -> a
RyanGlScott added inline comments.Dec 31 2018, 10:24 AM

Thoughts on the above?

RyanGlScott added inline comments.Jan 7 2019, 3:10 PM


Sorry to be so slow.

Sorry to be so slow.

No worries! Looking forward to your review (I can't tell if you meant to submit it alongside your comment or not).

Bother. I did type in a comment, but somehow it got lost. Anyway: go for it!


Ah yes, good point. SigmaCtxt is really a terribly bad name!

So ok, yes, I'm content with the GhciCtxt Bool idea.

RyanGlScott abandoned this revision.Jan 8 2019, 7:57 AM

I've migrated this over to GitLab in (once it validates, I'll merge).