GitLab

Due to the way `DerivEnv` is currently structured, there is an
invariant that every derived instance must consist of a class applied
to a non-empty list of argument types, where the last argument *must*
be an application of a type constructor to some arguments. This works
for many cases, but there are also some design patterns in standalone
`anyclass`/`via` deriving that are made impossible due to enforcing
this invariant, as documented in #13154.

This fixes #13154 by refactoring `TcDeriv` and friends to perform
fewer validity checks when using the `anyclass` or `via` strategies.
The highlights are as followed:

* Five fields of `DerivEnv` have been factored out into a new
  `DerivInstTys` data type. These fields only make sense for
  instances that satisfy the invariant mentioned above, so
  `DerivInstTys` is now only used in `stock` and `newtype` deriving,
  but not in other deriving strategies.
* There is now a `Note [DerivEnv and DerivSpecMechanism]` describing
  the bullet point above in more detail, as well as explaining the
  exact requirements that each deriving strategy imposes.
* I've refactored `mkEqnHelp`'s call graph to be slightly less
  complicated. Instead of the previous `mkDataTypeEqn`/`mkNewTypeEqn`
  dichotomy, there is now a single entrypoint `mk_eqn`.
* Various bits of code were tweaked so as not to use fields that are
  specific to `DerivInstTys` so that they may be used by all deriving
  strategies, since not all deriving strategies use `DerivInstTys`.

This introduces three new modules:

 - basicTypes/Predicate.hs describes predicates, moving
   this logic out of Type. Predicates don't really exist
   in Core, and so don't belong in Type.

 - typecheck/TcOrigin.hs describes the origin of constraints
   and types. It was easy to remove from other modules and
   can often be imported instead of other, scarier modules.

 - typecheck/Constraint.hs describes constraints as used in
   the solver. It is taken from TcRnTypes.

No work other than module splitting is in this patch.

This is the first step toward homogeneous equality, which will
rely more strongly on predicates. And homogeneous equality is the
next step toward a dependently typed core language.

The latest installment in my quest to clean up the code in
`TcDeriv*`. This time, my sights are set on
`TcDerivInfer.inferConstraints`, which infers the context for derived
instances. This function is a wee bit awkward at the moment:

* It's not terribly obvious from a quick glance, but
  `inferConstraints` is only ever invoked when using the `stock` or
  `anyclass` deriving strategies, as the code for inferring the
  context for `newtype`- or `via`-derived instances is located
  separately in `mk_coerce_based_eqn`. But there's no good reason
  for things to be this way, so I moved this code from
  `mk_coerce_based_eqn` to `inferConstraints` so that everything
  related to inferring instance contexts is located in one place.
* In this process, I discovered that the Haddocks for the auxiliary
  function `inferConstraintsDataConArgs` are completely wrong. It
  claims that it handles both `stock` and `newtype` deriving, but
  this is completely wrong, as discussed above—it only handles
  `stock`. To rectify this, I renamed this function to
  `inferConstraintsStock` to reflect its actual purpose and created
  a new `inferConstraintsCoerceBased` function to specifically
  handle `newtype` (and `via`) deriving.

Doing this revealed some opportunities for further simplification:

* Removing the context-inference–related code from
  `mk_coerce_based_eqn` made me realize that the overall structure
  of the function is basically identical to `mk_originative_eqn`.
  In fact, I was easily able to combine the two functions into a
  single `mk_eqn_from_mechanism` function.

  As part of this merger, I now invoke
  `atf_coerce_based_error_checks` from `doDerivInstErrorChecks1`.
* I discovered that GHC defined this function:

  ```hs
  typeToTypeKind = liftedTypeKind `mkVisFunTy` liftedTypeKind
  ```

  No fewer than four times in different modules. I consolidated all
  of these definitions in a single location in `TysWiredIn`.

This moves all URL references to Trac tickets to their corresponding
GitLab counterparts.

The big payload of this patch is:

  Add an AnonArgFlag to the FunTy constructor
  of Type, so that
    (FunTy VisArg   t1 t2) means (t1 -> t2)
    (FunTy InvisArg t1 t2) means (t1 => t2)

