Add kind equalities to GHC
AbandonedPublic

Authored by bgamari on Apr 5 2015, 8:10 PM.

Details

Reviewers
alanz
simonpj
goldfire
hvr
austin
Trac Issues
#7961
Summary

This implements kind equalities, according to the "System FC with
Explicit Kind Equalities" paper.

See https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1 for
details. This branch is available at github.com/goldfirere/ghc,
on the nokinds branch.

The initial diff is still very much a work in progress; there are
181 failures in the testsuite. A good deal of these have known causes,
and an unknown number are simple error message wibbles. (I haven't
had a chance to go through all the errors yet.)

Test Plan

testsuite; implement several Agda programs in Haskell
and see what happens; compile against all of Hackage.
Soon, I'll invite the community to try this
out.

There are a very large number of changes, so older changes are hidden. Show Older Changes
This revision now requires changes to proceed.May 10 2015, 6:19 PM
goldfire updated this revision to Diff 5177.Nov 18 2015, 8:01 AM

Getting closer to merging. This is WIP -- this doesn't even
compile at the moment.

  • Comments only
  • Testsuite
  • Comments only
  • Workin' the testsuite.
  • Workin' the testsuite.
  • Change an ASSERT to an ASSERT2
  • Remove some outdated ASSERTs
  • Zonk in getInitialKinds; remove old ASSERT.
  • Correct fix for Trac #21
  • Fix Trac #23.
  • Don't zonk types during typechecking (# .. #)
  • Fix Trac #31 by allowing reordering of kind variables.
  • Merge pull request Trac #36 from deepfire/nokinds
  • Comments only
  • Update installation instructions, thanks to Serge Kosyrev
  • README markdown formatting
  • Extend the flat-cache only with nom coercions
  • Add testcase from Trac #32
  • Fix other half of Trac #32
  • Tweak to Nix instructions
  • Tiny optimization in mkTcCoherenceLeftCo
  • Many levels of kinds test case
  • A goodly chunk of getting rid of co quantification
  • Finish removing coercion quantification.
  • Stage 1 compiles
  • Bugfixing
  • "base" builds
  • Stage 2 compiles
  • Add test from blog
  • Urk. We need to make (~) hetero again.
  • Make GADT equalities unboxed.
  • Bugfixing
  • Some more bugfixing. Good for HIW.
  • Merge branch 'nokinds' of ssh://github.com/goldfirere/ghc into nokinds
  • Need to solve constraints in sigs when not gen'ing
  • Fail less often when checking sigs
  • Support for dynamic paper
  • exactTyCoVarsOfType is now closed over kinds
  • occurCheckExpand must look into kinds, too.
  • Revert "One more analyzeType."
  • Revert "Fix compiler errors to analyzeType."
  • Revert "Further checkpoint in reducing import TyCoRep."
  • Revert "Checkpoint in reducing # of modules that import TyCoRep."
  • Finish removing analyzeType
  • Don't merge * and Constraint in instance matching
  • Remove kind roles.
  • New test for (C a, C b) => C (a b)
  • Fix tcGetGlobalTyCoVars, again
  • Checkpoint in simplifying forallco.
  • Undo changes to lifting algorithm
  • Simplify ForAllCo.
  • Remove comment obseleted by lack of kind roles
  • Comments only
  • Fix compilation on 7.8.3
  • Merge branch 'nokinds-dev' into nokinds
  • pprTraceIt, emit *unboxed* deriveds
  • Comments only
  • Unbox Deriveds; fix canDischarge
  • Formatting only
  • Be careful around dirtyTcCoToCo and Derived
  • Better debugging output
  • Start at removing eraseType
  • Finish removing type erasure.
  • Fix some syms
  • Add a missing .stderr
  • Comments only
  • Start of work toward coercion holes
  • Checkpoint in coercion holes
  • Another checkpoint in coercino holes
  • Finish? coercion holes
  • Stage 1 compiles.
  • Checkpoint in typechecking rules
  • Bugfixing. Still stuck on RULES
  • More RULE stuff. Don't optimize SubCo (UnivCo)
  • More bugfixing
  • Be lazier in TcHsSyn because of knots.
  • Typo
  • Remove a panic
  • Stage 2 compiles.
  • Better handling of locals with used_tcvs
  • Bugfixing
  • More bugfixing
  • Started abortive attempt to add pi (v :: Levity)
  • Remove notes about levity stuff
  • Start toward levity checking
  • checkpoint in parsing work
