[skip ci]

[ci skip]

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

This patch, authored by alexvieth and reviewed at D4451,
makes performance improvements by critically optimizing parts
of the flattener.

Summary:
T3064, T5321FD, T5321Fun, T9872a, T9872b, T9872c all pass.
T9872a and T9872c show improvements beyond the -5% threshold.
T9872d fails at 10.9% increased allocations.

Herbert Valerio Riedel authored 7 years ago and Ben Gamari committed 7 years ago

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

Summary:
This commit implements the plan in #13140:

* Today, roles in signature files default to representational. Let's change the
  default to nominal, as this is the most flexible implementation side. If a
  client of the signature needs to coerce with a type, the signature can be
  adjusted to have more stringent requirements.

* If a parameter is declared as nominal in a signature, it can be implemented
  by a data type which is actually representational.

* When merging abstract data declarations, we take the smallest role for every
  parameter. The roles are considered fix once we specify the structure of an
  ADT.

* Critically, abstract types are NOT injective, so we aren't allowed to
  make inferences like "if T a ~R T b, then a ~N b" based on the nominal
  role of a parameter in an abstract type (this would be unsound if the
  parameter ended up being phantom.)  This restriction is similar to the
  restriction we have on newtypes.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: simonpj, bgamari, austin, goldfire

Subscribers: goldfire, thomie

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

* Rename CoAxiom.Eqn = Pair Type to TypeEqn,
  and use it for fundeps

* Use the FunDepEqn for injectivity, which lets us share a bit
  more code, and (more important) brain cells

* When generating fundeps, take the max depth of the two
  constraints.  This aimed at tackling the strange loop in
  Trac #12860, but there is more to come for that.

* Improve pretty-printing with -ddump-tc-trace

It was implemented in terms of Uniques, but fortunately it's unused
so we can remove it.

GHC Trac: #4012

Summary:
Deriving `Typeable` has been a no-op since GHC 7.10, and now that we
require 7.10+ to build GHC, we can remove all the redundant `deriving Typeable`
statements in GHC.

Test Plan: ./validate

Reviewers: goldfire, austin, hvr, bgamari

Reviewed By: austin, hvr, bgamari

Subscribers: thomie

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

Several things here

* GHC no longer allows user-written Typeable instances,
  so remove them from hs-boot files.

* Generally, reduce the use of instances in hs-boot files. They are
  hard to track.  Mainly this involves using pprType, pprKind etc
  instead of just ppr.  There were a lot of instances in hs-boot
  files that weren't needed at all.

* Take TyThing out of Eq; it was used in exactly one place (in
  InteractiveEval), and equality is too big a hammer for that.

This moves code around to more sensible places.

- Construction for CoAxiom is localised in FamInstEnv

- orphNamesOfxx moves to CoreFVs

- roughMatchTcs, instanceCantMatch moves to Unify

- mkNewTypeCo moves from Coercion to FamInstEnv, and is
  renamed mkNewTypeCoAxiom, which makes more sense

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.

Now we use Array to store branches. This makes sense because we often
have to do random access (once inference is done). This also vastly
simplifies the awkward BranchList type.

This fixes #10837 and updates submodule utils/haddock.

For details see #6018, Phab:D202 and the wiki page:

https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies

This patch also wires-in Maybe data type and updates haddock submodule.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Subscribers: mpickering, bgamari, alanz, thomie, goldfire, simonmar,
             carter

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

GHC Trac Issues: #6018

this is resolving an old TODO comment

Summary: It looks like during .lhs -> .hs switch the comments were not updated. So doing exactly that.

Reviewers: austin, jstolarek, hvr, goldfire

Reviewed By: austin, jstolarek

Subscribers: thomie, goldfire

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

GHC Trac Issues: #9986

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

In some cases, the layout of the LANGUAGE/OPTIONS_GHC lines has been
reorganized, while following the convention, to

- place `{-# LANGUAGE #-}` pragmas at the top of the source file, before
  any `{-# OPTIONS_GHC #-}`-lines.

