GitLab

* Treat kind-equality constraints as *derived* equalities,
  with no evidence.  That is really what they are at the moment.

* Get rid of EvKindCast and friends.

* Postpone kind errors properly to the constraint solver
  (lots of small knock-on effects)

I moved SwapFlag to BasicTypes as well

and refactor canEqLeafTyVarEq along the same lines
as our earlier refactoring of canEqLeafFunEq

The main change is that canEqFailure does substitution:
see Note [Make sure that insolubles are fully rewritten] in TcCanonical.

However DV and I also found a way to simplify 'flatten' a bit, by
passing a CtFlavour instead of CtEvidence.

This patch finally adds 'left' and 'right' coercions back into
GHC.  Trac #7205 gives the details.

The main change is to add a new constructor to Coercion:

  data Coercion
    = ...
    | NthCo  Int         Coercion     -- OLD, still there
    | LRCo   LeftOrRight Coercion     -- NEW

  data LeftOrRight = CLeft | CRight

Plus:
  * Similar change to TcCoercion
  * Use LRCo when decomposing AppTys
  * Coercion optimisation needs to handle left/right

The rest is just knock-on effects.

A simple refactoring with no complicated fiddling.

1. Rejig CtLoc
   * CtLoc is now *not* parameterised (much simpler)
   * CtLoc includes the "depth" of the constraint
   * CtLoc includes the TcLclEnv at the birthplace
     That gives (a) the SrcSpan, (b) the [ErrCtxt]
     (c) the [TcIdBinder]
   * The CtLoc of a constraint is no longer in its CtEvidence
   * Where we passed 'depth' before, now we pass CtLoc

2. Some significant refactoring in TcErrors
   * Get rid of cec_extra
   * Traverse every constraint, so that we can be
     sure to generate bindings where necessary.
     (This was really a lurking bug before.)

3. Merge zonking into TcCanonical.  This turned out to be
   almost trivial; just a small change to TcCanonical.flattenTyVar.

   The nice consequence is that we don't need to zonk a constraint
   before solving it; instead it gets zonked "on the fly" as it were.

This single commit combines a lot of work done by
Thijs Alkemade <thijsalkemade@gmail.com>, plus a slew
of subsequent refactoring by Simon PJ.

The basic idea is
* Add a new expression form "_", a hole, standing for a not-yet-written expression
* Give a useful error message that
   (a) gives the type of the hole
   (b) gives the types of some enclosing value bindings that
       mention the hole

Driven by this goal I did a LOT of refactoring in TcErrors, which in turn
allows us to report enclosing value bindings for other errors, not just
holes.  (Thijs rightly did not attempt this!)

The major data type change is a new form of constraint
  data Ct = ...
    	  | CHoleCan {
    	      cc_ev       :: CtEvidence,
    	      cc_hole_ty  :: TcTauType,
    	      cc_depth    :: SubGoalDepth }

I'm still in two minds about whether this is the best plan. Another
possibility would be to have a predicate type for holes, somthing like
   class Hole a where
     holeValue :: a

It works the way it is, but there are some annoying special cases for
CHoleCan (just grep for "CHoleCan").

* Instead of Untouchables being a [Unique], it is simply an Int
  indicating the depth of nesting.  This works fine now that
  floatEqualities is promoting the floated unification variables
  to the outer level

* Remove the inert_tv_eqs (InScopeSet) from InertCans.  It wasn't
  being used.  See Note [Shadowing in a constraint] in TcRnTypes

* Rename inert_frozen to inert_insols

* Some simple refactoring in
     TcErrors.reportFlatsAndInsols
     TcInteract.kickOutRewritable
     TsSimplify.floatEqualities

* inert_solved becomes dictionaries-only, inert_solved_dicts

* inert_solved_dicts is used only to cache the result of uses
  of a top level instance declaration, just like inert_solved_funeqs

