1. 28 Jan, 2013 1 commit
    • Simon Peyton Jones's avatar
      Pure refactoring · f1fa6eb2
      Simon Peyton Jones authored
      * Move tidyType and friends from TcType to TypeRep
        (It was always wrong to have it in TcType.)
      
      * Move mkCoAxBranch and friends from FamInst to Coercion
      
      * Move pprCoAxBranch and friends from FamInstEnv to Coercion
      
      No change in functionality, though there might be a little
      wibble in error message output, because I combined two different
      functions both called pprCoAxBranch!
      f1fa6eb2
  2. 25 Jan, 2013 1 commit
  3. 22 Dec, 2012 1 commit
    • eir@cis.upenn.edu's avatar
      Implement overlapping type family instances. · 8366792e
      eir@cis.upenn.edu authored
      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.
      8366792e
  4. 19 Dec, 2012 2 commits
  5. 01 Dec, 2012 2 commits
    • Simon Peyton Jones's avatar
      Remove dead code predTreePredType · b5ce9deb
      Simon Peyton Jones authored
      b5ce9deb
    • eir@cis.upenn.edu's avatar
      Added GHC formalism to the GHC source tree. · 81b7e587
      eir@cis.upenn.edu authored
      As per a request from Simon PJ, I wrote up a formalism of the core
      language in GHC, System FC. The writeup lives in docs/core-spec.
      I also added comments to a number of files dealing with the core
      language reminding authors to update the formalism when updating the
      code. In the next commit will be a README file in docs/core-spec
      with more details of how to do this.
      81b7e587
  6. 26 Nov, 2012 1 commit
  7. 02 Oct, 2012 1 commit
  8. 17 Sep, 2012 1 commit
    • Simon Peyton Jones's avatar
      Add type "holes", enabled by -XTypeHoles, Trac #5910 · 8a9a7a8c
      Simon Peyton Jones authored
      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").
      8a9a7a8c
  9. 15 Sep, 2012 1 commit
    • Simon Peyton Jones's avatar
      Fix Trac #7237; mixup with empty tuples · 84bb8541
      Simon Peyton Jones authored
      When converting from Core to STG, we swith pattern matching on
      on a *nullary* unboxed tuple into matching using a PrimAlt on RealWorld#
         case e (RealWorld#) of { DEFAULT -> ... }
      This semms messy to me, but it works.  There was a bug in that we were
      changing to PrimAlt, but not using a DEFAULT AltCon.
      84bb8541
  10. 29 Aug, 2012 1 commit
  11. 20 Jul, 2012 1 commit
  12. 15 Jul, 2012 1 commit
  13. 13 Jun, 2012 1 commit
    • Simon Peyton Jones's avatar
      Simplify the implementation of Implicit Parameters · 5a8ac0f8
      Simon Peyton Jones authored
      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
      5a8ac0f8
  14. 15 May, 2012 1 commit
    • batterseapower's avatar
      Support code generation for unboxed-tuple function arguments · 09987de4
      batterseapower authored
      This is done by a 'unarisation' pre-pass at the STG level which
      translates away all (live) binders binding something of unboxed
      tuple type.
      
      This has the following knock-on effects:
        * The subkind hierarchy is vastly simplified (no UbxTupleKind or ArgKind)
        * Various relaxed type checks in typechecker, 'foreign import prim' etc
        * All case binders may be live at the Core level
      09987de4
  15. 10 May, 2012 1 commit
  16. 07 May, 2012 1 commit
    • Simon Peyton Jones's avatar
      Yet another major refactoring of the constraint solver · dd7522c3
      Simon Peyton Jones authored
      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.
      dd7522c3
  17. 27 Apr, 2012 1 commit
  18. 16 Apr, 2012 1 commit
  19. 05 Apr, 2012 1 commit
  20. 20 Mar, 2012 1 commit
  21. 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
  22. 17 Feb, 2012 1 commit
  23. 16 Feb, 2012 1 commit
  24. 25 Jan, 2012 1 commit
    • Iavor S. Diatchki's avatar
      Add support for type-level "strings". · 5851f847
      Iavor S. Diatchki authored
      These are types that look like "this" and "that".
      They are of kind `Symbol`, defined in module `GHC.TypeLits`.
      
      For each type-level symbol `X`, we have a singleton type, `TSymbol X`.
      
      The value of the singleton type can be named with the overloaded
      constant `tSymbol`.  Here is an example:
      
      tSymbol :: TSymbol "Hello"
      5851f847
  25. 13 Jan, 2012 1 commit
  26. 19 Dec, 2011 1 commit
  27. 13 Dec, 2011 1 commit
  28. 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
  29. 25 Nov, 2011 1 commit
  30. 21 Nov, 2011 1 commit
    • dreixel's avatar
      Rename ? to OpenKind and ?? to ArgKind · 18c7aea0
      dreixel authored
      The previous names were not informative at all, and now we have
      named kinds like Constraint and datatype promotion to kind, so
      we might as well name these too.
      
      I tried to update some comments to the new names, but certainly
      many references to the old names remain.
      18c7aea0
  31. 16 Nov, 2011 2 commits
  32. 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
  33. 05 Nov, 2011 1 commit
  34. 04 Nov, 2011 1 commit
  35. 07 Sep, 2011 1 commit
  36. 06 Sep, 2011 1 commit
    • 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
  37. 03 Aug, 2011 1 commit