| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Bug #15380 hangs because a knot-tied TyCon ended up in a kind.
Looking at the code in tcInferApps, I'm amazed this hasn't happened
before! I couldn't think of a good way to fix it (with dependent
types, we can't really keep types out of kinds, after all), so
I just went ahead and removed the knot.
This was remarkably easy to do. In tcTyVar, when we find a TcTyCon,
just use it. (Previously, we looked up the knot-tied TyCon and used
that.) Then, during the final zonk, replace TcTyCons with the real,
full-blooded TyCons in the global environment. It's all very easy.
The new bit is explained in the existing
Note [Type checking recursive type and class declarations]
in TcTyClsDecls.
Naturally, I removed various references to the knot and the
zonkTcTypeInKnot (and related) functions. Now, we can print types
during type checking with abandon!
NB: There is a teensy error message regression with this patch,
around the ordering of quantified type variables. This ordering
problem is fixed (I believe) with the patch for #14880. The ordering
affects only internal variables that cannot be instantiated with
any kind of visible type application.
There is also a teensy regression around the printing of types
in TH splices. I think this is really a TH bug and will file
separately.
Test case: dependent/should_fail/T15380
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
I've changed the name from `Valid substitutions` to `Valid hole fits`,
since "substitution" already has a well defined meaning within the
theory. As part of this change, the flags and output is reanamed, with
substitution turning into hole-fit in most cases. "hole fit" was already
used internally in the code, it's clear and shouldn't cause any
confusion.
In this update, I've also reworked how we manage side-effects in the
hole we are considering.
This allows us to consider local bindings such as where clauses and
arguments to functions, suggesting e.g. `a` for `head (x:xs) where head
:: [a] -> a`.
It also allows us to find suggestions such as `maximum` for holes of
type `Ord a => a -> [a]`, and `max` when looking for a match for the
hole in `g = foldl1 _`, where `g :: Ord a => [a] -> a`.
We also show much improved output for refinement hole fits, and
fixes #14990. We now show the correct type of the function, but we also
now show what the arguments to the function should be e.g. `foldl1 (_ ::
Integer -> Integer -> Integer)` when looking for `[Integer] -> Integer`.
I've moved the bulk of the code from `TcErrors.hs` to a new file,
`TcHoleErrors.hs`, since it was getting too big to not live on it's own.
This addresses the considerations raised in #14969, and takes proper
care to set the `tcLevel` of the variables to the right level before
passing it to the simplifier.
We now also zonk the suggestions properly, which improves the output of
the refinement hole fits considerably.
This also filters out suggestions from the `GHC.Err` module, since even
though `error` and `undefined` are indeed valid hole fits, they are
"trivial", and almost never useful to the user.
We now find the hole fits using the proper manner, namely by solving
nested implications. This entails that the givens are passed along using
the implications the hole was nested in, which in turn should mean that
there will be fewer weird bugs in the typed holes.
I've also added a new sorting method (as suggested by SPJ) and sort by
the size of the types needed to turn the hole fits into the type of the
hole. This gives a reasonable approximation to relevance, and is much
faster than the subsumption check. I've also added a flag to toggle
whether to use this new sorting algorithm (as is done by default) or the
subsumption algorithm. This fixes #14969
I've also added documentation for these new flags and update the
documentation according to the new output.
Reviewers: bgamari, goldfire
Reviewed By: bgamari
Subscribers: simonpj, rwbarton, thomie, carter
GHC Trac Issues: #14969, #14990, #10946
Differential Revision: https://phabricator.haskell.org/D4444
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 is an initial attempt at tackling the issue of how to order the
suggestions provided by the valid substitutions checker, by sorting
them by creating a graph of how they subsume each other. We'd like to
order them in such a manner that the most "relevant" suggestions are
displayed first, so that the suggestion that the user might be looking
for is displayed before more far-fetched suggestions (and thus also
displayed when they'd otherwise be cut-off by the
`-fmax-valid-substitutions` limit). The previous ordering was based on
the order in which the elements appear in the list of imports, which I
believe is less correlated with relevance than this ordering.
A drawback of this approach is that, since we now want to sort the
elements, we can no longer "bail out early" when we've hit the
`-fmax-valid-substitutions` limit.
Reviewers: bgamari, dfeuer
Reviewed By: dfeuer
Subscribers: dfeuer, rwbarton, thomie, carter
Differential Revision: https://phabricator.haskell.org/D4326
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This implements SPJ's suggestion on the ticket (#14273). We find the
relevant constraints (ones that whose free unification variables are all
mentioned in the type of the hole), and then clone the free unification
variables of the hole and the relevant constraints. We then add a
subsumption constraints and run the simplifier, and then check whether
all the constraints were solved.
Reviewers: bgamari
Reviewed By: bgamari
Subscribers: RyanGlScott, rwbarton, thomie, carter
GHC Trac Issues: #14273
Differential Revision: https://phabricator.haskell.org/D4315
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This builds on the previous "Valid substitutions include..." functionality,
but add subsumption checking as well, so that the suggested valid substitutions
show not only exact matches, but also identifiers that fit the hole by virtue of
subsuming the type of the hole (i.e. being more general than the type of the
hole).
Building on the previous example, in the given program
```
ps :: String -> IO ()
ps = putStrLn
ps2 :: a -> IO ()
ps2 _ = putStrLn "hello, world"
main :: IO ()
main = _ "hello, world"
```
The results would be something like
```
• Found hole: _ :: [Char] -> IO ()
• In the expression: _
In the expression: _ "hello, world"
In an equation for ‘main’: main = _ "hello, world"
• Relevant bindings include main :: IO () (bound at t1.hs:8:1)
Valid substitutions include
ps :: String -> IO () (defined at t1.hs:2:1)
ps2 :: forall a. a -> IO () (defined at t1.hs:5:1)
putStrLn :: String -> IO ()
(imported from ‘Prelude’ at t1.hs:1:1
(and originally defined in ‘System.IO’))
fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
(imported from ‘Prelude’ at t1.hs:1:1
(and originally defined in ‘GHC.Base’))
mempty :: forall a. Monoid a => a
(imported from ‘Prelude’ at t1.hs:1:1
(and originally defined in ‘GHC.Base’))
print :: forall a. Show a => a -> IO ()
(imported from ‘Prelude’ at t1.hs:1:1
(and originally defined in ‘System.IO’))
(Some substitutions suppressed;
use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)
```
Signed-off-by: Matthías Páll Gissurarson <mpg@mpg.is>
Modified according to suggestions from Simon PJ
Accept tests that match the expectations, still a few to look better at
Swithced to using tcLookup, after sit down with SPJ at ICFP. Implications are WIP.
Now works with polymorphism and constraints!
We still need to merge the latest master, before we can make a patch.
Wrap the type of the hole, instead of implication shenanigans,
As per SPJs suggestion, this is simpler and feels closer to
what we actually want to do.
Updated tests with the new implementation
Remove debugging trace and update documentation
Reviewers: austin, bgamari
Reviewed By: bgamari
Subscribers: RyanGlScott, rwbarton, thomie
Differential Revision: https://phabricator.haskell.org/D3930
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This major commit was initially triggered by #11339, but it spiraled
into a major review of the way in which type signatures for bindings
are handled, especially partial type signatures. On the way I fixed a
number of other bugs, namely
#12069
#12033
#11700
#11339
#11670
The main change is that I completely reorganised the way in which type
signatures in bindings are handled. The new story is in TcSigs
Note [Overview of type signatures]. Some specific:
* Changes in the data types for signatures in TcRnTypes:
TcIdSigInfo and new TcIdSigInst
* New module TcSigs deals with typechecking type signatures
and pragmas. It contains code mostly moved from TcBinds,
which is already too big
* HsTypes: I swapped the nesting of HsWildCardBndrs
and HsImplicitBndsrs, so that the wildcards are on the
oustide not the insidde in a LHsSigWcType. This is just
a matter of convenient, nothing deep.
There are a host of other changes as knock-on effects, and
it all took FAR longer than I anticipated :-). But it is
a significant improvement, I think.
Lots of error messages changed slightly, some just variants but
some modest improvements.
New tests
* typecheck/should_compile
* SigTyVars: a scoped-tyvar test
* ExPat, ExPatFail: existential pattern bindings
* T12069
* T11700
* T11339
* partial-sigs/should_compile
* T12033
* T11339a
* T11670
One thing to check:
* Small change to output from ghc-api/landmines.
Need to check with Alan Zimmerman
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch began as a modest refactoring of HsType and friends, to
clarify and tidy up exactly where quantification takes place in types.
Although initially driven by making the implementation of wildcards more
tidy (and fixing a number of bugs), I gradually got drawn into a pretty
big process, which I've been doing on and off for quite a long time.
There is one compiler performance regression as a result of all
this, in perf/compiler/T3064. I still need to look into that.
* The principal driving change is described in Note [HsType binders]
in HsType. Well worth reading!
* Those data type changes drive almost everything else. In particular
we now statically know where
(a) implicit quantification only (LHsSigType),
e.g. in instance declaratios and SPECIALISE signatures
(b) implicit quantification and wildcards (LHsSigWcType)
can appear, e.g. in function type signatures
* As part of this change, HsForAllTy is (a) simplified (no wildcards)
and (b) split into HsForAllTy and HsQualTy. The two contructors
appear when and only when the correponding user-level construct
appears. Again see Note [HsType binders].
HsExplicitFlag disappears altogether.
* Other simplifications
- ExprWithTySig no longer needs an ExprWithTySigOut variant
- TypeSig no longer needs a PostRn name [name] field
for wildcards
- PatSynSig records a LHsSigType rather than the decomposed
pieces
- The mysterious 'GenericSig' is now 'ClassOpSig'
* Renamed LHsTyVarBndrs to LHsQTyVars
* There are some uninteresting knock-on changes in Haddock,
because of the HsSyn changes
I also did a bunch of loosely-related changes:
* We already had type synonyms CoercionN/CoercionR for nominal and
representational coercions. I've added similar treatment for
TcCoercionN/TcCoercionR
mkWpCastN/mkWpCastN
All just type synonyms but jolly useful.
* I record-ised ForeignImport and ForeignExport
* I improved the (poor) fix to Trac #10896, by making
TcTyClsDecls.checkValidTyCl recover from errors, but adding a
harmless, abstract TyCon to the envt if so.
* I did some significant refactoring in RnEnv.lookupSubBndrOcc,
for reasons that I have (embarrassingly) now totally forgotten.
It had to do with something to do with import and export
Updates haddock submodule.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This puts the "Relevant bindings" section at the end.
It uses a TcErrors.Report Monoid to divide messages by importance and
then mappends them together. This is not the most efficient way since
there are various intermediate Reports and list appends, but it probably
doesn't matter since error messages shouldn't get that large, and are
usually prepended. In practice, everything is `important` except
`relevantBindings`, which is `supplementary`.
ErrMsg's errMsgShortDoc and errMsgExtraInfo were extracted into ErrDoc,
which has important, context, and suppelementary fields. Each of those
three sections is marked with a bullet character, '•' on unicode
terminals and '*' on ascii terminals. Since this breaks tons of tests,
I also modified testlib.normalise_errmsg to strip out '•'s.
--- Additional notes:
To avoid prepending * to an empty doc, I needed to filter empty docs.
This seemed less error-prone than trying to modify everyone who produces
SDoc to instead produce Maybe SDoc. So I added `Outputable.isEmpty`.
Unfortunately it needs a DynFlags, which is kind of bogus, but otherwise
I think I'd need another Empty case for SDoc, and then it couldn't be a
newtype any more.
ErrMsg's errMsgShortString is only used by the Show instance, which is
in turn only used by Show HscTypes.SourceError, which is in turn only
needed for the Exception instance. So it's probably possible to get rid
of errMsgShortString, but that would a be an unrelated cleanup.
Fixes #11014.
Test Plan: see above
Reviewers: austin, simonpj, thomie, bgamari
Reviewed By: thomie, bgamari
Subscribers: simonpj, nomeata, thomie
Differential Revision: https://phabricator.haskell.org/D1427
GHC Trac Issues: #11014
|
|
|
Fixes #10267. Typed holes in typed Template Haskell currently don't work.
See #10945 and #10946.
|