* That in turn simplifies xCtFlavor and rewriteCtFlavor, because
  they no longer need a "should I cache" parameter.  (Moreover the
  settings for this parameter were very subtle; it's easy to get
  loops if you cache too much.  Caching only top-level instance
  uses is much safer, and eliminates all these subtle cases.)

 * simplifying and tidying up canonicalisation,
 * removing the flat cache altogether
 * making the FunEq worklist into a deque

keep spontaneous unifications /only/ in the TcS tybinds. Relevant note
is Note [Spontaneously solved in TyBinds] in TcInteract.

(Before merging to HEAD we need to tidy up and write a proper commit message.)

This patch re-implements implicit parameters via a class
with a functional dependency:

    class IP (n::Symbol) a | n -> a where
      ip :: a

This definition is in the library module GHC.IP. Notice
how it use a type-literal, so we can have constraints like
   IP "x" Int
Now all the functional dependency machinery works right to make
implicit parameters behave as they should.

Much special-case processing for implicit parameters can be removed
entirely. One particularly nice thing is not having a dedicated
"original-name cache" for implicit parameters (the nsNames field of
NameCache).  But many other cases disappear:

  * BasicTypes.IPName
  * IPTyCon constructor in Tycon.TyCon
  * CIPCan constructor  in TcRnTypes.Ct
  * IPPred constructor  in Types.PredTree

Implicit parameters remain special in a few ways:

 * Special syntax.  Eg the constraint (IP "x" Int) is parsed
   and printed as (?x::Int).  And we still have local bindings
   for implicit parameters, and occurrences thereof.

 * A implicit-parameter binding  (let ?x = True in e) amounts
   to a local instance declaration, which we have not had before.
   It just generates an implication contraint (easy), but when
   going under it we must purge any existing bindings for
   ?x in the inert set.  See Note [Shadowing of Implicit Parameters]
   in TcSimplify

 * TcMType.sizePred classifies implicit parameter constraints as size-0,
   as before the change

There are accompanying patches to libraries 'base' and 'haddock'

All the work was done by Iavor Diatchki

By using Haskell's debugIsOn rather than CPP's "#ifdef DEBUG", we
don't need to kludge things to keep the warning checker happy etc.

We were wrongly reporting (a ~ F a) as an occurs-check error
when F is a type function.

This is the result of Simon and Dimitrios doing a code walk through.
There is no change in behaviour, but the structure is much better.
Main changes:

* Given constraints contain an EvTerm not an EvVar

* Correspondingly, TcEvidence is a recursive types that uses
  EvTerms rather than EvVars

* Rename CtFlavor to CtEvidence

* Every CtEvidence has a ctev_pred field.  And use record fields
  consistently for CtEvidence

* The solved-constraint fields of InertSet (namely inert_solved and
  inert_solved_funeqs) contain CtEvidence, not Ct

There is a long cascade of follow-on changes.

There was an ASSERT which does not hold during type checking (and
should not) which is later checked by Core Lint

constraint generation during solveInteractCts, needed for polytype
equality decomposition. More commentary to follow.

short note to document an example.

pretty much as we do for mkTcEqPred. Ugly and delicate but we have to rething the subkinding
story. For now I am doing the same thing as mkTcEqPred.

          (ii) evidence loops because of caching fixed

   (i) Replaced a lot of clunky and fragile EvVar handling code with
       a more uniform ``flavor transformer'' API in the canonicalizer
       and the interaction solver. Now EvVars are just fields inside
       the CtFlavors.
   (ii) Significantly simplified our caching story
This patch does not validate yet and more refactoring is on the way.

which (finally) fills out the functionality of polymorphic kinds.
It also fixes numerous bugs.

Main changes are:

Renaming stuff
~~~~~~~~~~~~~~
* New type in HsTypes:
     data HsBndrSig sig = HsBSig sig [Name]
  which is used for type signatures in patterns, and kind signatures
  in types.  So when you say
       f (x :: [a]) = x ++ x
  or
       data T (f :: k -> *) (x :: *) = MkT (f x)
  the signatures in both cases are a HsBndrSig.

* The [Name] in HsBndrSig records the variables bound by the
  pattern, that is 'a' in the first example, 'k' in the second,
  and nothing in the third.  The renamer initialises the field.

