1. 03 Nov, 2019 1 commit
    • Ryan Scott's avatar
      Reify oversaturated data family instances correctly (#17296) · 9ecf4bb1
      Ryan Scott authored
      `TcSplice` was not properly handling oversaturated data family
      instances, such as the example in #17296, as it dropped arguments due
      to carelessly zipping data family instance arguments with
      `tyConTyVars`. For data families, the number of `tyConTyVars` can
      sometimes be less than the number of arguments it can accept in a
      data family instance due to the fact that data family instances can
      be oversaturated.
      
      To account for this, `TcSplice.mkIsPolyTvs` has now been renamed to
      `tyConArgsPolyKinded` and now factors in `tyConResKind` in addition
      to `tyConTyVars`. I've also added
      `Note [Reified instances and explicit kind signatures]` which
      explains the various subtleties in play here.
      
      Fixes #17296.
      
      (cherry picked from commit e3636a68)
      9ecf4bb1
  2. 20 Feb, 2019 1 commit
    • Richard Eisenberg's avatar
      Fix #14729 by making the normaliser homogeneous · a53b2f45
      Richard Eisenberg authored
      This ports the fix to #12919 to the normaliser. (#12919 was about
      the flattener.) Because the fix is involved, this is done by
      moving the critical piece of code to Coercion, and then calling
      this from both the flattener and the normaliser.
      
      The key bit is: simplifying type families in a type is always
      a *homogeneous* operation. See #12919 for a discussion of why
      this is the Right Way to simplify type families.
      
      Also fixes #15549.
      
      test case: dependent/should_compile/T14729{,kind}
                 typecheck/should_compile/T15549[ab]
      
      (cherry picked from commit 2b90356d)
      a53b2f45
  3. 11 Jan, 2019 1 commit
  4. 03 Dec, 2018 2 commits
    • Simon Peyton Jones's avatar
      Introduce tcTypeKind, and use it · 03d48526
      Simon Peyton Jones authored
      In the type checker Constraint and * are distinct; and the function
      that takes the kind of a type should respect that distinction
      (Trac #15971).
      
      This patch implements the change:
      
      * Introduce Type.tcTypeKind, and use it throughout the type
        inference engine
      
      * Add new Note [Kinding rules for types] for the kinding
        rules, especially for foralls.
      
      * Redefine
          isPredTy ty = tcIsConstraintKind (tcTypeKind ty)
        (it had a much more complicated definition before)
      
      Some miscellaneous refactoring
      
      * Get rid of TyCoRep.isTYPE, Kind.isTYPEApp,
        in favour of TyCoRep.kindRep, kindRep_maybe
      
      * Rename Type.getRuntimeRepFromKind_maybe
        to getRuntimeRep_maybe
      
      I did some spot-checks on compiler perf, and it really doesn't
      budge (as expected).
      03d48526
    • Ryan Scott's avatar
      Fix #15954 by rejigging check_type's order · 2e6cc3d0
      Ryan Scott authored
      Summary:
      Previously, `check_type` (which catches illegal uses of
      unsaturated type synonyms without enabling `LiberalTypeSynonyms`,
      among other things) always checks for uses of polytypes before
      anything else. There is a problem with this plan, however:
      checking for polytypes requires decomposing `forall`s and other
      invisible arguments, an action which itself expands type synonyms!
      Therefore, if we have something like:
      
      ```lang=haskell
      type A a = Int
      type B (a :: Type -> Type) = forall x. x -> x
      type C = B A
      ```
      
      Then when checking `B A`, `A` will get expanded to `forall x. x -> x`
      before `check_type` has an opportunity to realize that `A` is an
      unsaturated type synonym! This is the root cause of #15954.
      
      This patch fixes the issue by moving the case of `check_type` that
      detects polytypes to be //after// the case that checks for
      `TyConApp`s. That way, the `TyConApp` case will properly flag things
      like the unsaturated use of `A` in the example above before we ever
      attempt to check for polytypes.
      
      Test Plan: make test TEST=T15954
      
      Reviewers: simonpj, bgamari, goldfire
      
      Reviewed By: simonpj
      
      Subscribers: rwbarton, carter
      
      GHC Trac Issues: #15954
      
      Differential Revision: https://phabricator.haskell.org/D5402
      2e6cc3d0
  5. 29 Nov, 2018 1 commit
    • Simon Peyton Jones's avatar
      Taming the Kind Inference Monster · 2257a86d
      Simon Peyton Jones authored
      My original goal was (Trac #15809) to move towards using level numbers
      as the basis for deciding which type variables to generalise, rather
      than searching for the free varaibles of the environment.  However
      it has turned into a truly major refactoring of the kind inference
      engine.
      
      Let's deal with the level-numbers part first:
      
      * Augment quantifyTyVars to calculate the type variables to
        quantify using level numbers, and compare the result with
        the existing approach.  That is; no change in behaviour,
        just a WARNing if the two approaches give different answers.
      
      * To do this I had to get the level number right when calling
        quantifyTyVars, and this entailed a bit of care, especially
        in the code for kind-checking type declarations.
      
      * However, on the way I was able to eliminate or simplify
        a number of calls to solveEqualities.
      
      This work is incomplete: I'm not /using/ level numbers yet.
      When I subsequently get rid of any remaining WARNings in
      quantifyTyVars, that the level-number answers differ from
      the current answers, then I can rip out the current
      "free vars of the environment" stuff.
      
      Anyway, this led me into deep dive into kind inference for type and
      class declarations, which is an increasingly soggy part of GHC.
      Richard already did some good work recently in
      
         commit 5e45ad10
         Date:   Thu Sep 13 09:56:02 2018 +0200
      
          Finish fix for #14880.
      
          The real change that fixes the ticket is described in
          Note [Naughty quantification candidates] in TcMType.
      
      but I kept turning over stones. So this patch has ended up
      with a pretty significant refactoring of that code too.
      
      Kind inference for types and classes
      ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      
      * Major refactoring in the way we generalise the inferred kind of
        a TyCon, in kcTyClGroup.  Indeed, I made it into a new top-level
        function, generaliseTcTyCon.  Plus a new Note to explain it
        Note [Inferring kinds for type declarations].
      
      * We decided (Trac #15592) not to treat class type variables specially
        when dealing with Inferred/Specified/Required for associated types.
        That simplifies things quite a bit. I also rewrote
        Note [Required, Specified, and Inferred for types]
      
      * Major refactoring of the crucial function kcLHsQTyVars:
        I split it into
             kcLHsQTyVars_Cusk  and  kcLHsQTyVars_NonCusk
        because the two are really quite different. The CUSK case is
        almost entirely rewritten, and is much easier because of our new
        decision not to treat the class variables specially
      
      * I moved all the error checks from tcTyClTyVars (which was a bizarre
        place for it) into generaliseTcTyCon and/or the CUSK case of
        kcLHsQTyVars.  Now tcTyClTyVars is extremely simple.
      
      * I got rid of all the all the subtleties in tcImplicitTKBndrs. Indeed
        now there is no difference between tcImplicitTKBndrs and
        kcImplicitTKBndrs; there is now a single bindImplicitTKBndrs.
        Same for kc/tcExplicitTKBndrs.  None of them monkey with level
        numbers, nor build implication constraints.  scopeTyVars is gone
        entirely, as is kcLHsQTyVarBndrs. It's vastly simpler.
      
        I found I could get rid of kcLHsQTyVarBndrs entirely, in favour of
        the bnew bindExplicitTKBndrs.
      
      Quantification
      ~~~~~~~~~~~~~~
      * I now deal with the "naughty quantification candidates"
        of the previous patch in candidateQTyVars, rather than in
        quantifyTyVars; see Note [Naughty quantification candidates]
        in TcMType.
      
        I also killed off closeOverKindsCQTvs in favour of the same
        strategy that we use for tyCoVarsOfType: namely, close over kinds
        at the occurrences.
      
        And candidateQTyVars no longer needs a gbl_tvs argument.
      
      * Passing the ContextKind, rather than the expected kind itself,
        to tc_hs_sig_type_and_gen makes it easy to allocate the expected
        result kind (when we are in inference mode) at the right level.
      
      Type families
      ~~~~~~~~~~~~~~
      * I did a major rewrite of the impenetrable tcFamTyPats. The result
        is vastly more comprehensible.
      
      * I got rid of kcDataDefn entirely, quite a big function.
      
      * I re-did the way that checkConsistentFamInst works, so
        that it allows alpha-renaming of invisible arguments.
      
      * The interaction of kind signatures and family instances is tricky.
          Type families: see Note [Apparently-nullary families]
          Data families: see Note [Result kind signature for a data family instance]
                         and Note [Eta-reduction for data families]
      
      * The consistent instantation of an associated type family is tricky.
        See Note [Checking consistent instantiation] and
            Note [Matching in the consistent-instantation check]
        in TcTyClsDecls.  It's now checked in TcTyClsDecls because that is
        when we have the relevant info to hand.
      
      * I got tired of the compromises in etaExpandFamInst, so I did the
        job properly by adding a field cab_eta_tvs to CoAxBranch.
        See Coercion.etaExpandCoAxBranch.
      
      tcInferApps and friends
      ~~~~~~~~~~~~~~~~~~~~~~~
      * I got rid of the mysterious and horrible ClsInstInfo argument
        to tcInferApps, checkExpectedKindX, and various checkValid
        functions.  It was horrible!
      
      * I got rid of [Type] result of tcInferApps.  This list was used
        only in tcFamTyPats, when checking the LHS of a type instance;
        and if there is a cast in the middle, the list is meaningless.
        So I made tcInferApps simpler, and moved the complexity
        (not much) to tcInferApps.
      
        Result: tcInferApps is now pretty comprehensible again.
      
      * I refactored the many function in TcMType that instantiate skolems.
      
      Smaller things
      
      * I rejigged the error message in checkValidTelescope; I think it's
        quite a bit better now.
      
      * checkValidType was not rejecting constraints in a kind signature
           forall (a :: Eq b => blah). blah2
        That led to further errors when we then do an ambiguity check.
        So I make checkValidType reject it more aggressively.
      
      * I killed off quantifyConDecl, instead calling kindGeneralize
        directly.
      
      * I fixed an outright bug in tyCoVarsOfImplic, where we were not
        colleting the tyvar of the kind of the skolems
      
      * Renamed ClsInstInfo to AssocInstInfo, and made it into its
        own data type
      
      * Some fiddling around with pretty-printing of family
        instances which was trickier than I thought.  I wanted
        wildcards to print as plain "_" in user messages, although
        they each need a unique identity in the CoAxBranch.
      
      Some other oddments
      
      * Refactoring around the trace messages from reportUnsolved.
      * A bit of extra tc-tracing in TcHsSyn.commitFlexi
      
      This patch fixes a raft of bugs, and includes tests for them.
      
       * #14887
       * #15740
       * #15764
       * #15789
       * #15804
       * #15817
       * #15870
       * #15874
       * #15881
      2257a86d
  6. 22 Nov, 2018 2 commits
    • Ryan Scott's avatar
      Overhaul -fprint-explicit-kinds to use VKA · f5d20838
      Ryan Scott authored
      This patch changes the behavior of `-fprint-explicit-kinds`
      so that it displays kind argument using visible kind application.
      In other words, the flag now:
      
      1. Prints instantiations of specified variables with `@(...)`.
      2. Prints instantiations of inferred variables with `@{...}`.
      
      In addition, this patch removes the `Use -fprint-explicit-kinds to
      see the kind arguments` error message that often arises when a type
      mismatch occurs due to different kinds. Instead, whenever there is a
      kind mismatch, we now enable the `-fprint-explicit-kinds` flag
      locally to help cue to the programmer where the error lies.
      (See `Note [Kind arguments in error messages]` in `TcErrors`.)
      As a result, these funny `@{...}` things can now appear to the user
      even without turning on the `-fprint-explicit-kinds` flag explicitly,
      so I took the liberty of documenting them in the users' guide.
      
      Test Plan: ./validate
      
      Reviewers: goldfire, simonpj, bgamari
      
      Reviewed By: simonpj
      
      Subscribers: rwbarton, carter
      
      GHC Trac Issues: #15871
      
      Differential Revision: https://phabricator.haskell.org/D5314
      f5d20838
    • Ryan Scott's avatar
      Fix #15852 by eta expanding data family instance RHSes, too · 014d6c1f
      Ryan Scott authored
      When I defined `etaExpandFamInstLHS`, I blatantly forgot
      to eta expand the RHSes of data family instances. (Actually, I
      claimed that they didn't //need// to be eta expanded. I'm not sure
      what I was thinking.)
      
      This fixes the issue by changing `etaExpandFamInstLHS` to
      `etaExpandFamInst` and, well, making it actually eta expand the RHS.
      
      Test Plan: make test TEST=T15852
      
      Reviewers: goldfire, bgamari
      
      Reviewed By: goldfire
      
      Subscribers: rwbarton, carter
      
      GHC Trac Issues: #15852
      
      Differential Revision: https://phabricator.haskell.org/D5328
      014d6c1f
  7. 08 Nov, 2018 1 commit
    • Ryan Scott's avatar
      Fix #15845 by defining etaExpandFamInstLHS and using it · 63a81707
      Ryan Scott authored
      Summary:
      Both #9692 and #14179 were caused by GHC being careless
      about using eta-reduced data family instance axioms. Each of those
      tickets were fixed by manually whipping up some code to eta-expand
      the axioms. The same sort of issue has now caused #15845, so I
      figured it was high time to factor out the code that each of these
      fixes have in common.
      
      This patch introduces the `etaExpandFamInstLHS` function, which takes
      a family instance's type variables, LHS types, and RHS type, and
      returns type variables and LHS types that have been eta-expanded if
      necessary, in the case of a data family instance. (If it's a type
      family instance, `etaExpandFamInstLHS` just returns the supplied type
      variables and LHS types unchanged).
      
      Along the way, I noticed that many references to
      `Note [Eta reduction for data families]` (in `FamInstEnv`) had
      slightly bitrotted (they either referred to a somewhat different
      name, or claimed that the Note lived in a different module), so
      I took the liberty of cleaning those up.
      
      Test Plan: make test TEST="T9692 T15845"
      
      Reviewers: goldfire, bgamari
      
      Reviewed By: goldfire
      
      Subscribers: rwbarton, carter
      
      GHC Trac Issues: #15845
      
      Differential Revision: https://phabricator.haskell.org/D5294
      63a81707
  8. 29 Oct, 2018 1 commit
    • Tobias Dammers's avatar
      Finish fix for #14880. · 5e45ad10
      Tobias Dammers authored
      The real change that fixes the ticket is described in
      Note [Naughty quantification candidates] in TcMType.
      
      Fixing this required reworking candidateQTyVarsOfType, the function
      that extracts free variables as candidates for quantification.
      One consequence is that we now must be more careful when quantifying:
      any skolems around must be quantified manually, and quantifyTyVars
      will now only quantify over metavariables. This makes good sense,
      as skolems are generally user-written and are listed in the AST.
      
      As a bonus, we now have more control over the ordering of such
      skolems.
      
      Along the way, this commit fixes #15711 and refines the fix
      to #14552 (by accepted a program that was previously rejected,
      as we can now accept that program by zapping variables to Any).
      
      This commit also does a fair amount of rejiggering kind inference
      of datatypes. Notably, we now can skip the generalization step
      in kcTyClGroup for types with CUSKs, because we get the
      kind right the first time. This commit also thus fixes #15743 and
       #15592, which both concern datatype kind generalisation.
      (#15591 is also very relevant.) For this aspect of the commit, see
      Note [Required, Specified, and Inferred in types] in TcTyClsDecls.
      
      Test cases: dependent/should_fail/T14880{,-2},
                  dependent/should_fail/T15743[cd]
                  dependent/should_compile/T15743{,e}
                  ghci/scripts/T15743b
                  polykinds/T15592
                  dependent/should_fail/T15591[bc]
                  ghci/scripts/T15591
      5e45ad10
  9. 24 Oct, 2018 2 commits
    • Simon Peyton Jones's avatar
      Refactor the treatment of predicate types · 0faf7fd3
      Simon Peyton Jones authored
      Trac #15648 showed that GHC was a bit confused about the
      difference between the types for
      
      * Predicates
      * Coercions
      * Evidence (in the typechecker constraint solver)
      
      This patch cleans it up. See especially Type.hs
      Note [Types for coercions, predicates, and evidence]
      
      Particular changes
      
      * Coercion types (a ~# b) and (a ~#R b) are not predicate types
        (so isPredTy reports False for them) and are not implicitly
        instantiated by the type checker.  This is a real change, but
        it consistently reflects that fact that (~#) and (~R#) really
        are different from predicates.
      
      * isCoercionType is renamed to isCoVarType
      
      * During type inference, simplifyInfer, we do /not/ want to infer
        a constraint (a ~# b), because that is no longer a predicate type.
        So we 'lift' it to (a ~ b). See TcType
        Note [Lift equality constaints when quantifying]
      
      * During type inference for pattern synonyms, we need to 'lift'
        provided constraints of type (a ~# b) to (a ~ b).  See
        Note [Equality evidence in pattern synonyms] in PatSyn
      
      * But what about (forall a. Eq a => a ~# b)? Is that a
        predicate type?  No -- it does not have kind Constraint.
        Is it an evidence type?  Perhaps, but awkwardly so.
      
        In the end I decided NOT to make it an evidence type,
        and to ensure the the type inference engine never
        meets it.  This made me /simplify/ the code in
        TcCanonical.makeSuperClasses; see TcCanonical
        Note [Equality superclasses in quantified constraints]
      
        Instead I moved the special treatment for primitive
        equality to TcInteract.doTopReactOther.  See TcInteract
        Note [Looking up primitive equalities in quantified constraints]
      
        Also see Note [Evidence for quantified constraints] in Type.
      
        All this means I can have
           isEvVarType ty = isCoVarType ty || isPredTy ty
        which is nice.
      
      All in all, rather a lot of work for a small refactoring,
      but I think it's a real improvement.
      0faf7fd3
    • Ryan Scott's avatar
      Fix #15792 by not reifying invisible arguments in AppTys · bfd93f90
      Ryan Scott authored
      Summary:
      The `reifyType` function in `TcSplice` is carefully designed
      to avoid reifying visible arguments to `TyConApp`s. However, the same
      care was not given towards the `AppTy` case, which lead to #15792.
      
      This patch changes to the `AppTy` case of `reifyType` so that it
      consults the kind of the function type to determine which of the
      argument types are invisible (and therefore should be dropped) during
      reification. This required crafting a variant of `tyConArgFlags`,
      which I dubbed `appTyArgFlags`, that accept an arbitrary function
      `Type` instead of a `TyCon`.
      
      Test Plan: make test TEST=T15792
      
      Reviewers: goldfire, bgamari, simonpj
      
      Reviewed By: simonpj
      
      Subscribers: simonpj, rwbarton, carter
      
      GHC Trac Issues: #15792
      
      Differential Revision: https://phabricator.haskell.org/D5252
      bfd93f90
  10. 01 Oct, 2018 1 commit
    • Ryan Scott's avatar
      Fix #15637 by using VTA more in GND · 309438e9
      Ryan Scott authored
      Summary:
      The code that GND was generating before could crumple over
      if it derived an instance for a class with an ambiguous type variable
      in the class head, such as the example in #15637. The solution is
      straightforward: simply instantiate all variables bound by the class
      head explicitly using visible type application, which will nip any
      ambiguity in the bud.
      
      Test Plan: make test TEST=T15637
      
      Reviewers: bgamari, simonpj, goldfire
      
      Reviewed By: simonpj
      
      Subscribers: simonpj, rwbarton, carter
      
      GHC Trac Issues: #15637
      
      Differential Revision: https://phabricator.haskell.org/D5148
      309438e9
  11. 15 Sep, 2018 1 commit
    • Ningning Xie's avatar
      Coercion Quantification · ea5ade34
      Ningning Xie authored
      This patch corresponds to #15497.
      
      According to https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2,
       we would like to have coercion quantifications back. This will
      allow us to migrate (~#) to be homogeneous, instead of its current
      heterogeneous definition. This patch is (lots of) plumbing only. There
      should be no user-visible effects.
      
      An overview of changes:
      
      - Both `ForAllTy` and `ForAllCo` can quantify over coercion variables,
      but only in *Core*. All relevant functions are updated accordingly.
      - Small changes that should be irrelevant to the main task:
          1. removed dead code `mkTransAppCo` in Coercion
          2. removed out-dated Note Computing a coercion kind and
             roles in Coercion
          3. Added `Eq4` in Note Respecting definitional equality in
             TyCoRep, and updated `mkCastTy` accordingly.
          4. Various updates and corrections of notes and typos.
      - Haddock submodule needs to be changed too.
      
      Acknowledgments:
      This work was completed mostly during Ningning Xie's Google Summer
      of Code, sponsored by Google. It was advised by Richard Eisenberg,
      supported by NSF grant 1704041.
      
      Test Plan: ./validate
      
      Reviewers: goldfire, simonpj, bgamari, hvr, erikd, simonmar
      
      Subscribers: RyanGlScott, monoidal, rwbarton, carter
      
      GHC Trac Issues: #15497
      
      Differential Revision: https://phabricator.haskell.org/D5054
      ea5ade34
  12. 02 Sep, 2018 1 commit
    • Ryan Scott's avatar
      Reject class instances with type families in kinds · 6dea7c16
      Ryan Scott authored
      Summary:
      GHC doesn't know how to handle type families that appear in
      class instances. Unfortunately, GHC didn't reject instances where
      type families appear in //kinds//, leading to #15515. This is easily
      rectified by calling `checkValidTypePat` on all arguments to a class
      in an instance (and not just the type arguments).
      
      Test Plan: make test TEST=T15515
      
      Reviewers: bgamari, goldfire, simonpj
      
      Reviewed By: simonpj
      
      Subscribers: simonpj, rwbarton, carter
      
      GHC Trac Issues: #15515
      
      Differential Revision: https://phabricator.haskell.org/D5068
      6dea7c16
  13. 31 Aug, 2018 1 commit
  14. 28 Aug, 2018 1 commit
    • Ryan Scott's avatar
      Rename kind vars in left-to-right order in bindHsQTyVars · 102284e7
      Ryan Scott authored
      Summary:
      When renaming kind variables in an `LHsQTyVars`, we were
      erroneously putting all of the kind variables in the binders
      //after// the kind variables in the body, resulting in #15568. The
      fix is simple: just swap the order of these two around.
      
      Test Plan: make test TEST=T15568
      
      Reviewers: simonpj, bgamari, goldfire
      
      Reviewed By: goldfire
      
      Subscribers: goldfire, rwbarton, carter
      
      GHC Trac Issues: #15568
      
      Differential Revision: https://phabricator.haskell.org/D5108
      102284e7
  15. 22 Aug, 2018 1 commit
    • Simon Peyton Jones's avatar
      Turn infinite loop into a panic · db6f1d9c
      Simon Peyton Jones authored
      In these two functions
        * TcIface.toIfaceAppTyArgsX
        * Type.piResultTys
      we take a type application (f t1 .. tn) and try to find
      its kind. It turned out that, if (f t1 .. tn) was ill-kinded
      the function would go into an infinite loop.
      
      That's not good: it caused the loop in Trac #15473.
      
      This patch doesn't fix the bug in #15473, but it does turn the
      loop into a decent panic, which is a step forward.
      db6f1d9c
  16. 21 Aug, 2018 1 commit
    • Andreas Klebinger's avatar
      Replace most occurences of foldl with foldl'. · 09c1d5af
      Andreas Klebinger authored
      This patch adds foldl' to GhcPrelude and changes must occurences
      of foldl to foldl'. This leads to better performance especially
      for quick builds where GHC does not perform strictness analysis.
      
      It does change strictness behaviour when we use foldl' to turn
      a argument list into function applications. But this is only a
      drawback if code looks ONLY at the last argument but not at the first.
      And as the benchmarks show leads to fewer allocations in practice
      at O2.
      
      Compiler performance for Nofib:
      
      O2 Allocations:
              -1 s.d.                -----            -0.0%
              +1 s.d.                -----            -0.0%
              Average                -----            -0.0%
      
      O2 Compile Time:
              -1 s.d.                -----            -2.8%
              +1 s.d.                -----            +1.3%
              Average                -----            -0.8%
      
      O0 Allocations:
              -1 s.d.                -----            -0.2%
              +1 s.d.                -----            -0.1%
              Average                -----            -0.2%
      
      Test Plan: ci
      
      Reviewers: goldfire, bgamari, simonmar, tdammers, monoidal
      
      Reviewed By: bgamari, monoidal
      
      Subscribers: tdammers, rwbarton, thomie, carter
      
      Differential Revision: https://phabricator.haskell.org/D4929
      09c1d5af
  17. 06 Aug, 2018 1 commit
    • Piyush P Kurur's avatar
      Support typechecking of type literals in backpack · 7d771987
      Piyush P Kurur authored
      Backpack is unable to type check signatures that expect a data which
      is a type level literal. This was reported in issue #15138. These
      commits are a fix for this. It also includes a minimal test case that
      was mentioned in the issue.
      
      Reviewers: bgamari, ezyang, goldfire
      
      Reviewed By: bgamari, ezyang
      
      Subscribers: simonpj, ezyang, rwbarton, thomie, carter
      
      GHC Trac Issues: #15138
      
      Differential Revision: https://phabricator.haskell.org/D4951
      7d771987
  18. 01 Aug, 2018 1 commit
    • Richard Eisenberg's avatar
      Remove the type-checking knot. · f8618a9b
      Richard Eisenberg authored
      Bug #15380 hangs because a knot-tied TyCon ended up in a kind.
      Looking at the code in tcInferApps, I'm amazed this hasn't happened
      before! I couldn't think of a good way to fix it (with dependent
      types, we can't really keep types out of kinds, after all), so
      I just went ahead and removed the knot.
      
      This was remarkably easy to do. In tcTyVar, when we find a TcTyCon,
      just use it. (Previously, we looked up the knot-tied TyCon and used
      that.) Then, during the final zonk, replace TcTyCons with the real,
      full-blooded TyCons in the global environment. It's all very easy.
      
      The new bit is explained in the existing
      Note [Type checking recursive type and class declarations]
      in TcTyClsDecls.
      
      Naturally, I removed various references to the knot and the
      zonkTcTypeInKnot (and related) functions. Now, we can print types
      during type checking with abandon!
      
      NB: There is a teensy error message regression with this patch,
      around the ordering of quantified type variables. This ordering
      problem is fixed (I believe) with the patch for #14880. The ordering
      affects only internal variables that cannot be instantiated with
      any kind of visible type application.
      
      There is also a teensy regression around the printing of types
      in TH splices. I think this is really a TH bug and will file
      separately.
      
      Test case: dependent/should_fail/T15380
      f8618a9b
  19. 25 Jul, 2018 1 commit
    • Simon Peyton Jones's avatar
      Treat isConstraintKind more consistently · c5d31df7
      Simon Peyton Jones authored
      It turned out that we were not being consistent
      about our use of isConstraintKind.
      
      It's delicate, because the typechecker treats Constraint and Type as
      /distinct/, whereas they are the /same/ in the rest of the compiler
      (Trac #11715).
      
      And had it wrong, which led to Trac #15412.  This patch does the
      following:
      
      * Rename isConstraintKind      to tcIsConstraintKind
               returnsConstraintKind to tcReturnsConstraintKind
        to emphasise that they use the 'tcView' view of types.
      
      * Move these functions, and some related ones (tcIsLiftedTypeKind),
        from Kind.hs, to group together in Type.hs, alongside isPredTy.
      
      It feels very unsatisfactory that these 'tcX' functions live in Type,
      but it happens because isPredTy is called later in the compiler
      too.  But it's a consequence of the 'Constraint vs Type' dilemma.
      c5d31df7
  20. 24 Jul, 2018 1 commit
    • Simon Peyton Jones's avatar
      Fix a nasty bug in piResultTys · e1b5a117
      Simon Peyton Jones authored
      I was failing to instantiate vigorously enough in Type.piResultTys
      and in the very similar function ToIface.toIfaceAppArgsX
      
      This caused Trac #15428.  The fix is easy.
      
      See Note [Care with kind instantiation] in Type.hs
      e1b5a117
  21. 10 Jul, 2018 3 commits
    • Richard Eisenberg's avatar
      Note [Ordering of implicit variables] · 7f4dd888
      Richard Eisenberg authored
      This addresses #14808
      
      [ci skip]
      7f4dd888
    • Simon Peyton Jones's avatar
      Fix decompsePiCos and visible type application · aedbf7f1
      Simon Peyton Jones authored
      Trac #15343 was caused by two things
      
      First, in TcHsType.tcHsTypeApp, which deals with the type argment
      in visible type application, we were failing to call
      solveLocalEqualities. But the type argument is like a user type
      signature so it's at least inconsitent not to do so.
      
      I thought that would nail it.  But it didn't. It turned out that we
      were ended up calling decomposePiCos on a type looking like this
          (f |> co) Int
      
      where co :: (forall a. ty) ~ (t1 -> t2)
      
      Now, 'co' is insoluble, and we'll report that later.  But meanwhile
      we don't want to crash in decomposePiCos.
      
      My fix involves keeping track of the type on both sides of the
      coercion, and ensuring that the outer shape matches before
      decomposing.  I wish there was a simpler way to do this. But
      I think this one is at least robust.
      
      I suppose it is possible that the decomposePiCos fix would
      have cured the original report, but I'm leaving the one-line
      tcHsTypeApp fix in too because it just seems more consistent.
      aedbf7f1
    • Ningning Xie's avatar
      Refactor coercion rule · 55a3f855
      Ningning Xie authored
      Summary:
      The patch is an attempt on #15192.
      
      It defines a new coercion rule
      
      ```
       | GRefl Role Type MCoercion
      ```
      
      which correspondes to the typing rule
      
      ```
           t1 : k1
        ------------------------------------
        GRefl r t1 MRefl: t1 ~r t1
      
           t1 : k1       co :: k1 ~ k2
        ------------------------------------
        GRefl r t1 (MCo co) : t1 ~r t1 |> co
      ```
      
      MCoercion wraps a coercion, which might be reflexive (MRefl)
      or not (MCo co). To know more about MCoercion see #14975.
      
      We keep Refl ty as a special case for nominal reflexive coercions,
      naemly, Refl ty :: ty ~n ty.
      
      This commit is meant to be a general performance improvement,
      but there are a few regressions. See #15192, comment:13 for
      more information.
      
      Test Plan: ./validate
      
      Reviewers: bgamari, goldfire, simonpj
      
      Subscribers: rwbarton, thomie, carter
      
      GHC Trac Issues: #15192
      
      Differential Revision: https://phabricator.haskell.org/D4747
      55a3f855
  22. 18 Jun, 2018 1 commit
    • Simon Peyton Jones's avatar
      Two small refactorings · 850ae8c5
      Simon Peyton Jones authored
      * Define Type.substTyVarBndrs, and use it
      
      * Rename substTyVarBndrCallback to substTyVarBndrUsing,
        and other analogous higher order functions.  I kept
        stumbling over the name.
      850ae8c5
  23. 15 Jun, 2018 1 commit
    • Simon Peyton Jones's avatar
      Fix corner case in typeKind, plus refactoring · f903e551
      Simon Peyton Jones authored
      This is a continuation of
      
          commit 9d600ea6
          Author: Simon Peyton Jones <simonpj@microsoft.com>
          Date:   Fri Jun 1 16:36:57 2018 +0100
      
              Expand type synonyms when Linting a forall
      
      That patch pointed out that there was a lurking hole in
      typeKind, where it could return an ill-scoped kind, because
      of not expanding type synonyms enough.
      
      This patch fixes it, quite nicely
      
      * Use occCheckExpand to expand those synonyms (it was always
        designed for that exact purpose), and call it from
               Type.typeKind
               CoreUtils.coreAltType
               CoreLint.lintTYpe
      
      * Consequently, move occCheckExpand from TcUnify.hs to
        Type.hs, and generalise it to take a list of type variables.
      
      I also tidied up lintType a bit.
      f903e551
  24. 14 Jun, 2018 1 commit
    • Vladislav Zavialov's avatar
      Embrace -XTypeInType, add -XStarIsType · d650729f
      Vladislav Zavialov authored
      Summary:
      Implement the "Embrace Type :: Type" GHC proposal,
      .../ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst
      
      GHC 8.0 included a major change to GHC's type system: the Type :: Type
      axiom. Though casual users were protected from this by hiding its
      features behind the -XTypeInType extension, all programs written in GHC
      8+ have the axiom behind the scenes. In order to preserve backward
      compatibility, various legacy features were left unchanged. For example,
      with -XDataKinds but not -XTypeInType, GADTs could not be used in types.
      Now these restrictions are lifted and -XTypeInType becomes a redundant
      flag that will be eventually deprecated.
      
      * Incorporate the features currently in -XTypeInType into the
        -XPolyKinds and -XDataKinds extensions.
      * Introduce a new extension -XStarIsType to control how to parse * in
        code and whether to print it in error messages.
      
      Test Plan: Validate
      
      Reviewers: goldfire, hvr, bgamari, alanz, simonpj
      
      Reviewed By: goldfire, ...
      d650729f
  25. 04 Jun, 2018 2 commits
    • Simon Peyton Jones's avatar
      Implement QuantifiedConstraints · 7df58960
      Simon Peyton Jones authored
      We have wanted quantified constraints for ages and, as I hoped,
      they proved remarkably simple to implement.   All the machinery was
      already in place.
      
      The main ticket is Trac #2893, but also relevant are
        #5927
        #8516
        #9123 (especially!  higher kinded roles)
        #14070
        #14317
      
      The wiki page is
        https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
      which in turn contains a link to the GHC Proposal where the change
      is specified.
      
      Here is the relevant Note:
      
      Note [Quantified constraints]
      ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      The -XQuantifiedConstraints extension allows type-class contexts like
      this:
      
        data Rose f x = Rose x (f (Rose f x))
      
        instance (Eq a, forall b. Eq b => Eq (f b))
              => Eq (Rose f a)  where
          (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2
      
      Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
      This quantified constraint is needed to solve the
       [W] (Eq (f (Rose f x)))
      constraint which arises form the (==) definition.
      
      Here are the moving parts
        * Language extension {-# LANGUAGE QuantifiedConstraints #-}
          and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension
      
        * A new form of evidence, EvDFun, that is used to discharge
          such wanted constraints
      
        * checkValidType gets some changes to accept forall-constraints
          only in the right places.
      
        * Type.PredTree gets a new constructor ForAllPred, and
          and classifyPredType analyses a PredType to decompose
          the new forall-constraints
      
        * Define a type TcRnTypes.QCInst, which holds a given
          quantified constraint in the inert set
      
        * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst],
          which holds all the Given forall-constraints.  In effect,
          such Given constraints are like local instance decls.
      
        * When trying to solve a class constraint, via
          TcInteract.matchInstEnv, use the InstEnv from inert_insts
          so that we include the local Given forall-constraints
          in the lookup.  (See TcSMonad.getInstEnvs.)
      
        * topReactionsStage calls doTopReactOther for CIrredCan and
          CTyEqCan, so they can try to react with any given
          quantified constraints (TcInteract.matchLocalInst)
      
        * TcCanonical.canForAll deals with solving a
          forall-constraint.  See
             Note [Solving a Wanted forall-constraint]
             Note [Solving a Wanted forall-constraint]
      
        * We augment the kick-out code to kick out an inert
          forall constraint if it can be rewritten by a new
          type equality; see TcSMonad.kick_out_rewritable
      
      Some other related refactoring
      ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      
      * Move SCC on evidence bindings to post-desugaring, which fixed
        #14735, and is generally nicer anyway because we can use
        existing CoreSyn free-var functions.  (Quantified constraints
        made the free-vars of an ev-term a bit more complicated.)
      
      * In LookupInstResult, replace GenInst with OneInst and NotSure,
        using the latter for multiple matches and/or one or more
        unifiers
      7df58960
    • Simon Peyton Jones's avatar
      Expand type synonyms when Linting a forall · 9d600ea6
      Simon Peyton Jones authored
      Trac #14939 showed a type like
         type Alg cls ob = ob
         f :: forall (cls :: * -> Constraint) (b :: Alg cls *). b
      
      where the kind of the forall looks like (Alg cls *), with a
      free cls. This tripped up Core Lint.
      
      I fixed this by making Core Lint a bit more forgiving, expanding
      type synonyms if necessary.
      
      I'm worried that this might not be the whole story; notably
      typeKind looks suspect.  But it certainly fixes this problem.
      9d600ea6
  26. 14 May, 2018 1 commit
    • Ryan Scott's avatar
      Fix #14875 by introducing PprPrec, and using it · 21e1a00c
      Ryan Scott authored
      Trying to determine when to insert parentheses during TH
      conversion is a bit of a mess. There is an assortment of functions
      that try to detect this, such as:
      
      * `hsExprNeedsParens`
      * `isCompoundHsType`
      * `hsPatNeedsParens`
      * `isCompoundPat`
      * etc.
      
      To make things worse, each of them have slightly different semantics.
      Plus, they don't work well in the presence of explicit type
      signatures, as #14875 demonstrates.
      
      All of these problems can be alleviated with the use of an explicit
      precedence argument (much like what `showsPrec` currently does). To
      accomplish this, I introduce a new `PprPrec` data type, and define
      standard predences for things like function application, infix
      operators, function arrows, and explicit type signatures (that last
      one is new). I then added `PprPrec` arguments to the various
      `-NeedsParens` functions, and use them to make smarter decisions
      about when things need to be parenthesized.
      
      A nice side effect is that functions like `isCompoundHsType` are
      now completely unneeded, since they're simply aliases for
      `hsTypeNeedsParens appPrec`. As a result, I did a bit of refactoring
      to remove these sorts of functions. I also did a pass over various
      utility functions in GHC for constructing AST forms and used more
      appropriate precedences where convenient.
      
      Along the way, I also ripped out the existing `TyPrec`
      data type (which was tailor-made for pretty-printing `Type`s) and
      replaced it with `PprPrec` for consistency.
      
      Test Plan: make test TEST=T14875
      
      Reviewers: alanz, goldfire, bgamari
      
      Reviewed By: bgamari
      
      Subscribers: rwbarton, thomie, carter
      
      GHC Trac Issues: #14875
      
      Differential Revision: https://phabricator.haskell.org/D4688
      21e1a00c
  27. 20 Apr, 2018 1 commit
    • Tobias Dammers's avatar
      Caching coercion roles in NthCo and coercionKindsRole refactoring · 2fbe0b51
      Tobias Dammers authored
      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
      approach.
      
      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
      ```
      
      after:
      ```
      ../../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
      2fbe0b51
  28. 01 Apr, 2018 1 commit
    • Richard Eisenberg's avatar
      Track type variable scope more carefully. · faec8d35
      Richard Eisenberg authored
      The main job of this commit is to track more accurately the scope
      of tyvars introduced by user-written foralls. For example, it would
      be to have something like this:
      
        forall a. Int -> (forall k (b :: k). Proxy '[a, b]) -> Bool
      
      In that type, a's kind must be k, but k isn't in scope. We had a
      terrible way of doing this before (not worth repeating or describing
      here, but see the old tcImplicitTKBndrs and friends), but now
      we have a principled approach: make an Implication when kind-checking
      a forall. Doing so then hooks into the existing machinery for
      preventing skolem-escape, performing floating, etc. This also means
      that we bump the TcLevel whenever going into a forall.
      
      The new behavior is done in TcHsType.scopeTyVars, but see also
      TcHsType.tc{Im,Ex}plicitTKBndrs, which have undergone significant
      rewriting. There are several Notes near there to guide you. Of
      particular interest there is that Implication constraints can now
      have skolems that are out of order; this situation is reported in
      TcErrors.
      
      A major consequence of this is a slightly tweaked process for type-
      checking type declarations. The new Note [Use SigTvs in kind-checking
      pass] in TcTyClsDecls lays it out.
      
      The error message for dependent/should_fail/TypeSkolEscape has become
      noticeably worse. However, this is because the code in TcErrors goes to
      some length to preserve pre-8.0 error messages for kind errors. It's time
      to rip off that plaster and get rid of much of the kind-error-specific
      error messages. I tried this, and doing so led to a lovely error message
      for TypeSkolEscape. So: I'm accepting the error message quality regression
      for now, but will open up a new ticket to fix it, along with a larger
      error-message improvement I've been pondering. This applies also to
      dependent/should_fail/{BadTelescope2,T14066,T14066e}, polykinds/T11142.
      
      Other minor changes:
       - isUnliftedTypeKind didn't look for tuples and sums. It does now.
      
       - check_type used check_arg_type on both sides of an AppTy. But the left
         side of an AppTy isn't an arg, and this was causing a bad error message.
         I've changed it to use check_type on the left-hand side.
      
       - Some refactoring around when we print (TYPE blah) in error messages.
         The changes decrease the times when we do so, to good effect.
         Of course, this is still all controlled by
         -fprint-explicit-runtime-reps
      
      Fixes #14066 #14749
      
      Test cases: dependent/should_compile/{T14066a,T14749},
                  dependent/should_fail/T14066{,c,d,e,f,g,h}
      faec8d35
  29. 27 Mar, 2018 1 commit
  30. 26 Mar, 2018 2 commits
    • alexvieth's avatar
      Fix performance of flattener patch (#12919) · b47a6c3a
      alexvieth authored
      This patch, authored by alexvieth and reviewed at D4451,
      makes performance improvements by critically optimizing parts
      of the flattener.
      
      Summary:
      T3064, T5321FD, T5321Fun, T9872a, T9872b, T9872c all pass.
      T9872a and T9872c show improvements beyond the -5% threshold.
      T9872d fails at 10.9% increased allocations.
      b47a6c3a
    • Richard Eisenberg's avatar
      Fix #12919 by making the flattener homegeneous. · e3dbb44f
      Richard Eisenberg authored
      This changes a key invariant of the flattener. Previously,
      flattening a type meant flattening its kind as well. But now,
      flattening is always homogeneous -- that is, the kind of the
      flattened type is the same as the kind of the input type.
      This is achieved by various wizardry in the TcFlatten.flatten_many
      function, as described in Note [flatten_many].
      
      There are several knock-on effects, including some refactoring
      in the canonicalizer to take proper advantage of the flattener's
      changed behavior. In particular, the tyvar case of can_eq_nc' no
      longer needs to take casts into account.
      
      Another effect is that flattening a tyconapp might change it
      into a casted tyconapp. This might happen if the result kind
      of the tycon contains a variable, and that variable changes
      during flattening. Because the flattener is homogeneous, it tacks
      on a cast to keep the tyconapp kind the same. However, this
      is problematic when flattening CFunEqCans, which need to have
      an uncasted tyconapp on the LHS and must remain homogeneous.
      The solution is a more involved canCFunEqCan, described in
      Note [canCFunEqCan].
      
      This patch fixes #13643 (as tested in typecheck/should_compile/T13643)
      and the panic in typecheck/should_compile/T13822 (as reported in #14024).
      Actually, there were two bugs in T13822: the first was just some
      incorrect logic in tryFill (part of the unflattener) -- also fixed
      in this patch -- and the other was the main bug fixed in this ticket.
      
      The changes in this patch exposed a long-standing flaw in OptCoercion,
      in that breaking apart an AppCo sometimes has unexpected effects on
      kinds. See new Note [EtaAppCo] in OptCoercion, which explains the
      problem and fix.
      
      Also here is a reversion of the major change in
      09bf135a, affecting ctEvCoercion.
      It turns out that making the flattener homogeneous changes the
      invariants on the algorithm, making the change in that patch
      no longer necessary.
      
      This patch also fixes:
        #14038 (dependent/should_compile/T14038)
        #13910 (dependent/should_compile/T13910)
        #13938 (dependent/should_compile/T13938)
        #14441 (typecheck/should_compile/T14441)
        #14556 (dependent/should_compile/T14556)
        #14720 (dependent/should_compile/T14720)
        #14749 (typecheck/should_compile/T14749)
      
      Sadly, this patch negatively affects performance of type-family-
      heavy code. The following patch fixes these performance degradations.
      However, the performance fixes are somewhat invasive and so I've
      kept them as a separate patch, labeling this one as [skip ci] so
      that validation doesn't fail on the performance cases.
      e3dbb44f
  31. 07 Feb, 2018 1 commit
  32. 26 Jan, 2018 1 commit
    • Joachim Breitner's avatar
      Turn EvTerm (almost) into CoreExpr (#14691) · 0e022e56
      Joachim Breitner authored
      Ideally, I'd like to do
      
          type EvTerm = CoreExpr
      
      and the type checker builds the evidence terms as it goes. This failed,
      becuase the evidence for `Typeable` refers to local identifiers that are
      added *after* the typechecker solves constraints. Therefore, `EvTerm`
      stays a data type with two constructors: `EvExpr` for `CoreExpr`
      evidence, and `EvTypeable` for the others.
      
      Delted `Note [Memoising typeOf]`, its reference (and presumably
      relevance) was removed in 8fa4bf9a.
      
      Differential Revision: https://phabricator.haskell.org/D4341
      0e022e56
  33. 03 Jan, 2018 1 commit