- Moreover, if the list of language extensions fit into a single
  `{-# LANGUAGE ... -#}`-line (shorter than 80 characters), keep it on one
  line. Otherwise split into `{-# LANGUAGE ... -#}`-lines for each
  individual language extension. In both cases, try to keep the
  enumeration alphabetically ordered.
  (The latter layout is preferable as it's more diff-friendly)

While at it, this also replaces obsolete `{-# OPTIONS ... #-}` pragma
occurences by `{-# OPTIONS_GHC ... #-}` pragmas.

The changes in more detail:

  * `TcBuiltInSynFamily` is now known as `BuiltinSynFamily` and
     lives in `CoAxiom`

  * `sfMatchFam` returns (CoAxiomRule, [Type], Type),
     which is enough to make Coersion or TcCoercion,
     depending on what what we need.

  * The rest of the compiler is updated to reflect these changes,
    most notably we can eliminate the cludge (XXX) in FamInstEnv
    and remove the lhs-boot file.

This fixes bugs #8185, #8234, and #8246. The new syntax is explained
in the comments to #8185, appears in the "Roles" subsection of the
manual, and on the [wiki:Roles] wiki page.

This change also removes the ability for a role annotation on type
synonyms, as noted in #8234.

This patch implements some simple evaluation of type-level expressions
featuring natural numbers.  We can evaluate *concrete* expressions that
use the built-in type families (+), (*), (^), and (<=?), declared in
GHC.TypeLits.   We can also do some type inference involving these
functions.  For example, if we encounter a constraint such as `(2 + x) ~ 5`
we can infer that `x` must be 3.  Note, however, this is used only to
resolve unification variables (i.e., as a form of a constraint improvement)
and not to generate new facts.  This is similar to how functional
dependencies work in GHC.

The patch adds a new form of coercion, `AxiomRuleCo`, which makes use
of a new form of axiom called `CoAxiomRule`.  This is the form of evidence
generate when we solve a constraint, such as `(1 + 2) ~ 3`.

The patch also adds support for built-in type-families, by adding a new
form of TyCon rhs: `BuiltInSynFamTyCon`.  such built-in type-family
constructors contain a record with functions that are used by the
constraint solver to simplify and improve constraints involving the
built-in function (see `TcInteract`).  The record in defined in `FamInst`.

The type constructors and rules for evaluating the type-level functions
are in a new module called `TcTypeNats`.

Roles are a solution to the GeneralizedNewtypeDeriving type-safety
problem.

Roles were first described in the "Generative type abstraction" paper,
by Stephanie Weirich, Dimitrios Vytiniotis, Simon PJ, and Steve Zdancewic.
The implementation is a little different than that paper. For a quick
primer, check out Note [Roles] in Coercion. Also see
http://ghc.haskell.org/trac/ghc/wiki/Roles
and
http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation
For a more formal treatment, check out docs/core-spec/core-spec.pdf.

This fixes Trac #1496, #4846, #7148.

This commit changes the syntax and story around overlapping type
family instances. Before, we had "unbranched" instances and
"branched" instances. Now, we have closed type families and
open ones.

The behavior of open families is completely unchanged. In particular,
coincident overlap of open type family instances still works, despite
emails to the contrary.

A closed type family is declared like this:
> type family F a where
>   F Int = Bool
>   F a   = Char
The equations are tried in order, from top to bottom, subject to
certain constraints, as described in the user manual. It is not
allowed to declare an instance of a closed family.

Quite a bit of tidying up here; the fix to #7524 is actually
only a small part.

* Be fully clear that the cab_tvs in a CoAxBranch are not
  fresh.  See Note [CoAxBranch type variables] in CoAxiom.

* Use CoAxBranch to replace the ATDfeault type in Class.
  CoAxBranch is perfect here.  This change allowed me to
  delete quite a bit of boilerplate code, including the
  corresponding IfaceSynType.

* Tidy up the construction of CoAxBranches, and when FamIntBranch is
  freshened.  The latter onw happens only in FamInst.newFamInst.

* Tidy the tyvars of a CoAxBranch when we build them, done in
  FamInst.mkCoAxBranch.  See Note [Tidy axioms when we build them]
  in that module.  This is what fixes #7524.

Much niceer now.

In particular I removed the fib_index and fib_loc fields.
The "master version" is in the CoAxiom; the FamInstBranches
are only for matching.

This commit mirrors work done in the commit for ClsInsts, 5efe9b...

Specifically:
- All FamInsts have *fresh* type variables. So, no more freshness work
in addLocalFamInst

Also:
- Some pretty-printing code around FamInsts was cleaned up a bit
This caused location information to be added to CoAxioms and index
information to be added to FamInstBranches.

An ordered, overlapping type family instance is introduced by 'type
instance
where', followed by equations. See the new section in the user manual
(7.7.2.2) for details. The canonical example is Boolean equality at the
type
level:

type family Equals (a :: k) (b :: k) :: Bool
type instance where
  Equals a a = True
  Equals a b = False

A branched family instance, such as this one, checks its equations in
order
and applies only the first the matches. As explained in the note
[Instance
checking within groups] in FamInstEnv.lhs, we must be careful not to
simplify,
say, (Equals Int b) to False, because b might later unify with Int.

This commit includes all of the commits on the overlapping-tyfams
branch. SPJ
requested that I combine all my commits over the past several months
into one
monolithic commit. The following GHC repos are affected: ghc, testsuite,
utils/haddock, libraries/template-haskell, and libraries/dph.

Here are some details for the interested:

- The definition of CoAxiom has been moved from TyCon.lhs to a
  new file CoAxiom.lhs. I made this decision because of the
  number of definitions necessary to support BranchList.

- BranchList is a GADT whose type tracks whether it is a
  singleton list or not-necessarily-a-singleton-list. The reason
  I introduced this type is to increase static checking of places
  where GHC code assumes that a FamInst or CoAxiom is indeed a
  singleton. This assumption takes place roughly 10 times
  throughout the code. I was worried that a future change to GHC
  would invalidate the assumption, and GHC might subtly fail to
  do the right thing. By explicitly labeling CoAxioms and
  FamInsts as being Unbranched (singleton) or
  Branched (not-necessarily-singleton), we make this assumption
  explicit and checkable. Furthermore, to enforce the accuracy of
  this label, the list of branches of a CoAxiom or FamInst is
  stored using a BranchList, whose constructors constrain its
  type index appropriately.

I think that the decision to use BranchList is probably the most
controversial decision I made from a code design point of view.
Although I provide conversions to/from ordinary lists, it is more
efficient to use the brList... functions provided in CoAxiom than
always to convert. The use of these functions does not wander far
from the core CoAxiom/FamInst logic.

BranchLists are motivated and explained in the note [Branched axioms] in
CoAxiom.lhs.

- The CoAxiom type has changed significantly. You can see the new
  type in CoAxiom.lhs. It uses a CoAxBranch type to track
  branches of the CoAxiom. Correspondingly various functions
  producing and consuming CoAxioms had to change, including the
  binary layout of interface files.

- To get branched axioms to work correctly, it is important to have a
  notion
  of type "apartness": two types are apart if they cannot unify, and no
  substitution of variables can ever get them to unify, even after type
family
  simplification. (This is different than the normal failure to unify
because
  of the type family bit.) This notion in encoded in tcApartTys, in
Unify.lhs.
  Because apartness is finer-grained than unification, the tcUnifyTys
now
  calls tcApartTys.

- CoreLinting axioms has been updated, both to reflect the new
  form of CoAxiom and to enforce the apartness rules of branch
  application. The formalization of the new rules is in
  docs/core-spec/core-spec.pdf.

- The FamInst type (in types/FamInstEnv.lhs) has changed
  significantly, paralleling the changes to CoAxiom. Of course,
  this forced minor changes in many files.

- There are several new Notes in FamInstEnv.lhs, including one
  discussing confluent overlap and why we're not doing it.

- lookupFamInstEnv, lookupFamInstEnvConflicts, and
  lookup_fam_inst_env' (the function that actually does the work)
  have all been more-or-less completely rewritten. There is a
  Note [lookup_fam_inst_env' implementation] describing the
  implementation. One of the changes that affects other files is
  to change the type of matches from a pair of (FamInst, [Type])
  to a new datatype (which now includes the index of the matching
  branch). This seemed a better design.

- The TySynInstD constructor in Template Haskell was updated to
  use the new datatype TySynEqn. I also bumped the TH version
  number, requiring changes to DPH cabal files. (That's why the
  DPH repo has an overlapping-tyfams branch.)

- As SPJ requested, I refactored some of the code in HsDecls:

 * splitting up TyDecl into SynDecl and DataDecl, correspondingly
   changing HsTyDefn to HsDataDefn (with only one constructor)

 * splitting FamInstD into TyFamInstD and DataFamInstD and
   splitting FamInstDecl into DataFamInstDecl and TyFamInstDecl

 * making the ClsInstD take a ClsInstDecl, for parallelism with
   InstDecl's other constructors

 * changing constructor TyFamily into FamDecl

 * creating a FamilyDecl type that stores the details for a family
   declaration; this is useful because FamilyDecls can appear in classes
but
   other decls cannot

 * restricting the associated types and associated type defaults for a
 * class
   to be the new, more restrictive types

 * splitting cid_fam_insts into cid_tyfam_insts and cid_datafam_insts,
   according to the new types

 * perhaps one or two more that I'm overlooking

None of these changes has far-reaching implications.

- The user manual, section 7.7.2.2, is updated to describe the new type
  family
  instances.