| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
| |
This patch clarifies a dark corner of quantified
constraints.
* See Note [Yukky eq_sel for a HoleDest] in TcSMonad
* Minor refactor, breaking out new function
TcInteract.doTopReactEqPred
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Add 'dumpAction' hook to DynFlags.
It allows GHC API users to catch dumped intermediate codes and
information. The format of the dump (Core, Stg, raw text, etc.) is now
reported allowing easier automatic handling.
* Add 'traceAction' hook to DynFlags.
Some dumps go through the trace mechanism (for instance unfoldings that
have been considered for inlining). This is problematic because:
1) dumps aren't written into files even with -ddump-to-file on
2) dumps are written on stdout even with GHC API
3) in this specific case, dumping depends on unsafe globally stored
DynFlags which is bad for GHC API users
We introduce 'traceAction' hook which allows GHC API to catch those
traces and to avoid using globally stored DynFlags.
* Avoid dumping empty logs via dumpAction/traceAction (but still write
empty files to keep the existing behavior)
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Previously an import cycle between Type and TyCoRep meant that several
functions in TyCoRep ended up SOURCE import coreView. This is quite
unfortunate as coreView is intended to be fused into a larger pattern
match and not incur an extra call.
Fix this with a bit of restructuring:
* Move the functions in `TyCoRep` which depend upon things in `Type`
into `Type`
* Fold contents of `Kind` into `Type` and turn `Kind` into a simple
wrapper re-exporting kind-ish things from `Type`
* Clean up the redundant imports that popped up as a result
Closes #17441.
Metric Decrease:
T4334
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This fixes #16512.
There are lots of parts of this patch:
* The main payload is in FamInst. See
Note [Coverage condition for injective type families] there
for the overview. But it doesn't fix the bug.
* We now bump the reduction depth every time we discharge
a CFunEqCan. See Note [Flatten when discharging CFunEqCan]
in TcInteract.
* Exploration of this revealed a new, easy to maintain invariant
for CTyEqCans. See Note [Almost function-free] in TcRnTypes.
* We also realized that type inference for injectivity was a
bit incomplete. This means we exchanged lookupFlattenTyVar for
rewriteTyVar. See Note [rewriteTyVar] in TcFlatten. The new
function is monadic while the previous one was pure, necessitating
some faff in TcInteract. Nothing too bad.
* zonkCt did not maintain invariants on CTyEqCan. It's not worth
the bother doing so, so we just transmute CTyEqCans to
CNonCanonicals.
* The pure unifier was finding the fixpoint of the returned
substitution, even when doing one-way matching (in tcUnifyTysWithTFs).
Fixed now.
Test cases: typecheck/should_fail/T16512{a,b}
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This introduces three new modules:
- basicTypes/Predicate.hs describes predicates, moving
this logic out of Type. Predicates don't really exist
in Core, and so don't belong in Type.
- typecheck/TcOrigin.hs describes the origin of constraints
and types. It was easy to remove from other modules and
can often be imported instead of other, scarier modules.
- typecheck/Constraint.hs describes constraints as used in
the solver. It is taken from TcRnTypes.
No work other than module splitting is in this patch.
This is the first step toward homogeneous equality, which will
rely more strongly on predicates. And homogeneous equality is the
next step toward a dependently typed core language.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
GHC has a wonderful-but-delicate mechanism for building recursive
dictionaries by adding a goal to the "solved dictionaries" before
solving the sub-goals. See Note [Solved dictionaries] in TcSMonad
Ticket #17267 showed that if you use this mechanism for local
/quantified/ constraints you can get a loop -- or even unsafe
coerce. This patch fixes the bug.
Specifically
* Make TcSMonad.addSolvedDict be conditional on using a
/top level/ instance, not a quantified one.
* Moreover, we /also/ don't want to add a solved dict
for equalities (a~b).
* Add lots more comments to Note [Solved dictionaries]
to explain the above cryptic stuff.
* Extend InstanceWhat to identify those strange built-in
equality instances.
A couple of other things along the way
* Delete the unused Type.isIPPred_maybe.
* Stop making addSolvedDict conditional on not being an
impolicit parameter. This comes from way back. But
it's irrelevant now because IP dicts are never solved
via an instance.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Currently, newtype constructors are not marked as used when they are
accessed under the hood by uses of `coerce`, as described in #10347.
This fixes #10347 by co-opting the `tcg_keep` field of `TcGblEnv`
to track uses of newtype constructors in the `Coercible` solver.
See `Note [Tracking unused binding and imports]` in `TcRnTypes`.
Since #10347 is fixed, I was able to simplify the code in `TcDeriv`
slightly, as the hack described in
`Note [Newtype deriving and unused constructors]`
is no longer necessary.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When the canonicaliser rewrites evidence of a Wanted, it
should preserve the ShadowInfo (ctev_nosh) field. That is,
a WDerive should rewrite to WDerive, and WOnly to WOnly.
Previously we were unconditionally making a WDeriv, thereby
rewriting WOnly to WDeriv. This bit Nick Frisby (issue #16735)
in the context of his plugin, but we don't have a compact test
case.
The fix is simple, but does involve a bit more plumbing,
to pass the old ShadowInfo around, to use when building
the new Wanted.
|
| |
|
|
|
| |
This moves all URL references to Trac tickets to their corresponding
GitLab counterparts.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch fixes a fairly long-standing bug (dating back to 2015) in
RdrName.bestImport, namely
commit 9376249b6b78610db055a10d05f6592d6bbbea2f
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Wed Oct 28 17:16:55 2015 +0000
Fix unused-import stuff in a better way
In that patch got the sense of the comparison back to front, and
thereby failed to implement the unused-import rules described in
Note [Choosing the best import declaration] in RdrName
This led to Trac #13064 and #15393
Fixing this bug revealed a bunch of unused imports in libraries;
the ones in the GHC repo are part of this commit.
The two important changes are
* Fix the bug in bestImport
* Modified the rules by adding (a) in
Note [Choosing the best import declaration] in RdrName
Reason: the previosu rules made Trac #5211 go bad again. And
the new rule (a) makes sense to me.
In unravalling this I also ended up doing a few other things
* Refactor RnNames.ImportDeclUsage to use a [GlobalRdrElt] for the
things that are used, rather than [AvailInfo]. This is simpler
and more direct.
* Rename greParentName to greParent_maybe, to follow GHC
naming conventions
* Delete dead code RdrName.greUsedRdrName
Bumps a few submodules.
Reviewers: hvr, goldfire, bgamari, simonmar, jrtc27
Subscribers: rwbarton, carter
Differential Revision: https://phabricator.haskell.org/D5312
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
| |
In TcSimplify.neededEvVars, in add_implic_seeds we were
deleting the 'givens'; but they are already deleted, so
this is a no-op. This patch just remove the redundant
delete.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Summary:
It's rather unfortunate that derived code can produce inaccessible
code warnings (as demonstrated in #8128, #8740, and #15398), since
the programmer has no control over the generated code. This patch
aims to suppress `-Winaccessible-code` in all derived code. It
accomplishes this by doing the following:
* Generalize the `ic_env :: TcLclEnv` field of `Implication` to
be of type `Env TcGblEnc TcLclEnv` instead. This way, it also
captures `DynFlags`, which record the flag state at the time
the `Implication` was created.
* When typechecking derived code, turn off `-Winaccessible-code`.
This way, any insoluble given `Implication`s that are created when
typechecking this derived code will remember that
`-Winaccessible-code` was disabled.
* During error reporting, consult the `DynFlags` of an
`Implication` before making the decision to report an inaccessible
code warning.
Test Plan: make test TEST="T8128 T8740 T15398"
Reviewers: simonpj, bgamari
Reviewed By: simonpj
Subscribers: monoidal, rwbarton, thomie, carter
GHC Trac Issues: #8128, #8740, #15398
Differential Revision: https://phabricator.haskell.org/D4993
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
There are several changes here.
* TcInteract has gotten too big, so I moved all the class-instance
matching out of TcInteract into a new module ClsInst. It parallels
the FamInst module.
The main export of ClsInst is matchGlobalInst.
This now works in TcM not TcS.
* A big reason to make matchGlobalInst work in TcM is that we can
then use it from TcValidity.checkSimplifiableClassConstraint.
That extends checkSimplifiableClassConstraint to work uniformly
for built-in instances, which means that we now get a warning
if we have givens (Typeable x, KnownNat n); see Trac #15322.
* This change also made me refactor LookupInstResult, in particular
by adding the InstanceWhat field. I also changed the name of the
type to ClsInstResult.
Then instead of matchGlobalInst reporting a staging error (which is
inappropriate for the call from TcValidity), we can do so in
TcInteract.checkInstanceOK.
* In TcValidity, we now check quantified constraints for termination.
For example, this signature should be rejected:
f :: (forall a. Eq (m a) => Eq (m a)) => blah
as discussed in Trac #15316. The main change here is that
TcValidity.check_pred_help now uses classifyPredType, and has a
case for ForAllPred which it didn't before.
This had knock-on refactoring effects in TcValidity.
|
| | |
|
| |
|
|
|
| |
We call checkReductionDepth in chooseInstance, so there's no
need to call it in selectNextWorkItem too
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Trac #15290 showed that it's possible that we might attempt to use a
quantified constraint to solve an equality in a situation where we
don't have anywhere to put the evidence bindings. This made GHC crash.
This patch stops the crash, but still rejects the pogram. See
Note [Instances in no-evidence implications] in TcInteract.
Finding this bug revealed another lurking bug:
* An infelicity in the treatment of superclasses -- we were expanding
them locally at the leaves, rather than at their binding site; see
(3a) in Note [The superclass story].
As a consequence, TcRnTypes.superclassesMightHelp must look inside
implications.
In more detail:
* Stop the crash, by making TcInteract.chooseInstance test for
the no-evidence-bindings case. In that case we simply don't
use the instance. This entailed a slight change to the type
of chooseInstance.
* Make TcSMonad.getPendingScDicts (now renamed getPendingGivenScs)
return only Givens from the /current level/; and make
TcRnTypes.superClassesMightHelp look inside implications.
* Refactor the simpl_loop and superclass-expansion stuff in
TcSimplify. The logic is much easier to understand now, and
has less duplication.
|
| |
|
|
|
|
|
| |
This is an easy fix for Trac #15244: just avoid adding
the same quantified Given constraint to the inert set twice.
See TcSMonad Note [Do not add duplicate quantified instances].
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We have wanted quantified constraints for ages and, as I hoped,
they proved remarkably simple to implement. All the machinery was
already in place.
The main ticket is Trac #2893, but also relevant are
#5927
#8516
#9123 (especially! higher kinded roles)
#14070
#14317
The wiki page is
https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
which in turn contains a link to the GHC Proposal where the change
is specified.
Here is the relevant Note:
Note [Quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The -XQuantifiedConstraints extension allows type-class contexts like
this:
data Rose f x = Rose x (f (Rose f x))
instance (Eq a, forall b. Eq b => Eq (f b))
=> Eq (Rose f a) where
(Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2
Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
This quantified constraint is needed to solve the
[W] (Eq (f (Rose f x)))
constraint which arises form the (==) definition.
Here are the moving parts
* Language extension {-# LANGUAGE QuantifiedConstraints #-}
and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension
* A new form of evidence, EvDFun, that is used to discharge
such wanted constraints
* checkValidType gets some changes to accept forall-constraints
only in the right places.
* Type.PredTree gets a new constructor ForAllPred, and
and classifyPredType analyses a PredType to decompose
the new forall-constraints
* Define a type TcRnTypes.QCInst, which holds a given
quantified constraint in the inert set
* TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst],
which holds all the Given forall-constraints. In effect,
such Given constraints are like local instance decls.
* When trying to solve a class constraint, via
TcInteract.matchInstEnv, use the InstEnv from inert_insts
so that we include the local Given forall-constraints
in the lookup. (See TcSMonad.getInstEnvs.)
* topReactionsStage calls doTopReactOther for CIrredCan and
CTyEqCan, so they can try to react with any given
quantified constraints (TcInteract.matchLocalInst)
* TcCanonical.canForAll deals with solving a
forall-constraint. See
Note [Solving a Wanted forall-constraint]
Note [Solving a Wanted forall-constraint]
* We augment the kick-out code to kick out an inert
forall constraint if it can be rewritten by a new
type equality; see TcSMonad.kick_out_rewritable
Some other related refactoring
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Move SCC on evidence bindings to post-desugaring, which fixed
#14735, and is generally nicer anyway because we can use
existing CoreSyn free-var functions. (Quantified constraints
made the free-vars of an ev-term a bit more complicated.)
* In LookupInstResult, replace GenInst with OneInst and NotSure,
using the latter for multiple matches and/or one or more
unifiers
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Trac #15122 turned out to be interesting.
* Were calling dischargeFmv in three places.
* In all three cases we dealt with the Given case
separately.
* In two of the three cases the Given code was right,
(albeit duplicated).
* In the third case (in TcCanonical.canCFunEqCan), we had
; case flav of
Given -> return () -- nothing more to do.
which was utterly wrong.
The solution is easy: move the Given-case handling into
dischargeFmv (now reenamed dischargeFunEq), and delete it
from the call sites.
Result: less code, easier to understand (dischargeFunEq handles
all three cases, not just two out of three), and Trac #15122 is fixed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
A Derived CFunEqCan does not "own" its FlatMetaTv (fmv), and should not
update it. But one caller (canCFunEqCan) was failing to satisfy the
precondition to dischargeFmv, which led to a crash (Trac #15170).
I fixed this by making dischargeFmv handle Deriveds (to avoid forcing
each caller to do so separately).
NB: this does not completely fix the original #15170 bug, but I'll
explain that on the ticket. The test case for this patch is actually
the program in comment:1.
|
| |
|
|
|
|
|
|
|
|
|
| |
Trac #15164 showed that it sometimes really matters to share
sub-proofs when solving constraints. Without it, we can get
exponentialy bad behaviour.
Fortunately, it's easily solved.
Note [Shortcut try_solve_from_instance] explains.
I did some minor assocaited refactoring.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Trac #15009 showed that, for Given TyVar/TyVar equalities, we really
want to orient them with the deepest-bound skolem on the left. As it
happens, we also want to do the same for Wanteds, but for a different
reason (more likely to be touchable). Either way, deepest wins:
see TcUnify Note [Deeper level on the left].
This observation led me to some significant changes:
* A SkolemTv already had a TcLevel, but the level wasn't really being
used. Now it is!
* I updated added invariant (SkolInf) to TcType
Note [TcLevel and untouchable type variables], documenting that
the level number of all the ic_skols should be the same as the
ic_tclvl of the implication
* FlatSkolTvs and FlatMetaTvs previously had a dummy level-number of
zero, which messed the scheme up. Now they get a level number the
same way as all other TcTyVars, instead of being a special case.
* To make sure that FlatSkolTvs and FlatMetaTvs are untouchable (which
was previously done via their magic zero level) isTouchableMetaTyVar
just tests for those two cases.
* TcUnify.swapOverTyVars is the crucial orientation function; see the
new Note [TyVar/TyVar orientation]. I completely rewrote this function,
and it's now much much easier to understand.
I ended up doing some related refactoring, of course
* I noticed that tcImplicitTKBndrsX and tcExplicitTKBndrsX were doing
a lot of useless work in the case where there are no skolems; I
added a fast-patch
* Elminate the un-used tcExplicitTKBndrsSig; and thereby get rid of
the higher-order parameter to tcExpliciTKBndrsX.
* Replace TcHsType.emitTvImplication with TcUnify.checkTvConstraints,
by analogy with TcUnify.checkConstraints.
* Inline TcUnify.buildImplication into its only call-site in
TcUnify.checkConstraints
* TcS.buildImplication becomes TcS.CheckConstraintsTcS, with a
simpler API
* Now that we have NoEvBindsVar we have no need of termEvidenceAllowed;
nuke the latter, adding Note [No evidence bindings] to TcEvidence.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Splitting TrieMap into a general and core specific part allows us to
define instances for TrieMap without creating a transitive dependency on
CoreSyn.
Test Plan: ci
Reviewers: goldfire, bgamari, simonmar, simonpj
Reviewed By: bgamari, simonpj
Subscribers: simonpj, nomeata, thomie, carter
GHC Trac Issues: #15082
Differential Revision: https://phabricator.haskell.org/D4618
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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}
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
09bf135ace55ce2572bf4168124d631e386c64bb, 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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
f20cf982f126aea968ed6a482551550ffb6650cf
(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.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 8fa4bf9.
Differential Revision: https://phabricator.haskell.org/D4341
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This rather subtle patch fixes Trac #14584. The problem was
that we'd allowed a coercion, bound in a nested scope, to escape
into an outer scope.
The main changes are
* TcSimplify.floatEqualities takes more care when floating
equalities to make sure we don't float one out that mentions
a locally-bound coercion.
See Note [What prevents a constraint from floating]
* TcSimplify.emitResidualConstraints (which emits the residual
constraints in simplifyInfer) now avoids burying the constraints
for escaping CoVars inside the implication constraint.
* Since I had do to this stuff with CoVars, I moved the
fancy footwork about not quantifying over CoVars from
TcMType.quantifyTyVars to its caller
TcSimplify.decideQuantifiedTyVars. I think its other
callers don't need to worry about all this CoVar stuff.
This turned out to be surprisigly tricky, and took me a solid
day to get right. I think the result is reasonably neat, though,
and well documented with Notes.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
