1. 26 Sep, 2020 1 commit
  2. 24 Sep, 2020 2 commits
    • Simon Peyton Jones's avatar
      Improve kind generalisation, error messages · 9fa26aa1
      Simon Peyton Jones authored and  Marge Bot's avatar Marge Bot committed
      This patch does two things:
      * It refactors GHC.Tc.Errors a bit.  In debugging Quick Look I was
        forced to look in detail at error messages, and ended up doing a bit
        of refactoring, esp in mkTyVarEqErr'.  It's still quite a mess, but
        a bit better, I think.
      * It makes a significant improvement to the kind checking of type and
        class declarations. Specifically, we now ensure that if kind
        checking fails with an unsolved constraint, all the skolems are in
        scope.  That wasn't the case before, which led to some obscure error
        messages; and occasional failures with "no skolem info" (eg #16245).
      Both of these, and the main Quick Look patch itself, affect a /lot/ of
      error messages, as you can see from the number of files changed.  I've
      checked them all; I think they are as good or better than before.
      Smaller things
      * I documented the various instances of VarBndr better.
        See Note [The VarBndr tyep and its uses] in GHC.Types.Var
      * Renamed GHC.Tc.Solver.simpl_top to simplifyTopWanteds
      * A bit of refactoring in bindExplicitTKTele, to avoid the
        footwork with Either.  Simpler now.
      * Move promoteTyVar from GHC.Tc.Solver to GHC.Tc.Utils.TcMType
      Fixes #16245 (comment 211369), memorialised as
      Also fixes the three bugs in #18640
    • Simon Peyton Jones's avatar
      Implement Quick Look impredicativity · 97cff919
      Simon Peyton Jones authored and  Marge Bot's avatar Marge Bot committed
      This patch implements Quick Look impredicativity (#18126), sticking
      very closely to the design in
          A quick look at impredicativity, Serrano et al, ICFP 2020
      The main change is that a big chunk of GHC.Tc.Gen.Expr has been
      extracted to two new modules
      which deal with typechecking n-ary applications, and the head of
      such applications, respectively.  Both contain a good deal of
      Three other loosely-related changes are in this patch:
      * I implemented (partly by accident) points (2,3)) of the accepted GHC
        proposal "Clean up printing of foralls", namely
        (see #16320).
        In particular, see Note [TcRnExprMode] in GHC.Tc.Module
        - :type instantiates /inferred/, but not /specified/, quantifiers
        - :type +d instantiates /all/ quantifiers
        - :type +v is killed off
        That completes the implementation of the proposal,
        since point (1) was done in
          commit df084681
          Author: Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io>
          Date:   Mon Feb 3 21:17:11 2020 +0100
          Always display inferred variables using braces
      * HsRecFld (which the renamer introduces for record field selectors),
        is now preserved by the typechecker, rather than being rewritten
        back to HsVar.  This is more uniform, and turned out to be more
        convenient in the new scheme of things.
      * The GHCi debugger uses a non-standard unification that allows the
        unification variables to unify with polytypes.  We used to hack
        this by using ImpredicativeTypes, but that doesn't work anymore
        so I introduces RuntimeUnkTv.  See Note [RuntimeUnkTv] in
      Updates haddock submodule.
      WARNING: this patch won't validate on its own.  It was too
      hard to fully disentangle it from the following patch, on
      type errors and kind generalisation.
      Changes to tests
      * Fixes #9730 (test added)
      * Fixes #7026 (test added)
      * Fixes most of #8808, except function `g2'` which uses a
        section (which doesn't play with QL yet -- see #18126)
        Test added
      * Fixes #1330. NB Church1.hs subsumes Church2.hs, which is now deleted
      * Fixes #17332 (test added)
      * Fixes #4295
      * This patch makes typecheck/should_run/T7861 fail.
        But that turns out to be a pre-existing bug: #18467.
        So I have just made T7861 into expect_broken(18467)
  3. 17 Jun, 2020 1 commit
    • Krzysztof Gogolewski's avatar
      Linear types (#15981) · 40fa237e
      Krzysztof Gogolewski authored and Ben Gamari's avatar Ben Gamari committed
      This is the first step towards implementation of the linear types proposal
      It features
      * A language extension -XLinearTypes
      * Syntax for linear functions in the surface language
      * Linearity checking in Core Lint, enabled with -dlinear-core-lint
      * Core-to-core passes are mostly compatible with linearity
      * Fields in a data type can be linear or unrestricted; linear fields
        have multiplicity-polymorphic constructors.
        If -XLinearTypes is disabled, the GADT syntax defaults to linear fields
      The following items are not yet supported:
      * a # m -> b syntax (only prefix FUN is supported for now)
      * Full multiplicity inference (multiplicities are really only checked)
      * Decent linearity error messages
      * Linear let, where, and case expressions in the surface language
        (each of these currently introduce the unrestricted variant)
      * Multiplicity-parametric fields
      * Syntax for annotating lambda-bound or let-bound with a multiplicity
      * Syntax for non-linear/multiple-field-multiplicity records
      * Linear projections for records with a single linear field
      * Linear pattern synonyms
      * Multiplicity coercions (test LinearPolyType)
      A high-level description can be found at
      Following the link above you will find a description of the changes made to Core.
      This commit has been authored by
      * Richard Eisenberg
      * Krzysztof Gogolewski
      * Matthew Pickering
      * Arnaud Spiwack
      With contributions from:
      * Mark Barbone
      * Alexander Vershilov
      Updates haddock submodule.