GitLab

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

I've forgotten the precise details already, but this patch
significantly refactors the way newtypes are handled, fixes
the foreign-export problem Trac #736 (which concerned newtypes),
and gets rid of a bogus unsafeCoerce in the foreign export
desugaring.

- Type synonym instances are turned into representation synonym tycons
- They are entered into the pool of family instances (FamInst environments)
  in the same way as data/newtype instances
- Still missing is writing the parent tycon information into ifaces and 
  various well-formedness checks.

At the moment GHC really does very little simplification of coercions.
This patch improves matters, but it's still not great, especially when
you have chains linked together with 'trans'. 

I'm also concerned that I have not yet implemented the 'leftc' and 'rightc'
coercions we added to the paper. 

But at least things are better than they were.  In particular
	g `trans` sym g
now cancels to give the identity.

A type variable has a flag saying whether it is a *type* variable or
a *coercion* variable.  This patch adds assertions to check the flag.

And it adds fixes to places which were Wrong (and hence fired the
assertion)! 

Also removed isCoVar from Coercion, since it's done by Var.isCoVar.

This large commit combines several interrelated changes:

  - IfaceSyn now contains actual Names rather than the special
    IfaceExtName type.  The binary interface file contains
    a symbol table of Names, where each entry is a (package,
    ModuleName, OccName) triple.  Names in the IfaceSyn point
    to entries in the symbol table.

    This reduces the size of interface files, which should
    hopefully improve performance (not measured yet).

    The toIfaceXXX functions now do not need to pass around
    a function from Name -> IfaceExtName, which makes that
    code simpler.

  - Names now do not point directly to their parents, and the
    nameParent operation has gone away.  It turned out to be hard to
    keep this information consistent in practice, and the parent info
    was only valid in some Names.  Instead we made the following
    changes:

    * ImportAvails contains a new field 
          imp_parent :: NameEnv AvailInfo
      which gives the family info for any Name in scope, and
      is used by the renamer when renaming export lists, amongst
      other things.  This info is thrown away after renaming.

    * The mi_ver_fn field of ModIface now maps to
      (OccName,Version) instead of just Version, where the
      OccName is the parent name.  This mapping is used when
      constructing the usage info for dependent modules.
      There may be entries in mi_ver_fn for things that are not in
      scope, whereas imp_parent only deals with in-scope things.

    * The md_exports field of ModDetails now contains
      [AvailInfo] rather than NameSet.  This gives us
      family info for the exported names of a module.

Also:

   - ifaceDeclSubBinders moved to IfaceSyn (seems like the
     right place for it).

   - heavily refactored renaming of import/export lists.

   - Unfortunately external core is now broken, as it relied on
     IfaceSyn.  It requires some attention.

Before the coKindFun could be applied to too many arguments;
now it expects exactly the right number of arguments.  That
makes it easier to write the coKindFuns, and localises the work.

The newtype deriving mechanism is much trickier to support than it
seems at first.  Kevin didn't get it quite right when moving to FC,
and I ended up re-writing quite a bit of it.  

I think it's right now, but I have not yet tested it thoroughly.

Mon Sep 18 19:35:24 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
  * Straightened out implicit coercions for indexed types
  Mon Sep  4 23:46:14 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
    * Straightened out implicit coercions for indexed types
    - HscTypes.implicitTyThings and LoadIface.ifaceDeclSubBndrs now
      include the coercion of indexed data/newtypes.
    - Name generation for the internal names of indexed data/newtypes now uses
      the same counter that generates the dfun unique indexes (ie, class and type
      instances are counted with the one counter).  We could make this two 
      separate counters if that's what's preferred.
    - The unique index of a data/newtype instances needs to go into the iface, so
      that we can generate the same names on slurping in the iface as when the
      original module was generated.  This is a bit yucky, but I don't see a way
      to avoid that (other than putting the full blown internal tycon name and 
      coercion name into the iface, which IMHO would be worse).
    - The predicate for when a datacon has a wrapper didn't take GADT
      equations nor whether it comes froma  family instance into account.
    
    *** WARNING!  This patch changed the interface file format. ***
    ***           Please recompile from scratch.                ***

Mon Sep 18 19:24:27 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
  * Indexed newtypes
  Thu Aug 31 22:09:21 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
    * Indexed newtypes
    - This patch makes indexed newtypes work
    - Only lightly tested
    - We need to distinguish between open and closed newtypes in a number of 
      places, because looking through newtypes doesn't work easily for open ones.

Mon Sep 18 19:12:51 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
  * Fixed bug in coercion for indexed data types
  Fri Aug 25 16:45:29 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
    * Fixed bug in coercion for indexed data types
    - Significant examples are starting to work; eg, generic finite maps:
    
    class GMapKey k where
      data GMap k :: * -> *
      empty       :: GMap k v
      lookup      :: k -> GMap k v -> Maybe v
      insert      :: k -> v -> GMap k v -> GMap k v
    
    instance GMapKey Int where
      data GMap Int v        = GMapInt (Map.Map Int v)
      empty                  = GMapInt Map.empty
      lookup k (GMapInt m)   = Map.lookup k m
      insert k v (GMapInt m) = GMapInt (Map.insert k v m)
    
    instance GMapKey Char where
      data GMap Char v        = GMapChar (GMap Int v)
      empty                   = GMapChar empty
      lookup k (GMapChar m)   = lookup (ord k) m
      insert k v (GMapChar m) = GMapChar (insert (ord k) v m)
    
    instance GMapKey () where
      data GMap () v           = GMapUnit (Maybe v)
      empty                    = GMapUnit Nothing
      lookup () (GMapUnit v)   = v
      insert () v (GMapUnit _) = GMapUnit $ Just v
    
    instance (GMapKey a, GMapKey b) => GMapKey (a, b) where
      data GMap (a, b) v            = GMapPair (GMap a (GMap b v))
      empty		                = GMapPair empty
      lookup (a, b) (GMapPair gm)   = lookup a gm >>= lookup b 
      insert (a, b) v (GMapPair gm) = GMapPair $ case lookup a gm of
    				    Nothing  -> insert a (insert b v empty) gm
    				    Just gm2 -> insert a (insert b v gm2  ) gm
    
    instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
      data GMap (Either a b) v                = GMapEither (GMap a v) (GMap b v)
      empty                                   = GMapEither empty empty
      lookup (Left  a) (GMapEither gm1  _gm2) = lookup a gm1
      lookup (Right b) (GMapEither _gm1 gm2 ) = lookup b gm2
      insert (Left  a) v (GMapEither gm1 gm2) = GMapEither (insert a v gm1) gm2
      insert (Right a) v (GMapEither gm1 gm2) = GMapEither gm1 (insert a v gm2)