goldfire updated this revision to Diff 5200.Nov 18 2015, 10:50 PM

This version is working well. Next step: remove lifted equality
from the solver.

  • Parsing changes actually work. On the first shot.
  • Remove ITstar
  • Finish parser changes.
  • Checkpoint in various bugfixing
  • Remove buildCoherenceCo
  • Checkpoint. It's a bit borked.
  • More TypeInType stuff
  • Merge remote-tracking branch 'github/nokinds' into nokinds
goldfire updated this revision to Diff 5238.Nov 20 2015, 11:32 PM

Merged with master. Now: just need to work the testsuite
and address a few lingering TODOs.

Oh. and write the manual section.

  • Wibble in GHC.Types
  • Make (~) hetero.
  • Checkpoint in making ~ a class.
  • No more boxed equalities in solver.
  • Workin' the testsuite
  • Checkpoint in bugfixing
  • Be more careful about FVs in FloatIn
  • In a decent state now.
  • instance Typeable (a -> b)
  • Fix test case around *
  • Notes only.
  • Merge remote-tracking branch 'origin/master' into nokinds-dev
  • Restore separate functions for TcCoercions
  • Sequelae from TcCoercion stuff
  • A little cleaning
  • Define the mkTc function
  • Stage 1 compiles.
  • Stage 2 compiles
  • Merge branch 'nokinds' into nokinds-dev
goldfire updated this revision to Diff 5256.Nov 22 2015, 10:41 AM

Still WIP!

  • Checkpoint in bugfixing
  • Checkpoint in bugfixing
  • Better tracking of kinds v types
  • Workin' the testsuite
  • Implement bogus tycons. And other things.
  • Workin' the testsuite
  • Checkpoint; zonkCo zonks harder.
  • Workin' the testsuite.

@alanz, can you offer any advice on the notes below?

Thanks!

compiler/parser/Parser.y
1637

@alanz, I found this extra call to ams and left it as is. But I find it baffling. What is it doing? Should it be there? With the changes I've made around here, some of the ghc-api/annotations tests are failing, but I'm not sure whether I should accept the new output. Any advice?

compiler/parser/RdrHsSyn.hs
1066

As the comment says, I think this restructuring leaves behind an annotation for the ~ in the lazy marker behind. Is that a problem?

Made an inline comment on the annotations.

compiler/parser/Parser.y
1637

I think that under certain circumstances this type is split, and the AnnRarrow would go missing if it were not added to the first type. But it may just be an artefact.

I would be loathe to remove it, though.

This is the specific commit that brought in the extra AnnRarrow annotation

https://github.com/ghc/ghc/commit/2a0fb5d19500b7d9f0a595ebe08788b675258362

In D808#44427, @alanz wrote:

This is the specific commit that brought in the extra AnnRarrow annotation

https://github.com/ghc/ghc/commit/2a0fb5d19500b7d9f0a595ebe08788b675258362

Thanks -- that's helpful. When you have a chance, could you add a comment in the source code around there? Without any help, that extra annotation looks very very fishy.

Also, did you see my other inline comment in RdrHsSyn? I'm worried about a mistake there, too.

I did, but it is hard to comment without looking at the whole thing.

Currently checking out/compiling D808 so I can look properly

A more detailed response.

I presume there is a body of test code exercising these various features that can be used to check the identity transform in ghc-exactprint once this lands.

compiler/parser/Parser.y
1664

Why are tyapps located? they are only used in two places, and in both the location is removed.

1671

In the context of D1512 this will once more bring in an unlocated RdrName. I would prefer HsAppInfix to carry the Located RdrName instead.

compiler/parser/RdrHsSyn.hs
1066

