| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Both `bindLHsTyVarBndrs` and `bindHsQTyVars` take two separate
`Maybe` arguments, which I find terribly confusing. Thankfully, it's
possible to remove one `Maybe` argument from each of these functions,
which this patch accomplishes:
* `bindHsQTyVars` takes a `Maybe SDoc` argument, which is `Just` if
GHC should warn about any of the quantified type variables going
unused. However, every call site uses `Nothing` in practice. This
makes sense, since it doesn't really make sense to warn about
unused type variables bound by an `LHsQTyVars`. For instance, you
wouldn't warn about the `a` in `data Proxy a = Proxy` going unused.
As a result, I simply remove this `Maybe SDoc` argument altogether.
* `bindLHsTyVarBndrs` also takes a `Maybe SDoc` argument for the same
reasons that `bindHsQTyVars` took one. To make things more
confusing, however, `bindLHsTyVarBndrs` also takes a separate
`HsDocContext` argument, which is pretty-printed (to an `SDoc`) in
warnings and error messages.
In practice, the `Maybe SDoc` and the `HsDocContext` often contain
the same text. See the call sites for `bindLHsTyVarBndrs` in
`rnFamInstEqn` and `rnConDecl`, for instance. There are only a
handful of call sites where the text differs between the
`Maybe SDoc` and `HsDocContext` arguments:
* In `rnHsRuleDecl`, where the `Maybe SDoc` says "`In the rule`"
and the `HsDocContext` says "`In the transformation rule`".
* In `rnHsTyKi`/`rn_ty`, where the `Maybe SDoc` says
"`In the type`" but the `HsDocContext` is inhereted from the
surrounding context (e.g., if `rnHsTyKi` were called on a
top-level type signature, the `HsDocContext` would be
"`In the type signature`" instead)
In both cases, warnings/error messages arguably _improve_ by
unifying making the `Maybe SDoc`'s text match that of the
`HsDocContext`. As a result, I decided to remove the `Maybe SDoc`
argument to `bindLHsTyVarBndrs` entirely and simply reuse the text
from the `HsDocContext`. (I decided to change the phrase
"transformation rule" to "rewrite rule" while I was in the area.)
The `Maybe SDoc` argument has one other purpose: signaling when to
emit "`Unused quantified type variable`" warnings. To recover this
functionality, I replaced the `Maybe SDoc` argument with a
boolean-like `WarnUnusedForalls` argument. The only
`bindLHsTyVarBndrs` call site that chooses _not_ to emit these
warnings in `bindHsQTyVars`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch simplifies GHC to use simple subsumption.
Ticket #17775
Implements GHC proposal #287
https://github.com/ghc-proposals/ghc-proposals/blob/master/
proposals/0287-simplify-subsumption.rst
All the motivation is described there; I will not repeat it here.
The implementation payload:
* tcSubType and friends become noticably simpler, because it no
longer uses eta-expansion when checking subsumption.
* No deeplyInstantiate or deeplySkolemise
That in turn means that some tests fail, by design; they can all
be fixed by eta expansion. There is a list of such changes below.
Implementing the patch led me into a variety of sticky corners, so
the patch includes several othe changes, some quite significant:
* I made String wired-in, so that
"foo" :: String rather than
"foo" :: [Char]
This improves error messages, and fixes #15679
* The pattern match checker relies on knowing about in-scope equality
constraints, andd adds them to the desugarer's environment using
addTyCsDs. But the co_fn in a FunBind was missed, and for some reason
simple-subsumption ends up with dictionaries there. So I added a
call to addTyCsDs. This is really part of #18049.
* I moved the ic_telescope field out of Implication and into
ForAllSkol instead. This is a nice win; just expresses the code
much better.
* There was a bug in GHC.Tc.TyCl.Instance.tcDataFamInstHeader.
We called checkDataKindSig inside tc_kind_sig, /before/
solveEqualities and zonking. Obviously wrong, easily fixed.
* solveLocalEqualitiesX: there was a whole mess in here, around
failing fast enough. I discovered a bad latent bug where we
could successfully kind-check a type signature, and use it,
but have unsolved constraints that could fill in coercion
holes in that signature -- aargh.
It's all explained in Note [Failure in local type signatures]
in GHC.Tc.Solver. Much better now.
* I fixed a serious bug in anonymous type holes. IN
f :: Int -> (forall a. a -> _) -> Int
that "_" should be a unification variable at the /outer/
level; it cannot be instantiated to 'a'. This was plain
wrong. New fields mode_lvl and mode_holes in TcTyMode,
and auxiliary data type GHC.Tc.Gen.HsType.HoleMode.
This fixes #16292, but makes no progress towards the more
ambitious #16082
* I got sucked into an enormous refactoring of the reporting of
equality errors in GHC.Tc.Errors, especially in
mkEqErr1
mkTyVarEqErr
misMatchMsg
misMatchMsgOrCND
In particular, the very tricky mkExpectedActualMsg function
is gone.
It took me a full day. But the result is far easier to understand.
(Still not easy!) This led to various minor improvements in error
output, and an enormous number of test-case error wibbles.
One particular point: for occurs-check errors I now just say
Can't match 'a' against '[a]'
rather than using the intimidating language of "occurs check".
* Pretty-printing AbsBinds
Tests review
* Eta expansions
T11305: one eta expansion
T12082: one eta expansion (undefined)
T13585a: one eta expansion
T3102: one eta expansion
T3692: two eta expansions (tricky)
T2239: two eta expansions
T16473: one eta
determ004: two eta expansions (undefined)
annfail06: two eta (undefined)
T17923: four eta expansions (a strange program indeed!)
tcrun035: one eta expansion
* Ambiguity check at higher rank. Now that we have simple
subsumption, a type like
f :: (forall a. Eq a => Int) -> Int
is no longer ambiguous, because we could write
g :: (forall a. Eq a => Int) -> Int
g = f
and it'd typecheck just fine. But f's type is a bit
suspicious, and we might want to consider making the
ambiguity check do a check on each sub-term. Meanwhile,
these tests are accepted, whereas they were previously
rejected as ambiguous:
T7220a
T15438
T10503
T9222
* Some more interesting error message wibbles
T13381: Fine: one error (Int ~ Exp Int)
rather than two (Int ~ Exp Int, Exp Int ~ Int)
T9834: Small change in error (improvement)
T10619: Improved
T2414: Small change, due to order of unification, fine
T2534: A very simple case in which a change of unification order
means we get tow unsolved constraints instead of one
tc211: bizarre impredicative tests; just accept this for now
Updates Cabal and haddock submodules.
Metric Increase:
T12150
T12234
T5837
haddock.base
Metric Decrease:
haddock.compiler
haddock.Cabal
haddock.base
Merge note: This appears to break the
`UnliftedNewtypesDifficultUnification` test. It has been marked as
broken in the interest of merging.
(cherry picked from commit 66b7b195cb3dce93ed5078b80bf568efae904cc5)
|
|
|
|
|
|
|
|
| |
As noted in !3132, this has rather severe knock-on consequences in
user-code. We'll need to revisit this before merging something along
these lines.
This reverts commit 9749fe1223d182b1f8e7e4f7378df661c509f396.
|
| |
|
|
|
|
| |
Update Haddock submodule
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Previously, if we had a [W] (a :: k1) ~ (rhs :: k2), we would
spit out a [D] k1 ~ k2 and part the W as irreducible, hoping for
a unification. But we needn't do this. Instead, we now spit out
a [W] co :: k2 ~ k1 and then use co to cast the rhs of the original
Wanted. This means that we retain the connection between the
spat-out constraint and the original.
The problem with this new approach is that we cannot use the
casted equality for substitution; it's too like wanteds-rewriting-
wanteds. So, we forbid CTyEqCans that mention coercion holes.
All the details are in Note [Equalities with incompatible kinds]
in TcCanonical.
There are a few knock-on effects, documented where they occur.
While debugging an error in this patch, Simon and I ran into
infelicities in how patterns and matches are printed; we made
small improvements.
This patch includes mitigations for #17828, which causes spurious
pattern-match warnings. When #17828 is fixed, these lines should
be removed.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We now always show "forall {a}. T" for inferred variables,
previously this was controlled by -fprint-explicit-foralls.
This implements part 1 of https://github.com/ghc-proposals/ghc-proposals/pull/179.
Part of GHC ticket #16320.
Furthermore, when printing a levity restriction error, we now display
the HsWrap of the expression. This lets users see the full elaboration with
-fprint-typechecker-elaboration (see also #17670)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Previously, `hsScopedTvs` (and its cousin `hsWcScopedTvs`) pretended
that visible dependent quantification could not possibly happen at
the term level, and cemented that assumption with an `ASSERT`:
```hs
hsScopedTvs (HsForAllTy { hst_fvf = vis_flag, ... }) =
ASSERT( vis_flag == ForallInvis )
...
```
It turns out that this assumption is wrong. You can end up tripping
this `ASSERT` if you stick it to the man and write a type for a term
that uses visible dependent quantification anyway, like in this
example:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
x :: forall a -> a -> a
x = x
```
That won't typecheck, but that's not the point. Before the
typechecker has a chance to reject this, the renamer will try
to use `hsScopedTvs` to bring `a` into scope over the body of `x`,
since `a` is quantified by a `forall`. This, in turn, causes the
`ASSERT` to fail. Bummer.
Instead of walking on this dangerous ground, this patch makes GHC
adopt a more hardline stance by pattern-matching directly on
`ForallInvis` in `hsScopedTvs`:
```hs
hsScopedTvs (HsForAllTy { hst_fvf = ForallInvis, ... }) = ...
```
Now `a` will not be brought over the body of `x` at all (which is how
it should be), there's no chance of the `ASSERT` failing anymore (as
it's gone), and best of all, the behavior of `hsScopedTvs` does not
change. Everyone wins!
Fixes #17687.
|
|
|
|
|
|
|
|
|
| |
This changes GHC's treatment of so-called Naughty Quantification
Candidates to issue errors, instead of zapping to Any.
Close #16775.
No new test cases, because existing ones cover this well.
|
|
|
|
|
|
|
|
|
|
|
| |
Silly users sometimes try to use visible dependent quantification
and polymorphic recursion without a CUSK or SAK. This causes
unexpected errors. So we now adjust expectations with a bit
of helpful messaging.
Closes #17541 and closes #17131.
test cases: dependent/should_fail/T{17541{,b},17131}
|
|
|
|
| |
This makes error messages a tad less noisy.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Rename requires_th to req_th for consistency with other req functions
(e.g. req_interp, req_profiling etc.)
- req_th (previously requires_th) now checks for interpreter (via
req_interp). With this running TH tests are skipped when running the
test suite with stage=1.
- Test tweaks:
- T9360a, T9360b: Use req_interp
- recomp009, T13938, RAE_T32a: Use req_th
- Fix check-makefiles linter: it now looks for Makefiles instead of .T
files (which are actually Python files)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Issue #16418 showed that we were carrying on too eagerly after a bogus
type signature was identified (a bad telescope in fact), leading to a
subsequent crash.
This led me in to a maze of twisty little passages in the typechecker's
error recovery, and I ended up doing some refactoring in TcRnMonad.
Some specfifics
* TcRnMonad.try_m is now called attemptM.
* I switched the order of the result pair in tryTc,
to make it consistent with other similar functions.
* The actual exception used in the Tc monad is irrelevant so,
to avoid polluting type signatures, I made tcTryM, a simple
wrapper around tryM, and used it.
The more important changes are in
* TcSimplify.captureTopConstraints, where we should have been calling
simplifyTop rather than reportUnsolved, so that levity defaulting
takes place properly.
* TcUnify.emitResidualTvConstraint, where we need to set the correct
status for a new implication constraint. (Previously we ended up
with an Insoluble constraint wrapped in an Unsolved implication,
which meant that insolubleWC gave the wrong answer.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Before this patch GHC was trying to be too clever
(Trac #16344); it succeeded in kind-checking this
polymorphic-recursive declaration
data T ka (a::ka) b
= MkT (T Type Int Bool)
(T (Type -> Type) Maybe Bool)
As Note [No polymorphic recursion] discusses, the "solution" was
horribly fragile. So this patch deletes the key lines in
TcHsType, and a wodge of supporting stuff in the renamer.
There were two regressions, both the same: a closed type family
decl like this (T12785b) does not have a CUSK:
type family Payload (n :: Peano) (s :: HTree n x) where
Payload Z (Point a) = a
Payload (S n) (a `Branch` stru) = a
To kind-check the equations we need a dependent kind for
Payload, and we don't get that any more. Solution: make it
a CUSK by giving the result kind -- probably a good thing anyway.
The other case (T12442) was very similar: a close type family
declaration without a CUSK.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The type-variables-escaping-their-scope-via-kinds check in
`TcValidity` was failing to properly expand type synonyms, which led
to #16391. This is easily fixed by using `occCheckExpand` before
performing the validity check.
Along the way, I refactored this check out into its own function,
and sprinkled references to Notes to better explain all of the moving
parts. Many thanks to @simonpj for the suggestions.
Bumps the haddock submodule.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This implements GHC proposal 35
(https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst)
by adding the ability to write kinds with
visible dependent quantification (VDQ).
Most of the work for supporting VDQ was actually done _before_ this
patch. That is, GHC has been able to reason about kinds with VDQ for
some time, but it lacked the ability to let programmers directly
write these kinds in the source syntax. This patch is primarly about
exposing this ability, by:
* Changing `HsForAllTy` to add an additional field of type
`ForallVisFlag` to distinguish between invisible `forall`s (i.e,
with dots) and visible `forall`s (i.e., with arrows)
* Changing `Parser.y` accordingly
The rest of the patch mostly concerns adding validity checking to
ensure that VDQ is never used in the type of a term (as permitting
this would require full-spectrum dependent types). This is
accomplished by:
* Adding a `vdqAllowed` predicate to `TcValidity`.
* Introducing `splitLHsSigmaTyInvis`, a variant of `splitLHsSigmaTy`
that only splits invisible `forall`s. This function is used in
certain places (e.g., in instance declarations) to ensure that GHC
doesn't try to split visible `forall`s (e.g., if it tried splitting
`instance forall a -> Show (Blah a)`, then GHC would mistakenly
allow that declaration!)
This also updates Template Haskell by introducing a new `ForallVisT`
constructor to `Type`.
Fixes #16326. Also fixes #15658 by documenting this feature in the
users' guide.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Implements GHC Proposal #24: .../ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst
Fixes Trac #16334, Trac #16315
With this patch, scoping rules for type and kind variables have been
unified: kind variables no longer receieve special treatment. This
simplifies both the language and the implementation.
User-facing changes
-------------------
* Kind variables are no longer implicitly quantified when an explicit
forall is used:
p :: Proxy (a :: k) -- still accepted
p :: forall k a. Proxy (a :: k) -- still accepted
p :: forall a. Proxy (a :: k) -- no longer accepted
In other words, now we adhere to the "forall-or-nothing" rule more
strictly.
Related function: RnTypes.rnImplicitBndrs
* The -Wimplicit-kind-vars warning has been deprecated.
* Kind variables are no longer implicitly quantified in constructor
declarations:
data T a = T1 (S (a :: k) | forall (b::k). T2 (S b) -- no longer accepted
data T (a :: k) = T1 (S (a :: k) | forall (b::k). T2 (S b) -- still accepted
Related function: RnTypes.extractRdrKindSigVars
* Implicitly quantified kind variables are no longer put in front of
other variables:
f :: Proxy (a :: k) -> Proxy (b :: j)
f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b -- old order
f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b -- new order
This is a breaking change for users of TypeApplications. Note that
we still respect the dpendency order: 'k' before 'a', 'j' before 'b'.
See "Ordering of specified variables" in the User's Guide.
Related function: RnTypes.rnImplicitBndrs
* In type synonyms and type family equations, free variables on the RHS
are no longer implicitly quantified unless used in an outermost kind
annotation:
type T = Just (Nothing :: Maybe a) -- no longer accepted
type T = Just Nothing :: Maybe (Maybe a) -- still accepted
The latter form is a workaround due to temporary lack of an explicit
quantification method. Ideally, we would write something along these
lines:
type T @a = Just (Nothing :: Maybe a)
Related function: RnTypes.extractHsTyRdrTyVarsKindVars
* Named wildcards in kinds are fixed (Trac #16334):
x :: (Int :: _t) -- this compiles, infers (_t ~ Type)
Related function: RnTypes.partition_nwcs
Implementation notes
--------------------
* One of the key changes is the removal of FKTV in RnTypes:
- data FreeKiTyVars = FKTV { fktv_kis :: [Located RdrName]
- , fktv_tys :: [Located RdrName] }
+ type FreeKiTyVars = [Located RdrName]
We used to keep track of type and kind variables separately, but
now that they are on equal footing when it comes to scoping, we
can put them in the same list.
* extract_lty and family are no longer parametrized by TypeOrKind,
as we now do not distinguish kind variables from type variables.
* PatSynExPE and the related Note [Pattern synonym existentials do not scope]
have been removed (Trac #16315). With no implicit kind quantification,
we can no longer trigger the error.
* reportFloatingKvs and the related Note [Free-floating kind vars]
have been removed. With no implicit kind quantification,
we can no longer trigger the error.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
| |
For some reason gitlab is not reporting these as failures in CI. It's
not clear to me why as the junit output looks fine.
Fixes #16112 and #16113
They were fixed by 682783828275cca5fd8bf5be5b52054c75e0e22c
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch makes us fail fast in TcSimplify.solveLocalEqualities,
and in TcHsType.tc_hs_sig_type, if there are insoluble constraints.
Previously we ploughed on even if there were insoluble constraints,
leading to a cascade of hard-to-understand type errors. Failing
eagerly is much better; hence a lot of testsuite error message
changes. Eg if we have
f :: [Maybe] -> blah
f xs = e
then trying typecheck 'f x = e' with an utterly bogus type
is just asking for trouble.
I can't quite remember what provoked me to make this change,
but I think the error messages are notably improved, by
removing confusing clutter and focusing on the real error.
|
|
|
|
| |
As noted in #16112.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Summary:
Previously, `check_type` (which catches illegal uses of
unsaturated type synonyms without enabling `LiberalTypeSynonyms`,
among other things) always checks for uses of polytypes before
anything else. There is a problem with this plan, however:
checking for polytypes requires decomposing `forall`s and other
invisible arguments, an action which itself expands type synonyms!
Therefore, if we have something like:
```lang=haskell
type A a = Int
type B (a :: Type -> Type) = forall x. x -> x
type C = B A
```
Then when checking `B A`, `A` will get expanded to `forall x. x -> x`
before `check_type` has an opportunity to realize that `A` is an
unsaturated type synonym! This is the root cause of #15954.
This patch fixes the issue by moving the case of `check_type` that
detects polytypes to be //after// the case that checks for
`TyConApp`s. That way, the `TyConApp` case will properly flag things
like the unsaturated use of `A` in the example above before we ever
attempt to check for polytypes.
Test Plan: make test TEST=T15954
Reviewers: simonpj, bgamari, goldfire
Reviewed By: simonpj
Subscribers: rwbarton, carter
GHC Trac Issues: #15954
Differential Revision: https://phabricator.haskell.org/D5402
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 changes the behavior of `-fprint-explicit-kinds`
so that it displays kind argument using visible kind application.
In other words, the flag now:
1. Prints instantiations of specified variables with `@(...)`.
2. Prints instantiations of inferred variables with `@{...}`.
In addition, this patch removes the `Use -fprint-explicit-kinds to
see the kind arguments` error message that often arises when a type
mismatch occurs due to different kinds. Instead, whenever there is a
kind mismatch, we now enable the `-fprint-explicit-kinds` flag
locally to help cue to the programmer where the error lies.
(See `Note [Kind arguments in error messages]` in `TcErrors`.)
As a result, these funny `@{...}` things can now appear to the user
even without turning on the `-fprint-explicit-kinds` flag explicitly,
so I took the liberty of documenting them in the users' guide.
Test Plan: ./validate
Reviewers: goldfire, simonpj, bgamari
Reviewed By: simonpj
Subscribers: rwbarton, carter
GHC Trac Issues: #15871
Differential Revision: https://phabricator.haskell.org/D5314
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Fix Trac #15898, by being smarter about when to print
a space before a promoted data constructor, in a HsType.
I had to implement a mildly tiresome function
HsType.lhsTypeHasLeadingPromotionQuote
It has multiple cases, of course, but it's very simple.
The patch improves the error-message output in a bunch of
cases, and (to my surprise) actually fixes a bug in the
output of T14343 (Trac #14343), thus
- In the expression: _ :: Proxy '('( 'True, 'False), 'False)
+ In the expression: _ :: Proxy '( '( 'True, 'False), 'False)
I discovered that there were two copies of the PromotionFlag
type (a boolean, with helpfully named data cons), one in
IfaceType and one in HsType. So I combined into one,
PromotionFlag, and moved it to BasicTypes. That's why
quite a few files are touched, but it's all routine.
|
|
|
|
| |
Oops. Forgot to `git add`.
|
|
|
|
|
|
|
|
| |
We thought that visible dependent quantification was impossible
in terms, but Iceland Jack discovered otherwise in #15859. This fixes an
ASSERT failure that arose.
test case: dependent/should_fail/T15859
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch fixes Trac #15558. There turned out to be
two distinct problems
* In TcExpr.tc_poly_expr_nc we had
tc_poly_expr_nc (L loc expr) res_ty
= do { traceTc "tcPolyExprNC" (ppr res_ty)
; (wrap, expr')
<- tcSkolemiseET GenSigCtxt res_ty $ \ res_ty ->
setSrcSpan loc $
-- NB: setSrcSpan *after* skolemising,
-- so we get better skolem locations
tcExpr expr res_ty
Putting the setSrcSpan inside the tcSkolemise means that
the location on the Implication constraint is the /call/
to the function rather than the /argument/ to the call,
and that is really quite wrong.
I don't know what Richard's comment NB means -- I moved the
setSrcSpan outside, and the "binding site" info in error
messages actually improved.
The reason I found this is that it affects the span reported
for Trac #15558.
* In TcErrors.mkGivenErrorReporter we carefully munge the location
for an insoluble Given constraint (Note [Inaccessible code]).
But the 'implic' passed in wasn't necesarily the immediately-
enclosing implication -- but for location-munging purposes
it jolly well should be.
Solution: use the innermost implication. This actually
simplifies the code -- no need to pass an implication in to
mkGivenErrorReporter.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
TypeInType came with a new function: decideKindGeneralisationPlan.
This type-level counterpart to the term-level decideGeneralisationPlan
chose whether or not a kind should be generalized. The thinking was
that if `let` should not be generalized, then kinds shouldn't either
(under the same circumstances around -XMonoLocalBinds).
However, this is too conservative -- the situation described in the
motivation for "let should be be generalized" does not occur in types.
This commit thus removes decideKindGeneralisationPlan, always
generalizing.
One consequence is that tc_hs_sig_type_and_gen no longer calls
solveEqualities, which reports all unsolved constraints, instead
relying on the solveLocalEqualities in tcImplicitTKBndrs. An effect
of this is that reporing kind errors gets delayed more frequently.
This seems to be a net benefit in error reporting; often, alongside
a kind error, the type error is now reported (and users might find
type errors easier to understand).
Some of these errors ended up at the top level, where it was
discovered that the GlobalRdrEnv containing the definitions in the
local module was not in the TcGblEnv, and thus errors were reported
with qualified names unnecessarily. This commit rejiggers some of
the logic around captureTopConstraints accordingly.
One error message (typecheck/should_fail/T1633)
is a regression, mentioning the name of a default method. However,
that problem is already reported as #10087, its solution is far from
clear, and so I'm not addressing it here.
This commit fixes #15141. As it's an internal refactor, there is
no concrete test case for it.
Along the way, we no longer need the hsib_closed field of
HsImplicitBndrs (it was used only in decideKindGeneralisationPlan)
and so it's been removed, simplifying the datatype structure.
Along the way, I removed code in the validity checker that looks
at coercions. This isn't related to this patch, really (though
it was, at one point), but it's an improvement, so I kept it.
This updates the haddock submodule.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Trac #15343 was caused by two things
First, in TcHsType.tcHsTypeApp, which deals with the type argment
in visible type application, we were failing to call
solveLocalEqualities. But the type argument is like a user type
signature so it's at least inconsitent not to do so.
I thought that would nail it. But it didn't. It turned out that we
were ended up calling decomposePiCos on a type looking like this
(f |> co) Int
where co :: (forall a. ty) ~ (t1 -> t2)
Now, 'co' is insoluble, and we'll report that later. But meanwhile
we don't want to crash in decomposePiCos.
My fix involves keeping track of the type on both sides of the
coercion, and ensuring that the outer shape matches before
decomposing. I wish there was a simpler way to do this. But
I think this one is at least robust.
I suppose it is possible that the decomposePiCos fix would
have cured the original report, but I'm leaving the one-line
tcHsTypeApp fix in too because it just seems more consistent.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Summary:
There was a buglet in `stripInvisArgs` (which is part of the
pretty-printing pipeline for types) in which only invisble arguments
which came before any visible arguments would be suppressed, but any
invisble arguments that came //after// visible ones would still be
printed, even if `-fprint-explicit-kinds` wasn't enabled.
The fix is simple: make `stripInvisArgs` recursively process the
remaining types even after a visible argument is encountered.
Test Plan: make test TEST=T15308
Reviewers: goldfire, bgamari
Reviewed By: bgamari
Subscribers: simonpj, rwbarton, thomie, carter
GHC Trac Issues: #15308
Differential Revision: https://phabricator.haskell.org/D4891
|
|
|
|
|
| |
This was a stderr file for a WIP test in D4728. I ended up removing
the test, but forgot to remove the stderr file.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Trac #14845 brought to light a corner case where a data
constructor could not be promoted (even with `-XTypeInType`) due to
an unpromotable constraint in its context. However, the error message
was less than helpful, so this patch adds an additional check to
`tcTyVar` catch unpromotable data constructors like these //before//
they're promoted, and to give a sensible error message in such cases.
Test Plan: make test TEST="T13895 T14845"
Reviewers: simonpj, goldfire, bgamari
Reviewed By: bgamari
Subscribers: rwbarton, thomie, carter
GHC Trac Issues: #13895, #14845
Differential Revision: https://phabricator.haskell.org/D4728
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Consider (Trac #15215)
data T a = MkT ...
data S a = ...T...MkT....
If there is an error in the definition of 'T' we add a
"fake type constructor" to the type environment, so that we
can continue to typecheck 'S'. But we /were not/ adding
a fake anything for 'MkT' and so there was an internal
error when we met 'MkT' in the body of 'S'.
The fix is to add fake tycons for all the 'implicits' of 'T'.
This is done by mk_fake_tc in TcTyClsDecls.checkValidTyCl,
which now returns a /list/ of TyCons rather than just one.
On the way I did some refactoring:
* Rename TcTyDecls.tcAddImplicits to tcAddTyConsToGblEnv
and make it /include/ the TyCons themeselves as well
as their implicits
* Some incidental refactoring about tcRecSelBinds. The main
thing is that I've avoided creating a HsValBinds that we
immediately decompose. That meant moving some deck chairs
around.
NB: The new error message for the regression test T15215
has the opaque error "Illegal constraint in a type:", flagged
in Trac #14845. But that's the fault of the latter ticket.
The fix here not to blame.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Summary:
Implement the "Embrace Type :: Type" GHC proposal,
.../ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst
GHC 8.0 included a major change to GHC's type system: the Type :: Type
axiom. Though casual users were protected from this by hiding its
features behind the -XTypeInType extension, all programs written in GHC
8+ have the axiom behind the scenes. In order to preserve backward
compatibility, various legacy features were left unchanged. For example,
with -XDataKinds but not -XTypeInType, GADTs could not be used in types.
Now these restrictions are lifted and -XTypeInType becomes a redundant
flag that will be eventually deprecated.
* Incorporate the features currently in -XTypeInType into the
-XPolyKinds and -XDataKinds extensions.
* Introduce a new extension -XStarIsType to control how to parse * in
code and whether to print it in error messages.
Test Plan: Validate
Reviewers: goldfire, hvr, bgamari, alanz, simonpj
Reviewed By: goldfire, simonpj
Subscribers: rwbarton, thomie, mpickering, carter
GHC Trac Issues: #15195
Differential Revision: https://phabricator.haskell.org/D4748
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Summary:
Some recent commits happened to fix other issues:
* c2417b87ff59c92fbfa8eceeff2a0d6152b11a47 fixed #13601 and #13780
* 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 fixed the original program in #13877
Let's add regression tests for each of these to ensure they stay fixed.
Test Plan: make test TEST="T13601 T13780a T13780c T13877"
Reviewers: goldfire, bgamari, austin
Reviewed By: bgamari
Subscribers: rwbarton, thomie
GHC Trac Issues: #13601, #13780, #13877
Differential Revision: https://phabricator.haskell.org/D3794
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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}
|
|
|
|
|
|
|
|
|
|
|
|
| |
Trac #13135 showed that we were failing to apply the
correct substitution to the un-substituted tyvars during
type-family improvement using injectivity. Specifically
in TcInteractlinjImproveEqns we need to use instFlexiX.
An outright bug, easy to fix.
Slight refactoring along the way. The quantified tyars of the axiom are
readily to hand; we don't need to take the free tyvars of the LHS
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Summary:
Add prettyprinter tests, which take a file, parse it, pretty print it,
re-parse the pretty printed version and then compare the original and
new ASTs (ignoring locations)
Updates haddock submodule to match the AST changes.
There are three issues outstanding
1. Extra parens around a context are not reproduced. This will require an
AST change and will be done in a separate patch.
2. Currently if an `HsTickPragma` is found, this is not pretty-printed,
to prevent noise in the output.
I am not sure what the desired behaviour in this case is, so have left
it as before. Test Ppr047 is marked as expected fail for this.
3. Apart from in a context, the ParsedSource AST keeps all the parens from
the original source. Something is happening in the renamer to remove the
parens around visible type application, causing T12530 to fail, as the
dumped splice decl is after the renamer.
This needs to be fixed by keeping the parens, but I do not know where they
are being removed. I have amended the test to pass, by removing the parens
in the expected output.
Test Plan: ./validate
Reviewers: goldfire, mpickering, simonpj, bgamari, austin
Reviewed By: simonpj, bgamari
Subscribers: simonpj, goldfire, thomie, mpickering
Differential Revision: https://phabricator.haskell.org/D2752
GHC Trac Issues: #3384
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Here we consolidate the pretty-printing logic for types in IfaceType. We
need IfaceType regardless and the printer for Type can be implemented in
terms of that for IfaceType. See #11660.
Note that this is very much a work-in-progress. Namely I still have yet
to ponder how to ease the hs-boot file situation, still need to rip out
more dead code, need to move some of the special cases for, e.g., `*` to
the IfaceType printer, and need to get it to validate. That being said,
it comes close to validating as-is.
Test Plan: Validate
Reviewers: goldfire, austin
Subscribers: goldfire, thomie, simonpj
Differential Revision: https://phabricator.haskell.org/D2528
GHC Trac Issues: #11660
|
| |
|
| |
|