Visible kind application

Authored by mynguyen on Oct 17 2018, 1:44 AM.



This patch implements visible kind application (GHC Proposal 15/trac`Trac #12045`), as well as #15360 and #15362.
It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be
written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind
application, just like in term-level.

This patch however is not ready to be merged, as there are a few problems I can't figure out myself. In tests T13550
and T12045TH1, the data instances are printed without parentheses and I just can't find out why. For test T13524,
my patch yields error and only works when I switch the order of the 2 arguments. For test T15415, my patch runs
without error/warning due to my new handling of wildcard. I hope to get feedback on the patch and help on how to
fix/handle these above-mentioned cases.

Test Plan

Tests T12045a/b/c/TH1/TH2, T15362, T15592a

Diff Detail

rGHC Glasgow Haskell Compiler
Lint WarningsExcuse: around 80 chars
Warningcompiler/deSugar/DsMeta.hs:582TXT3Line Too Long
Warningcompiler/deSugar/DsMeta.hs:623TXT3Line Too Long
Warningcompiler/hsSyn/Convert.hs:1335TXT3Line Too Long
Warningcompiler/hsSyn/Convert.hs:1339TXT3Line Too Long
Warningcompiler/hsSyn/Convert.hs:1342TXT3Line Too Long
Warningcompiler/hsSyn/Convert.hs:1350TXT3Line Too Long
Warningcompiler/hsSyn/Convert.hs:1456TXT3Line Too Long
Warningcompiler/hsSyn/Convert.hs:1475TXT3Line Too Long
Warningcompiler/hsSyn/Convert.hs:1480TXT3Line Too Long
Warningcompiler/hsSyn/Convert.hs:1570TXT3Line Too Long
Warningcompiler/hsSyn/HsTypes.hs:1074TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:834TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:837TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:968TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:1518TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:1535TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:1538TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:1539TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:1564TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:1638TXT3Line Too Long
Warningcompiler/rename/RnSource.hs:785TXT3Line Too Long
Warningcompiler/rename/RnTypes.hs:1644TXT3Line Too Long
Warningcompiler/rename/RnTypes.hs:1649TXT3Line Too Long
Warningcompiler/typecheck/TcHsType.hs:82TXT3Line Too Long
Warningcompiler/typecheck/TcHsType.hs:386TXT3Line Too Long
No Unit Test Coverage
Build Status
Buildable 25493
Build 64759: [GHC] Linux/amd64: Continuous Integration
Build 64758: [GHC] OSX/amd64: Continuous Integration
Build 64757: [GHC] Windows/amd64: Continuous Integration
Build 64756: arc lint + arc unit
There are a very large number of changes, so older changes are hidden. Show Older Changes
RyanGlScott added inline comments.Dec 4 2018, 9:25 AM

Similarly, keep the old type signature here.


This documentation is now out of date, since it refers to the "left-hand-side type patterns", but we now use a single Type to refer to the entire left-hand-side. It would be good to update this documentation accordingly (and perhaps provide an example of what each of the fields of TySynEqn represent).

This revision now requires changes to proceed.Dec 4 2018, 9:25 AM
mynguyen added inline comments.Dec 4 2018, 9:49 AM

I see. So I should keep the type signature here, but can still change the implementation here to make sure that the Name is actually not used, and [TypeQ] in type signature is just one TypeQ?


Thanks so much @RyanGlScott! This is indeed what I wanted to write. Will update patch real soon. (This is what happens when I try to write code at 3am...)


again, so much thanks!