The original AnnTilde is attached to loc, which is discarded in this case. If you move this function into the P monad you can re-attach it to the tilde_loc.

goldfire added inline comments.Nov 22 2015, 1:04 PM
compiler/parser/Parser.y
1664

To propagate the location upwards, for use in sLL and sL1. I believe it's necessary.

1671

OK. Will do.

compiler/parser/RdrHsSyn.hs
1066

But I don't think that any new annotation is needed, as the ~ goes from being special syntax to just a normal(-ish) type operator. To rephrase: is a stale annotation in the mapping troublesome? I didn't see any functions for removing a mapping, so I thought that it probably isn't.

alanz added inline comments.Nov 22 2015, 1:08 PM
compiler/parser/Parser.y
1671

And I would not be upset if HsAppPrefix carried a LHsType, but it is not critical, it just means a repacking of the type when processing it in ghc-exactprint

goldfire added inline comments.Nov 22 2015, 1:09 PM
compiler/parser/Parser.y
1671

I'm already in the midst of this change. It just made sense when changing HsAppInfix. And it's simplifying my code somewhat, so it's just a better design all around. Thanks.

alanz added inline comments.Nov 22 2015, 1:11 PM
compiler/parser/RdrHsSyn.hs
1066

ok, so eqTyCon_Rdr corresponds to '~', so does not need an annotation.

The disconnected annotation is not a problem, there are several other cases where it happens too. So this should be fine.

goldfire updated this revision to Diff 5263.Nov 22 2015, 11:22 PM

Fewer testcase failures!

  • Always use implic cts when deferring type errors
  • Checkpoint in testsuite work
  • Checkpoint. Refactored HsAppType a bit.
  • Get rid of atrocious boxity stuff
  • Optionally keep solving deriveds
  • Workin' the testsuite
  • Workin' the testsuite. Fix bug in unifier.
goldfire updated this revision to Diff 5348.Nov 29 2015, 12:05 AM

Finished full pass through testsuite, but now I clearly
need a second pass. On my machine, there are 62 unexpected
failures. I expect just about all of them to be output
wibbles. But I need help on a few points, as I will post
shortly.

  • Add TcTyMode, among other fixes.
  • Rewrite bindHsTyVars to check for types vs kinds
  • Checkpoint in telescope chicanery.
  • Removed skolem-capture stuff, as it's NMF.
  • Make ~ homo again; fix SetLevels bug.
  • Small simplification to Data.Type.Coercion
  • Workin' the testsuite.
  • Workin' the testsuite
  • Testsuite.
  • More testsuite. More testsuite.
  • Checkpoint
  • Remove kind error message
  • Checkpoint in working on TcTyCon
  • Testsuite complete?
  • More testsuite.
  • Comments.

