1. 25 Apr, 2012 1 commit
  2. 02 Mar, 2012 1 commit
    • Simon Peyton Jones's avatar
      Hurrah! This major commit adds support for scoped kind variables, · 3bf54e78
      Simon Peyton Jones authored
      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)
      3bf54e78
  3. 13 Jan, 2012 1 commit
  4. 12 Jan, 2012 1 commit
  5. 09 Jan, 2012 1 commit
  6. 03 Jan, 2012 1 commit
    • Simon Peyton Jones's avatar
      Major refactoring of CoAxioms · 98a642cf
      Simon Peyton Jones authored
      This patch should have no user-visible effect.  It implements a
      significant internal refactoring of the way that FC axioms are
      handled.  The ultimate goal is to put us in a position to implement
      "pattern-matching axioms".  But the changes here are only does
      refactoring; there is no change in functionality.
      
      Specifically:
      
       * We now treat data/type family instance declarations very,
         very similarly to types class instance declarations:
      
         - Renamed InstEnv.Instance as InstEnv.ClsInst, for symmetry with
           FamInstEnv.FamInst.  This change does affect the GHC API, but
           for the better I think.
      
         - Previously, each family type/data instance declaration gave rise
           to a *TyCon*; typechecking a type/data instance decl produced
           that TyCon.  Now, each type/data instance gives rise to
           a *FamInst*, by direct analogy with each class instance
           declaration giving rise to a ClsInst.
      
         - Just as each ClsInst contains its evidence, a DFunId, so each FamInst
           contains its evidence, a CoAxiom.  See Note [FamInsts and CoAxioms]
           in FamInstEnv.  The CoAxiom is a System-FC thing, and can relate any
           two types, whereas the FamInst relates directly to the Haskell source
           language construct, and always has a function (F tys) on the LHS.
      
         - Just as a DFunId has its own declaration in an interface file, so now
           do CoAxioms (see IfaceSyn.IfaceAxiom).
      
         These changes give rise to almost all the refactoring.
      
       * We used to have a hack whereby a type family instance produced a dummy
         type synonym, thus
            type instance F Int = Bool -> Bool
         translated to
            axiom FInt :: F Int ~ R:FInt
            type R:FInt = Bool -> Bool
         This was always a hack, and now it's gone.  Instead the type instance
         declaration produces a FamInst, whose axiom has kind
            axiom FInt :: F Int ~ Bool -> Bool
         just as you'd expect.
      
       * Newtypes are done just as before; they generate a CoAxiom. These
         CoAxioms are "implicit" (do not generate an IfaceAxiom declaration),
         unlike the ones coming from family instance declarations.  See
         Note [Implicit axioms] in TyCon
      
      On the whole the code gets significantly nicer.  There were consequential
      tidy-ups in the vectoriser, but I think I got them right.
      98a642cf
  7. 19 Dec, 2011 1 commit
  8. 05 Dec, 2011 1 commit
    • Simon Peyton Jones's avatar
      Allow full constraint solving under a for-all (Trac #5595) · 2e6dcdf7
      Simon Peyton Jones authored
      The main idea is that when we unify
          forall a. t1  ~  forall a. t2
      we get constraints from unifying t1~t2 that mention a.
      We are producing a coercion witnessing the equivalence of
      the for-alls, and inside *that* coercion we need bindings
      for the solved constraints arising from t1~t2.
      
      We didn't have way to do this before.  The big change is
      that here's a new type TcEvidence.TcCoercion, which is
      much like Coercion.Coercion except that there's a slot
      for TcEvBinds in it.
      
      This has a wave of follow-on changes. Not deep but broad.
      
      * New module TcEvidence, which now contains the HsWrapper
        TcEvBinds, EvTerm etc types that used to be in HsBinds
      
      * The typechecker works exclusively in terms of TcCoercion.
      
      * The desugarer converts TcCoercion to Coercion
      
      * The main payload is in TcUnify.unifySigmaTy. This is the
        function that had a gross hack before, but is now beautiful.
      
      * LCoercion is gone!  Hooray.
      
      Many many fiddly changes in conssequence.  But it's nice.
      2e6dcdf7
  9. 28 Nov, 2011 1 commit
    • dimitris's avatar
      Solved goal caching and zonking optimisations. · 4bc84da3
      dimitris authored
      1) Stopped rewriting and caching solveds in the inerts because
      profiling showed that a lot of time was spent on rewriting
      already solved goals.
      
      2) Optimisations in zonkEvBinds for common-case
      evidence bindings generated from the constraint solver.
      
      3) Now solved goals cache their evidence terms, so that we can more
      aggressively optimize Refl coercions during constraint solving.
      This patch also includes a rewrite of rewriteInertEqsFromInertEq
      which greatly improves its efficiency.
      4bc84da3
  10. 17 Nov, 2011 1 commit
  11. 16 Nov, 2011 1 commit
  12. 11 Nov, 2011 1 commit
    • dreixel's avatar
      New kind-polymorphic core · 09015be8
      dreixel authored
      This big patch implements a kind-polymorphic core for GHC. The current
      implementation focuses on making sure that all kind-monomorphic programs still
      work in the new core; it is not yet guaranteed that kind-polymorphic programs
      (using the new -XPolyKinds flag) will work.
      
      For more information, see http://haskell.org/haskellwiki/GHC/Kinds
      09015be8
  13. 04 Nov, 2011 1 commit
  14. 07 Sep, 2011 2 commits
  15. 06 Sep, 2011 2 commits
    • batterseapower's avatar
      Implement -XConstraintKind · 9729fe7c
      batterseapower authored
      Basically as documented in http://hackage.haskell.org/trac/ghc/wiki/KindFact,
      this patch adds a new kind Constraint such that:
      
        Show :: * -> Constraint
        (?x::Int) :: Constraint
        (Int ~ a) :: Constraint
      
      And you can write *any* type with kind Constraint to the left of (=>):
      even if that type is a type synonym, type variable, indexed type or so on.
      
      The following (somewhat related) changes are also made:
       1. We now box equality evidence. This is required because we want
          to give (Int ~ a) the *lifted* kind Constraint
       2. For similar reasons, implicit parameters can now only be of
          a lifted kind. (?x::Int#) => ty is now ruled out
       3. Implicit parameter constraints are now allowed in superclasses
          and instance contexts (this just falls out as OK with the new
          constraint solver)
      
      Internally the following major changes were made:
       1. There is now no PredTy in the Type data type. Instead
          GHC checks the kind of a type to figure out if it is a predicate
       2. There is now no AClass TyThing: we represent classes as TyThings
          just as a ATyCon (classes had TyCons anyway)
       3. What used to be (~) is now pretty-printed as (~#). The box
          constructor EqBox :: (a ~# b) -> (a ~ b)
       4. The type LCoercion is used internally in the constraint solver
          and type checker to represent coercions with free variables
          of type (a ~ b) rather than (a ~# b)
      9729fe7c
    • batterseapower's avatar
      6bad38a4
  16. 08 Aug, 2011 1 commit
  17. 03 Aug, 2011 3 commits
  18. 23 Jul, 2011 1 commit
    • Simon Peyton Jones's avatar
      A nice tidy-up for CvSubst and liftCoSubst · 525aca2c
      Simon Peyton Jones authored
      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!
      525aca2c
  19. 15 Jul, 2011 1 commit
  20. 12 May, 2011 1 commit
    • Simon Peyton Jones's avatar
      The final batch of changes for the new coercion representation · c8c2f6bb
      Simon Peyton Jones authored
      * 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.
      c8c2f6bb
  21. 19 Apr, 2011 1 commit
    • Simon Peyton Jones's avatar
      This BIG PATCH contains most of the work for the New Coercion Representation · fdf86568
      Simon Peyton Jones authored
      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
      fdf86568
  22. 16 Jan, 2011 2 commits
    • Iavor S. Diatchki's avatar
      Add basic support for number type literals. · 9cbc204d
      Iavor S. Diatchki authored
      We add a new kind, Nat, inhabited by a family of types,
      one for each natural number:
      
      0, 1, 2 .. :: Nat
      
      In terms of GHC's sub-kind relation, Nat is only a sub-kind of itself.
      
      The numeric types are empty because there are no primitives of these
      types, and the kind "Nat" is not related to *, the kind of types which
      can be defined in Haskell programs.
      9cbc204d
    • Iavor S. Diatchki's avatar
      Fix example comment. · 2abe72b4
      Iavor S. Diatchki authored
      2abe72b4
  23. 12 Nov, 2010 1 commit
    • simonpj@microsoft.com's avatar
      A (final) re-engineering of the new typechecker · c80364f8
      simonpj@microsoft.com authored
      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
      c80364f8
  24. 06 Oct, 2010 1 commit
  25. 16 Sep, 2010 1 commit
  26. 13 Sep, 2010 1 commit
  27. 14 Jun, 2010 1 commit
  28. 01 Mar, 2010 1 commit
  29. 04 Jan, 2010 1 commit
    • simonpj@microsoft.com's avatar
      Substantial improvements to coercion optimisation · b06d623b
      simonpj@microsoft.com authored
      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.
      b06d623b
  30. 16 Dec, 2009 3 commits
  31. 11 Dec, 2009 1 commit
    • simonpj@microsoft.com's avatar
      Use full equality for CSE · 21eeb926
      simonpj@microsoft.com authored
      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
      21eeb926
  32. 12 Nov, 2009 1 commit
    • simonpj@microsoft.com's avatar
      A radical overhaul of the coercion infrastucture · cd0e2c0c
      simonpj@microsoft.com authored
      * 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.
      cd0e2c0c
  33. 08 Nov, 2009 1 commit