1. 01 Feb, 2018 1 commit
    • Simon Peyton Jones's avatar
      Experiment with eliminating the younger tyvar · 618a805b
      Simon Peyton Jones authored
      This patch is comments only, plus a minor refactor that
      does not change behaviour.
      
      It just records an idea I had for reducing kick-out in the type
      constraint-solver.
      
      See Note [Eliminate younger unification variables] in TcUnify.
      
      Sadly, it didn't improve perf, so I've put it aside, leaving
      some breadcrumbs for future generations of GHC hackers.
      618a805b
  2. 26 Jan, 2018 1 commit
    • Joachim Breitner's avatar
      Turn EvTerm (almost) into CoreExpr (#14691) · 0e022e56
      Joachim Breitner authored
      Ideally, I'd like to do
      
          type EvTerm = CoreExpr
      
      and the type checker builds the evidence terms as it goes. This failed,
      becuase the evidence for `Typeable` refers to local identifiers that are
      added *after* the typechecker solves constraints. Therefore, `EvTerm`
      stays a data type with two constructors: `EvExpr` for `CoreExpr`
      evidence, and `EvTypeable` for the others.
      
      Delted `Note [Memoising typeOf]`, its reference (and presumably
      relevance) was removed in 8fa4bf9a.
      
      Differential Revision: https://phabricator.haskell.org/D4341
      0e022e56
  3. 21 Dec, 2017 1 commit
    • Simon Peyton Jones's avatar
      Refactor coercion holes · a492af06
      Simon Peyton Jones authored
      In fixing Trac #14584 I found that it would be /much/ more
      convenient if a "hole" in a coercion (much like a unification
      variable in a type) acutally had a CoVar associated with it
      rather than just a Unique.  Then I can ask what the free variables
      of a coercion is, and get a set of CoVars including those
      as-yet-un-filled in holes.
      
      Once that is done, it makes no sense to stuff coercion holes
      inside UnivCo.  They were there before so we could know the
      kind and role of a "hole" coercion, but once there is a CoVar
      we can get that info from the CoVar.  So I removed HoleProv
      from UnivCoProvenance and added HoleCo to Coercion.
      
      In summary:
      
      * Add HoleCo to Coercion and remove HoleProv from UnivCoProvanance
      
      * Similarly in IfaceCoercion
      
      * Make CoercionHole have a CoVar in it, not a Unique
      
      * Make tyCoVarsOfCo return the free coercion-hole variables
        as well as the ordinary free CoVars.  Similarly, remember
        to zonk the CoVar in a CoercionHole
      
      We could go further, and remove CoercionHole as a distinct type
      altogther, just collapsing it into HoleCo.  But I have not done
      that yet.
      a492af06
  4. 19 Dec, 2017 1 commit
  5. 30 Oct, 2017 2 commits
  6. 20 Oct, 2017 1 commit
  7. 18 Oct, 2017 2 commits
    • 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
    • Simon Peyton Jones's avatar
      Don't deeply expand insolubles · 74cd1be0
      Simon Peyton Jones authored
      Trac #13450 went bananas if we expand insoluble constraints.
      Better just to leave them un-expanded.
      
      I'm not sure in detail about why it goes so badly wrong; but
      regardless, the less we mess around with insoluble contraints
      the better the error messages will be.
      74cd1be0
  8. 11 Oct, 2017 1 commit
    • Simon Peyton Jones's avatar
      Remove wc_insol from WantedConstraints · f20cf982
      Simon Peyton Jones authored
      This patch is a pure refactoring, which I've wanted to do for
      some time.  The main payload is
      
      * Remove the wc_insol field from WantedConstraints;
        instead put all the insolubles in wc_simple
      
      * Remove inert_insols from InertCans
        Instead put all the insolubles in inert_irreds
      
      * Add a cc_insol flag to CIrredCan, to record that
        the constraint is definitely insoluble
      
      Reasons
      
      * Quite a bit of code gets slightly simpler
      * Fewer concepts to keep separate
      * Insolubles don't happen at all in production code that is
        just being recompiled, so previously there was a lot of
        moving-about of empty sets
      
      A couple of error messages acutally improved.
      f20cf982
  9. 25 Sep, 2017 1 commit
    • Simon Peyton Jones's avatar
      Fix solving of implicit parameter constraints · abed9bf5
      Simon Peyton Jones authored
      Trac #14218 showed that we were not solving implicit-parameter
      constraints correctly.  In particular,
      
      - A tuple constraint could "hide" an implicit-parameter wanted
        constraint, and that in turn could that we solved it from the
        wrong implicit-parameter binding.
      
      - As a special case the HasCallStack constraint (which is just
        short for (IP "callStack" CallStack), was getting mis-solved.
      
      The big change is to arrange that, in TcSMonad.findDict when looking
      for a dictionary, either when looking for a matching inert or solved
      dictionary, we fail for
      
        - Tuples that are hiding implicit parameters
          See Note [Tuples hiding implicit parameters]
      
        - HasCallStack constraints where we have not yet pushed
          on the call-site info
          See Note [Solving CallStack constraints]
      
      I also did a little refactoring
      
      * Move naturallyCoherentClass from Class to TcInteract, its sole
        use site.  Class.hs seems like the wrong place.  (And I also
        do not understand the reason that we need the eq/Coercible/
        Typable stuff in this predicate, but I'll tackle that separately.)
      
      * Move the code that pushes call-site info onto a call stack
        from the "interact" part to the "canonicalise" part of the solver.
      abed9bf5
  10. 19 Sep, 2017 1 commit
    • Herbert Valerio Riedel's avatar
      compiler: introduce custom "GhcPrelude" Prelude · f63bc730
      Herbert Valerio Riedel authored
      This switches the compiler/ component to get compiled with
      -XNoImplicitPrelude and a `import GhcPrelude` is inserted in all
      modules.
      
      This is motivated by the upcoming "Prelude" re-export of
      `Semigroup((<>))` which would cause lots of name clashes in every
      modulewhich imports also `Outputable`
      
      Reviewers: austin, goldfire, bgamari, alanz, simonmar
      
      Reviewed By: bgamari
      
      Subscribers: goldfire, rwbarton, thomie, mpickering, bgamari
      
      Differential Revision: https://phabricator.haskell.org/D3989
      f63bc730
  11. 28 Jul, 2017 1 commit
  12. 27 Jul, 2017 3 commits
    • Richard Eisenberg's avatar
      Fix #12176 by being a bit more careful instantiating. · 1696dbf4
      Richard Eisenberg authored
      Previously, looking up a TyCon that said "no" to mightBeUnsaturated
      would then instantiate all of its invisible binders. But this is
      wrong for vanilla type synonyms, whose RHS kind might legitimately
      start with invisible binders. So a little more care is taken now,
      only to instantiate those invisible binders that need to be (so that
      the TyCon isn't unsaturated).
      1696dbf4
    • Richard Eisenberg's avatar
      Track visibility in TypeEqOrigin · fb752133
      Richard Eisenberg authored
      A type equality error can arise from a mismatch between
      *invisible* arguments just as easily as from visible arguments.
      But we should really prefer printing out errors from visible
      arguments over invisible ones. Suppose we have a mismatch between
      `Proxy Int` and `Proxy Maybe`. Would you rather get an error
      between `Int` and `Maybe`? Or between `*` and `* -> *`? I thought
      so, too.
      
      There is a fair amount of plumbing with this one, but I think
      it's worth it.
      
      This commit introduces a performance regression in test
      perf/compiler/T5631. The cause of the regression is not the
      new visibility stuff, directly: it's due to a change from
      zipWithM to zipWith3M in TcUnify. To my surprise, zipWithM
      is nicely optimized (it fuses away), but zipWith3M is not.
      There are other examples of functions that could be made faster,
      so I've posted a separate ticket, #14037, to track these
      improvements. For now, I've accepted the small (6.6%) regression.
      fb752133
    • Richard Eisenberg's avatar
      Improve error messages around kind mismatches. · 8e15e3d3
      Richard Eisenberg authored
      Previously, when canonicalizing (or unifying, in uType) a
      heterogeneous equality, we emitted a kind equality and used the
      resulting coercion to cast one side of the heterogeneous equality.
      
      While sound, this led to terrible error messages. (See the bugs
      listed below.) The problem is that using the coercion built from
      the emitted kind equality is a bit like a wanted rewriting a wanted.
      The solution is to keep heterogeneous equalities as irreducible.
      
      See Note [Equalities with incompatible kinds] in TcCanonical.
      
      This commit also removes a highly suspicious switch to FM_SubstOnly
      when flattening in the kinds of a type variable. I have no idea
      why this was there, other than as a holdover from pre-TypeInType.
      I've not left a Note because there is simply no reason I can conceive
      of that the FM_SubstOnly should be there.
      
      One challenge with this patch is that the emitted derived equalities
      might get emitted several times: when a heterogeneous equality is
      in an implication and then gets floated out from the implication,
      the Derived is present both in and out of the implication. This
      causes a duplicate error message. (Test case:
      typecheck/should_fail/T7368) Solution: track the provenance of
      Derived constraints and refuse to float out a constraint that has
      an insoluble Derived.
      
      Lastly, this labels one test (dependent/should_fail/RAE_T32a)
      as expect_broken, because the problem is really #12919. The
      different handling of constraints in this patch exposes the error.
      
      This fixes bugs #11198, #12373, #13530, and #13610.
      
      test cases:
      typecheck/should_fail/{T8262,T8603,tcail122,T12373,T13530,T13610}
      8e15e3d3
  13. 20 Jul, 2017 1 commit
  14. 28 Jun, 2017 1 commit
    • Simon Peyton Jones's avatar
      Fix constraint solving for forall-types · fae672f6
      Simon Peyton Jones authored
      Trac #13879 showed that when we were trying to solve
      
        (forall z1 (y1::z1). ty1)  ~  (forall z2 (y2:z2). ty2)
      
      we'd end up spitting out z1~z2 with no binding site for them.
      Those kind equalities need to be inside the implication.
      
      I ended up re-factoring the code for solving forall-equalities.
      It's quite nice now.
      fae672f6
  15. 02 Jun, 2017 1 commit
    • Ryan Scott's avatar
      Use lengthIs and friends in more places · a786b136
      Ryan Scott authored
      While investigating #12545, I discovered several places in the code
      that performed length-checks like so:
      
      ```
      length ts == 4
      ```
      
      This is not ideal, since the length of `ts` could be much longer than 4,
      and we'd be doing way more work than necessary! There are already a slew
      of helper functions in `Util` such as `lengthIs` that are designed to do
      this efficiently, so I found every place where they ought to be used and
      did just that. I also defined a couple more utility functions for list
      length that were common patterns (e.g., `ltLength`).
      
      Test Plan: ./validate
      
      Reviewers: austin, hvr, goldfire, bgamari, simonmar
      
      Reviewed By: bgamari, simonmar
      
      Subscribers: goldfire, rwbarton, thomie
      
      Differential Revision: https://phabricator.haskell.org/D3622
      a786b136
  16. 26 May, 2017 1 commit
    • Simon Peyton Jones's avatar
      Re-engineer Given flatten-skolems · 8dc6d645
      Simon Peyton Jones authored
      The big change here is to fix an outright bug in flattening of Givens,
      albeit one that is very hard to exhibit.  Suppose we have the constraint
          forall a. (a ~ F b) => ..., (forall c. ....(F b)...) ...
      
      Then
       - we'll flatten the (F) b to a fsk, say  (F b ~ fsk1)
       - we'll rewrite the (F b) inside the inner implication to 'fsk1'
       - when we leave the outer constraint we are suppose to unflatten;
         but that fsk1 will still be there
       - if we re-simplify the entire outer implication, we'll re-flatten
         the Given (F b) to, say, (F b ~ fsk2)
      Now we have two fsks standing for the same thing, and that is very
      wrong.
      
      Solution: make fsks behave more like fmvs:
       - A flatten-skolem is now a MetaTyVar, whose MetaInfo is FlatSkolTv
       - We "fill in" that meta-tyvar when leaving the implication
       - The old FlatSkol form of TcTyVarDetails is gone completely
       - We track the flatten-skolems for the current implication in
         a new field of InertSet, inert_fsks.
      
      See Note [The flattening story] in TcFlatten.
      
      In doing this I found various other things to fix:
      
      * I removed the zonkSimples from TcFlatten.unflattenWanteds; it wasn't
        needed.   But I added one in TcSimplify.floatEqualities, which does
        the zonk precisely when it is needed.
      
      * Trac #13674 showed up a case where we had
           - an insoluble Given,   e.g.  a ~ [a]
           - the same insoluble Wanted   a ~ [a]
        We don't use the Given to rewwrite the Wanted (obviously), but
        we therefore ended up reporting
            Can't deduce (a ~ [a]) from (a ~ [a])
        which is silly.
      
        Conclusion: when reporting errors, make the occurs check "win"
        See Note [Occurs check wins] in TcErrors
      8dc6d645
  17. 25 May, 2017 1 commit
  18. 19 May, 2017 1 commit
    • Simon Peyton Jones's avatar
      Ensure that insolubles are fully rewritten · 433b80de
      Simon Peyton Jones authored
      I was alerted to this by Trac #12468 and #11325.  We were treating
      insolubles (and "hole" constraints are treated as insoluble)
      inconsistently.  In some places we were carefully rewriting them
      e.g. Note [Make sure that insolubles are fully rewritten] in
      TcCanonical.  But in TcSimplify we weren't feeding them into
      the solver.
      
      As a result, "hole" constraints were not being rewritten, which
      some users found confusing, and I think rightly so.
      
      This patch also fixes a bug in TcSMonad.emitInsoluble, in which two
      different "hole" constriants could be treated (bogusly) as duplicates,
      thereby losing one.
      433b80de
  19. 09 May, 2017 1 commit
  20. 03 May, 2017 1 commit
    • Richard Eisenberg's avatar
      Fix #13333 by fixing the covar's type in ctEvCoercion · 09bf135a
      Richard Eisenberg authored
      The change is noted in Note [Given in ctEvCoercion]. This patch
      also adds a bit more commentary to TcFlatten, documenting some
      key invariants of the flattening algorithm. While in the area,
      I also removed some stale commentary from TcCanonical.
      09bf135a
  21. 31 Mar, 2017 1 commit
    • Ben Gamari's avatar
      Clean up coreView/tcView. · 6575f4b6
      Ben Gamari authored
      In Core, Constraint should be considered fully equal to
      TYPE LiftedRep, in all ways. Accordingly, coreView should
      unwrap Constraint to become TYPE LiftedRep. Of course, this
      would be a disaster in the type checker.
      
      So, where previously we used coreView in both the type checker
      and in Core, we now have coreView and tcView, which differ only
      in their treatment of Constraint.
      
      Historical note: once upon a past, we had tcView distinct from
      coreView. Back then, it was because newtypes were unwrapped in
      Core but not in the type checker. The distinction is back, but
      for a different reason than before.
      
      This had a few knock-on effects:
      
       * The Typeable solver must explicitly handle Constraint to ensure
         that we produce the correct evidence.
      
       * TypeMap now respects the Constraint/Type distinction
      
      Finished by: bgamari
      
      Test Plan: ./validate
      
      Reviewers: simonpj, austin, bgamari
      
      Reviewed By: simonpj
      
      Subscribers: rwbarton, thomie
      
      Differential Revision: https://phabricator.haskell.org/D3316
      6575f4b6
  22. 27 Mar, 2017 1 commit
    • Simon Peyton Jones's avatar
      Fix error-message suppress on given equalities · e0ad55f8
      Simon Peyton Jones authored
      I'd got the logic slightly wrong when reporting type errors
      for insoluble 'given' equalities.  We suppress insoluble givens
      under some circumstances (see Note [Given errors]), but we then
      suppressed subsequent 'wanted' errors because the (suppressed)
      'given' error "won".  Result: no errors at all :-(.
      
      This patch fixes it and
       - Renames TcType.isTyVarUnderDatatype to the more
         perspicuous TcType.isInsolubleOccursCheck
      
      In doing this I realise that I don't understand why we need
      to keep the insolubles partitioned out separately at all...
      but that is for another day.
      e0ad55f8
  23. 27 Feb, 2017 1 commit
  24. 18 Feb, 2017 1 commit
    • Ben Gamari's avatar
      Generalize kind of the (->) tycon · b207b536
      Ben Gamari authored
      This is generalizes the kind of `(->)`, as discussed in #11714.
      
      This involves a few things,
      
       * Generalizing the kind of `funTyCon`, adding two new `RuntimeRep`
      binders,
        ```lang=haskell
      (->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                     (a :: TYPE r1) (b :: TYPE r2).
              a -> b -> *
        ```
      
       * Unsaturated applications of `(->)` are expressed as explicit
      `TyConApp`s
      
       * Saturated applications of `(->)` are expressed as `FunTy` as they are
      currently
      
       * Saturated applications of `(->)` are expressed by a new `FunCo`
      constructor in coercions
      
       * `splitTyConApp` needs to ensure that `FunTy`s are split to a
      `TyConApp`
         of `(->)` with the appropriate `RuntimeRep` arguments
      
       * Teach CoreLint to check that all saturated applications of `(->)` are
      represented with `FunTy`
      
      At the moment I assume that `Constraint ~ *`, which is an annoying
      source of complexity. This will
      be simplified once D3023 is resolved.
      
      Also, this introduces two known regressions,
      
      `tcfail181`, `T10403`
      =====================
      Only shows the instance,
      
          instance Monad ((->) r) -- Defined in ‘GHC.Base’
      
      in its error message when -fprint-potential-instances is used. This is
      because its instance head now mentions 'LiftedRep which is not in scope.
      I'm not entirely sure of the right way to fix this so I'm just accepting
      the new output for now.
      
      T5963 (Typeable)
      ================
      
      T5963 is now broken since Data.Typeable.Internals.mkFunTy computes its
      fingerprint without the RuntimeRep variables that (->) expects. This
      will be fixed with the merge of D2010.
      
      Haddock performance
      ===================
      
      The `haddock.base` and `haddock.Cabal` tests regress in allocations by
      about 20%. This certainly hurts, but it's also not entirely unexpected:
      the size of every function type grows with this patch and Haddock has a
      lot of functions in its heap.
      b207b536
  25. 13 Feb, 2017 1 commit
  26. 19 Jan, 2017 1 commit
    • Richard Eisenberg's avatar
      Update levity polymorphism · e7985ed2
      Richard Eisenberg authored
      This commit implements the proposal in
      https://github.com/ghc-proposals/ghc-proposals/pull/29 and
      https://github.com/ghc-proposals/ghc-proposals/pull/35.
      
      Here are some of the pieces of that proposal:
      
      * Some of RuntimeRep's constructors have been shortened.
      
      * TupleRep and SumRep are now parameterized over a list of RuntimeReps.
      * This
      means that two types with the same kind surely have the same
      representation.
      Previously, all unboxed tuples had the same kind, and thus the fact
      above was
      false.
      
      * RepType.typePrimRep and friends now return a *list* of PrimReps. These
      functions can now work successfully on unboxed tuples. This change is
      necessary because we allow abstraction over unboxed tuple types and so
      cannot
      always handle unboxed tuples specially as we did before.
      
      * We sometimes have to create an Id from a PrimRep. I thus split PtrRep
      * into
      LiftedRep and UnliftedRep, so that the created Ids have the right
      strictness.
      
      * The RepType.RepType type was removed, as it didn't seem to help with
      * much.
      
      * The RepType.repType function is also removed, in favor of typePrimRep.
      
      * I have waffled a good deal on whether or not to keep VoidRep in
      TyCon.PrimRep. In the end, I decided to keep it there. PrimRep is *not*
      represented in RuntimeRep, and typePrimRep will never return a list
      including
      VoidRep. But it's handy to have in, e.g., ByteCodeGen and friends. I can
      imagine another design choice where we have a PrimRepV type that is
      PrimRep
      with an extra constructor. That seemed to be a heavier design, though,
      and I'm
      not sure what the benefit would be.
      
      * The last, unused vestiges of # (unliftedTypeKind) have been removed.
      
      * There were several pretty-printing bugs that this change exposed;
      * these are fixed.
      
      * We previously checked for levity polymorphism in the types of binders.
      * But we
      also must exclude levity polymorphism in function arguments. This is
      hard to check
      for, requiring a good deal of care in the desugarer. See Note [Levity
      polymorphism
      checking] in DsMonad.
      
      * In order to efficiently check for levity polymorphism in functions, it
      * was necessary
      to add a new bit of IdInfo. See Note [Levity info] in IdInfo.
      
      * It is now safe for unlifted types to be unsaturated in Core. Core Lint
      * is updated
      accordingly.
      
      * We can only know strictness after zonking, so several checks around
      * strictness
      in the type-checker (checkStrictBinds, the check for unlifted variables
      under a ~
      pattern) have been moved to the desugarer.
      
      * Along the way, I improved the treatment of unlifted vs. banged
      * bindings. See
      Note [Strict binds checks] in DsBinds and #13075.
      
      * Now that we print type-checked source, we must be careful to print
      * ConLikes correctly.
      This is facilitated by a new HsConLikeOut constructor to HsExpr.
      Particularly troublesome
      are unlifted pattern synonyms that get an extra void# argument.
      
      * Includes a submodule update for haddock, getting rid of #.
      
      * New testcases:
        typecheck/should_fail/StrictBinds
        typecheck/should_fail/T12973
        typecheck/should_run/StrictPats
        typecheck/should_run/T12809
        typecheck/should_fail/T13105
        patsyn/should_fail/UnliftedPSBind
        typecheck/should_fail/LevPolyBounded
        typecheck/should_compile/T12987
        typecheck/should_compile/T11736
      
      * Fixed tickets:
        #12809
        #12973
        #11736
        #13075
        #12987
      
      * This also adds a test case for #13105. This test case is
      * "compile_fail" and
      succeeds, because I want the testsuite to monitor the error message.
      When #13105 is fixed, the test case will compile cleanly.
      e7985ed2
  27. 09 Jan, 2017 1 commit
  28. 25 Nov, 2016 2 commits
    • Simon Peyton Jones's avatar
      Another major constraint-solver refactoring · 1eec1f21
      Simon Peyton Jones authored
      This patch takes further my refactoring of the constraint
      solver, which I've been doing over the last couple of months
      in consultation with Richard.
      
      It fixes a number of tricky bugs that made the constraint
      solver actually go into a loop, including
      
        Trac #12526
        Trac #12444
        Trac #12538
      
      The main changes are these
      
      * Flatten unification variables (fmvs/fuvs) appear on the LHS
        of a tvar/tyvar equality; thus
                 fmv ~ alpha
        and not
                 alpha ~ fmv
      
        See Note [Put flatten unification variables on the left]
        in TcUnify.  This is implemented by TcUnify.swapOverTyVars.
      
      * Don't reduce a "loopy" CFunEqCan where the fsk appears on
        the LHS:
            F t1 .. tn ~ fsk
        where 'fsk' is free in t1..tn.
        See Note [FunEq occurs-check principle] in TcInteract
      
        This neatly stops some infinite loops that people reported;
        and it allows us to delete some crufty code in reduce_top_fun_eq.
        And it appears to be no loss whatsoever.
      
        As well as fixing loops, ContextStack2 and T5837 both terminate
        when they didn't before.
      
      * Previously we generated "derived shadow" constraints from
        Wanteds, but we could (and sometimes did; Trac #xxxx) repeatedly
        generate a derived shadow from the same Wanted.
      
        A big change in this patch is to have two kinds of Wanteds:
           [WD] behaves like a pair of a Wanted and a Derived
           [W]  behaves like a Wanted only
        See CtFlavour and ShadowInfo in TcRnTypes, and the ctev_nosh
        field of a Wanted.
      
        This turned out to be a lot simpler.  A [WD] gets split into a
        [W] and a [D] in TcSMonad.maybeEmitShaodow.
      
        See TcSMonad Note [The improvement story and derived shadows]
      
      * Rather than have a separate inert_model in the InertCans, I've
        put the derived equalities back into inert_eqs.  We weren't
        gaining anything from a separate field.
      
      * Previously we had a mode for the constraint solver in which it
        would more aggressively solve Derived constraints; it was used
        for simplifying the context of a 'deriving' clause, or a 'default'
        delcaration, for example.
      
        But the complexity wasn't worth it; now I just make proper Wanted
        constraints.  See TcMType.cloneWC
      
      * Don't generate injectivity improvement for Givens; see
        Note [No FunEq improvement for Givens] in TcInteract
      
      * solveSimpleWanteds leaves the insolubles in-place rather than
        returning them.  Simpler.
      
      I also did lots of work on comments, including fixing Trac #12821.
      1eec1f21
    • Simon Peyton Jones's avatar
      Fix a bug in mk_superclasses_of · 0476a64e
      Simon Peyton Jones authored
      This bug meant that we were less eager about expanding
      tuple superclasses than we should have been; i.e. we stopped
      too soon.  That's not fatal, beause we expand more superclasses
      later, but it's less efficient.
      0476a64e
  29. 21 Oct, 2016 3 commits
    • Simon Peyton Jones's avatar
      Improve TcCanonical.unifyWanted and unifyDerived · 6ddba642
      Simon Peyton Jones authored
      When debugging something else I noticed that these functions
      were emitting constraints like
         [W] a ~ a
      which is plain stupid.  So I fixed it not to do that.  Should
      result in fewer constraints getting generated.
      6ddba642
    • Simon Peyton Jones's avatar
      Define emitNewWantedEq, and use it · e1fc5a33
      Simon Peyton Jones authored
      This is just a minor refactoring
      e1fc5a33
    • Simon Peyton Jones's avatar
      Refactor occurrence-check logic · 9417e579
      Simon Peyton Jones authored
      This patch does two related things
      
      * Combines the occurrence-check logic in the on-the-fly unifier with
        that in the constraint solver.  They are both doing the same job,
        after all.  The resulting code is now in TcUnify:
           metaTyVarUpdateOK
           occCheckExpand
           occCheckForErrors (called in TcErrors)
      
      * In doing this I disovered checking for family-free-ness and foralls
        can be unnecessarily inefficient, because it expands type synonyms.
        It's easy just to cache this info in the type syononym TyCon, which
        I am now doing.
      9417e579
  30. 20 Oct, 2016 1 commit
    • Edward Z. Yang's avatar
      New story for abstract data types in hsig files. · 518f2895
      Edward Z. Yang authored
      Summary:
      In the old implementation of hsig files, we directly
      reused the implementation of abstract data types from
      hs-boot files.  However, this was WRONG.  Consider the
      following program (an abridged version of bkpfail24):
      
          {-# LANGUAGE GADTs #-}
          unit p where
              signature H1 where
                  data T
              signature H2 where
                  data T
              module M where
                  import qualified H1
                  import qualified H2
      
                  f :: H1.T ~ H2.T => a -> b
                  f x = x
      
      Prior to this patch, M was accepted, because the type
      inference engine concluded that H1.T ~ H2.T does not
      hold (indeed, *presently*, it does not).  However, if
      we subsequently instantiate p with the same module for
      H1 and H2, H1.T ~ H2.T does hold!  Unsound.
      
      The key is that abstract types from signatures need to
      be treated like *skolem variables*, since you can interpret
      a Backpack unit as a record which is universally quantified
      over all of its abstract types, as such (with some fake
      syntax for structural records):
      
          p :: forall t1 t2. { f :: t1 ~ t2 => a -> b }
          p = { f = \x -> x } -- ill-typed
      
      Clearly t1 ~ t2 is not solvable inside p, and also clearly
      it could be true at some point in the future, so we better
      not treat the lambda expression after f as inaccessible.
      
      The fix seems to be simple: do NOT eagerly fail when trying
      to simplify the given constraints.  Instead, treat H1.T ~ H2.T
      as an irreducible constraint (rather than an insoluble
      one); this causes GHC to treat f as accessible--now we will
      typecheck the rest of the function (and correctly fail).
      Per the OutsideIn(X) paper, it's always sound to fail less
      when simplifying givens.
      
      We do NOT apply this fix to hs-boot files, where abstract
      data is also guaranteed to be nominally distinct (since
      it can't be implemented via a reexport or a type synonym.)
      This is a somewhat unnatural state of affairs (there's
      no way to really interpret this in Haskell land) but
      no reason to change behavior.
      
      I deleted "representationally distinct abstract data",
      which is never used anywhere in GHC.
      
      In the process of constructing this fix, I also realized
      our implementation of type synonym matching against abstract
      data was not sufficiently restrictive.  In order for
      a type synonym T to be well-formed type, it must be a
      nullary synonym (i.e., type T :: * -> *, not type T a = ...).
      Furthermore, since we use abstract data when defining
      instances, they must not have any type family applications.
      
      More details in #12680.  This probably deserves some sort
      of short paper report.
      Signed-off-by: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>
      
      Test Plan: validate
      
      Reviewers: goldfire, simonpj, austin, bgamari
      
      Subscribers: thomie
      
      Differential Revision: https://phabricator.haskell.org/D2594
      518f2895
  31. 30 Sep, 2016 1 commit
    • Simon Peyton Jones's avatar
      Fix a bug in occurs checking · 66a8c194
      Simon Peyton Jones authored
      1. Trac #12593 exposed a long-standing bug in the occurs
         checking machinery.  When unifying two type variables
                a ~ b
         where a /= b, we were assuming that there could be
         no occurs-check error.  But there can: 'a' can occur
         in b's kind!  When the RHS was a non-tyvar we used
         occurCheckExpand, which /did/ look in kinds, but not
         when the RHS was a tyvar.
      
         This bug has been lurking ever since TypeInType, maybe
         longer.  And it was present both in TcUnify (the on-the-fly
         unifier), and in TcInteract.
      
         I ended up refactoring both so that the tyvar/tyvar
         path naturally goes through the same occurs-check as
         non-tyvar rhss.  It's simpler and more robust now.
      
         One good thing is that both unifiers now share
             TcType.swapOverVars
             TcType.canSolveByUnification
         previously they had different logic for the same goals
      
      2. Fixing this bug exposed another!  In T11635 we end
         up unifying
         (alpha :: forall k. k->*) ~ (beta :: forall k. k->*)
         Now that the occurs check is done for tyvars too, we
         look inside beta's kind.  And then reject the program
         becuase of the forall inside there.  But in fact that
         forall is fine -- it does not count as impredicative
         polymoprhism.   See Note [Checking for foralls]
         in TcType.
      
      3. All this fuss around occurrence checking forced me
         to look at TcUnify.checkTauTvUpdate
                and TcType.occurCheckExpand
         There's a lot of duplication there, and I managed
         to elminate quite a bit of it. For example,
         checkTauTvUpdate called a local 'defer_me'; and then
         called occurCheckExpand, which then used a very
         similar 'fast_check'.
      
         Things are better, but there is more to do.
      66a8c194
  32. 28 Jun, 2016 1 commit
    • Simon Peyton Jones's avatar
      Deal correctly with unused imports for 'coerce' · 23b80ac4
      Simon Peyton Jones authored
      We only do newtype unwrapping for Coercible constraints if
      the newtype's data constructor is in scope.  We were trying to
      record the fact that the data constructor was thereby 'used', so
      that an import statement would not be flagged as unnecsssary
      (by -Wunused-imports).
      
      But the code was simply wrong. It was wrong because it assumed
      that only one level of unwrapping happened, whereas
      tcTopNormaliseNewTypeTF_maybe actually unwraps multiple layers.
      So we need to return a /list/ of data constructors that are used.
      
      This entailed a bit of refactoring, as usual.
      
      Fixes Trac #12067
      23b80ac4
  33. 25 Jun, 2016 1 commit
    • eir@cis.upenn.edu's avatar
      s/Invisible/Inferred/g s/Visible/Required/g · 5fdb854c
      eir@cis.upenn.edu authored
      This renames VisibilityFlag from
      
      > data VisibilityFlag = Visible | Specified | Invisible
      
      to
      
      > data ArgFlag = Required | Specified | Inferred
      
      The old name was quite confusing, because both Specified
      and Invisible were invisible! The new names are hopefully clearer.
      5fdb854c