| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Add 19 new messages. Update test outputs accordingly.
- Pretty print suggest-extensions hints: remove space before
interspersed commas.
- Refactor Rank's MonoType constructors. Each MonoType constructor
should represent a specific case. With the Doc suggestion belonging
to the TcRnMessage diagnostics instead.
- Move Rank from Validity to its own `GHC.Tc.Types.Rank` module.
- Remove the outdated `check_irred_pred` check.
- Remove the outdated duplication check in `check_valid_theta`, which
was subsumed by `redundant-constraints`.
- Add missing test cases for quantified-constraints/T16474 & th/T12387a.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch primarily:
* Documents `checkInferredVars` (previously called
`check_inferred_vars`) more carefully. This is the
function which throws an error message if a user quantifies an
inferred type variable in a place where specificity cannot be
observed. See `Note [Unobservably inferred type variables]` in
`GHC.Rename.HsType`.
Note that I now invoke `checkInferredVars` _alongside_
`rnHsSigType`, `rnHsWcSigType`, etc. rather than doing so _inside_
of these functions. This results in slightly more call sites for
`checkInferredVars`, but it makes it much easier to enumerate the
spots where the inferred type variable restriction comes into
effect.
* Removes the inferred type variable restriction for default method
type signatures, per the discussion in #18432. As a result, this
patch fixes #18432.
Along the way, I performed some various cleanup:
* I moved `no_nested_foralls_contexts_err` into `GHC.Rename.Utils`
(under the new name `noNestedForallsContextsErr`), since it now
needs to be invoked from multiple modules. I also added a helper
function `addNoNestedForallsContextsErr` that throws the error
message after producing it, as this is a common idiom.
* In order to ensure that users cannot sneak inferred type variables
into `SPECIALISE instance` pragmas by way of nested `forall`s, I
now invoke `addNoNestedForallsContextsErr` when renaming
`SPECIALISE instance` pragmas, much like when we rename normal
instance declarations. (This probably should have originally been
done as a part of the fix for #18240, but this task was somehow
overlooked.) As a result, this patch fixes #18455 as a side effect.
|
| |
|
|
| |
This is the full testcase for T15316.
|
| |
|
|
|
|
| |
As noted in #17458, QuantifiedConstraints and UndecideableInstances
could previously be used to write programs which can loop at runtime.
This was fixed in !1870.
|
| |
|
|
| |
This one came in a comment from James Payor
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
The test case in #15918 no longer triggers an `ASSERT` failure on
GHC HEAD, likely due to commit
682783828275cca5fd8bf5be5b52054c75e0e22c (`Make a smart mkAppTyM`).
This patch adds a regression test for #15918 to finally put it to
rest.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Since the introduction of quantified constraints, GHC has rejected
a quantified constraint with (~) in the head, thus
f :: (forall a. blah => a ~ ty) => stuff
I am frankly dubious that this is ever useful. But /is/ necessary for
Coercible (representation equality version of (~)) and it does no harm
to allow it for (~) as well. Plus, our users are asking for it
(Trac #15359, #15625).
It was really only excluded by accident, so
this patch lifts the restriction. See TcCanonical
Note [Equality superclasses in quantified constraints]
There are a number of wrinkles:
* If the context of the quantified constraint is empty, we
can get trouble when we get down to unboxed equality (a ~# b)
or (a ~R# b), as Trac #15625 showed. This is even more of
a corner case, but it produced an outright crash, so I elaborated
the superclass machinery in TcCanonical.makeStrictSuperClasses
to add a void argument in this case. See
Note [Equality superclasses in quantified constraints]
* The restriction on (~) was in TcValidity.checkValidInstHead.
In lifting the restriction I discovered an old special case for
(~), namely
| clas_nm `elem` [ heqTyConName, eqTyConName]
, nameModule clas_nm /= this_mod
This was (solely) to support the strange instance
instance a ~~ b => a ~ b
in Data.Type.Equality. But happily that is no longer
with us, since
commit f265008fb6f70830e7e92ce563f6d83833cef071
Refactor (~) to reduce the suerpclass stack
So I removed the special case.
* I found that the Core invariants on when we could have
co = <expr>
were entirely not written down. (Getting this wrong ws
the proximate source of the crash in Trac #15625. So
- Documented them better in CoreSyn
Note [CoreSyn type and coercion invariant],
- Modified CoreOpt and CoreLint to match
- Modified CoreUtils.bindNonRec to match
- Made MkCore.mkCoreLet use bindNonRec, rather
than duplicate its logic
- Made Simplify.rebuildCase case-to-let respect
Note [CoreSyn type and coercion invariant],
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch responds to Trac #15334 by making it an error to
write an instance declaration for a tuple constraint like
(Eq [a], Show [a]).
I then discovered that instance validity checking was
scattered betweeen TcInstDcls and TcValidity, so I took
the time to bring it all together, into
TcValidity.checkValidInstHead
In doing so I discovered that there are lot of special
cases. I have not changed them, but at least they are
all laid out clearly now.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The level numbers we were getting simply didn't obey the
invariant (ImplicInv) in TcType
Note [TcLevel and untouchable type variables]
That leads to chaos. Easy to fix. I improved the documentation.
I also added an assertion in TcSimplify that checks that
level numbers go up by 1 as we dive inside implications, so
that we catch the problem at source rather than than through
its obscure consequences.
That in turn showed up that TcRules was also generating
constraints that didn't obey (ImplicInv), so I fixed that too.
I have no idea what consequences were lurking behing that
bug, but anyway now it's fixed. Hooray.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 patch adds "quantified constraint" context in error message when
UndecidableInstances checking fails for quantified constraints.
See Trac #15231:comment#1.
This patch also pretty-prints the instance head for better error messages.
Test Plan: make test TEST="T15231"
Reviewers: bgamari, simonpj
Reviewed By: simonpj
Subscribers: simonpj, rwbarton, thomie, carter
GHC Trac Issues: #15231
Differential Revision: https://phabricator.haskell.org/D4819
|
| |
|
|
|
|
|
| |
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
|
