1. 14 Jun, 2018 1 commit
  2. 08 Jun, 2018 1 commit
  3. 07 Jun, 2018 1 commit
  4. 04 Jun, 2018 1 commit
    • 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 ...
      7df58960
  5. 30 May, 2018 2 commits
    • Matthías Páll Gissurarson's avatar
      Improved Valid Hole Fits · e0b44e2e
      Matthías Páll Gissurarson authored
      I've changed the name from `Valid substitutions` to `Valid hole fits`,
      since "substitution" already has a well defined meaning within the
      theory. As part of this change, the flags and output is reanamed, with
      substitution turning into hole-fit in most cases. "hole fit" was already
      used internally in the code, it's clear and shouldn't cause any
      confusion.
      
      In this update, I've also reworked how we manage side-effects in the
      hole we are considering.
      
      This allows us to consider local bindings such as where clauses and
      arguments to functions, suggesting e.g. `a` for `head (x:xs) where head
      :: [a] -> a`.
      
      It also allows us to find suggestions such as `maximum` for holes of
      type `Ord a => a -> [a]`, and `max` when looking for a match for the
      hole in `g = foldl1 _`, where `g :: Ord a => [a] -> a`.
      
      We also show much improved output for refinement hole fits, and
      fixes #14990. We now show the correct type of the function, but we also
      now show what the arguments to the function should be e.g. `foldl1 (_ ::
      Integer -> Integer -> Integer)` when looking for `[Integer] -> Integer`.
      
      I've moved the bulk of the code from `TcErrors.hs` to a new file,
      `TcHoleErrors.hs`, since it was getting too big to not live on it's own.
      
      This addresses the considerations raised in #14969, and takes proper
      care to set the `tcLevel` of the variables to the right level before
      passing it to the simplifier.
      
      We now also zonk the suggestions properly, which improves the output of
      the refinement hole fits considerably.
      
      This also filters out suggestions from the `GHC.Err` module, since even
      though `error` and `undefined` are indeed valid hole fits, they are
      "trivial", and almost never useful to the user.
      
      We now find the hole fits using the proper manner, namely by solving
      nested implications. This entails that the givens are passed along using
      the implications the hole was nested in, which in turn should mean that
      there will be fewer weird bugs in the typed holes.
      
      I've also added a new sorting method (as suggested by SPJ) and sort by
      the size of the types needed to turn the hole fits into the type of the
      hole. This gives a reasonable approximation to relevance, and is much
      faster than the subsumption check. I've also added a flag to toggle
      whether to use this new sorting algorithm (as is done by default) or the
      subsumption algorithm. This fixes #14969
      
      I've also added documentation for these new flags and update the
      documentation according to the new output.
      
      Reviewers: bgamari, goldfire
      
      Reviewed By: bgamari
      
      Subscribers: simonpj, rwbarton, thomie, carter
      
      GHC Trac Issues: #14969, #14990, #10946
      
      Differential Revision: https://phabricator.haskell.org/D4444
      e0b44e2e
    • Alp Mestanogullari's avatar
      T14732 now passes with the profasm way · c65159dc
      Alp Mestanogullari authored
      Simon PJ recently fixed the problem behind this failure
      so we can now expect this test to pass in all ways again.
      
      The fixes got introduced in the following commits:
        86bba7d5
        d191db48
      
      Test Plan: T14732 (profasm way)
      
      Reviewers: bgamari, RyanGlScott, simonpj
      
      Reviewed By: RyanGlScott, simonpj
      
      Subscribers: simonpj, RyanGlScott, rwbarton, thomie, carter
      
      GHC Trac Issues: #15163
      
      Differential Revision: https://phabricator.haskell.org/D4725
      c65159dc
  6. 26 May, 2018 1 commit
  7. 20 May, 2018 1 commit
  8. 14 May, 2018 1 commit
  9. 27 Apr, 2018 1 commit
    • Simon Peyton Jones's avatar
      Make out-of-scope errors more prominent · 08003e7f
      Simon Peyton Jones authored
      Generally, when the type checker reports an error, more serious
      ones suppress less serious ones.
      
      A "variable out of scope" error is arguably the most serious of all,
      so this patch moves it to the front of the list instead of the end.
      
      This patch also fixes Trac #14149, which had
      -fdefer-out-of-scope-variables, but also had a solid type error.
      As things stood, the type error was not reported at all, and
      compilation "succeeded" with error code 0.  Yikes.
      
      Note that
      
      - "Hole errors" (including out of scope) are never suppressed.
        (maybeReportHoleError vs maybeReportError in TcErorrs)
        They can just get drowned by the noise.
      
      - But with the new orientation, out of scope errors will suppress
        type errors.  That would be easy to change.
      08003e7f
  10. 23 Apr, 2018 1 commit
  11. 19 Apr, 2018 1 commit
  12. 02 Apr, 2018 1 commit
  13. 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
  14. 26 Mar, 2018 1 commit
    • 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
  15. 19 Mar, 2018 1 commit
    • Ryan Scott's avatar
      Fix #14934 by including axSub0R in typeNatCoAxiomRules · c3aea396
      Ryan Scott authored
      For some reason, `axSub0R` was left out of `typeNatCoAxiomRules` in
      `TcTypeNats`, which led to disaster when trying to look up `Sub0R` from
      an interface file, as demonstrated in #14934.
      
      The fix is simple—just add `axSub0R` to that list. To help prevent
      an issue like this happening in the future, I added a
      `Note [Adding built-in type families]` to `TcTypeNats`, which
      contains a walkthrough of all the definitions in `TcTypeNats` you
      need to update when adding a new built-in type family.
      
      Test Plan: make test TEST=T14934
      
      Reviewers: bgamari, simonpj
      
      Reviewed By: simonpj
      
      Subscribers: simonpj, rwbarton, thomie, carter
      
      GHC Trac Issues: #14934
      
      Differential Revision: https://phabricator.haskell.org/D4508
      c3aea396
  16. 18 Feb, 2018 1 commit
    • Matthías Páll Gissurarson's avatar
      Add valid refinement substitution suggestions for typed holes · 918c0b39
      Matthías Páll Gissurarson authored
      This adds valid refinement substitution suggestions for typed holes and
      documentation thereof.
      
      Inspired by Agda's refinement facilities, this extends the typed holes
      feature to be able to search for valid refinement substitutions, which
      are substitutions that have one or more holes in them.
      
      When the flag `-frefinement-level-substitutions=n` where `n > 0` is
      passed, we also look for valid refinement substitutions, i.e.
      substitutions that are valid, but adds more holes. Consider the
      following:
      
        f :: [Integer] -> Integer
        f = _
      
      Here the valid substitutions suggested will be (with the new
      `-funclutter-valid-substitutions` flag for less verbosity set):
      
      ```
        Valid substitutions include
          f :: [Integer] -> Integer
          product :: forall (t :: * -> *).
                    Foldable t => forall a. Num a => t a -> a
          sum :: forall (t :: * -> *).
                Foldable t => forall a. Num a => t a -> a
          maximum :: forall (t :: * -> *).
                    Foldable t => forall a. Ord a => t a -> a
          minimum :: forall (t :: * -> *).
                    Foldable t => forall a. Ord a => t a -> a
          head :: forall a. [a] -> a
          (Some substitutions suppressed; use -fmax-valid-substitutions=N or
      -fno-max-valid-substitutions)
      ```
      
      When the `-frefinement-level-substitutions=1` flag is given, we
      additionally compute and report valid refinement substitutions:
      
      ```
        Valid refinement substitutions include
          foldl1 _ :: forall (t :: * -> *).
                      Foldable t => forall a. (a -> a -> a) -> t a -> a
          foldr1 _ :: forall (t :: * -> *).
                      Foldable t => forall a. (a -> a -> a) -> t a -> a
          head _ :: forall a. [a] -> a
          last _ :: forall a. [a] -> a
          error _ :: forall (a :: TYPE r).
                      GHC.Stack.Types.HasCallStack => [Char] -> a
          errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
          (Some refinement substitutions suppressed; use
      -fmax-refinement-substitutions=N or -fno-max-refinement-substitutions)
      ```
      
      Which are substitutions with holes in them. This allows e.g. beginners
      to discover the fold functions and similar.
      
      We find these refinement suggestions by considering substitutions that
      don't fit the type of the hole, but ones that would fit if given an
      additional argument. We do this by creating a new type variable with
      newOpenFlexiTyVarTy (e.g. `t_a1/m[tau:1]`), and then considering
      substitutions of the type `t_a1/m[tau:1] -> v` where `v` is the type of
      the hole. Since the simplifier is free to unify this new type variable
      with any type (and it is cloned before each check to avoid
      side-effects), we can now discover any identifiers that would fit if
      given another identifier of a suitable type. This is then generalized
      so that we can consider any number of additional arguments by setting
      the `-frefinement-level-substitutions` flag to any number, and then
      considering substitutions like e.g. `foldl _ _` with two additional
      arguments.
      
      This can e.g. help beginners discover the `fold` functions.
      This could also help more advanced users figure out which morphisms
      they can use when arrow chasing.
      Then you could write `m = _ . m2 . m3` where `m2` and `m3` are some
      morphisms, and not only get exact fits, but also help in finding
      morphisms that might get you a little bit closer to where you want to
      go in the diagram.
      
      Reviewers: bgamari
      
      Reviewed By: bgamari
      
      Subscribers: rwbarton, thomie, carter
      
      Differential Revision: https://phabricator.haskell.org/D4357
      918c0b39
  17. 16 Feb, 2018 1 commit
  18. 08 Feb, 2018 1 commit
    • Simon Peyton Jones's avatar
      Fix isDroppableCt (Trac #14763) · 6edafe3b
      Simon Peyton Jones authored
      When finishing up an implication constraint, it's a bit tricky to
      decide which Derived constraints to retain (for error reporting) and
      which to discard.  I got this wrong in commit
         f20cf982
         (Remove wc_insol from WantedConstraints)
      
      The particular problem in Trac #14763 was that we were reporting as an
      error a fundep-generated constraint
        (ex ~ T)
      where 'ex' is an existentially-bound variable in a pattern match.
      But this isn't really an error at all.
      
      This patch fixes the problem. Indeed, since I had to understand
      this rather tricky code, I took the opportunity to clean it up
      and document better.  See
        isDroppableCt :: Ct -> Bool
      and Note [Dropping derived constraints]
      
      I also removed wl_deriv altogether from the WorkList data type.  It
      was there in the hope of gaining efficiency by not even processing
      lots of derived constraints, but it has turned out that most derived
      constraints (notably equalities) must be processed anyway; see
      Note [Prioritise equalities] in TcSMonad.
      
      The two are coupled because to decide which constraints to put in
      wl_deriv I was using another variant of isDroppableCt.  Now it's much
      simpler -- and perhaps even more efficient too.
      6edafe3b
  19. 07 Feb, 2018 1 commit
    • Simon Peyton Jones's avatar
      Fix solveOneFromTheOther for RecursiveSuperclasses · 65069806
      Simon Peyton Jones authored
      This patch fixes the redundant superclass expansion
      in Trac #14774.
      
      The main change is to fix TcInterac.solveOneFromTheOther, so
      that it does not prefer a work-item with a binding if that binding
      transitively depends on the inert item we are comparing it with.
      
      Explained in Note [Replacement vs keeping] in TcInert, esp
      item (c) of the "Constraints coming from the same level" part.
      
      To make this work I refactored out a new function
      TcEvidence.findNeededEvVars, which was previously buried
      inside TcSimplify.neededEvVars.
      
      I added quite a few more comments and signposts about superclass
      expansion.
      65069806
  20. 01 Feb, 2018 1 commit
    • Simon Peyton Jones's avatar
      Add -ddump-ds-preopt · efce943c
      Simon Peyton Jones authored
      This allows you to see the output immediately after desugaring
      but before any optimisation.
      
      I've wanted this for some time, but I was triggered into action
      by Trac #13032 comment:9.
      
      Interestingly, the change means that with -dcore-lint we will
      now Lint the output before the very simple optimiser;
      and this showed up Trac #14749.  But that's not the fault
      of -ddump-ds-preopt!
      efce943c
  21. 31 Jan, 2018 2 commits
    • Simon Peyton Jones's avatar
      Look inside implications in simplifyRule · e9ae0cae
      Simon Peyton Jones authored
      Trac #14732 was a perpelexing bug in which -fdefer-typed-holes
      caused a mysterious type error in a RULE.  This turned out to
      be because we are more aggressive about creating implications
      when deferring (see TcUnify.implicationNeeded), and the rule
      mechanism hadn't caught up.
      
      This fixes it.
      e9ae0cae
    • Simon Peyton Jones's avatar
      Prioritise equalities when solving, incl deriveds · efba0546
      Simon Peyton Jones authored
      We already prioritise equalities when solving, but
      Trac #14723 showed that we were not doing so consistently
      enough, and as a result the type checker could go into a loop.
      Yikes.
      
      See Note [Prioritise equalities] in TcSMonad.
      
      Fixng this bug changed the solve order enough to demonstrate
      a problem with fundeps: Trac #14745.
      efba0546
  22. 18 Jan, 2018 1 commit
  23. 04 Jan, 2018 1 commit
    • Simon Peyton Jones's avatar
      Drop dead Given bindings in setImplicationStatus · 954cbc7c
      Simon Peyton Jones authored
      Trac #13032 pointed out that we sometimes generate unused
      bindings for Givens, and (worse still) we can't always discard
      them later (we don't drop a case binding unless we can prove
      that the scrutinee is non-bottom.
      
      It looks as if this may be a major reason for the performace
      problems in #14338 (see comment:29).
      
      This patch fixes the problem at source, by pruning away all the
      dead Givens.  See Note [Delete dead Given evidence bindings]
      
      Remarkably, compiler allocation falls by 23% in
      perf/compiler/T12227!
      
      I have not confirmed whether this change actualy helps with
      954cbc7c
  24. 21 Dec, 2017 1 commit
    • Ryan Scott's avatar
      Improve treatment of sectioned holes · 4d41e921
      Ryan Scott authored
      Summary:
      Previously, GHC was pretty-printing left-section holes
      incorrectly and not parsing right-sectioned holes at all. This patch
      fixes both problems.
      
      Test Plan: make test TEST=T14590
      
      Reviewers: bgamari, simonpj
      
      Reviewed By: simonpj
      
      Subscribers: simonpj, rwbarton, thomie, mpickering, carter
      
      GHC Trac Issues: #14590
      
      Differential Revision: https://phabricator.haskell.org/D4273
      4d41e921
  25. 01 Dec, 2017 1 commit
    • Edward Z. Yang's avatar
      Make use of boot TyThings during typechecking. · 69987720
      Edward Z. Yang authored
      
      
      Summary:
      Suppose that you are typechecking A.hs, which transitively imports,
      via B.hs, A.hs-boot.  When we poke on B.hs and discover that it
      has a reference to a type from A, what TyThing should we wire
      it up with?  Clearly, if we have already typechecked A, we
      should use the most up-to-date TyThing: the one we freshly
      generated when we typechecked A.  But what if we haven't typechecked
      it yet?
      
      For the longest time, GHC adopted the policy that this was
      *an error condition*; that you MUST NEVER poke on B.hs's reference
      to a thing defined in A.hs until A.hs has gotten around to checking
      this.  However, actually ensuring this is the case has proven
      to be a bug farm.  The problem was especially poignant with
      type family consistency checks, which eagerly happen before
      any typechecking takes place.
      
      This patch takes a different strategy: if we ever try to access
      an entity from A which doesn't exist, we just fall back on the
      definition of A from the hs-boot file.  This means that you may
      end up with a mix of A.hs and A.hs-boot TyThings during the
      course of typechecking.
      Signed-off-by: Edward Z. Yang's avatarEdward Z. Yang <ezyang@fb.com>
      
      Test Plan: validate
      
      Reviewers: simonpj, bgamari, austin, goldfire
      
      Subscribers: thomie, rwbarton
      
      GHC Trac Issues: #14396
      
      Differential Revision: https://phabricator.haskell.org/D4154
      69987720
  26. 22 Nov, 2017 2 commits
    • Vladislav Zavialov's avatar
      Test Trac #14488 · 0db4627b
      Vladislav Zavialov authored
      Summary:
      The refactoring in 3f5673f3 also fixed a
      previously unreported issue in the typechecker that prevented defining a
      lens to a record field with a constraint. This patch adds a regression
      test.
      
      Test Plan: make test TEST=14488
      
      Reviewers: bgamari
      
      Reviewed By: bgamari
      
      Subscribers: int-e, rwbarton, thomie
      
      GHC Trac Issues: #14488
      
      Differential Revision: https://phabricator.haskell.org/D4213
      0db4627b
    • Evan Rutledge Borden's avatar
      Add warn-missing-export-lists · 63e4ac37
      Evan Rutledge Borden authored
      Many industrial users have aligned around the idea that implicit exports
      are an anti-pattern. They lead to namespace pollution and byzantine
      naming schemes. They also prevent GHC's dead code analysis and create
      more obstacles to optimization. This warning allows teams/projects to
      warn on or enforce via -Werror explicit export lists.
      
      This warning also serves as a complement to warn-missing-import-lists.
      
      This was originally discussed here:
      https://github.com/ghc-proposals/ghc-proposals/pull/93
      
      Test Plan: Three new minimal tests have been added to the type checker.
      
      Reviewers: bgamari
      
      Reviewed By: bgamari
      
      Subscribers: rwbarton, thomie
      
      Differential Revision: https://phabricator.haskell.org/D4197
      63e4ac37
  27. 08 Nov, 2017 1 commit
    • Simon Peyton Jones's avatar
      Fix another dark corner in the shortcut solver · 30058b0e
      Simon Peyton Jones authored
      The shortcut solver for type classes (Trac #12791) was eagerly
      solving a constaint from an OVERLAPPABLE instance. It happened
      to be the only one in scope, so it was unique, but since it's
      specfically flagged as overlappable it's really a bad idea to
      solve using it, rather than using the Given dictionary.
      
      This led to Trac #14434, a nasty and hard to identify bug.
      30058b0e
  28. 25 Oct, 2017 1 commit
  29. 20 Oct, 2017 1 commit
    • Simon Peyton Jones's avatar
      Improve kick-out in the constraint solver · 3acd6164
      Simon Peyton Jones authored
      This patch was provoked by Trac #14363.  Turned out that we were
      kicking out too many constraints in TcSMonad.kickOutRewritable, and
      that mean that the work-list never became empty: infinite loop!
      
      That in turn made me look harder at the Main Theorem in
      Note [Extending the inert equalities].
      
      Main changes
      
      * Replace TcType.isTyVarExposed by TcType.isTyVarHead.  The
        over-agressive isTyVarExposed is what caused Trac #14363.
        See Note [K3: completeness of solving] in TcSMonad.
      
      * TcType.Make anyRewriteableTyVar role-aware.  In particular,
            a ~R ty
        cannot rewrite
            b ~R f a
        See Note [anyRewriteableTyVar must be role-aware].  That means
        it has to be given a role argument, which forces a little
        refactoring.
      
        I think this change is fixing a bug that hasn't yet been reported.
        The actual reported bug is handled by the previous bullet.  But
        this change is definitely the Right Thing
      
      The main changes are in TcSMonad.kick_out_rewritable, and in TcType
      (isTyVarExposed ---> isTyVarHead).
      
      I did a little unforced refactoring:
      
       * Use the cc_eq_rel field of a CTyEqCan when it is available, rather
         than recomputing it.
      
       * Define eqCanRewrite :: EqRel -> EqRel -> EqRel, and use it, instead
         of duplicating its logic
      3acd6164
  30. 18 Oct, 2017 1 commit
    • Simon Peyton Jones's avatar
      Better solving for representational equalities · 5a66d574
      Simon Peyton Jones authored
      This patch adds a bit of extra solving power for representational
      equality constraints to fix Trac #14333
      
      The main changes:
      
      * Fix a buglet in TcType.isInsolubleOccursCheck which wrongly
        reported a definite occurs-check error for (a ~R# b a)
      
      * Get rid of TcSMonad.emitInsolubles.  It had an ad-hoc duplicate-removal
        piece that is better handled in interactIrred, now that insolubles
        are Irreds.
      
        We need a little care to keep inert_count (which does not include
        insolubles) accurate.
      
      * Refactor TcInteract.solveOneFromTheOther, to return a much simpler
        type.  It was just over-complicated before.
      
      * Make TcInteract.interactIrred look for constraints that match
        either way around, in TcInteract.findMatchingIrreds
      
      This wasn't hard and it cleaned up quite a bit of code.
      5a66d574
  31. 03 Oct, 2017 2 commits
    • Ryan Scott's avatar
      Track the order of user-written tyvars in DataCon · ef26182e
      Ryan Scott authored
      After typechecking a data constructor's type signature, its type
      variables are partitioned into two distinct groups: the universally
      quantified type variables and the existentially quantified type
      variables. Then, when prompted for the type of the data constructor,
      GHC gives this:
      
      ```lang=haskell
      MkT :: forall <univs> <exis>. (...)
      ```
      
      For H98-style datatypes, this is a fine thing to do. But for GADTs,
      this can sometimes produce undesired results with respect to
      `TypeApplications`. For instance, consider this datatype:
      
      ```lang=haskell
      data T a where
        MkT :: forall b a. b -> T a
      ```
      
      Here, the user clearly intended to have `b` be available for visible
      type application before `a`. That is, the user would expect
      `MkT @Int @Char` to be of type `Int -> T Char`, //not//
      `Char -> T Int`. But alas, up until now that was not how GHC
      operated—regardless of the order in which the user actually wrote
      the tyvars, GHC would give `MkT` the type:
      
      ```lang=haskell
      MkT :: forall a b. b -> T a
      ```
      
      Since `a` is universal and `b` is existential. This makes predicting
      what order to use for `TypeApplications` quite annoying, as
      demonstrated in #11721 and #13848.
      
      This patch cures the problem by tracking more carefully the order in
      which a user writes type variables in data constructor type
      signatures, either explicitly (with a `forall`) or implicitly
      (without a `forall`, in which case the order is inferred). This is
      accomplished by adding a new field `dcUserTyVars` to `DataCon`, which
      is a subset of `dcUnivTyVars` and `dcExTyVars` that is permuted to
      the order in which the user wrote them. For more details, refer to
      `Note [DataCon user type variables]` in `DataCon.hs`.
      
      An interesting consequence of this design is that more data
      constructors require wrappers. This is because the workers always
      expect the first arguments to be the universal tyvars followed by the
      existential tyvars, so when the user writes the tyvars in a different
      order, a wrapper type is needed to swizzle the tyvars around to match
      the order that the worker expects. For more details, refer to
      `Note [Data con wrappers and GADT syntax]` in `MkId.hs`.
      
      Test Plan: ./validate
      
      Reviewers: austin, goldfire, bgamari, simonpj
      
      Reviewed By: goldfire, simonpj
      
      Subscribers: ezyang, goldfire, rwbarton, thomie
      
      GHC Trac Issues: #11721, #13848
      
      Differential Revision: https://phabricator.haskell.org/D3687
      ef26182e
    • Simon Peyton Jones's avatar
      Fix bug in the short-cut solver · a8fde183
      Simon Peyton Jones authored
      Trac #13943 showed that the relatively-new short-cut solver
      for class constraints (aka -fsolve-constant-dicts) was wrong.
      In particular, see "Type families" under Note [Shortcut solving]
      in TcInteract.
      
      The short-cut solver recursively solves sub-goals, but it doesn't
      flatten type-family applications, and as a result it erroneously
      thought that C (F a) cannot possibly match (C 0), which is
      simply untrue.  That led to an inifinte loop in the short-cut
      solver.
      
      The significant change is the one line
      
      +                 , all isTyFamFree preds  -- See "Type families" in
      +                                          -- Note [Shortcut solving]
      
      but, as ever, I do some other refactoring.  (E.g. I changed the
      name of the function to shortCutSolver rather than the more
      generic trySolveFromInstance.)
      
      I also made the short-cut solver respect the solver-depth limit,
      so that if this happens again it won't just produce an infinite
      loop.
      
      A bit of other refactoring, notably moving isTyFamFree
      from TcValidity to TcType
      a8fde183
  32. 21 Sep, 2017 1 commit
    • Matthías Páll Gissurarson's avatar
      Also show types that subsume a hole as valid substitutions for that hole. · 1c920832
      Matthías Páll Gissurarson authored
      
      
      This builds on the previous "Valid substitutions include..." functionality,
      but add subsumption checking as well, so that the suggested valid substitutions
      show not only exact matches, but also identifiers that fit the hole by virtue of
      subsuming the type of the hole (i.e. being more general than the type of the
      hole).
      
      Building on the previous example, in the given program
      
      ```
      ps :: String -> IO ()
      ps = putStrLn
      
      ps2 :: a -> IO ()
      ps2 _ = putStrLn "hello, world"
      
      main :: IO ()
      main = _ "hello, world"
      ```
      
      The results would be something like
      
      ```
          • Found hole: _ :: [Char] -> IO ()
          • In the expression: _
            In the expression: _ "hello, world"
            In an equation for ‘main’: main = _ "hello, world"
          • Relevant bindings include main :: IO () (bound at t1.hs:8:1)
            Valid substitutions include
              ps :: String -> IO () (defined at t1.hs:2:1)
              ps2 :: forall a. a -> IO () (defined at t1.hs:5:1)
              putStrLn :: String -> IO ()
                (imported from ‘Prelude’ at t1.hs:1:1
                 (and originally defined in ‘System.IO’))
              fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
                (imported from ‘Prelude’ at t1.hs:1:1
                 (and originally defined in ‘GHC.Base’))
              mempty :: forall a. Monoid a => a
                (imported from ‘Prelude’ at t1.hs:1:1
                 (and originally defined in ‘GHC.Base’))
              print :: forall a. Show a => a -> IO ()
                (imported from ‘Prelude’ at t1.hs:1:1
                 (and originally defined in ‘System.IO’))
              (Some substitutions suppressed;
               use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)
      ```
      Signed-off-by: Matthías Páll Gissurarson's avatarMatthías Páll Gissurarson <mpg@mpg.is>
      
      Modified according to suggestions from Simon PJ
      
      Accept tests that match the expectations, still a few to look better at
      
      Swithced to using tcLookup, after sit down with SPJ at ICFP. Implications are WIP.
      
      Now works with polymorphism and constraints!
      
      We still need to merge the latest master, before we can make a patch.
      
      Wrap the type of the hole, instead of implication shenanigans,
      
      As per SPJs suggestion, this is simpler and feels closer to
      what we actually want to do.
      
      Updated tests with the new implementation
      
      Remove debugging trace and update documentation
      
      Reviewers: austin, bgamari
      
      Reviewed By: bgamari
      
      Subscribers: RyanGlScott, rwbarton, thomie
      
      Differential Revision: https://phabricator.haskell.org/D3930
      1c920832
  33. 31 Aug, 2017 1 commit
    • Simon Peyton Jones's avatar
      Really fix Trac #14158 · 2c133b67
      Simon Peyton Jones authored
      I dug more into how #14158 started working. I temporarily reverted the
      patch that "fixed" it, namely
      
          commit a6c448b4
          Author: Simon Peyton Jones <simonpj@microsoft.com>
          Date:   Mon Aug 28 17:33:59 2017 +0100
      
          Small refactor of getRuntimeRep
      
      Sure enough, there was a real bug, described in the new
      TcExpr Note [Visible type application zonk]
      
      In general, syntactic substituion should be kind-preserving!
      Maybe we should check that invariant...
      2c133b67
  34. 29 Aug, 2017 2 commits
  35. 24 Aug, 2017 1 commit