1. 17 Jan, 2017 1 commit
    • David Feuer's avatar
      Split mkInlineUnfolding into two functions · d360ec39
      David Feuer authored
      Previously, `mkInlineUnfolding` took a `Maybe` argument indicating
      whether the caller requested a specific arity.  This was not
      self-documenting at call sites. Now we distinguish between
      `mkInlineUnfolding` and `mkInlineUnfoldingWithArity`.
      Reviewers: simonpj, austin, bgamari
      Reviewed By: simonpj, bgamari
      Subscribers: thomie
      Differential Revision: https://phabricator.haskell.org/D2933
  2. 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.
  3. 30 May, 2013 1 commit
    • Simon Peyton Jones's avatar
      Make 'SPECIALISE instance' work again · 1ed04090
      Simon Peyton Jones authored
      This is a long-standing regression (Trac #7797), which meant that in
      particular the Eq [Char] instance does not get specialised.
      (The *methods* do, but the dictionary itself doesn't.)  So when you
      call a function
           f :: Eq a => blah
      on a string type (ie a=[Char]), 7.6 passes a dictionary of un-specialised
      This only matters when calling an overloaded function from a
      specialised context, but that does matter in some programs.  I
      remember (though I cannot find the details) that Nick Frisby discovered
      this to be the source of some pretty solid performanc regresisons.
      Anyway it works now. The key change is that a DFunUnfolding now takes
      a form that is both simpler than before (the DFunArg type is eliminated)
      and more general:
      data Unfolding
        = ...
        | DFunUnfolding {     -- The Unfolding of a DFunId
          			-- See Note [DFun unfoldings]
            		  	--     df = /\a1..am. \d1..dn. MkD t1 .. tk
                              --                                 (op1 a1..am d1..dn)
           		      	--     	    	      	       	   (op2 a1..am d1..dn)
              df_bndrs :: [Var],      -- The bound variables [a1..m],[d1..dn]
              df_con   :: DataCon,    -- The dictionary data constructor (never a newtype datacon)
              df_args  :: [CoreExpr]  -- Args of the data con: types, superclasses and methods,
          }                           -- in positional order
      That in turn allowed me to re-enable the DFunUnfolding specialisation in
      DsBinds.  Lots of details here in TcInstDcls:
      	  Note [SPECIALISE instance pragmas]
      I also did some refactoring, in particular to pass the InScopeSet to
      exprIsConApp_maybe (which in turn means it has to go to a RuleFun).
      NB: Interface file format has changed!
  4. 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
  5. 06 Nov, 2012 1 commit
  6. 28 Jul, 2012 1 commit
  7. 27 Jun, 2012 3 commits
    • chak@cse.unsw.edu.au.'s avatar
    • chak@cse.unsw.edu.au.'s avatar
    • Simon Peyton Jones's avatar
      Add silent superclass parameters (again) · aa1e0976
      Simon Peyton Jones authored
      Silent superclass parameters solve the problem that
      the superclasses of a dicionary construction can easily
      turn out to be (wrongly) bottom.  The problem and solution
      are described in
         Note [Silent superclass arguments] in TcInstDcls
      I first implemented this fix (with Dimitrios) in Dec 2010, but removed
      it again in Jun 2011 becuase we thought it wasn't necessary any
      more. (The reason we thought it wasn't necessary is that we'd stopped
      generating derived superclass constraints for *wanteds*.  But we were
      wrong; that didn't solve the superclass-loop problem.)
      So we have to re-implement it.  It's not hard.  Main features:
        * The IdDetails for a DFunId says how many silent arguments it has
        * A DFunUnfolding describes which dictionary args are
          just parameters (DFunLamArg) and which are a function to apply
          to the parameters (DFunPolyArg).  This adds the DFunArg type
          to CoreSyn
        * Consequential changes to IfaceSyn.  (Binary hi file format changes
        * TcInstDcls changes to generate the right dfuns
        * CoreSubst.exprIsConApp_maybe handles the new DFunUnfolding
      The thing taht is *not* done yet is to alter the vectoriser to
      pass the relevant extra argument when building a PA dictionary.
  8. 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.
       * 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.
  9. 14 Nov, 2011 3 commits
  10. 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)
  11. 24 Aug, 2011 2 commits
  12. 23 Jun, 2011 1 commit
  13. 22 Jun, 2011 1 commit
    • Simon Peyton Jones's avatar
      Remove "silent superclass parameters" · a9d48fd9
      Simon Peyton Jones authored
      We introduced silent superclass parameters as a way to avoid
      superclass loops, but we now solve that problem a different
      way ("derived" superclass constraints carry no evidence). So
      they aren't needed any more.
      Apart from being a needless complication, they broke DoCon.
      Admittedly in a very obscure way, but still the result is
      hard to explain. To see the details see Trac #5051, with
      test case typecheck/should_compile/T5051.  (The test is
      nice and small!)
  14. 26 Jan, 2011 1 commit
  15. 13 Dec, 2010 1 commit
    • simonpj@microsoft.com's avatar
      Fix recursive superclasses (again). Fixes Trac #4809. · a3bab050
      simonpj@microsoft.com authored
      This patch finally deals with the super-delicate question of
      superclases in possibly-recursive dictionaries.  The key idea
      is the DFun Superclass Invariant (see TcInstDcls):
           In the body of a DFun, every superclass argument to the
           returned dictionary is
             either   * one of the arguments of the DFun,
             or       * constant, bound at top level
      To establish the invariant, we add new "silent" superclass
      argument(s) to each dfun, so that the dfun does not do superclass
      selection internally.  There's a bit of hoo-ha to make sure that
      we don't print those silent arguments in error messages; a knock
      on effect was a change in interface-file format.
      A second change is that instead of the complex and fragile
      "self dictionary binding" in TcInstDcls and TcClassDcl,
      using the same mechanism for existential pattern bindings.
      See Note [Subtle interaction of recursion and overlap] in TcInstDcls
      and Note [Binding when looking up instances] in InstEnv.
      Main notes are here:
        * Note [Silent Superclass Arguments] in TcInstDcls,
          including the DFun Superclass Invariant
      Main code changes are:
        * The code for MkId.mkDictFunId and mkDictFunTy
        * DFunUnfoldings get a little more complicated;
          their arguments are a new type DFunArg (in CoreSyn)
        * No "self" argument in tcInstanceMethod
        * No special tcSimplifySuperClasss
        * No "dependents" argument to EvDFunApp
         It turns out that it's quite tricky to generate the right
         DFunUnfolding for a specialised dfun, when you use SPECIALISE
         INSTANCE.  For now I've just commented it out (in DsBinds) but
         that'll lose some optimisation, and I need to get back to
  16. 26 Nov, 2010 3 commits
  17. 25 Nov, 2010 2 commits
  18. 14 Sep, 2010 1 commit
  19. 25 Nov, 2010 1 commit
  20. 14 Sep, 2010 1 commit
  21. 15 Sep, 2010 1 commit
  22. 09 Sep, 2010 4 commits