Track type variable scope more carefully.

Authored by goldfire on Sep 29 2017, 10:22 AM.


Trac Issues
The main job of this commit is to track more accurately the scope
 of tyvars introduced by user-written foralls. For example, it would
 be to have something like this:
   forall a. Int -> (forall k (b :: k). Proxy '[a, b]) -> Bool
 In that type, a's kind must be k, but k isn't in scope. We had a
 terrible way of doing this before (not worth repeating or describing
 here, but see the old tcImplicitTKBndrs and friends), but now
 we have a principled approach: make an Implication when kind-checking
 a forall. Doing so then hooks into the existing machinery for
 preventing skolem-escape, performing floating, etc. This also means
 that we bump the TcLevel whenever going into a forall.
 The new behavior is done in TcHsType.scopeTyVars, but see also{Im,Ex}plicitTKBndrs, which have undergone significant
 rewriting. There are several Notes near there to guide you. Of
 particular interest there is that Implication constraints can now
 have skolems that are out of order; this situation is reported in
 A major consequence of this is a slightly tweaked process for type-
 checking type declarations. The new Note [Use SigTvs in kind-checking
 pass] in TcTyClsDecls lays it out.
 The error message for dependent/should_fail/TypeSkolEscape has become
 noticeably worse. However, this is because the code in TcErrors goes to
 some length to preserve pre-8.0 error messages for kind errors. It's time
 to rip off that plaster and get rid of much of the kind-error-specific
 error messages. I tried this, and doing so led to a lovely error message
 for TypeSkolEscape. So: I'm accepting the error message quality regression
 for now, but will open up a new ticket to fix it, along with a larger
 error-message improvement I've been pondering. This applies also to
 dependent/should_fail/{BadTelescope2,T14066,T14066e}, polykinds/T11142.
 Other minor changes:
  - isUnliftedTypeKind didn't look for tuples and sums. It does now.
  - check_type used check_arg_type on both sides of an AppTy. But the left
    side of an AppTy isn't an arg, and this was causing a bad error message.
    I've changed it to use check_type on the left-hand side.
  - Some refactoring around when we print (TYPE blah) in error messages.
    The changes decrease the times when we do so, to good effect.
    Of course, this is still all controlled by
 Fixes #14066 #14749
 Test cases: dependent/should_compile/{T14066a,T14749},
goldfire created this revision.Sep 29 2017, 10:22 AM
bgamari requested changes to this revision.Oct 3 2017, 10:10 AM

Bumping out of review queue.

This revision now requires changes to proceed.Oct 3 2017, 10:10 AM
goldfire updated this revision to Diff 14533.Nov 1 2017, 10:17 PM

The big new thing in this version is TcSimplify.solveLocalEqualities,
which seems right but could use review. Otherwise, continuing to
fix bugs...

bgamari requested changes to this revision.Nov 2 2017, 10:57 AM

Alright, bumping out of review queue again.

This revision now requires changes to proceed.Nov 2 2017, 10:57 AM
austin resigned from this revision.Nov 9 2017, 5:40 PM
goldfire updated this revision to Diff 14896.Dec 7 2017, 10:16 AM

Checkpoint for live review. More comments coming at some point!

goldfire updated this revision to Diff 15546.Feb 23 2018, 8:11 AM

Final (?) revision. Posting for validation and final review.

goldfire retitled this revision from Bump TcLevel when introducing type variables to Track type variable scope more carefully..Feb 23 2018, 8:12 AM
goldfire edited the summary of this revision. (Show Details)
goldfire updated this revision to Diff 15547.Feb 23 2018, 8:15 AM

Oops. Forgot to commit the last few bits.

simonpj accepted this revision.Feb 27 2018, 5:23 AM

Big patch! I skimmed only.

One thing: could you add a Note for the entire solveEqualities, idea? There are quite a few moving parts and an overview would be good.


This is an unrelated fix to the pretty-printer. Mention in commit message.


Why did this type change? Comment?


What's the difference between the two? I think a bit more explanation would help -- and then refer to this note elsewhere


Refer to the Note explaining the difference


What's going on with this TyConSkol thing?


Refer to the Note explaining the difference


Refer to the Note explaining the difference


Interesting. What happened to errors_as_warns?


Interesting. Why didn't we need this before?


Do you really need this? Why? Seems jolly odd.


"above"? where above? I think you mean the comments on the fields of EvBindsVar.


Check other uses of promotion (eg in TcSimplify) which might use this.


Refer to Note explaining difference


Aha -- helpful comment. I wonder about a type

type TcCastedTyVar = TcType   -- a tyvar or tyvar |> co

Maybe useful in other places!


I'm happy to see this covar code disappear!

Is there an invariant that we can say here -- that covars can't occur, somehow?




Why do we now need this associated flag?