The big payoff is that we have a simple, local test to make
when decomposing a type, leading to many fewer calls to
isPredTy. To me the code seems a lot tidier, and probably
more efficient (isPredTy has to take the kind of the type).

See Note [Function types] in TyCoRep.

There are lots of consequences

* I made FunTy into a record, so that it'll be easier
  when we add a linearity field, something that is coming
  down the road.

* Lots of code gets touched in a routine way, simply because it
  pattern matches on FunTy.

* I wanted to make a pattern synonym for (FunTy2 arg res), which
  picks out just the argument and result type from the record. But
  alas the pattern-match overlap checker has a heart attack, and
  either reports false positives, or takes too long.  In the end
  I gave up on pattern synonyms.

  There's some commented-out code in TyCoRep that shows what I
  wanted to do.

* Much more clarity about predicate types, constraint types
  and (in particular) equality constraints in kinds.  See TyCoRep
  Note [Types for coercions, predicates, and evidence]
  and Note [Constraints in kinds].

  This made me realise that we need an AnonArgFlag on
  AnonTCB in a TyConBinder, something that was really plain
  wrong before. See TyCon Note [AnonTCB InivsArg]

* When building function types we must know whether we
  need VisArg (mkVisFunTy) or InvisArg (mkInvisFunTy).
  This turned out to be pretty easy in practice.

* Pretty-printing of types, esp in IfaceType, gets
  tidier, because we were already recording the (->)
  vs (=>) distinction in an ad-hoc way.  Death to
  IfaceFunTy.

* mkLamType needs to keep track of whether it is building
  (t1 -> t2) or (t1 => t2).  See Type
  Note [mkLamType: dictionary arguments]

Other minor stuff

* Some tidy-up in validity checking involving constraints;
  Trac #16263

