Matthew Pickering authored 3 years ago and Marge Bot committed 3 years ago

Note [Tidying multiple names at once] indicates that if multiple
variables have the same name then we shouldn't prioritise one of them
and instead rename them all to a1, a2, a3... etc

This patch implements that change, some error message changes as
expected.

Closes #20932

Summary:
This patch implements visible kind application (GHC Proposal 15/#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.

There are a few remaining issues with this patch, as documented in
ticket #16082.

Includes a submodule update for Haddock.

Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a

Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack

Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter

GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816`

Differential Revision: https://phabricator.haskell.org/D5229

TcSimplify.decideQuantification was doing the Wrong Thing when
"growing" the type variables to quantify over. We were trying to do
this on a tyvar set where we'd split off the dependent type varaibles;
and we just got it wrong.  A kind variable wasn't being generalised
properly, with confusing knock on consequences.

All this led to Trac #13371 and Trac #13393.

This commit tidies it all up:

* The type TcDepVars is renamed as CandidateQTvs;
  and splitDepVarsOfType to candidateQTyVarsOfType

* The code in TcSimplify.decideQuantification is simpler.
  It no longer does the tricky "grow" stuff over TcDepVars.
  Instead it use ordinary VarSets (thereby eliminating the
  nasty growThetaTyVarsDSet) and uses that to filter the
  result of candidateQTyVarsOfType.

* I documented that candidateQTyVarsOfType returns the type
  variables in a good order in which to quantify, and rewrote
  it to use an accumulator pattern, so that we would predicatably
  get left-to-right ordering.

In doing all this I also made UniqDFM behave a little more nicely:

* When inserting an element that is there already, keep the old tag,
  while still overwriting with the new value.

* This means that when doing udfmToList we get back elements in the
  order they were originally inserted, rather than in reverse order.

It's not a big deal, but in a subsequent commit I use it to improve
the order of type variables in inferred types.

All this led to a lot of error message wibbles:
 - changing the order of quantified variables
 - changing the order in which instances are listed in GHCi
 - changing the tidying of variables in typechecker erors

There's a submodule update for 'array' because one of its tests
has an error-message change.

I may not have associated all of them with the correct commit.

This patch does a raft of useful tidy-ups in the type checker.
I've been meaning to do this for some time, and finally made
time to do it en route to ICFP.

1. Modify TcType.ExpType to make a distinct data type,
   InferResult for the Infer case, and consequential
   refactoring.

2. Define a new function TcUnify.fillInferResult, to fill in
   an InferResult. It uses TcMType.promoteTcType to promote
   the type to the level of the InferResult.
   See TcMType Note [Promoting a type]
   This refactoring is in preparation for an improvement
   to typechecking pattern bindings, coming next.

   I flirted with an elaborate scheme to give better
   higher rank inference, but it was just too complicated.
   See TcMType Note [Promotion and higher rank types]

3. Add to InferResult a new field ir_inst :: Bool to say
   whether or not the type used to fill in the
   InferResult should be deeply instantiated.  See
   TcUnify Note [Deep instantiation of InferResult].

4. Add a TcLevel to SkolemTvs. This will be useful generally

    - it's a fast way to see if the type
      variable escapes when floating (not used yet)

    - it provides a good consistency check when updating a
      unification variable (TcMType.writeMetaTyVarRef, the
      level_check_ok check)

   I originally had another reason (related to the flirting
   in (2), but I left it in because it seems like a step in
   the right direction.

5. Reduce and simplify the plethora of uExpType,
   tcSubType and related functions in TcUnify.  It was
   such an opaque mess and it's still not great, but it's
   better.

6. Simplify the uo_expected field of TypeEqOrigin.  Richard
   had generatlised it to a ExpType, but it was almost always
   a Check type.  Now it's back to being a plain TcType which
   is much, much easier.

7. Improve error messages by refraining from skolemisation when
   it's clear that there's an error: see
   TcUnify Note [Don't skolemise unnecessarily]

8. Type.isPiTy and isForAllTy seem to be missing a coreView check,
   so I added it

9. Kill off tcs_used_tcvs.  Its purpose is to track the
   givens used by wanted constraints.  For dictionaries etc
   we do that via the free vars of the /bindings/ in the
   implication constraint ic_binds.  But for coercions we
   just do update-in-place in the type, rather than
   generating a binding.  So we need something analogous to
   bindings, to track what coercions we have added.

   That was the purpose of tcs_used_tcvs.  But it only
   worked for a /single/ iteration, whereas we may have
   multiple iterations of solving an implication.  Look
   at (the old) 'setImplicationStatus'.  If the constraint
   is unsolved, it just drops the used_tvs on the floor.
   If it becomes solved next time round, we'll pick up
   coercions used in that round, but ignore ones used in
   the first round.

   There was an outright bug.  Result = (potentialy) bogus
   unused-constraint errors.  Constructing a case where this
   actually happens seems quite trick so I did not do so.

   Solution: expand EvBindsVar to include the (free vars of
   the) coercions, so that the coercions are tracked in
   essentially the same way as the bindings.

   This turned out to be much simpler.  Less code, more
   correct.

10. Make the ic_binds field in an implication have type
      ic_binds :: EvBindsVar
    instead of (as previously)
       ic_binds :: Maybe EvBindsVar
    This is notably simpler, and faster to use -- less
    testing of the Maybe.  But in the occaional situation
    where we don't have anywhere to put the bindings, the
    belt-and-braces error check is lost.  So I put it back
    as an ASSERT in 'setImplicationStatus' (see the use of
    'termEvidenceAllowed')

All these changes led to quite bit of error message wibbling

This major commit was initially triggered by #11339, but it spiraled
into a major review of the way in which type signatures for bindings
are handled, especially partial type signatures.  On the way I fixed a
number of other bugs, namely
   #12069
   #12033
   #11700
   #11339
   #11670

The main change is that I completely reorganised the way in which type
signatures in bindings are handled. The new story is in TcSigs
Note [Overview of type signatures].  Some specific:

* Changes in the data types for signatures in TcRnTypes:
  TcIdSigInfo and new TcIdSigInst

* New module TcSigs deals with typechecking type signatures
  and pragmas. It contains code mostly moved from TcBinds,
  which is already too big

* HsTypes: I swapped the nesting of HsWildCardBndrs
  and HsImplicitBndsrs, so that the wildcards are on the
  oustide not the insidde in a LHsSigWcType.  This is just
  a matter of convenient, nothing deep.

There are a host of other changes as knock-on effects, and
it all took FAR longer than I anticipated :-).  But it is
a significant improvement, I think.

Lots of error messages changed slightly, some just variants but
some modest improvements.

New tests

* typecheck/should_compile
    * SigTyVars: a scoped-tyvar test
    * ExPat, ExPatFail: existential pattern bindings
    * T12069
    * T11700
    * T11339

* partial-sigs/should_compile
    * T12033
    * T11339a
    * T11670

One thing to check:

* Small change to output from ghc-api/landmines.
  Need to check with Alan Zimmerman

varSetElemsWellScoped introduces unnecessary non-determinism in
inferred type signatures.
Removing this instance required changing the representation of
TcDepVars to use deterministic sets.
This is the last occurence of varSetElemsWellScoped, allowing me to
finally remove it.

Test Plan:
./validate
I will update the expected outputs when commiting, some reordering
of type variables in types is expected.

Reviewers: goldfire, simonpj, austin, bgamari

Reviewed By: simonpj

Subscribers: thomie, simonmar

Differential Revision: https://phabricator.haskell.org/D2135

GHC Trac Issues: #4012

barrucadu authored 9 years ago and Herbert Valerio Riedel committed 9 years ago

Both gcc and clang tell which warning flag a reported warning can be
controlled with, this patch makes ghc do the same. More generally, this
allows for annotated compiler output, where an optional annotation is
displayed in brackets after the severity.

This also adds a new flag `-f(no-)show-warning-groups` to control
whether to show which warning-group (such as `-Wall` or `-Wcompat`)
a warning belongs to. This flag is on by default.

This implements #10752

Reviewed By: quchen, bgamari, hvr

Differential Revision: https://phabricator.haskell.org/D1943

The idea here is described in [wiki:Typechecker]. Briefly,
this refactor keeps solid track of "synthesis" mode vs
"checking" in GHC's bidirectional type-checking algorithm.
When in synthesis mode, the expected type is just an IORef
to write to.

In addition, this patch does a significant reworking of
RebindableSyntax, allowing much more freedom in the types
of the rebindable operators. For example, we can now have
`negate :: Int -> Bool` and
`(>>=) :: m a -> (forall x. a x -> m b) -> m b`. The magic
is in tcSyntaxOp.

This addresses tickets #11397, #11452, and #11458.

Tests:
  typecheck/should_compile/{RebindHR,RebindNegate,T11397,T11458}
  th/T11452

This re-working of the typechecker algorithm is based on
the paper "Visible type application", by Richard Eisenberg,
Stephanie Weirich, and Hamidhasan Ahmed, to be published at
ESOP'16.

This patch introduces -XTypeApplications, which allows users
to say, for example `id @Int`, which has type `Int -> Int`. See
the changes to the user manual for details.

This patch addresses tickets #10619, #5296, #10589.

This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).

There are several noteworthy changes with this patch:
 * We now have casts in types. These change the kind
   of a type. See new constructor `CastTy`.

 * All types and all constructors can be promoted.
   This includes GADT constructors. GADT pattern matches
   take place in type family equations. In Core,
   types can now be applied to coercions via the
   `CoercionTy` constructor.

 * Coercions can now be heterogeneous, relating types
   of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
   proves both that `t1` and `t2` are the same and also that
   `k1` and `k2` are the same.

 * The `Coercion` type has been significantly enhanced.
   The documentation in `docs/core-spec/core-spec.pdf` reflects
   the new reality.

 * The type of `*` is now `*`. No more `BOX`.

 * Users can write explicit kind variables in their code,
   anywhere they can write type variables. For backward compatibility,
   automatic inference of kind-variable binding is still permitted.

 * The new extension `TypeInType` turns on the new user-facing
   features.

 * Type families and synonyms are now promoted to kinds. This causes
   trouble with parsing `*`, leading to the somewhat awkward new
   `HsAppsTy` constructor for `HsType`. This is dispatched with in
   the renamer, where the kind `*` can be told apart from a
   type-level multiplication operator. Without `-XTypeInType` the
   old behavior persists. With `-XTypeInType`, you need to import
   `Data.Kind` to get `*`, also known as `Type`.

 * The kind-checking algorithms in TcHsType have been significantly
   rewritten to allow for enhanced kinds.

 * The new features are still quite experimental and may be in flux.

 * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.

 * TODO: Update user manual.

Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.

This patch began as a modest refactoring of HsType and friends, to
clarify and tidy up exactly where quantification takes place in types.
Although initially driven by making the implementation of wildcards more
tidy (and fixing a number of bugs), I gradually got drawn into a pretty
big process, which I've been doing on and off for quite a long time.

There is one compiler performance regression as a result of all
this, in perf/compiler/T3064.  I still need to look into that.

* The principal driving change is described in Note [HsType binders]
  in HsType.  Well worth reading!

* Those data type changes drive almost everything else.  In particular
  we now statically know where

       (a) implicit quantification only (LHsSigType),
           e.g. in instance declaratios and SPECIALISE signatures

       (b) implicit quantification and wildcards (LHsSigWcType)
           can appear, e.g. in function type signatures

* As part of this change, HsForAllTy is (a) simplified (no wildcards)
  and (b) split into HsForAllTy and HsQualTy.  The two contructors
  appear when and only when the correponding user-level construct
  appears.  Again see Note [HsType binders].

  HsExplicitFlag disappears altogether.

* Other simplifications

     - ExprWithTySig no longer needs an ExprWithTySigOut variant

     - TypeSig no longer needs a PostRn name [name] field
       for wildcards

     - PatSynSig records a LHsSigType rather than the decomposed
       pieces

     - The mysterious 'GenericSig' is now 'ClassOpSig'

* Renamed LHsTyVarBndrs to LHsQTyVars

* There are some uninteresting knock-on changes in Haddock,
  because of the HsSyn changes

I also did a bunch of loosely-related changes:

* We already had type synonyms CoercionN/CoercionR for nominal and
  representational coercions.  I've added similar treatment for

      TcCoercionN/TcCoercionR

      mkWpCastN/mkWpCastN

  All just type synonyms but jolly useful.

* I record-ised ForeignImport and ForeignExport

* I improved the (poor) fix to Trac #10896, by making
  TcTyClsDecls.checkValidTyCl recover from errors, but adding a
  harmless, abstract TyCon to the envt if so.

* I did some significant refactoring in RnEnv.lookupSubBndrOcc,
  for reasons that I have (embarrassingly) now totally forgotten.
  It had to do with something to do with import and export

Updates haddock submodule.

elaforge authored 9 years ago and Ben Gamari committed 9 years ago

This puts the "Relevant bindings" section at the end.

It uses a TcErrors.Report Monoid to divide messages by importance and
then mappends them together.  This is not the most efficient way since
there are various intermediate Reports and list appends, but it probably
doesn't matter since error messages shouldn't get that large, and are
usually prepended.  In practice, everything is `important` except
`relevantBindings`, which is `supplementary`.

ErrMsg's errMsgShortDoc and errMsgExtraInfo were extracted into ErrDoc,
which has important, context, and suppelementary fields.  Each of those
three sections is marked with a bullet character, '•' on unicode
terminals and '*' on ascii terminals.  Since this breaks tons of tests,
I also modified testlib.normalise_errmsg to strip out '•'s.

--- Additional notes:

To avoid prepending * to an empty doc, I needed to filter empty docs.
This seemed less error-prone than trying to modify everyone who produces
SDoc to instead produce Maybe SDoc.  So I added `Outputable.isEmpty`.
Unfortunately it needs a DynFlags, which is kind of bogus, but otherwise
I think I'd need another Empty case for SDoc, and then it couldn't be a
newtype any more.

ErrMsg's errMsgShortString is only used by the Show instance, which is
in turn only used by Show HscTypes.SourceError, which is in turn only
needed for the Exception instance.  So it's probably possible to get rid
of errMsgShortString, but that would a be an unrelated cleanup.

Fixes #11014.

Test Plan: see above

Reviewers: austin, simonpj, thomie, bgamari

Reviewed By: thomie, bgamari

Subscribers: simonpj, nomeata, thomie

Differential Revision: https://phabricator.haskell.org/D1427

GHC Trac Issues: #11014

When examining #10615, I found the wildcard handling hard
to understand.  This patch refactors quite a bit, but with
no real change in behaviour.

 * Split out TcIdSigInfo from TcSigInfo, as a separate type,
   like TcPatSynInfo.

 * Make TcIdSigInfo express more invariants by pushing the
   wildard info into TcIdSigBndr

 * Remove all special treatment of unification variables that arise
   from wildcards; so the TauTv of TcType.MetaInfo loses its Bool
   argument.

A ton of konck on changes.  The result is significantly simpler, I think.

Adopts sugggestion in Trac #10224, comment:3

The patch "Treat out-of-scope variables as holes" makes
lots of error messages change a bit. This patch has all
the change.