This is lurching toward its goal. But I need a bit of help:

  • stranal/sigs/UnsatFun is failing. I haven't a clue what the output to this test case means and would be grateful for any assistance. (You can build from github.com/goldfirere/ghc.git on the nokinds-dev branch.)
  • typecheck/should_compile/T6018 is failing. I think this is a bug in the algorithm @simonpj wrote around derived constraints and injective type families. Brief overview: The problem is that we end up with s0 ~ s1 and s0 ~ s2 in the inert set, where we want to find s1 ~ s2. And, because we process deriveds last, the model doesn't get updated accordingly until the end, and then there isn't the right kick-out to re-process TF injectivity stuff.
  • typecheck/should_fail/T9999 and typecheck/should_fail/tcfail122 are failing with bad error messages. These messages lose helpful information, in comparison to HEAD. But I don't see an easy way to fix. Both are kind errors, say * -> * not matching with *. The problem is that I can't report what the types are that we're comparing. By the time the error is reported, the types have already been unified: the error report would say a |> <<coercion hole>> doesn't match with a, which is useless. (It doesn't say that by default. Enable -fprint-explicit-coercions to see the ugly output.) I don't know how to proceed.

There might be other spots I can't fix, but I tend to think not, at this point. Other than stranal/sigs/UnsatFun, for which I don't know the severity, none of the other problems should hold us up unduly. The error message degradation is regrettable (and I've sweated avoiding a similar fate in other scenarios) but not so bad that it's a showstopper.

This still has to rebase against the latest. But I'm going to nab more testcases first.

I think I solved the T6018 problem. It turns out that there was an eensy-weensy bug in simplifyInfer which triggered very rarely. I just rebuilt all the core libraries as a test-run, and the error triggered somewhere in there. It was a much simpler test case and I was able to figure out what was wrong.

goldfire updated this revision to Diff 5587.Dec 9 2015, 1:09 PM

Working on a few validation bugs.

  • Address some TODOs. Remove HCoercible.
  • More TODOs.
  • Use runTcSDerived after toDerivedWC
  • More TODOs. Simplify Unify algorithm as per SPJ.
  • Be more careful when zonking.
  • More TODOs.
  • More TODO stuff
  • Checkpoint.
  • Remove old code dealing with hetero eqs.
  • Get AmapCoerce to work. Finally.
  • Merge remote-tracking branch 'origin/master' into nokinds-dev
  • Sequelae from merge.
  • Stage 1 compiles; fix bug in Unify
  • Stage 2 compiles.
  • Testsuite wibbles.
  • Actually fix unify bug.
  • Fix Unify fix.
  • Merge remote-tracking branch 'origin/master' into nokinds-dev
  • Stage 1 compiles.
  • Stage 2 compiles.
  • Print phantom kind coercions
  • Remove calls to coercionKind that slow us down.
  • Specialise mapType/mapCoercion
  • Use -fprint-explicit-coercions even in HsSyn
  • Restore mkKindCo optimisation
  • Zonk carefully in canEqNC
  • Skip eager refl check for non-flat types
  • Fix coercionKind recursion
  • Coercion destructor optimizations
  • Optimize (* ~ *)
  • Comments only
  • Merge remote-tracking branch 'origin/master' into nokinds-dev
  • Stage 1 compiles
  • Few small bugs
  • Stage 2 compiles
  • Fix renaming bug
  • Don't solve hetero wanteds.
  • Bugfix around TcLevel invariant
  • Bugfixing
  • Compile haddock/with 7.8. Submodule update.
  • Bugfixing
  • More zonking.
  • Merge pull request Trac #61 from bgamari/nokinds-dev
  • Fix warnings when bootstrapping from 7.8
  • Always put deferred type errs in an EvBindsVar
  • Comments; fix mkGADTVars
  • Bind a telescope properly in TcHsType
  • Don't confuse funtys and foralltys in DmdAnal
  • Restore old behavior of splitForAllTy
thomie added inline comments.Dec 9 2015, 6:06 PM
compiler/parser/ApiAnnotation.hs
256

Is this removal of AnnStar etc. intentional? They were just added in D1473 by @alanz. But maybe you already discussed this.

testsuite/tests/typecheck/should_fail/T7857.hs
1 ↗(On Diff #5348)

FlexibleContexts doesn't seem necessary, at least in my testing.

testsuite/tests/typecheck/should_fail/T9260.stderr
5

Please double check this change in error message. Note:

  • Expected and Actual are interchanged.
  • Fin is no longer mentioned.
hvr requested changes to this revision.Dec 10 2015, 1:29 AM

Can we please avoid adding/updating un-compressible/un-xdiffable binary files into ghc.git?

core-spec.pdf should never have been committed into ghc.git into the first place.

If we really must, adding the intermediate .tex files generated by ott into Git would be far more tolerable, as those are compressible and diff-able way better than a pdf

This revision now requires changes to proceed.Dec 10 2015, 1:29 AM
thomie requested changes to this revision.Dec 10 2015, 2:43 AM
thomie added a reviewer: thomie.

Please see my previous comment: https://phabricator.haskell.org/D808#47093

And I like @hvr's suggestion to switch to committing the .tex file instead of the .pdf. I do know that committing generated files is a no-no, but didn't consider this middle path. Will do.

Thanks, both, for the suggestions.

compiler/parser/ApiAnnotation.hs
256

Yes. There is no need for * to have special treatment in lexing/parsing any more. Or rather, there is, but it's impossible for the lexer/parser to be able to do the special treatment. So this bit is now done in the renamer, where we have enough info to do the right thing. But in any case, no need for this token.

testsuite/tests/typecheck/should_fail/T9260.stderr
5

Well spotted! I guess I missed the change in ordering. Fixed now.

goldfire updated this revision to Diff 5596.Dec 11 2015, 12:24 AM

Posting to get performance validation numbers.
I have no non-performance failures on my machine right now.
Going to rebase against master.

  • Rejig rejigConRes to do the right thing
  • Merge pull request Trac #62 from bgamari/nokinds-dev
  • Fix nasty nasty mdo bug
  • Align expected/actual
  • Some testsuite stuff
  • Restore kind coercions in Unify algorithm
  • Kick out by coercion hole
  • Revert "Kick out by coercion hole"
  • Revert "Don't solve hetero wanteds."
  • More bugfixing
  • Remove outdated lint check
  • Fix telescope checking
  • Finish? scope checking
  • Compile with 7.8
  • Remove debugging output; testsuite
  • More testsuite. Fix Trac #63.
  • Fix assoc type defaults; bits & bobs.
  • Get OptCoercion to compile.
  • Reverted to rejigged datacon wrappers.
  • Don't drop case expressions over any unlifted type
  • Fix splitForAllTys goof in RtClosureInspect
  • Testsuite wibble
  • Testsuite.
  • Testsuite wibbles.
alanz added inline comments.Dec 11 2015, 12:38 AM
compiler/parser/ApiAnnotation.hs
256

In that case, whichever token does carry the '*' will have to carry a SourceText, so that we can retain the original text for the unicode variant, or we will have to bring ITStar back, and just add another parser rule to make it the same as the current token, but with the annotation added.

If you like I can prepare a patch against your current branch to do this.

goldfire updated this revision to Diff 5597.Dec 11 2015, 12:44 AM

Rebased against master. Could this be the last update?

  • Merge remote-tracking branch 'origin/master' into nokinds-dev
  • tiny fix
goldfire added inline comments.Dec 11 2015, 12:46 AM
compiler/parser/ApiAnnotation.hs
256

Shouldn't be necessary. * and <<unicode star>> are just normal identifiers now. They're exported from Data.Kind. So there really shouldn't be any weird interactions here.

Bah. So Harbormaster won't validate. It (quite sensibly) can't find my haddock update.

I tried to push to the haddock repo at git.haskell.org on a branch wip/rae-nokinds but that was rejected by a hook, with no explanation. Can anyone help? Currently, my haddock commit is at github.com/goldfirere/haddock.git on the wip/rae-nokinds branch (but you shouldn't need the branch name, due to submodule magic).

It would be lovely if someone could convince Harbormaster to validate before I wake up. I truly hope just to adjust performance numbers and merge. I'll then post several tickets tracking the few remaining loose ends (a few error message regressions, slightly more eager deferred type errors, performance).

Thanks.

@alanz told me where to point haddock. Validating now.

goldfire updated this revision to Diff 5606.Dec 11 2015, 9:20 AM

Adjusted performance numbers. Also see Trac #11196 which tracks
performance problems.

  • Write a missing Note
  • Testsuite wibbles.
  • Update perf numbers
thomie resigned from this revision.Dec 11 2015, 2:31 PM
thomie removed a reviewer: thomie.

Thanks.

goldfire updated this revision to Diff 5618.Dec 11 2015, 3:28 PM

Fixed testsuite failures. ?

  • Testsuite wibbles.
  • Label things as broken from Trac #11203
  • Testsuite wibble.
  • Case fixing.
  • Finish case fixing
bgamari commandeered this revision.Dec 11 2015, 6:54 PM
bgamari edited reviewers, added: goldfire; removed: bgamari.

This has landed as 6746549772c5cc0ac66c0fce562f297f4d4b80a2. Abandoning.

bgamari abandoned this revision.Dec 11 2015, 6:54 PM