* As a result I was able to get rid of
     RnHsSyn.extractHsTyNames :: LHsType Name -> NameSet
  and its friends altogether.  Deleted the entire module!
  This led to some knock-on refactoring; in particular the
  type renamer now returns the free variables just like the
  term renamer.

Kind-checking types: mainly TcHsType
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A major change is that instead of kind-checking types in two
passes, we now do one. Under the old scheme, the first pass did
kind-checking and (hackily) annotated the HsType with the
inferred kinds; and the second pass desugared the HsType to a
Type.  But now that we have kind variables inside types, the
first pass (TcHsType.tc_hs_type) can go straight to Type, and
zonking will squeeze out any kind unification variables later.

This is much nicer, but it was much more fiddly than I had expected.

The nastiest corner is this: it's very important that tc_hs_type
uses lazy constructors to build the returned type. See
Note [Zonking inside the knot] in TcHsType.

Type-checking type and class declarations: mainly TcTyClsDecls
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
I did tons of refactoring in TcTyClsDecls.  Simpler and nicer now.

Typechecking bindings: mainly TcBinds
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
I rejigged (yet again) the handling of type signatures in TcBinds.
It's a bit simpler now.  The main change is that tcTySigs goes
right through to a TcSigInfo in one step; previously it was split
into two, part here and part later.

Unsafe coercions
~~~~~~~~~~~~~~~~
Usually equality coercions have exactly the same kind on both
sides.  But we do allow an *unsafe* coercion between Int# and Bool,
say, used in
    case error Bool "flah" of { True -> 3#; False -> 0# }
-->
    (error Bool "flah") |> unsafeCoerce Bool Int#

So what is the instantiation of (~#) here?
   unsafeCoerce Bool Int# :: (~#) ??? Bool Int#
I'm using OpenKind here for now, but it's un-satisfying that
the lhs and rhs of the ~ don't have precisely the same kind.

More minor
~~~~~~~~~~
* HsDecl.TySynonym has its free variables attached, which makes
  the cycle computation in TcTyDecls.mkSynEdges easier.

* Fixed a nasty reversed-comparison bug in FamInstEnv:
  @@ -490,7 +490,7 @@ lookup_fam_inst_env' match_fun one_sided ie fam tys
     n_tys = length tys
     extra_tys = drop arity tys
     (match_tys, add_extra_tys)
-       | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
+       | arity < n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
        | otherwise     = (tys,            \res_tys -> res_tys)

to emit kind constraints when decomposing an application.
Resulting code is actually shorter!

I have forgotten what the original driver for this change was.
There is quite a bit of refactoring in TcCanonical; the rest
is minor.

This patch implements the idea of deferring (most) type errors to
runtime, instead emitting only a warning at compile time.  The
basic idea is very simple:

 * The on-the-fly unifier in TcUnify never fails; instead if it
   gets stuck it emits a constraint.

 * The constraint solver tries to solve the constraints (and is
   entirely unchanged, hooray).

 * The remaining, unsolved constraints (if any) are passed to
   TcErrors.reportUnsolved.  With -fdefer-type-errors, instead of
   emitting an error message, TcErrors emits a warning, AND emits
   a binding for the constraint witness, binding it
   to (error "the error message"), via the new form of evidence
   TcEvidence.EvDelayedError.  So, when the program is run,
   when (and only when) that witness is needed, the program will
   crash with the exact same error message that would have been
   given at compile time.

Simple really.  But, needless to say, the exercise forced me
into some major refactoring.

 * TcErrors is almost entirely rewritten

 * EvVarX and WantedEvVar have gone away entirely

 * ErrUtils is changed a bit:
     * New Severity field in ErrMsg
     * Renamed the type Message to MsgDoc (this change
       touches a lot of files trivially)

 * One minor change is that in the constraint solver we try
   NOT to combine insoluble constraints, like Int~Bool, else
   all such type errors get combined together and result in
   only one error message!

 * I moved some definitions from TcSMonad to TcRnTypes,
   where they seem to belong more