| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
| |
This is a small change in user-facing behavior. When we
have a unification variable left over in a CUSK, we previously
would issue an error. But, we can just quantify. This also
teaches kcLHsQTyVars to use quantifyTyVars instead of its own,
ad-hoc quantification scheme.
Fixes #15273.
test case: polykinds/T11648b
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The uo_thing field of TypeEqOrigin is used to track the
"thing" (either term or type) that has the type (kind) stored
in the TypeEqOrigin fields. Previously, this was sometimes a
proper Core Type, which needed zonking and tidying. Now, it
is only HsSyn: much simpler, and the error messages now use
the user-written syntax.
But this aspect of uo_thing didn't cause #13819; it was the
sibling field uo_arity that did. uo_arity stored the number
of arguments of uo_thing, useful when reporting something
like "should have written 2 fewer arguments". We wouldn't want
to say that if the thing didn't have two arguments. However,
in practice, GHC was getting this wrong, and this message
didn't seem all that helpful. Furthermore, the calculation
of the number of arguments is what caused #13819 to fall over.
This patch just removes uo_arity. In my opinion, the change
to error messages is a nudge in the right direction.
Test case: typecheck/should_fail/T13819
|
| |
|
|
|
| |
"One fewer arguments to ..." rather than
"One fewer argument to ..."
|
| |
|
|
|
|
|
|
|
|
|
|
| |
We now check that a CUSK is really a CUSK and issue an error if
it isn't. This also involves more solving and zonking in
kcHsTyVarBndrs, which was the outright bug reported in #11648.
Test cases: polykinds/T11648{,b}
This updates the haddock submodule.
[skip ci]
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).
There are several noteworthy changes with this patch:
* We now have casts in types. These change the kind
of a type. See new constructor `CastTy`.
* All types and all constructors can be promoted.
This includes GADT constructors. GADT pattern matches
take place in type family equations. In Core,
types can now be applied to coercions via the
`CoercionTy` constructor.
* Coercions can now be heterogeneous, relating types
of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
proves both that `t1` and `t2` are the same and also that
`k1` and `k2` are the same.
* The `Coercion` type has been significantly enhanced.
The documentation in `docs/core-spec/core-spec.pdf` reflects
the new reality.
* The type of `*` is now `*`. No more `BOX`.
* Users can write explicit kind variables in their code,
anywhere they can write type variables. For backward compatibility,
automatic inference of kind-variable binding is still permitted.
* The new extension `TypeInType` turns on the new user-facing
features.
* Type families and synonyms are now promoted to kinds. This causes
trouble with parsing `*`, leading to the somewhat awkward new
`HsAppsTy` constructor for `HsType`. This is dispatched with in
the renamer, where the kind `*` can be told apart from a
type-level multiplication operator. Without `-XTypeInType` the
old behavior persists. With `-XTypeInType`, you need to import
`Data.Kind` to get `*`, also known as `Type`.
* The kind-checking algorithms in TcHsType have been significantly
rewritten to allow for enhanced kinds.
* The new features are still quite experimental and may be in flux.
* TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.
* TODO: Update user manual.
Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.
|
| |
|
|
|
|
|
| |
This matches GCC's choice of Unicode quotation marks (i.e. U+2018 and U+2019)
and therefore looks more familiar on the console. This addresses #2507.
Signed-off-by: Herbert Valerio Riedel <hvr@gnu.org>
|
| | |
|
| | |
|
| |
|
