1. 09 Jun, 2019 1 commit
    • Richard Eisenberg's avatar
      Fix #16517 by bumping the TcLevel for method sigs · a22e51ea
      Richard Eisenberg authored
      There were actually two bugs fixed here:
      
      1. candidateQTyVarsOfType needs to be careful that it does not
         try to zap metavariables from an outer scope as "naughty"
         quantification candidates. This commit adds a simple check
         to avoid doing so.
      
      2. We weren't bumping the TcLevel in kcHsKindSig, which was used
         only for class method sigs. This mistake led to the acceptance
         of
      
           class C a where
             meth :: forall k. Proxy (a :: k) -> ()
      
         Note that k is *locally* quantified. This patch fixes the
         problem by using tcClassSigType, which correctly bumps the
         level. It's a bit inefficient because tcClassSigType does other
         work, too, but it would be tedious to repeat much of the code
         there with only a few changes. This version works well and is
         simple.
      
      And, while updating comments, etc., I noticed that tcRnType was
      missing a pushTcLevel, leading to #16767, which this patch also
      fixes, by bumping the level. In the refactoring here, I also
      use solveEqualities. This initially failed ghci/scripts/T15415,
      but that was fixed by teaching solveEqualities to respect
      -XPartialTypeSignatures.
      
      This patch also cleans up some Notes around error generation that
      came up in conversation.
      
      Test case: typecheck/should_fail/T16517, ghci/scripts/T16767
      a22e51ea
  2. 22 May, 2019 1 commit
    • Ryan Scott's avatar
      Use HsTyPats in associated type family defaults · 6efe04de
      Ryan Scott authored
      Associated type family default declarations behave strangely in a
      couple of ways:
      
      1. If one tries to bind the type variables with an explicit `forall`,
         the `forall`'d part will simply be ignored. (#16110)
      2. One cannot use visible kind application syntax on the left-hand
         sides of associated default equations, unlike every other form
         of type family equation. (#16356)
      
      Both of these issues have a common solution. Instead of using
      `LHsQTyVars` to represent the left-hand side arguments of an
      associated default equation, we instead use `HsTyPats`, which is what
      other forms of type family equations use. In particular, here are
      some highlights of this patch:
      
      * `FamEqn` is no longer parameterized by a `pats` type variable, as
        the `feqn_pats` field is now always `HsTyPats`.
      * The new design for `FamEqn` in chronicled in
        `Note [Type family instance declarations in HsSyn]`.
      * `TyFamDefltEqn` now becomes the same thing as `TyFamInstEqn`. This
        means that many of `TyFamDefltEqn`'s code paths can now reuse the
        code paths for `TyFamInstEqn`, resulting in substantial
        simplifications to various parts of the code dealing with
        associated type family defaults.
      
      Fixes #16110 and #16356.
      6efe04de
  3. 14 May, 2019 1 commit
    • Vladislav Zavialov's avatar
      Guard CUSKs behind a language pragma · a5fdd185
      Vladislav Zavialov authored
      GHC Proposal #36 describes a transition plan away from CUSKs and to
      top-level kind signatures:
      
      1. Introduce a new extension, -XCUSKs, on by default, that detects CUSKs
         as they currently exist.
      2. We turn off the -XCUSKs extension in a few releases and remove it
         sometime thereafter.
      
      This patch implements phase 1 of this plan, introducing a new language
      extension to control whether CUSKs are enabled. When top-level kind
      signatures are implemented, we can transition to phase 2.
      a5fdd185
  4. 07 May, 2019 1 commit
    • Ryan Scott's avatar
      Check for duplicate variables in associated default equations · 78a5c4ce
      Ryan Scott authored
      A follow-up to !696's, which attempted to clean up the error messages
      for ill formed associated type family default equations. The previous
      attempt, !696, forgot to account for the possibility of duplicate
      kind variable arguments, as in the following example:
      
      ```hs
      class C (a :: j) where
        type T (a :: j) (b :: k)
        type T (a :: k) (b :: k) = k
      ```
      
      This patch addresses this shortcoming by adding an additional check
      for this. Fixes #13971 (hopefully for good this time).
      78a5c4ce
  5. 03 May, 2019 1 commit
  6. 04 Apr, 2019 1 commit
    • Ryan Scott's avatar
      Tweak error messages for narrowly-kinded assoc default decls · 33b0a291
      Ryan Scott authored
      This program, from #13971, currently has a rather confusing error
      message:
      
      ```hs
      class C a where
        type T a :: k
        type T a = Int
      ```
      ```
          • Kind mis-match on LHS of default declaration for ‘T’
          • In the default type instance declaration for ‘T’
            In the class declaration for ‘C’
      ```
      
      It's not at all obvious why GHC is complaining about the LHS until
      you realize that the default, when printed with
      `-fprint-explicit-kinds`, is actually `type T @{k} @* a = Int`.
      That is to say, the kind of `a` is being instantiated to `Type`,
      whereas it ought to be a kind variable. The primary thrust of this
      patch is to weak the error message to make this connection
      more obvious:
      
      ```
          • Illegal argument ‘*’ in:
              ‘type T @{k} @* a = Int’
              The arguments to ‘T’ must all be type variables
          • In the default type instance declaration for ‘T’
            In the class declaration for ‘C’
      ```
      
      Along the way, I performed some code cleanup suggested by @rae in
      ghc/ghc#13971 (comment 191287). Before,
      we were creating a substitution from the default declaration's type
      variables to the type family tycon's type variables by way of
      `tcMatchTys`. But this is overkill, since we already know (from the
      aforementioned validity checking) that all the arguments in a default
      declaration must be type variables anyway. Therefore, creating the
      substitution is as simple as using `zipTvSubst`. I took the
      opportunity to perform this refactoring while I was in town.
      
      Fixes #13971.
      33b0a291
  7. 15 Mar, 2019 2 commits
  8. 09 Mar, 2019 1 commit
    • Simon Peyton Jones's avatar
      Stop inferring over-polymorphic kinds · 1f5cc9dc
      Simon Peyton Jones authored
      Before this patch GHC was trying to be too clever
      (Trac #16344); it succeeded in kind-checking this
      polymorphic-recursive declaration
      
          data T ka (a::ka) b
            = MkT (T Type           Int   Bool)
                  (T (Type -> Type) Maybe Bool)
      
      As Note [No polymorphic recursion] discusses, the "solution" was
      horribly fragile.  So this patch deletes the key lines in
      TcHsType, and a wodge of supporting stuff in the renamer.
      
      There were two regressions, both the same: a closed type family
      decl like this (T12785b) does not have a CUSK:
        type family Payload (n :: Peano) (s :: HTree n x) where
          Payload Z (Point a) = a
          Payload (S n) (a `Branch` stru) = a
      
      To kind-check the equations we need a dependent kind for
      Payload, and we don't get that any more.  Solution: make it
      a CUSK by giving the result kind -- probably a good thing anyway.
      
      The other case (T12442) was very similar: a close type family
      declaration without a CUSK.
      1f5cc9dc
  9. 05 Mar, 2019 1 commit
    • Simon Peyton Jones's avatar
      Be more careful when naming TyCon binders · 80dfcee6
      Simon Peyton Jones authored
      This patch fixes two rather gnarly test cases:
        * Trac #16342 (mutual recursion)
          See Note [Tricky scoping in generaliseTcTyCon]
      
        * Trac #16221 (shadowing)
          See Note [Unification variables need fresh Names]
      
      The main changes are:
      
      * Substantial reworking of TcTyClsDecls.generaliseTcTyCon
        This is the big change, and involves the rather tricky
        function TcHsSyn.zonkRecTyVarBndrs.
      
        See Note [Inferring kinds for type declarations] and
        Note [Tricky scoping in generaliseTcTyCon] for the details.
      
      * bindExplicitTKBndrs_Tv and bindImplicitTKBndrs_Tv both now
        allocate /freshly-named/ unification variables. Indeed, more
        generally, unification variables are always fresh; see
        Note [Unification variables need fresh Names] in TcMType
      
      * Clarify the role of tcTyConScopedTyVars.
        See Note [Scoped tyvars in a TcTyCon] in TyCon
      
      As usual, this dragged in some more refactoring:
      
      * Renamed TcMType.zonkTyCoVarBndr to zonkAndSkolemise
      
      * I renamed checkValidTelescope to checkTyConTelescope;
        it's only used on TyCons, and indeed takes a TyCon as argument.
      
      * I folded the slightly-mysterious reportFloatingKvs into
        checkTyConTelescope. (Previously all its calls immediately
        followed a call to checkTyConTelescope.)  It makes much more
        sense there.
      
      * I inlined some called-once functions to simplify
        checkValidTyFamEqn. It's less spaghetti-like now.
      
      * This patch also fixes Trac #16251.  I'm not quite sure why #16251
        went wrong in the first place, nor how this patch fixes it, but
        hey, it's good, and life is short.
      80dfcee6
  10. 27 Feb, 2019 1 commit
    • Vladislav Zavialov's avatar
      Treat kind/type variables identically, demolish FKTV · 5bc195b1
      Vladislav Zavialov authored
      Implements GHC Proposal #24: .../ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst
      Fixes Trac #16334, Trac #16315
      
      With this patch, scoping rules for type and kind variables have been
      unified: kind variables no longer receieve special treatment. This
      simplifies both the language and the implementation.
      
      User-facing changes
      -------------------
      
      * Kind variables are no longer implicitly quantified when an explicit
        forall is used:
      
          p ::             Proxy (a :: k)    -- still accepted
          p :: forall k a. Proxy (a :: k)    -- still accepted
          p :: forall   a. Proxy (a :: k)    -- no longer accepted
      
        In other words, now we adhere to the "forall-or-nothing" rule more
        strictly.
      
        Related function: RnTypes.rnImplicitBndrs
      
      * The -Wimplicit-kind-vars warning has been deprecated.
      
      * Kind variables are no longer implicitly quantified in constructor
        declarations:
      
          data T a        = T1 (S (a :: k) | forall (b::k). T2 (S b)  -- no longer accepted
          data T (a :: k) = T1 (S (a :: k) | forall (b::k). T2 (S b)  -- still accepted
      
        Related function: RnTypes.extractRdrKindSigVars
      
      * Implicitly quantified kind variables are no longer put in front of
        other variables:
      
          f :: Proxy (a :: k) -> Proxy (b :: j)
      
          f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b   -- old order
          f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b   -- new order
      
        This is a breaking change for users of TypeApplications. Note that
        we still respect the dpendency order: 'k' before 'a', 'j' before 'b'.
        See "Ordering of specified variables" in the User's Guide.
      
        Related function: RnTypes.rnImplicitBndrs
      
      * In type synonyms and type family equations, free variables on the RHS
        are no longer implicitly quantified unless used in an outermost kind
        annotation:
      
          type T = Just (Nothing :: Maybe a)         -- no longer accepted
          type T = Just Nothing :: Maybe (Maybe a)   -- still accepted
      
        The latter form is a workaround due to temporary lack of an explicit
        quantification method. Ideally, we would write something along these
        lines:
      
          type T @a = Just (Nothing :: Maybe a)
      
        Related function: RnTypes.extractHsTyRdrTyVarsKindVars
      
      * Named wildcards in kinds are fixed (Trac #16334):
      
          x :: (Int :: _t)    -- this compiles, infers (_t ~ Type)
      
        Related function: RnTypes.partition_nwcs
      
      Implementation notes
      --------------------
      
      * One of the key changes is the removal of FKTV in RnTypes:
      
        - data FreeKiTyVars = FKTV { fktv_kis    :: [Located RdrName]
        -                          , fktv_tys    :: [Located RdrName] }
        + type FreeKiTyVars = [Located RdrName]
      
        We used to keep track of type and kind variables separately, but
        now that they are on equal footing when it comes to scoping, we
        can put them in the same list.
      
      * extract_lty and family are no longer parametrized by TypeOrKind,
        as we now do not distinguish kind variables from type variables.
      
      * PatSynExPE and the related Note [Pattern synonym existentials do not scope]
        have been removed (Trac #16315). With no implicit kind quantification,
        we can no longer trigger the error.
      
      * reportFloatingKvs and the related Note [Free-floating kind vars]
        have been removed. With no implicit kind quantification,
        we can no longer trigger the error.
      5bc195b1
  11. 24 Feb, 2019 1 commit
    • Simon Peyton Jones's avatar
      Add AnonArgFlag to FunTy · 6cce36f8
      Simon Peyton Jones authored
      The big payload of this patch is:
      
        Add an AnonArgFlag to the FunTy constructor
        of Type, so that
          (FunTy VisArg   t1 t2) means (t1 -> t2)
          (FunTy InvisArg t1 t2) means (t1 => t2)
      
      The big payoff is that we have a simple, local test to make
      when decomposing a type, leading to many fewer calls to
      isPredTy. To me the code seems a lot tidier, and probably
      more efficient (isPredTy has to take the kind of the type).
      
      See Note [Function types] in TyCoRep.
      
      There are lots of consequences
      
      * I made FunTy into a record, so that it'll be easier
        when we add a linearity field, something that is coming
        down the road.
      
      * Lots of code gets touched in a routine way, simply because it
        pattern matches on FunTy.
      
      * I wanted to make a pattern synonym for (FunTy2 arg res), which
        picks out just the argument and result type from the record. But
        alas the pattern-match overlap checker has a heart attack, and
        either reports false positives, or takes too long.  In the end
        I gave up on pattern synonyms.
      
        There's some commented-out code in TyCoRep that shows what I
        wanted to do.
      
      * Much more clarity about predicate types, constraint types
        and (in particular) equality constraints in kinds.  See TyCoRep
        Note [Types for coercions, predicates, and evidence]
        and Note [Constraints in kinds].
      
        This made me realise that we need an AnonArgFlag on
        AnonTCB in a TyConBinder, something that was really plain
        wrong before. See TyCon Note [AnonTCB InivsArg]
      
      * When building function types we must know whether we
        need VisArg (mkVisFunTy) or InvisArg (mkInvisFunTy).
        This turned out to be pretty easy in practice.
      
      * Pretty-printing of types, esp in IfaceType, gets
        tidier, because we were already recording the (->)
        vs (=>) distinction in an ad-hoc way.  Death to
        IfaceFunTy.
      
      * mkLamType needs to keep track of whether it is building
        (t1 -> t2) or (t1 => t2).  See Type
        Note [mkLamType: dictionary arguments]
      
      Other minor stuff
      
      * Some tidy-up in validity checking involving constraints;
        Trac #16263
      6cce36f8
  12. 22 Feb, 2019 1 commit
  13. 14 Feb, 2019 1 commit
    • Simon Peyton Jones's avatar
      Make a smart mkAppTyM · 68278382
      Simon Peyton Jones authored
      This patch finally delivers on Trac #15952.  Specifically
      
      * Completely remove Note [The tcType invariant], along with
        its complicated consequences (IT1-IT6).
      
      * Replace Note [The well-kinded type invariant] with:
      
            Note [The Purely Kinded Type Invariant (PKTI)]
      
      * Instead, establish the (PKTI) in TcHsType.tcInferApps,
        by using a new function mkAppTyM when building a type
        application.  See Note [mkAppTyM].
      
      * As a result we can remove the delicate mkNakedXX functions
        entirely.  Specifically, mkNakedCastTy retained lots of
        extremly delicate Refl coercions which just cluttered
        everything up, and(worse) were very vulnerable to being
        silently eliminated by (say) substTy. This led to a
        succession of bug reports.
      
      The result is noticeably simpler to explain, simpler
      to code, and Richard and I are much more confident that
      it is correct.
      
      It does not actually fix any bugs, but it brings us closer.
      E.g. I hoped it'd fix #15918 and #15799, but it doesn't quite
      do so.  However, it makes it much easier to fix.
      
      I also did a raft of other minor refactorings:
      
      * Use tcTypeKind consistently in the type checker
      
      * Rename tcInstTyBinders to tcInvisibleTyBinders,
        and refactor it a bit
      
      * Refactor tcEqType, pickyEqType, tcEqTypeVis
        Simpler, probably more efficient.
      
      * Make zonkTcType zonk TcTyCons, at least if they have
        any free unification variables -- see zonk_tc_tycon
        in TcMType.zonkTcTypeMapper.
      
        Not zonking these TcTyCons was actually a bug before.
      
      * Simplify try_to_reduce_no_cache in TcFlatten (a lot)
      
      * Combine checkExpectedKind and checkExpectedKindX.
        And then combine the invisible-binder instantation code
        Much simpler now.
      
      * Fix a little bug in TcMType.skolemiseQuantifiedTyVar.
        I'm not sure how I came across this originally.
      
      * Fix a little bug in TyCoRep.isUnliftedRuntimeRep
        (the ASSERT was over-zealous).  Again I'm not certain
        how I encountered this.
      
      * Add a missing solveLocalEqualities in
        TcHsType.tcHsPartialSigType.
        I came across this when trying to get level numbers
        right.
      68278382
  14. 08 Feb, 2019 1 commit
    • Simon Peyton Jones's avatar
      Minor refactor of CUSK handling · 9bb23d5f
      Simon Peyton Jones authored
      Previously, in getFamDeclInitialKind, we were figuring
      out whether the enclosing class decl had a CUSK very
      indirectly, via tcTyConIsPoly.  This patch just makes
      the computation much more direct and easy to grok.
      
      No change in behaviour.
      9bb23d5f
  15. 02 Feb, 2019 1 commit
  16. 03 Jan, 2019 1 commit
    • My Nguyen's avatar
      Visible kind application · 17bd1635
      My Nguyen authored
      Summary:
      This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362.
      It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be
      written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind
      application, just like in term-level.
      
      There are a few remaining issues with this patch, as documented in
      ticket #16082.
      
      Includes a submodule update for Haddock.
      
      Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a
      
      Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack
      
      Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter
      
      GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816`
      
      Differential Revision: https://phabricator.haskell.org/D5229
      17bd1635
  17. 21 Dec, 2018 1 commit
    • Ryan Scott's avatar
      Fix #16002 by moving a validity check to the renamer · 28f41f1a
      Ryan Scott authored
      Summary:
      The validity check which rejected things like:
      
      ```lang=haskell
      type family B x where
        A x = x
      ```
      
      Used to live in the typechecker. But it turns out that this validity
      check was //only// being run on closed type families without CUSKs!
      This meant that GHC would silently accept something like this:
      
      ```lang=haskell
      type family B (x :: *) :: * where
        A x = x
      ```
      
      This patch fixes the issue by moving this validity check to the
      renamer, where we can be sure that the check will //always// be run.
      
      Test Plan: make test TEST=T16002
      
      Reviewers: simonpj, bgamari
      
      Reviewed By: simonpj
      
      Subscribers: goldfire, rwbarton, carter
      
      GHC Trac Issues: #16002
      
      Differential Revision: https://phabricator.haskell.org/D5420
      28f41f1a
  18. 15 Dec, 2018 1 commit
    • Ben Gamari's avatar
      Use https links in user-facing startup and error messages · a1c0b706
      Ben Gamari authored
      I consider myself lucky that in my circle of friends, `http` urls (as
      opposed to `https` urls) are frowned upon in that we generally
      apologize in the rase cases that we share an `http` url.
      
      This pull request changes `http` links into their `https` analogues in
      the following places:
      
      * In the GHCI startup message (and parts of the User's Guide, where
      there are verbatim transcripts of GHCi sessions).
      * In a couple of error messages, asking the user to report a bug.
      
      (I also took the liberty to change a single space before the reportabug
      url into two spaces, harmonizing this occurence with the others.)
      
      I'm not trying to start a war. I just had a moment to spare and felt
      like preparing this diff. Merge or don't merge as you wish!
      
      Reviewers: bgamari, erikd, simonmar
      
      Subscribers: goldfire, rwbarton, carter
      
      Differential Revision: https://phabricator.haskell.org/D5450
      a1c0b706
  19. 11 Dec, 2018 1 commit
    • Ryan Scott's avatar
      Fix #16008 with a pinch of addConsistencyConstraints · 3899966e
      Ryan Scott authored
      Summary:
      #16008 happened because we forgot to typecheck nullary
      associated type family instances in a way that's consistent with the
      type variables bound by the parent class. Oops. Easily fixed with a
      use of `checkConsistencyConstraints`.
      
      Test Plan: make test TEST=T16008
      
      Reviewers: simonpj, goldfire, bgamari
      
      Reviewed By: goldfire
      
      Subscribers: rwbarton, carter
      
      GHC Trac Issues: #16008
      
      Differential Revision: https://phabricator.haskell.org/D5435
      3899966e
  20. 06 Dec, 2018 1 commit
    • Simon Peyton Jones's avatar
      Remove a tcTrace · 081f44bf
      Simon Peyton Jones authored
      This tcTrace, in tcTyFamInstEqn, caused a knot-tying loop, because
      it was printing a type after zonking-to-Type.  Easy solution: don't
      do that.
      081f44bf
  21. 03 Dec, 2018 2 commits
    • Simon Peyton Jones's avatar
      Comments only · a46511a8
      Simon Peyton Jones authored
      a46511a8
    • 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
  22. 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
  23. 24 Nov, 2018 1 commit
  24. 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
  25. 27 Oct, 2018 1 commit
    • mayac's avatar
      More explicit foralls (GHC Proposal 0007) · 512eeb9b
      mayac authored
      Allow the user to explicitly bind type/kind variables in type and data
      family instances (including associated instances), closed type family
      equations, and RULES pragmas. Follows the specification of GHC
      Proposal 0007, also fixes #2600. Advised by Richard Eisenberg.
      
      This modifies the Template Haskell AST -- old code may break!
      
      Other Changes:
      - convert HsRule to a record
      - make rnHsSigWcType more general
      - add repMaybe to DsMeta
      
      Includes submodule update for Haddock.
      
      Test Plan: validate
      
      Reviewers: goldfire, bgamari, alanz
      
      Subscribers: simonpj, RyanGlScott, goldfire, rwbarton,
                   thomie, mpickering, carter
      
      GHC Trac Issues: #2600, #14268
      
      Differential Revision: https://phabricator.haskell.org/D4894
      512eeb9b
  26. 26 Oct, 2018 1 commit
    • Simon Peyton Jones's avatar
      Fix generalisation for type constructors · 4de4b225
      Simon Peyton Jones authored
      Fixing the way that we close-over-kinds when taking the
      free vars of a type revealed that the way we generalise
      type constructors was a bit wrong.
      
      This fixes it.  See TcTyClDecls
      Note [Generalisation for type constructors]
      4de4b225
  27. 04 Oct, 2018 1 commit
    • Simon Peyton Jones's avatar
      Distinguish Inferred from Specified tyvars · 2f09753f
      Simon Peyton Jones authored
      In a declared type we need to distinguish between Inferred
      and Specified type variables. This was exposed by Trac #15592.
      
      See Note [Work out final tyConBinders] in TcTyClsDecls.
      
      I had to change the definition of HasField in GHC.Records to
         class HasField x r a | x r -> a where
      so as to have an /inferred/ kind argument rather than a
      specfied one.  So
         HasField :: forall {k}. k -> * -> * -> Constraint
      2f09753f
  28. 01 Oct, 2018 2 commits
    • Ryan Scott's avatar
      Quantify class variables first in associated families' kinds · a57fa247
      Ryan Scott authored
      Summary:
      Previously, `kcLHsQTyVars` would always quantify class-bound
      variables invisibly in the kinds of associated types, resulting in
      #15591. We counteract this by explicitly passing the class-bound
      variables to `kcLHsQTyVars` and quantifying over the ones that are
      mentioned in the associated type such that (1) they are specified,
      and (2) they come before other kind variables.
      See `Note [Kind variable ordering for associated types]`.
      
      Test Plan: make test TEST=T15591
      
      Reviewers: goldfire, simonpj, bgamari
      
      Reviewed By: simonpj
      
      Subscribers: rwbarton, carter
      
      GHC Trac Issues: #15591
      
      Differential Revision: https://phabricator.haskell.org/D5159
      a57fa247
    • 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
  29. 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
  30. 31 Aug, 2018 1 commit
    • Simon Peyton Jones's avatar
      Remove knot-tying bug in TcHsSyn.zonkTyVarOcc · 565ef4cc
      Simon Peyton Jones authored
      There was a subtle knot-tying bug in TcHsSyn.zonkTyVarOcc, revealed
      in Trac #15552.
      
      I fixed it by
      
      * Eliminating the short-circuiting optimisation in zonkTyVarOcc,
        instead adding a finite map to get sharing of zonked unification
        variables.
      
        See Note [Sharing when zonking to Type] in TcHsSyn
      
      * On the way I /added/ the short-circuiting optimisation to
        TcMType.zonkTcTyVar, which has no such problem.  This turned
        out (based on non-systematic measurements) to be a modest win.
      
        See Note [Sharing in zonking] in TcMType
      
      On the way I renamed some of the functions in TcHsSyn:
      
      * Ones ending in "X" (like zonkTcTypeToTypeX) take a ZonkEnv
      
      * Ones that do not end in "x" (like zonkTcTypeToType), don't.
        Instead they whiz up an empty ZonkEnv.
      565ef4cc
  31. 23 Aug, 2018 1 commit
  32. 21 Aug, 2018 1 commit
    • Simon Peyton Jones's avatar
      Add a solveEqualities to tcClassDecl1 · 43b08cfb
      Simon Peyton Jones authored
      Trac #15505 showed that, when we have a type error, we
      could have an unfilled-in coercion hole.  We don't want an
      assertion error in that case.
      
      The underlying cause is that tcClassDecl1 should call
      solveEqualities to fully solve all top-level equalities
      (or fail in the attempt).
      
      I also refactored the ClassDecl case for tcTyClDecl1 into
      a new function tcClassDecl1.  That makes it symmetrical
      with the others.
      43b08cfb
  33. 17 Aug, 2018 1 commit
    • Joachim Breitner's avatar
      Rename SigTv to TyVarTv (#15480) · a50244c6
      Joachim Breitner authored
      because since #15050, these are no longer used in pattern SIGnatures,
      but still in other places where meta-variables should only be unified
      with TYpe VARiables.
      
      I also found mentions of `SigTv` in parts of the renamer and desugarer
      that do not seem to directly relate to `SigTv` as used in the type
      checker, but rather to uses of `forall a.` in type signatures. I renamed
      these to `ScopedTv`.
      
      Differential Revision: https://phabricator.haskell.org/D5074
      a50244c6
  34. 02 Aug, 2018 1 commit
    • Richard Eisenberg's avatar
      Remove decideKindGeneralisationPlan · c955a514
      Richard Eisenberg authored
      TypeInType came with a new function: decideKindGeneralisationPlan.
      This type-level counterpart to the term-level decideGeneralisationPlan
      chose whether or not a kind should be generalized. The thinking was
      that if `let` should not be generalized, then kinds shouldn't either
      (under the same circumstances around -XMonoLocalBinds).
      
      However, this is too conservative -- the situation described in the
      motivation for "let should be be generalized" does not occur in types.
      
      This commit thus removes decideKindGeneralisationPlan, always
      generalizing.
      
      One consequence is that tc_hs_sig_type_and_gen no longer calls
      solveEqualities, which reports all unsolved constraints, instead
      relying on the solveLocalEqualities in tcImplicitTKBndrs. An effect
      of this is that reporing kind errors gets delayed more frequently.
      This seems to be a net benefit in error reporting; often, alongside
      a kind error, the type error is now reported (and users might find
      type errors easier to understand).
      
      Some of these errors ended up at the top level, where it was
      discovered that the GlobalRdrEnv containing the definitions in the
      local module was not in the TcGblEnv, and thus errors were reported
      with qualified names unnecessarily. This commit rejiggers some of
      the logic around captureTopConstraints accordingly.
      
      One error message (typecheck/should_fail/T1633)
      is a regression, mentioning the name of a default method. However,
      that problem is already reported as #10087, its solution is far from
      clear, and so I'm not addressing it here.
      
      This commit fixes #15141. As it's an internal refactor, there is
      no concrete test case for it.
      
      Along the way, we no longer need the hsib_closed field of
      HsImplicitBndrs (it was used only in decideKindGeneralisationPlan)
      and so it's been removed, simplifying the datatype structure.
      
      Along the way, I removed code in the validity checker that looks
      at coercions. This isn't related to this patch, really (though
      it was, at one point), but it's an improvement, so I kept it.
      
      This updates the haddock submodule.
      c955a514
  35. 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
  36. 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
  37. 15 Jul, 2018 1 commit
    • Richard Eisenberg's avatar
      Move check for dcUserTyVarBinders invariant · fe0fa63e
      Richard Eisenberg authored
      Previously, this check was done in mkDataCon. But this
      sometimes caused assertion failures if an invalid data
      con was made. I've moved the check to checkValidDataCon,
      where we can be sure the datacon is otherwise valid first.
      fe0fa63e