1. 03 Jul, 2020 1 commit
    • Simon Peyton Jones's avatar
      Improve handling of data type return kinds · 4bf18646
      Simon Peyton Jones authored
      Following a long conversation with Richard, this patch tidies up the
      handling of return kinds for data/newtype declarations (vanilla,
      family, and instance).
      I have substantially edited the Notes in TyCl, so they would
      bear careful reading.
      Fixes #18300, #18357
      In GHC.Tc.Instance.Family.newFamInst we were checking some Lint-like
      properties with ASSSERT.  Instead Richard and I have added
      a proper linter for axioms, and called it from lintGblEnv, which in
      turn is called in tcRnModuleTcRnM
      New tests (T18300, T18357) cause an ASSERT failure in HEAD.
  2. 27 May, 2020 1 commit
    • Takenobu Tani's avatar
      core-spec: Modify file paths according to new module hierarchy · ede24126
      Takenobu Tani authored and  Marge Bot's avatar Marge Bot committed
      This patch updates file paths according to new module hierarchy [1]:
        * GHC/Core.hs                <= coreSyn/CoreSyn.hs
        * GHC/Core/Coercion.hs       <= types/Coercion.hs
        * GHC/Core/Coercion/Axiom.hs <= types/CoAxiom.hs
        * GHC/Core/Coercion/Opt.hs   <= types/OptCoercion.hs
        * GHC/Core/DataCon.hs        <= basicTypes/DataCon.hs
        * GHC/Core/FamInstEnv.hs     <= types/FamInstEnv.hs
        * GHC/Core/Lint.hs           <= coreSyn/CoreLint.hs
        * GHC/Core/Subst.hs          <= coreSyn/CoreSubst.hs
        * GHC/Core/TyCo/Rep.hs       <= types/TyCoRep.hs
        * GHC/Core/TyCon.hs          <= types/TyCon.hs
        * GHC/Core/Type.hs           <= types/Type.hs
        * GHC/Core/Unify.hs          <= types/Unify.hs
        * GHC/Types/Literal.hs       <= basicTypes/Literal.hs
        * GHC/Types/Var.hs           <= basicTypes/Var.hs
      [1]: https://gitlab.haskell.org/ghc/ghc/-/wikis/Make-GHC-codebase-more-modular
      [skip ci]
  3. 21 Mar, 2020 1 commit
    • Richard Eisenberg's avatar
      Update core spec to reflect changes to Core. · 9a96ff6b
      Richard Eisenberg authored and  Marge Bot's avatar Marge Bot committed
      Key changes:
       * Adds a new rule for forall-coercions over coercion variables, which
      was implemented but conspicuously missing from the spec.
       * Adds treatment for FunCo.
       * Adds treatment for ForAllTy over coercion variables.
       * Improves commentary (including restoring a Note lost in
      03d48526) in the source.
      No changes to running code.
  4. 02 Jan, 2019 1 commit
  5. 25 Oct, 2018 1 commit
  6. 27 Jul, 2018 1 commit
    • Ningning Xie's avatar
      update core-spec for GRefl and re-factored Refl · e5f3de2c
      Ningning Xie authored and Ben Gamari's avatar Ben Gamari committed
      Ticket #15192 introduced the generalized reflexive coercion `GRefl` and
      nominal reflexive `Refl`, and removed `CoherenceCo`. Update core-spec
      accordingly.  Not sure about notations though; suggestions on more
      concise notations would be great.
      Test Plan: Read core-spec.pdf
      Reviewers: goldfire, bgamari
      Reviewed By: goldfire
      Subscribers: rwbarton, thomie, carter
      Differential Revision: https://phabricator.haskell.org/D4984
  7. 16 Jul, 2018 2 commits
    • Ryan Scott's avatar
      Modernize S_TPush in the core spec · 7fe49936
      Ryan Scott authored
      The specification for the `S_TPush` rule in the core spec's
      operational semantics is woefully out-of-date. Let's bring it in line
      with the presentation in //System FC with Explicit Kind Equality//.
      Test Plan: Read it
      Reviewers: goldfire, bgamari
      Reviewed By: goldfire
      Subscribers: rwbarton, thomie, carter
      Differential Revision: https://phabricator.haskell.org/D4970
    • Ryan Scott's avatar
      Fix parse errors in core-spec.pdf · 8b6a9e55
      Ryan Scott authored
      `core-spec.pdf` was emitting parse errors due to not specifying
      role arguments in some uses of `nth`. This patch adds those
      role arguments. (Credit goes to Richard Eisenberg for actually
      figuring out what said arguments should be.)
      Test Plan: Read it
      Reviewers: goldfire, bgamari
      Reviewed By: goldfire
      Subscribers: rwbarton, thomie, carter
      GHC Trac Issues: #15373
      Differential Revision: https://phabricator.haskell.org/D4965
  8. 12 Jul, 2018 1 commit
  9. 20 Apr, 2018 1 commit
    • Tobias Dammers's avatar
      Caching coercion roles in NthCo and coercionKindsRole refactoring · 2fbe0b51
      Tobias Dammers authored and Ben Gamari's avatar Ben Gamari committed
      While addressing nonlinear behavior related to coercion roles,
      particularly `NthCo`, we noticed that coercion roles are recalculated
      often even though they should be readily at hand already in most cases.
      This patch adds a `Role` to the `NthCo` constructor so that we can cache
      them rather than having to recalculate them on the fly.
      https://ghc.haskell.org/trac/ghc/ticket/11735#comment:23 explains the
      Performance improvement over GHC HEAD, when compiling Grammar.hs (see below):
      GHC 8.2.1:
      ghc Grammar.hs  176.27s user 0.23s system 99% cpu 2:56.81 total
      before patch (but with other optimizations applied):
      ghc Grammar.hs -fforce-recomp  175.77s user 0.19s system 100% cpu 2:55.78 total
      ../../ghc/inplace/bin/ghc-stage2 Grammar.hs  10.32s user 0.17s system 98% cpu 10.678 total
      Introduces the following regressions:
      - perf/compiler/parsing001 (possibly false positive)
      - perf/compiler/T9872
      - perf/compiler/haddock.base
      Reviewers: goldfire, bgamari, simonpj
      Reviewed By: simonpj
      Subscribers: rwbarton, thomie, carter
      GHC Trac Issues: #11735
      Differential Revision: https://phabricator.haskell.org/D4394
  10. 30 Oct, 2017 1 commit
  11. 24 Apr, 2017 1 commit
  12. 18 Apr, 2017 1 commit
  13. 02 Dec, 2016 1 commit
  14. 11 Dec, 2015 1 commit
    • eir@cis.upenn.edu's avatar
      Add kind equalities to GHC. · 67465497
      eir@cis.upenn.edu authored
      This implements the ideas originally put forward in
      "System FC with Explicit Kind Equality" (ICFP'13).
      There are several noteworthy changes with this patch:
       * We now have casts in types. These change the kind
         of a type. See new constructor `CastTy`.
       * All types and all constructors can be promoted.
         This includes GADT constructors. GADT pattern matches
         take place in type family equations. In Core,
         types can now be applied to coercions via the
         `CoercionTy` constructor.
       * Coercions can now be heterogeneous, relating types
         of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
         proves both that `t1` and `t2` are the same and also that
         `k1` and `k2` are the same.
       * The `Coercion` type has been significantly enhanced.
         The documentation in `docs/core-spec/core-spec.pdf` reflects
         the new reality.
       * The type of `*` is now `*`. No more `BOX`.
       * Users can write explicit kind variables in their code,
         anywhere they can write type variables. For backward compatibility,
         automatic inference of kind-variable binding is still permitted.
       * The new extension `TypeInType` turns on the new user-facing
       * Type families and synonyms are now promoted to kinds. This causes
         trouble with parsing `*`, leading to the somewhat awkward new
         `HsAppsTy` constructor for `HsType`. This is dispatched with in
         the renamer, where the kind `*` can be told apart from a
         type-level multiplication operator. Without `-XTypeInType` the
         old behavior persists. With `-XTypeInType`, you need to import
         `Data.Kind` to get `*`, also known as `Type`.
       * The kind-checking algorithms in TcHsType have been significantly
         rewritten to allow for enhanced kinds.
       * The new features are still quite experimental and may be in flux.
       * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.
       * TODO: Update user manual.
      Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
      Updates Haddock submodule.
  15. 24 Apr, 2015 1 commit
  16. 07 Mar, 2015 1 commit
  17. 18 Sep, 2014 1 commit
  18. 29 Jan, 2014 1 commit
  19. 14 Jan, 2014 1 commit
  20. 25 Nov, 2013 1 commit
  21. 09 Sep, 2013 1 commit
  22. 16 Aug, 2013 1 commit
    • eir@cis.upenn.edu's avatar
      Fix Trac #8138. · ac382ab9
      eir@cis.upenn.edu authored
      The code in CoreLint did not take into account the possibility of
      ~R# arguments to functions. These can arise in argToPat in SpecConstr.
      Now, CoreLint does not fail when it sees a ~R# parameter.
      This commit also updates the core-spec document accordingly.
  23. 02 Aug, 2013 2 commits
  24. 31 Jul, 2013 1 commit
  25. 21 Jun, 2013 1 commit
    • eir@cis.upenn.edu's avatar
      Revise implementation of overlapping type family instances. · 569b2652
      eir@cis.upenn.edu authored
      This commit changes the syntax and story around overlapping type
      family instances. Before, we had "unbranched" instances and
      "branched" instances. Now, we have closed type families and
      open ones.
      The behavior of open families is completely unchanged. In particular,
      coincident overlap of open type family instances still works, despite
      emails to the contrary.
      A closed type family is declared like this:
      > type family F a where
      >   F Int = Bool
      >   F a   = Char
      The equations are tried in order, from top to bottom, subject to
      certain constraints, as described in the user manual. It is not
      allowed to declare an instance of a closed family.
  26. 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
      where', followed by equations. See the new section in the user manual
      ( for details. The canonical example is Boolean equality at the
      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
      and applies only the first the matches. As explained in the note
      checking within groups] in FamInstEnv.lhs, we must be careful not to
      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
      - 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
        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
        simplification. (This is different than the normal failure to unify
        of the type family bit.) This notion in encoded in tcApartTys, in
        Because apartness is finer-grained than unification, the tcUnifyTys
        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
      - 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
         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, is updated to describe the new type
  27. 01 Dec, 2012 1 commit
    • 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.