GitLab

These turn out to be a useful special case of splitTyConApp_maybe.

A refactoring only; no change in behaviour

A "lifting substitition" takes a *type* to a *coercion*, using a
substitution that takes a *type variable* to a *coercion*.  We were
using a CvSubst for this purpose, which was an awkward exception: in
every other use of CvSubst, type variables map only to types.

Turned out that Coercion.liftCoSubst is quite a small function, so I
rewrote it with a special substitution type Coercion.LiftCoSubst, just
for that purpose.  In doing so I found that the function itself was
bizarrely over-complicated ... a direct result of mis-using CvSubst.

So this patch makes it all simpler, faster, and easier to understand.
No bugs fixed though!

This change gets rid of a debug WARNING; it wasn't
actually making anything go wrong, but it's best to
have the correct in-scope set.

* Fix bugs in the packing and unpacking of data
  constructors with equality predicates in their types

* Remove PredCo altogether; instead, coercions between predicated
  types (like  (Eq a, [a]~b) => blah) are treated as if they
  were precisely their underlying representation type
       Eq a -> ((~) [a] b) -> blah
  in this case

* Similarly, Type.coreView no longer treats equality
  predciates specially.

* Implement the cast-of-coercion optimisation in
  Simplify.simplCoercionF

Numerous other small bug-fixes and refactorings.

Annoyingly, OptCoercion had Windows line endings, and this
patch switches to Unix, so it looks as if every line has changed.

See the paper "Practical aspects of evidence based compilation in System FC"

* Coercion becomes a data type, distinct from Type

* Coercions become value-level things, rather than type-level things,
  (although the value is zero bits wide, like the State token)
  A consequence is that a coerion abstraction increases the arity by 1
  (just like a dictionary abstraction)

* There is a new constructor in CoreExpr, namely Coercion, to inject
  coercions into terms