In the type checker Constraint and * are distinct; and the function
that takes the kind of a type should respect that distinction
(Trac #15971).

This patch implements the change:

* Introduce Type.tcTypeKind, and use it throughout the type
  inference engine

* Add new Note [Kinding rules for types] for the kinding
  rules, especially for foralls.

* Redefine
    isPredTy ty = tcIsConstraintKind (tcTypeKind ty)
  (it had a much more complicated definition before)

Some miscellaneous refactoring

* Get rid of TyCoRep.isTYPE, Kind.isTYPEApp,
  in favour of TyCoRep.kindRep, kindRep_maybe

* Rename Type.getRuntimeRepFromKind_maybe
  to getRuntimeRep_maybe

I did some spot-checks on compiler perf, and it really doesn't
budge (as expected).

My original goal was (Trac #15809) to move towards using level numbers
as the basis for deciding which type variables to generalise, rather
than searching for the free varaibles of the environment.  However
it has turned into a truly major refactoring of the kind inference
engine.

Let's deal with the level-numbers part first:

* Augment quantifyTyVars to calculate the type variables to
  quantify using level numbers, and compare the result with
  the existing approach.  That is; no change in behaviour,
  just a WARNing if the two approaches give different answers.

* To do this I had to get the level number right when calling
  quantifyTyVars, and this entailed a bit of care, especially
  in the code for kind-checking type declarations.

* However, on the way I was able to eliminate or simplify
  a number of calls to solveEqualities.

This work is incomplete: I'm not /using/ level numbers yet.
When I subsequently get rid of any remaining WARNings in
quantifyTyVars, that the level-number answers differ from
the current answers, then I can rip out the current
"free vars of the environment" stuff.

Anyway, this led me into deep dive into kind inference for type and
class declarations, which is an increasingly soggy part of GHC.
Richard already did some good work recently in

   commit 5e45ad10
   Date:   Thu Sep 13 09:56:02 2018 +0200

    Finish fix for #14880.

    The real change that fixes the ticket is described in
    Note [Naughty quantification candidates] in TcMType.

but I kept turning over stones. So this patch has ended up
with a pretty significant refactoring of that code too.

Kind inference for types and classes
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

* Major refactoring in the way we generalise the inferred kind of
  a TyCon, in kcTyClGroup.  Indeed, I made it into a new top-level
  function, generaliseTcTyCon.  Plus a new Note to explain it
  Note [Inferring kinds for type declarations].

* We decided (Trac #15592) not to treat class type variables specially
  when dealing with Inferred/Specified/Required for associated types.
  That simplifies things quite a bit. I also rewrote
  Note [Required, Specified, and Inferred for types]

* Major refactoring of the crucial function kcLHsQTyVars:
  I split it into
       kcLHsQTyVars_Cusk  and  kcLHsQTyVars_NonCusk
  because the two are really quite different. The CUSK case is
  almost entirely rewritten, and is much easier because of our new
  decision not to treat the class variables specially

* I moved all the error checks from tcTyClTyVars (which was a bizarre
  place for it) into generaliseTcTyCon and/or the CUSK case of
  kcLHsQTyVars.  Now tcTyClTyVars is extremely simple.

* I got rid of all the all the subtleties in tcImplicitTKBndrs. Indeed
  now there is no difference between tcImplicitTKBndrs and
  kcImplicitTKBndrs; there is now a single bindImplicitTKBndrs.
  Same for kc/tcExplicitTKBndrs.  None of them monkey with level
  numbers, nor build implication constraints.  scopeTyVars is gone
  entirely, as is kcLHsQTyVarBndrs. It's vastly simpler.

  I found I could get rid of kcLHsQTyVarBndrs entirely, in favour of
  the bnew bindExplicitTKBndrs.

Quantification
~~~~~~~~~~~~~~
* I now deal with the "naughty quantification candidates"
  of the previous patch in candidateQTyVars, rather than in
  quantifyTyVars; see Note [Naughty quantification candidates]
  in TcMType.

  I also killed off closeOverKindsCQTvs in favour of the same
  strategy that we use for tyCoVarsOfType: namely, close over kinds
  at the occurrences.

  And candidateQTyVars no longer needs a gbl_tvs argument.

* Passing the ContextKind, rather than the expected kind itself,
  to tc_hs_sig_type_and_gen makes it easy to allocate the expected
  result kind (when we are in inference mode) at the right level.

Type families
~~~~~~~~~~~~~~
* I did a major rewrite of the impenetrable tcFamTyPats. The result
  is vastly more comprehensible.

* I got rid of kcDataDefn entirely, quite a big function.

* I re-did the way that checkConsistentFamInst works, so
  that it allows alpha-renaming of invisible arguments.

* The interaction of kind signatures and family instances is tricky.
    Type families: see Note [Apparently-nullary families]
    Data families: see Note [Result kind signature for a data family instance]
                   and Note [Eta-reduction for data families]

* The consistent instantation of an associated type family is tricky.
  See Note [Checking consistent instantiation] and
      Note [Matching in the consistent-instantation check]
  in TcTyClsDecls.  It's now checked in TcTyClsDecls because that is
  when we have the relevant info to hand.

* I got tired of the compromises in etaExpandFamInst, so I did the
  job properly by adding a field cab_eta_tvs to CoAxBranch.
  See Coercion.etaExpandCoAxBranch.

tcInferApps and friends
~~~~~~~~~~~~~~~~~~~~~~~
* I got rid of the mysterious and horrible ClsInstInfo argument
  to tcInferApps, checkExpectedKindX, and various checkValid
  functions.  It was horrible!

* I got rid of [Type] result of tcInferApps.  This list was used
  only in tcFamTyPats, when checking the LHS of a type instance;
  and if there is a cast in the middle, the list is meaningless.
  So I made tcInferApps simpler, and moved the complexity
  (not much) to tcInferApps.

  Result: tcInferApps is now pretty comprehensible again.

* I refactored the many function in TcMType that instantiate skolems.

Smaller things

* I rejigged the error message in checkValidTelescope; I think it's
  quite a bit better now.

* checkValidType was not rejecting constraints in a kind signature
     forall (a :: Eq b => blah). blah2
  That led to further errors when we then do an ambiguity check.
  So I make checkValidType reject it more aggressively.

* I killed off quantifyConDecl, instead calling kindGeneralize
  directly.

* I fixed an outright bug in tyCoVarsOfImplic, where we were not
  colleting the tyvar of the kind of the skolems

* Renamed ClsInstInfo to AssocInstInfo, and made it into its
  own data type

* Some fiddling around with pretty-printing of family
  instances which was trickier than I thought.  I wanted
  wildcards to print as plain "_" in user messages, although
  they each need a unique identity in the CoAxBranch.

Some other oddments

* Refactoring around the trace messages from reportUnsolved.
* A bit of extra tc-tracing in TcHsSyn.commitFlexi

This patch fixes a raft of bugs, and includes tests for them.

 * #14887
 * #15740
 * #15764
 * #15789
 * #15804
 * #15817
 * #15870
 * #15874
 * #15881

The level numbers we were getting simply didn't obey the
invariant (ImplicInv) in TcType
   Note [TcLevel and untouchable type variables]

That leads to chaos. Easy to fix.  I improved the documentation.

I also added an assertion in TcSimplify that checks that
level numbers go up by 1 as we dive inside implications, so
that we catch the problem at source rather than than through
its obscure consequences.

That in turn showed up that TcRules was also generating
constraints that didn't obey (ImplicInv), so I fixed that too.
I have no idea what consequences were lurking behing that
bug, but anyway now it's fixed.  Hooray.

* Define Type.substTyVarBndrs, and use it

* Rename substTyVarBndrCallback to substTyVarBndrUsing,
  and other analogous higher order functions.  I kept
  stumbling over the name.

Minor refactor and comments, following Ryan's excellent DeriveAnyClass
bug (Trac #14932)

The way GHC was handling `DeriveAnyClass` was subtly wrong
in two notable ways:

* In `inferConstraintsDAC`, we were //always// bumping the `TcLevel`
  of newly created unification variables, under the assumption that
  we would always place those unification variables inside an
  implication constraint. But #14932 showed precisely the scenario
  where we had `DeriveAnyClass` //without// any of the generated
  constraints being used inside an implication, which made GHC
  incorrectly believe the unification variables were untouchable.
* Even worse, we were using the generated unification variables from
  `inferConstraintsDAC` in every single iteration of `simplifyDeriv`.
  In #14933, however, we have a scenario where we fill in a
  unification variable with a skolem in one iteration, discard it,
  proceed on to another iteration, use the same unification variable
  (still filled in with the old skolem), and try to unify it with
  a //new// skolem! This results in an utter disaster.

The root of both these problems is `inferConstraintsDAC`. This patch
fixes the issue by no longer generating unification variables
directly in `inferConstraintsDAC`. Instead, we store the original
variables from a generic default type signature in `to_metas`, a new
field of `ThetaOrigin`, and in each iteration of `simplifyDeriv`, we
generate fresh meta tyvars (avoiding the second issue). Moreover,
this allows us to more carefully fine-tune the `TcLevel` under which
we create these meta tyvars, fixing the first issue.

Test Plan: make test TEST="T14932 T14933"

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14932, #14933

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

Summary:
At its core, this patch is a simple tweak that allows a user
to write:

```lang=haskell
deriving instance _ => Eq (Foo a)
```

Which is functionally equivalent to:

```lang=haskell
data Foo a = ...
  deriving Eq
```

But with the added flexibility that `StandaloneDeriving` gives you
(namely, the ability to use it anywhere, not just in the same module
that `Foo` was declared in). This fixes #13324, and should hopefully
address a use case brought up in #10607.

Currently, only the use of a single, extra-constraints wildcard is
permitted in a standalone deriving declaration. Any other wildcard
is rejected, so things like
`deriving instance (Eq a, _) => Eq (Foo a)` are currently forbidden.

There are quite a few knock-on changes brought on by this change:

* The `HsSyn` type used to represent standalone-derived instances
  was previously `LHsSigType`, which isn't sufficient to hold
  wildcard types. This needed to be changed to `LHsSigWcType` as a
  result.

* Previously, `DerivContext` was a simple type synonym for
  `Maybe ThetaType`, under the assumption that you'd only ever be in
  the `Nothing` case if you were in a `deriving` clause. After this
  patch, that assumption no longer holds true, as you can also be
  in this situation with standalone deriving when an
  extra-constraints wildcard is used.

  As a result, I changed `DerivContext` to be a proper datatype that
  reflects the new wrinkle that this patch adds, and plumbed this
  through the relevant parts of `TcDeriv` and friends.

* Relatedly, the error-reporting machinery in `TcErrors` also assumed
  that if you have any unsolved constraints in a derived instance,
  then you should be able to fix it by switching over to standalone
  deriving. This was always sound advice before, but with this new
  feature, it's possible to have unsolved constraints even when
  you're standalone-deriving something!

  To rectify this, I tweaked some constructors of `CtOrigin` a bit
  to reflect this new subtlety.

This requires updating the Haddock submodule. See my fork at
https://github.com/RyanGlScott/haddock/commit/067d52fd4be15a1842cbb05f42d9d482de0ad3a7

Test Plan: ./validate

Reviewers: simonpj, goldfire, bgamari

Reviewed By: simonpj

Subscribers: goldfire, rwbarton, thomie, mpickering, carter

GHC Trac Issues: #13324

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

Trac #14394 showed that it's possible to get redundant
constraints in the inferred provided constraints of a pattern
synonym.  This patch removes the redundancy with mkMinimalBySCs.

To do this I had to generalise the type of mkMinimalBySCs slightly.
And, to reduce confusing reversal, I made it stable: it now returns
its result in the same order as its input.  That led to a raft of
error message wibbles, mostly for the better.

I'm astonished that anything worked without this!

Fixes Trac #14339

This switches the compiler/ component to get compiled with
-XNoImplicitPrelude and a `import GhcPrelude` is inserted in all
modules.

This is motivated by the upcoming "Prelude" re-export of
`Semigroup((<>))` which would cause lots of name clashes in every
modulewhich imports also `Outputable`

Reviewers: austin, goldfire, bgamari, alanz, simonmar

Reviewed By: bgamari

Subscribers: goldfire, rwbarton, thomie, mpickering, bgamari

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

As of ed7a830d this module uses
MultiWayIf, the parsing behavior of which changed in 8.0.2 due
to #10807. Reformat the code so that it compiles under both 8.0.1 and
8.0.2/8.2.1.

Test Plan: Validate bootstrapping with 8.0.1

Reviewers: austin

Subscribers: rwbarton, thomie, RyanGlScott

GHC Trac Issues: #14130

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

Addresses point (2) of https://phabricator.haskell.org/D3337#107865.

Before, several functions in `TcDeriv` and `TcDerivInfer` which compute
an `EarlyDerivSpec` were manually threading through about 10 different
arguments, which contribute to quite a lot of clutter whenever they need
to be updated. To minimize this plumbing, and to make it clearer which
of these 10 values are being used where, I refactored the code in
`TcDeriv` and `TcDerivInfer` to use a new `DerivM` type:

```lang=haskell
type DerivM = ReaderT DerivEnv TcRn
```

where `DerivEnv` contains the 10 aforementioned values. In addition to
cleaning up the code, this should make some subsequent changes planned
for later less noisy.

Test Plan: ./validate

Reviewers: austin, bgamari

Subscribers: rwbarton, thomie

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

Summary:
Addresses point (1) of https://phabricator.haskell.org/D3337#107865.

Before, `inferConstraints` awkwardly combined all of the logic needed to handle
stock, newtype, and anyclass deriving. Really, though, the stock/newtype logic
is quite different from the anyclass logic, so this splits off
`inferConstraintsDataConArgs` (so named because it infers constraints by
inspecting the types of the arguments to data constructors) from
`inferConstraints` to handle the stock/newtype-specific bits.

Aside from making the code somewhat clearer, this allows us to factor out
superclass constraint inference, which is done regardless of deriving strategy.

Test Plan: If it builds, ship it

Reviewers: bgamari, austin

Subscribers: rwbarton, thomie

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

While investigating #12545, I discovered several places in the code
that performed length-checks like so:

```
length ts == 4
```

This is not ideal, since the length of `ts` could be much longer than 4,
and we'd be doing way more work than necessary! There are already a slew
of helper functions in `Util` such as `lengthIs` that are designed to do
this efficiently, so I found every place where they ought to be used and
did just that. I also defined a couple more utility functions for list
length that were common patterns (e.g., `ltLength`).

Test Plan: ./validate

Reviewers: austin, hvr, goldfire, bgamari, simonmar

Reviewed By: bgamari, simonmar

Subscribers: goldfire, rwbarton, thomie

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

A very small refactoring

These occurrences of pushTcLevelM weren't using the resulting TcLevel,
so they can be replaced with the (ostensibly more efficient) pushTcLevelM_.

No change in behavior.

[ci skip]

For some odd reason inferConstraints was using a CPS style,
which is entirely unnecessary.  This patch straightens it out.

No change in what it does.

This patch fixes Trac #13272.  The general approach was fine, but
we were simply not generating the correct implication constraint
(in particular generating fresh unification variables).  I added
a lot more commentary to Note [Gathering and simplifying
constraints for DeriveAnyClass]

I'm still not very happy with the overall architecture.  It feels
more complicate than it should.

Summary:
Currently, `DeriveAnyClass` has two glaring flaws:

* It only works on classes whose argument is of kind `*` or `* -> *` (#9821).
* The way it infers constraints makes no sense. It basically co-opts the
  algorithms used to infer contexts for `Eq` (for `*`-kinded arguments) or
  `Functor` (for `(* -> *)`-kinded arguments). This tends to produce overly
  constrained instances, which in extreme cases can lead to legitimate things
  failing to typecheck (#12594). Or even worse, it can trigger GHC panics
  (#12144 and #12423).

This completely reworks the way `DeriveAnyClass` infers constraints to fix
these two issues. It now uses the type signatures of the derived class's
methods to infer constraints (and to simplify them). A high-level description
of how this works is included in the GHC users' guide, and more technical notes
on what is going on can be found as comments (and a Note) in `TcDerivInfer`.

Fixes #9821, #12144, #12423, #12594.

Test Plan: ./validate

Reviewers: dfeuer, goldfire, simonpj, austin, bgamari

Subscribers: dfeuer, thomie

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

Here we consolidate the pretty-printing logic for types in IfaceType. We
need IfaceType regardless and the printer for Type can be implemented in
terms of that for IfaceType. See #11660.

Note that this is very much a work-in-progress. Namely I still have yet
to ponder how to ease the hs-boot file situation, still need to rip out
more dead code, need to move some of the special cases for, e.g., `*` to
the IfaceType printer, and need to get it to validate. That being said,
it comes close to validating as-is.

Test Plan: Validate

Reviewers: goldfire, austin

Subscribers: goldfire, thomie, simonpj

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

GHC Trac Issues: #11660

Summary:
Keeping a promise I made to Simon to clean up these modules.

This change splits up the massive `TcDeriv` and `TcGenDeriv` modules into
somewhat more manageable pieces. The new modules are:

* `TcGenFunctor`: This contains the deriving machinery for `Functor`,
  `Foldable`, and `Traversable` (which all use the same underlying algorithm).
* `TcDerivInfer`: This is the new home for `inferConstraints`,
  `simplifyInstanceContexts`, and related functions, whose role is to come up
  with the derived instance context and subsequently simplify it.
* `TcDerivUtils`: This is a grab-bag module that contains several
  error-checking utilities originally in `TcDeriv`, as well as some functions
  that `TcDeriv` and `TcDerivInfer` both need.

The end result is that `TcDeriv` is now less than 1,600 SLOC (originally 2,686
SLOC), and `TcGenDeriv` is now about 2,000 SLOC (originally 2,964).

In addition, this also implements a couple of tiny refactorings:

* I transformed `type Condition = (DynFlags, TyCon) -> Validity` into
  `type Condition = DynFlags -> TyCon -> Validity`
* I killed the `DerivSpecGeneric` constructor for `DerivSpecMechanism`, and
  merged its functionality into `DerivSpecStock`. In addition,
  `hasStockDeriving` now contains key-value pairs for `Generic` and `Generic1`,
  so they're no longer treated as an awkward special case in `TcDeriv`.

Test Plan: ./validate

Reviewers: simonpj, austin, bgamari

Reviewed By: simonpj

Subscribers: thomie, mpickering

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