12 ↗(On Diff #18994)

Thanks - you are correct. Somehow I thought the kind of App would be App :: forall (f :: k -> *). k -> * following the signature there, but I just checked with :k and indeed it's forall k (f :: k -> *). k -> *. Will move this to should_fail.

RyanGlScott added inline comments.Dec 4 2018, 10:21 AM

No, I would instead change the implementation so that it takes the Name and [TypeQ] arguments and forms a single TypeQ out of them. I had something like this in mind:

dataInstD :: CxtQ -> Name -> [TypeQ] -> Maybe Kind -> [ConQ] -> [DerivClauseQ]
dataInstD ctxt tc tys ksig cons derivs =
    ctxt1 <- ctxt
    let ty1 = foldl' appT (conT tc) tys
    cons1 <- sequence cons
    derivs1 <- sequence derivs
    return (DataInstD ctxt1 Nothing ty1 ksig cons1 derivs1)

I'm not sure if that typechecks, but hopefully you get the idea.


Urgh, now that I think more about this, I'm not sure if it's possible to keep the old type signature for TySynEqn. The problem is that you've changed TySynEqn to require more information than it did previously. That is to say, before, if you wanted to build a type family like this:

type family Foo where
  Foo = Int

Then before, you could simply do this:

TySynInstD ''Foo (TySynEqn [] (ConT ''Int))

That is, the name of the type family was passed to TySynInstD, so there was no need to put it in TySynEqn. After you changes, however, you must do this:

TySynInstD (TySynEqn (ConT ''Foo) (ConT ''Int))

Note that the name of the type family has moved to TySynEqn instead. This means that in order to construct a TySynEqn, you must know what the name of the type family is, which is a requirement that simply didn't exist before. That is to say, the existing type signature simply doesn't have enough information to satisfy this requirement.

In light of this, I don't see any alternative except to make some sort of backwards-incompatible change to the type signature of tySynEqn. If we're going to do so, then I think it might be best to just use the current type signature in T.H.T.Lib.Internal:

tySynEqn :: (Maybe [TyVarBndrQ]) -> TypeQ -> TypeQ -> TySynEqnQ

That is, delete the version of tySynEqn in T.H.T.Lib, and simply reexport the one from T.HT.Lib.Internal. Also make sure to note in libraries/template-haskell/ that the type of tySynEqn has changed (and why it changed). Thanks!

mynguyen added inline comments.Dec 4 2018, 9:12 PM

I got it - I guess I'm just not sure why we can't just change the type signature in Lib to mimic what's in Lib.Internal. Like why is there a convention that we should minimize change to Lib?


Good call, thank you! Again, the same question as above, if I can change the type signature of tySynEqn here to what's in Lib.Internal, what's preventing me from doing the same for dataInstD and newtypeInstD above?

mynguyen updated this revision to Diff 19012.Dec 5 2018, 12:07 AM
mynguyen marked an inline comment as done.

Updating D5229: Visible kind application

Updated to address previous comments. Everything seems to work now, except bug
#15795 (which I secretly hope noone would ever run into), and #14579
(which I am likely misunderstanding). As always, I hope to receive feedback
and help from you all.

mynguyen marked 12 inline comments as done.Dec 5 2018, 12:11 AM
mynguyen added inline comments.

Ahhh nevermind, I see why now.

Everything seems to work now, except bug
#15795 (which I secretly hope noone would ever run into)

Hah, indeed! Personally, I wouldn't consider Trac #15795 to be a blocking issue for this patch, so I would be fine with leaving that issue as future work.

and #14579
(which I am likely misunderstanding).

I've added an inline comment about this one.


I think this might be best illustrated by adding the following snippet at the end of these Haddocks:

-- For instance, if you had the following type family:
-- @
-- type family Foo (a :: k) :: k where
--   forall k (a :: k). Foo \@k a = a
-- @
-- The @Foo \@k a = a@ equation would be represented as follows:
-- @
-- 'TySynEqn' ('Just' ['PlainTV' k, 'KindedTV' a ('VarT' k)])
--            ('AppT' ('AppKindT' ('ConT' ''Foo) ('VarT' k)) ('VarT' a))
--            ('VarT' a)
-- @

Don't forget to mention your changes to L.H.T.Syntax here!


This test case is very nearly correct. The reason you get these error messages:

T14579a.hs:15:32: error: Not in scope: type variable ‘a’

T14579a.hs:15:51: error: Not in scope: type variable ‘a’

T14579a.hs:16:25: error: Not in scope: type variable ‘a’

T14579a.hs:16:44: error: Not in scope: type variable ‘a’

Is because by default, the a in the Eq (Glurp a) instance head isn't brought into scope over the body of the instance. To make that happen, you have to enable the ScopedTypeVariables extension. Doing that (and importing Data.Coerce) makes this compile:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Bug where

import Data.Coerce
import Data.Kind
import Data.Proxy

newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
  deriving Eq

newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a))

instance Eq a => Eq (Glurp a) where
  (==) = coerce @(Wat ('Proxy @a) -> Wat ('Proxy @a) -> Bool)
                @(Glurp a         -> Glurp a         -> Bool)
int-index added inline comments.Dec 5 2018, 4:37 AM

I foresee no other changes to the Parser.y grammar. Time to uncomment this.


Let's not discard the annotations:

(addAccAnns, acc') <- eitherToP $ mergeOpsAcc acc

and then a few lines below:

; addAccAnns
; addAnnsAt bl anns
; return (cL bl bt)

Here we can discard the annotations because we immediately fail afterwards. Is it worth a comment?


Let's not discard the annotations:

{ (addAccAnns, acc') <- eitherToP $ mergeOpsAcc acc
; addAccAnns
; go ... }

This should be named clause [opd] like the one above.


This entire comment is from an earlier version of the code, I suppose it's a rebase artefact.

Let's keep the version that is in master:

-- clause [end]
-- See Note [Non-empty 'acc' in mergeOps clause [end]]

Why this empty line?


Why this empty line?


Unnecessary whitespace changes on this and neighbouring lines.


I don't think it's a good idea to mess with unsetWOptM or setXOptM for this purpose, after all they control flags that supposedly the user has set. In general, it is fragile and may have unintended side effects.

Before this patch, we had emitWildCardHoleConstraints neither here nor in tcWildCardOcc. Why was it insufficient, what prompted adding emitWildCardHoleConstraints to tcWildCardOcc?


No need for unLoc before ppr.


Another place that modifies flags/options. What happens if we call tcHsTypeApp here instead, as it doesn't emit hole constraints?

mynguyen added inline comments.Dec 5 2018, 4:04 PM

I agree that messing with flag controls isn't the best thing to do. This problem however is quite complicated and I didn't see any other way out of it.

So for this particular question, why was the old tcHsTypeApp insufficient: This is because I've refactored wildcards so that unnamed wildcards won't be renamed during renamer, and HsWildCardBndrsto only include named wildcards in it hswc_ext. Thus the wc_ty :: LHsWcType GhcRn now no longer has any unnamed wildcards in it, and instead the unnamed wildcards stay unchanged in hs_ty here. Thus even if we don't call emitWildCardHoleConstraints here, tcCheckLHsType hs_ty kind will eventually reach emitWildCardHoleConstraints in tcWildCardOcc and trigger error/warning on @_.

So why have emitWildCardHoleConstraints in tcWildCardOcc? Again, since we don't have unnamed wildcards renamed and in HsWildCardBndrs anymore, the emitWildCardHoleConstraints wcs in tcRnType won't check the unnamed wildcards. But we still need to emit hole constraints on such wildcards in general, so the solution is to do it in tcWildCardOcc, where unnamed wildcards are given fresh wild tyvars. But then again, we don't want to ever perform emitWildCardHoleConstraints when it's @_, so the solution was to add unsetWOptM and setXOptM whenever necessary to make sure @_ passes without fuss, while everything else works as it should.

So now the next question is, why did we refactor wildcards, stop renaming them, omit them from HsWildCardBndrs, and have to deal with all the above? If we don't do it, unnamed wildcards will be passed to emitWildCardHoleConstraints at some point in the renamer/typechecker, and we'll have no way to decide whether or not a wildcard is called with visible kind application to stop it. There were other reasons as well as I discussed this with Richard way back in the summer, but I didn't document any and I can't remember off the top of my head.

Please let me know if you have any other way to solve this! :)

mynguyen added inline comments.Dec 5 2018, 4:18 PM

hmm, I just never considered using tcHsTypeApp for visible kind application. I guess the main difference is that visible type application has a specific LHsWcType while kind application doesn't?
How would you suggest using tcHsTypeApp here?

int-index added inline comments.Dec 6 2018, 12:47 AM

I did not realize this. So we have

-- | Located Haskell Wildcard Type
type LHsWcType    pass = HsWildCardBndrs pass (LHsType pass)    -- Wildcard only

and it stores wildcard info. It's used when type-checking type applications. Why don't we do the exact same thing for kind application?

-- | Located Haskell Wildcard Kind
type LHsWcKind    pass = HsWildCardBndrs pass (LHsKind pass)    -- Wildcard only

data HsType pass
  | HsAppKindTy         (XAppKindTy pass) -- type level type app
                        (LHsType pass)
                        (LHsWcKind pass)

Then we can reuse tcHsTypeApp. You know this code better than me, so let me know if I'm suggesting nonsense :)

mynguyen updated this revision to Diff 19036.Dec 6 2018, 11:09 AM

Updating D5229: Visible kind application

Address final comments

mynguyen added inline comments.Dec 6 2018, 11:04 PM

I definitely think your suggestion is valid, and one that I perhaps would have tried at first. However, when I started this I'd only known Haskell for around 2 weeks, and with my understanding at the time I thought it's best to stay with the current structure in HsType for HsAppKindTy (you can see that it's actually modeled upon HsAppTy), and haven't looked back since.

I think the answer to why we don't use the same structure for HsAppType and HsAppKindTy might be the same answer to why we have HsExpr and HsType separately (or not? Could we somehow make an exception and adopt the structure from HsAppType here in HsAppKindTy and leave the rest the same?).

So why don't we? I am afraid I'm not qualified to give a high level and correct answer to this, but I imagine if we could eventually have HsExpr and HsType in the same structure, we'd be really close to having dependent types. For now, I see that the way expressions and types are typechecked are totally different, and restructuring HsAppKindTy at this point, supposed it's possible, would take more time and brain than I have (it's finals time for me in college + I really want to move on to visible applications in patterns after this patch!).

simonpj added inline comments.Dec 10 2018, 9:59 AM

Why do we need a new HsExplicitListTy case here when we didn't before?

goldfire added inline comments.Dec 10 2018, 11:29 AM

The Note talks about visible kind application.... but this function is all about visible type application. So I think a longer note explaining (at a higher level) how this all works would be helpful.


I agree with everything My says here.

If I recall correctly, the decision to refactor anonymous wildcards was the result of several issues:

  • emitWildCardHoleConstraints was called in tcHsPartialSigType. The wildcards in play there would include both the wildcards in a type outside any VKA and those inside a VKA. Even by twiddling DynFlags settings, we would be unable to suppress the errors/warnings from wildcards inside a VKA. The alternative would be to capture the DynFlags (or something smaller) in the hole somehow.
  • Note that this contrasts with what happens in terms, because the VTA is a HsWcType in the HsAppType constructor. In a VKA, we have a HsKind.
  • By treating anonymous wildcards and named ones separately, it means that we can issue errors/warnings for Proxy @_k a and not for Proxy @_ a. That is, named wildcards still emit errors/warnings, while anonymous ones do not.

I do think there is a user-facing design question here around all this that we should bring back to the proposals process (or at least the GHC committee).


To put blame where blame is due, I advised using HsKind here instead of HsWcType. Here's why:

foo :: Proxy @_w a -> Proxy @_w b

Do a and b have the same kind, or not? It looks pretty clear that they do. But if we have HsWcType in VKA, then they wouldn't -- both _ws would scope locally over their own VKA. Contrast with the situation for VTA, where we generally expect that types mentioned in terms have their own local scopes. (For example, (x :: a) in terms, where a is not in scope, means x :: forall a. a).) One consequence of this design choice is the challenge that we had around emitting wild card constraints. Maybe it was the wrong choice.... but I still don't think it was.

RyanGlScott accepted this revision.Dec 10 2018, 11:35 AM

As far as the parts of the code that I'm qualified to review go, everything looks quite lovely. One minor comment inline.


The type of tySynInstD has also changed (for the same unavoidable reasons as in tySynEqn), so it would be good to mention that change as well.

This revision is now accepted and ready to land.Dec 10 2018, 11:35 AM
RyanGlScott requested changes to this revision.Dec 10 2018, 12:44 PM

Actually, I did notice one more thing as I tried to adapt some code to this patch.


Please export appKindT from here. (Currently, it's defined in L.H.T.Lib.Internal, but not reexported from here like it ought to be.)

This revision now requires changes to proceed.Dec 10 2018, 12:44 PM

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.

This is oh-so-close!


"are then both" --> "is then"


This should have a top-level comment describing it.


I think this is now out-of-date. But this change actually causes some user-facing behavior change. Previously,

type family F a b (r :: a :~: b) where
  F _ _ Refl = Int

was rejected, because the two _s were considered to be different... and yet the Refl forced them to be the same. Now, I imagine your patch will accept this. I'm actually OK with this change, but regardless the commentary should be updated.


Perhaps Note [The wildcard story for types] in HsTypes is a good place to add this information to.


Because we want to say ... '[] @Nat ....

But, @mynguyen, please comment this reason in the code.


promotedNilDataCon = promoteDataCon nilDataCon and is shorter.


Prefer Specified <- tyConBinderArgFlag ki_binder here. Using == calls another function, whereas <- is more direct.


On further examination, tcHsTypeApp just has too much of an impedance mismatch here. That function does validity checking and zonking, which is unnecessary for a VKA (because the outer type it's used in will get validity-checked and zonked).


... "or if there is no kind application"


This should really be impossible, because the case was eliminated above. Even though the behavior here is very sensible, I think panicking is better. If nothing else, it helps readers understand better what is going on.


These comments should be expanded to include the new behavior (i.e. checking for saturation and supplying invisible arguments if not)


With the new treatment for unsaturation here, we don't need this to be a special case.

Instead, call this function zonk_tycon_kind, remove the guard (that checks about saturation), and call this only in the ATcTyCon case above. (A TcTyCon might have an unzonked kind. A normal TyCon never will. We thus need to zonk and call mkNakedCastTy only for TcTyCons.) Perhaps even better would be simply to inline this behavior into the ATcTyCon case -- no need for a separate function.


Oops deleted space.


Perhaps better to abstract this into a function?


This Note doesn't explain what's going on here. This is all about allowing _s in type family patterns -- nothing to do with kind application. Also, when a Note is in another file, you should name the file.

I wonder if this pair of lines should be a new function allowWildcards :: TcM a -> TcM a. It's a little less scary that way.


This should be Required, not Specified. It's for the a in a -> b. The only reason you don't have trouble here is that the only usage of tyCoBinderArgFlag has already checked for invisibility. Once you fix this Specified to be Required, you should be able to drop that invisibility check in tcInferApps (the first substantial case in go).

8 ↗(On Diff #19036)

These extra lines are regrettable.

Fortunately, fixing is easy: just pattern-match in TcHsType.addTypeCtxt. If the ty is a HsWildCardTy, just don't call addErrCtxt. To wit:

addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt (L _ (HsWildCardTy _)) thing = thing   -- "In the type '_'" just isn't helpful.
addTypeCtxt (L _ ty) thing
  = addErrCtxt doc thing
    doc = text "In the type" <+> quotes (ppr ty)

This change is regrettable. Do we know why this is happening? @RyanGlScott, perhaps?

RyanGlScott added inline comments.Dec 10 2018, 1:30 PM

Wow, that program does typecheck with this patch! Moreover, that means this patch fixes Trac #14366! Let's add a regression test for that, too.


While I can't say with certainty, my suspicion is that the fact that this patch removed some uses of rnAnonWildCard (which appear to give wildcards their _ names) is to blame.

mynguyen added inline comments.Dec 10 2018, 9:12 PM

Hi Richard, the comment is actually already out-of-date before this patch, as tc_fam_ty_pats mentioned here doesn't exist in GHC anymore. I don't know how it's handled currently and not confident enough to rewrite the note without knowing it - do you happen to know where the "new" tc_fam_ty_pats is now?


I will add it :) Thanks for all the comments!


It is to allow VKA with promoted empty list. I will add it :)


I guess I understand the intention here but how are we handling the ATyCon case if we only call this new function with ATcTyCon?


I agree. Where should I put that function though? Like what file would be most appropriate?


Oops, this is embarrassing - a while ago that example data T f a = MkT (f a) :k T @k didn't work and I was messing around to see if I could make it work (which never happened of course because it's not supposed to work). Forgot to revert this afterwards. Thank you for noticing!


Thanks for the catch!


I too think the culprit is the removal of rnAnonWildCard and HsWildCardInfo. I will look into the ppr of HsWildCard and see if I can fix it.

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.


It's tcFamTyPats in TcTyClsDecls. Right now, though, the _s in type family patterns are producing meta-variables, not skolems. But it seems this is desired behavior.


Good question. You don't need to do anything for ATyCon. Just return the tycon with its kind -- no zonking required.


I'd put it in TcHsType. But I think we can do better by adding a new field to TcLclEnv that tracks whether or not we want to emit these constraints.

mynguyen updated this revision to Diff 19182.Dec 17 2018, 11:25 PM

Updating D5229: Visible kind application

Addressed more comments and integrated the changes into HIE. For printed outputs, there are some regrettable cases where "w" have
become "_", but this can be salvaged in further iterations of the patch.

Regrettable changes can be observed in tests T12447, UncurryNamed, WildcardInstantiations, T11670, name but a few. I also saw this while I was running the testsuite:

New Metrics these metrics trivially pass because the previous git commit doesn't have recorded metrics for the following tests. If the tests exist on the previous commit, then check it out and run the tests to generate the missing metrics.

not sure if that matters - everything else behaves as expected.

RyanGlScott updated the Trac tickets for this revision.Dec 18 2018, 11:14 AM

To be perfectly honest, the error message regressions related to wildcards aren't as bad as I thought there were going to be. For the most part, we're just swapping uses of w with _, and although that can look odd in certain places, I don't think it's necessarily wrong. Personally speaking, I'd be quite fine with this state of affairs (even if it ends up making it into the final 8.8 release), as long as we make a ticket tracking how we could make small improvements.

Also, don't worry about the message involving git metrics. It can be rather verbose, but I think that message is intended to help debug things on Harbormaster more than anything (updating git metrics is entirely automated, and you shouldn't need to do anything special regarding it).

All of my concerns have been addresses here, so I'd be fine landing the patch. What say you, @goldfire?

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.


Yes, I see why you don't like this. But it will be hard to get this right.

What if we had bravo :: forall _0. Num _0 => _0? I think that communicates the idea nicely. I'm going to try a fix locally that does this just to see what will happen.


This change isn't great -- the old error message has the right character for the _ but the new one reports the error at the beginning of the type.


This is problematic, too.


Maybe just add -XFlexibleInstances?