Regression testing and user feedback for GHC 7.0 taught
us a lot.  This patch fixes numerous small bugs, and some
major ones (eg Trac #4484, #4492), and improves type
error messages.

The main changes are:

* Entirely remove the "skolem equivalance class" stuff;
  a very useful simplification

* Instead, when flattening "wanted" constraints we generate
  unification variables (not flatten-skolems) for the
  flattened type function application

* We then need a fixup pass at the end, TcSimplify.solveCTyFunEqs,
  which resolves any residual equalities of form
      F xi ~ alpha

* When we come across a definite failure (e.g. Int ~ [a]),
  we now defer reporting the error until the end, in case we
  learn more about 'a'.  That is particularly important for
  occurs-check errors.  These are called "frozen" type errors.

* Other improvements in error message generation.

* Better tracing messages

This major patch implements the new OutsideIn constraint solving
algorithm in the typecheker, following our JFP paper "Modular type
inference with local assumptions".  

Done with major help from Dimitrios Vytiniotis and Brent Yorgey.

This just ensures that an unsafe coercion is as localised as possible.
For example, instead of
    UnsafeCo (Int -> t1) (Int -> t2)
use 
    Int -> UnsafeCo t1 t2

The main purpose of this patch is to add a bunch of new rules
to the coercion optimiser.  They are documented in the (revised)
Appendix of the System FC paper.  

Some code has moved about:

- OptCoercion is now a separate module, mainly because it
  now uses tcMatchTy, which is defined in Unify, so OptCoercion
  must live higehr up in the hierarchy

- Functions that manipulate Kinds has moved from 
  Type.lhs to Coercion.lhs.  Reason: the function typeKind
  now needs to call coercionKind.  And in any case, a Kind is
  a flavour of Type, so it builds on top of Type; indeed Coercions
  and Kinds are both flavours of Type.

  This change required fiddling with a number of imports, hence
  the one-line changes to otherwise-unrelated modules

- The representation of CoTyCons in TyCon has changed.   Instead of
  an extensional representation (a kind checker) there is now an
  intensional representation (namely TyCon.CoTyConDesc).  This was
  needed for one of the new coercion optimisations.

* Fix a bug that meant that 
     (right (inst (forall tv.co) ty)) 
  wasn't getting optimised.  This showed up in the
  compiled code for ByteCodeItbls

* Add a substitution to optCoercion, so that it simultaneously
  substitutes and optimises.  Both call sites wanted this, and
  optCoercion itself can use it, so it seems a win all round.

In CSE we were getting lots of apprarently-unequal expressions with
the same hash code.  In fact they were perfectly equal -- but we were
using a cheap-and-cheerful equality tests for CoreExpr that said False
for any lambda expression!

This patch adds a proper equality test for Core, with alpha-renaming.
It's easy to do, and will avoid silly cases of CSE failing to fire.

We should get less of this:
  WARNING: file compiler/simplCore/CSE.lhs line 326
  extendCSEnv: long list, length 18
from a compiler built with -DDEBUG

* Core Lint now does full checking of kinds and coercion terms
  which picks up kind errors in coercions that were previously
  simply not checked for

* Coercion.lhs now provides optCoercion which optimises coercion
  terms.  It implements all of Dimitrios's rules

* The constructors for coercion terms now make no attempt to be
  "smart"; instead we rely solely on the coercion optimiser

* CoercionTyCons in TyCon.lhs always had a "custom" kinding rule
  (the coKindFun field of CoercionTyCon) but its type was not 
  clever enough to do both 
     (a) *figure out the result kind*, assuming the whole thing
         is well-kinded in the first place
     (b) *check* the kinds of everything, failing gracefully if
         they aren't right. 
  We need (b) for the new CoreLint stuff. The field now has type
        CoTyConKindChecker
  which does the job nicely.

In preparation for implementing the PushC rule for coercion-swizzling
in the Simplifier, I had to inmplement the three new decomposition
operators for coercions, which I've called csel1, csel2, and cselR.

     co :: ((s1~t1) => r1) ~ ((s2~t2) => r2)
     ---------------------------------------
              csel1 co :: s1~s2

and similarly csel2, cselR.

On the way I fixed the coercionKind function for types of form
          (s1~t2) => r2
which currently are expressed as a forall type.  

And I refactored quite a bit to help myself understand what is
going on.

* Remove trace from optCoercion

* Use simplCoercion for type arguments in the Simplifier
  (because they might be coercions)

Coercion terms can get big (see Trac #2859 for example), so this
patch puts the infrastructure in place to optimise them:

  * Adds Coercion.optCoercion :: Coercion -> Coercion

  * Calls optCoercion in Simplify.lhs

The optimiser doesn't work right at the moment, so it is 
commented out, but Tom is going to work on it.

- During fianlisation we use to occasionally swivel variable-variable equalities
- Now, normalisation ensures that they are always oriented as appropriate for
  instantation.
- Also fixed #1899 properly; the previous fix fixed a symptom, not the cause.

Modules that need it import it themselves instead.

Previously, cheapEqExpr would always return False if it encountered a cast.
This was bad for two reasons. Firstly, CSE (which uses cheapEqExpr to compare
expressions) never eliminated expressions which contained casts and secondly,
it was inconsistent with exprIsBig. This patch fixes this.

Older GHCs can't parse OPTIONS_GHC.
This also changes the URL referenced for the -w options from
WorkingConventions#Warnings to CodingStyle#Warnings for the compiler
modules.

This patch introduces type checking for type families of which associated
type synonyms are a special case. E.g.

        type family Sum n m

        type instance Sum Zero n = n
        type instance Sum (Succ n) m = Succ (Sum n m)

where

        data Zero       -- empty type
        data Succ n     -- empty type

In addition we support equational constraints of the form:

        ty1 ~ ty2

(where ty1 and ty2 are arbitrary tau types) in any context where
type class constraints are already allowed, e.g.

        data Equals a b where
                Equals :: a ~ b => Equals a b

The above two syntactical extensions are disabled by default. Enable
with the -XTypeFamilies flag.

For further documentation about the patch, see:

        * the master plan
          http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions

        * the user-level documentation
          http://haskell.org/haskellwiki/GHC/Indexed_types

The patch is mostly backwards compatible, except for:

        * Some error messages have been changed slightly.

        * Type checking of GADTs now requires a bit more type declarations:
          not only should the type of a GADT case scrutinee be given, but also
          that of any identifiers used in the branches and the return type.

Please report any unexpected behavior and incomprehensible error message 
for existing code.

Contributors (code and/or ideas):
        Tom Schrijvers
        Manuel Chakravarty
        Simon Peyton-Jones
        Martin Sulzmann 
with special thanks to Roman Leshchinskiy