For expediency, the initial implementation of linear types in GHC
made it so that let and where binders would always be considered
unrestricted. This was rather unpleasant, and probably a big obstacle
to adoption. At any rate, this was not how the proposal was designed.

This patch fixes this infelicity. It was surprisingly difficult to
build, which explains, in part, why it took so long to materialise.

As of this patch, let or where bindings marked with %1 will be
linear (respectively %p for an arbitrary multiplicity p). Unmarked let
will infer their multiplicity.

Here is a prototypical example of program that used to be rejected and
is accepted with this patch:

```haskell
f :: A %1 -> B
g :: B %1 -> C

h :: A %1 -> C
h x = g y
  where
    y = f x
```

Exceptions:
- Recursive let are unrestricted, as there isn't a clear semantics of
  what a linear recursive binding would be.
- Destructive lets with lazy bindings are unrestricted, as their
  desugaring isn't linear (see also #23461).
- (Strict) destructive lets with inferred polymorphic type are
  unrestricted. Because the desugaring isn't linear (See #18461
  down-thread).

Closes #18461 and #18739

Co-authored-by: @jackohughes

Krzysztof Gogolewski authored 1 year ago and Marge Bot committed 1 year ago

Co-authored-by: Thomas BAGREL <thomas.bagrel@tweag.io>

Krzysztof Gogolewski authored 1 year ago and Marge Bot committed 1 year ago

In this correct program

f :: a %1 -> a
f x = case x of x { _DEFAULT -> x }

after checking the alternative we weren't popping the case binder 'x'
from the usage environment, which meant that the lambda-bound 'x'
was counted twice: in the scrutinee and (incorrectly) in the alternative.
In fact, we weren't checking the usage of 'x' at all.
Now the code for handling _DEFAULT is similar to the one handling
data constructors.

Fixes #23025.

Haskell-mouse authored 1 year ago and Marge Bot committed 1 year ago

I've turned all occurrences of TcRnUnknownMessage in GHC.Rename.HsType
module into a proper TcRnMessage.
Instead, these TcRnMessage messages were introduced:

TcRnDataKindsError
TcRnUnusedQuantifiedTypeVar
TcRnIllegalKindSignature
TcRnUnexpectedPatSigType
TcRnSectionPrecedenceError
TcRnPrecedenceParsingError
TcRnIllegalKind
TcRnNegativeNumTypeLiteral
TcRnUnexpectedKindVar
TcRnBindMultipleVariables
TcRnBindVarAlreadyInScope

Krzysztof Gogolewski authored 2 years ago and Marge Bot committed 2 years ago

Lint was not able to see that x*y <= x*y, because this inequality
was decomposed to x <= x*y && y <= x*y, but there was no rule
to see that x <= x*y.

Fixes #22546.

Vladislav Zavialov authored 2 years ago and Marge Bot committed 2 years ago

Before this patch, GHC unconditionally printed ticks before promoted
data constructors:

	ghci> type T = True  -- unticked (user-written)
	ghci> :kind! T
	T :: Bool
	= 'True              -- ticked (compiler output)

After this patch, GHC prints ticks only when necessary:

	ghci> type F = False    -- unticked (user-written)
	ghci> :kind! F
	F :: Bool
	= False                 -- unticked (compiler output)

	ghci> data False        -- introduce ambiguity
	ghci> :kind! F
	F :: Bool
	= 'False                -- ticked by necessity (compiler output)

The old behavior can be enabled by -fprint-redundant-promotion-ticks.

Summary of changes:
* Rename PrintUnqualified to NamePprCtx
* Add QueryPromotionTick to it
* Consult the GlobalRdrEnv to decide whether to print a tick (see mkPromTick)
* Introduce -fprint-redundant-promotion-ticks

Co-authored-by: Artyom Kuznetsov <hi@wzrd.ht>

Simon Peyton Jones authored 2 years ago and Simon Peyton Jones committed 2 years ago

This big patch addresses the rats-nest of issues that have plagued
us for years, about the relationship between Type and Constraint.
See #11715/#21623.

The main payload of the patch is:
* To introduce CONSTRAINT :: RuntimeRep -> Type
* To make TYPE and CONSTRAINT distinct throughout the compiler

Two overview Notes in GHC.Builtin.Types.Prim

* Note [TYPE and CONSTRAINT]

* Note [Type and Constraint are not apart]
  This is the main complication.

The specifics

* New primitive types (GHC.Builtin.Types.Prim)
  - CONSTRAINT
  - ctArrowTyCon (=>)
  - tcArrowTyCon (-=>)
  - ccArrowTyCon (==>)
  - funTyCon     FUN     -- Not new
  See Note [Function type constructors and FunTy]
  and Note [TYPE and CONSTRAINT]

* GHC.Builtin.Types:
  - New type Constraint = CONSTRAINT LiftedRep
  - I also stopped nonEmptyTyCon being built-in; it only needs to be wired-in

* Exploit the fact that Type and Constraint are distinct throughout GHC
  - Get rid of tcView in favour of coreView.
  - Many tcXX functions become XX functions.
    e.g. tcGetCastedTyVar --> getCastedTyVar

* Kill off Note [ForAllTy and typechecker equality], in (old)
  GHC.Tc.Solver.Canonical.  It said that typechecker-equality should ignore
  the specified/inferred distinction when comparein two ForAllTys.  But
  that wsa only weakly supported and (worse) implies that we need a separate
  typechecker equality, different from core equality. No no no.

* GHC.Core.TyCon: kill off FunTyCon in data TyCon.  There was no need for it,
  and anyway now we have four of them!

* GHC.Core.TyCo.Rep: add two FunTyFlags to FunCo
  See Note [FunCo] in that module.

* GHC.Core.Type.  Lots and lots of changes driven by adding CONSTRAINT.
  The key new function is sORTKind_maybe; most other changes are built
  on top of that.

  See also `funTyConAppTy_maybe` and `tyConAppFun_maybe`.

* Fix a longstanding bug in GHC.Core.Type.typeKind, and Core Lint, in
  kinding ForAllTys.  See new tules (FORALL1) and (FORALL2) in GHC.Core.Type.
  (The bug was that before (forall (cv::t1 ~# t2). blah), where
  blah::TYPE IntRep, would get kind (TYPE IntRep), but it should be
  (TYPE LiftedRep).  See Note [Kinding rules for types] in GHC.Core.Type.

* GHC.Core.TyCo.Compare is a new module in which we do eqType and cmpType.
  Of course, no tcEqType any more.

* GHC.Core.TyCo.FVs. I moved some free-var-like function into this module:
  tyConsOfType, visVarsOfType, and occCheckExpand.  Refactoring only.

* GHC.Builtin.Types.  Compiletely re-engineer boxingDataCon_maybe to
  have one for each /RuntimeRep/, rather than one for each /Type/.
  This dramatically widens the range of types we can auto-box.
  See Note [Boxing constructors] in GHC.Builtin.Types
  The boxing types themselves are declared in library ghc-prim:GHC.Types.

  GHC.Core.Make.  Re-engineer the treatment of "big" tuples (mkBigCoreVarTup
  etc) GHC.Core.Make, so that it auto-boxes unboxed values and (crucially)
  types of kind Constraint. That allows the desugaring for arrows to work;
  it gathers up free variables (including dictionaries) into tuples.
  See  Note [Big tuples] in GHC.Core.Make.

  There is still work to do here: #22336. But things are better than
  before.

* GHC.Core.Make.  We need two absent-error Ids, aBSENT_ERROR_ID for types of
  kind Type, and aBSENT_CONSTRAINT_ERROR_ID for vaues of kind Constraint.
  Ditto noInlineId vs noInlieConstraintId in GHC.Types.Id.Make;
  see Note [inlineId magic].

* GHC.Core.TyCo.Rep. Completely refactor the NthCo coercion.  It is now called
  SelCo, and its fields are much more descriptive than the single Int we used to
  have.  A great improvement.  See Note [SelCo] in GHC.Core.TyCo.Rep.

* GHC.Core.RoughMap.roughMatchTyConName.  Collapse TYPE and CONSTRAINT to
  a single TyCon, so that the rough-map does not distinguish them.

* GHC.Core.DataCon
  - Mainly just improve documentation

* Some significant renamings:
  GHC.Core.Multiplicity: Many -->  ManyTy (easier to grep for)
                         One  -->  OneTy
  GHC.Core.TyCo.Rep TyCoBinder      -->   GHC.Core.Var.PiTyBinder
  GHC.Core.Var      TyCoVarBinder   -->   ForAllTyBinder
                    AnonArgFlag     -->   FunTyFlag
                    ArgFlag         -->   ForAllTyFlag
  GHC.Core.TyCon    TyConTyCoBinder --> TyConPiTyBinder
  Many functions are renamed in consequence
  e.g. isinvisibleArgFlag becomes isInvisibleForAllTyFlag, etc

* I refactored FunTyFlag (was AnonArgFlag) into a simple, flat data type
    data FunTyFlag
      = FTF_T_T           -- (->)  Type -> Type
      | FTF_T_C           -- (-=>) Type -> Constraint
      | FTF_C_T           -- (=>)  Constraint -> Type
      | FTF_C_C           -- (==>) Constraint -> Constraint

* GHC.Tc.Errors.Ppr.  Some significant refactoring in the TypeEqMisMatch case
  of pprMismatchMsg.

* I made the tyConUnique field of TyCon strict, because I
  saw code with lots of silly eval's.  That revealed that
  GHC.Settings.Constants.mAX_SUM_SIZE can only be 63, because
  we pack the sum tag into a 6-bit field.  (Lurking bug squashed.)

Fixes
* #21530

Updates haddock submodule slightly.

Performance changes
~~~~~~~~~~~~~~~~~~~
I was worried that compile times would get worse, but after
some careful profiling we are down to a geometric mean 0.1%
increase in allocation (in perf/compiler).  That seems fine.

There is a big runtime improvement in T10359

Metric Decrease:
    LargeRecord
    MultiLayerModulesTH_OneShot
    T13386
    T13719
Metric Increase:
    T8095

Necessary for newer cross-compiling backends (JS, Wasm) that don't
support TH yet.

Finley McIlwaine authored 2 years ago and Marge Bot committed 2 years ago

When a newtype introduces GADT eq_specs due to a defaulted
RuntimeRep, we detect this and print the error message with
explicit kinds.

This also refactors newtype type checking to use the new
diagnostic infra.

Fixes #21447

sheaf authored 2 years ago and Marge Bot committed 2 years ago

The testsuite output now contains diagnostic codes, so many tests need
to be updated at once.
We decided it was best to keep the diagnostic codes in the testsuite
output, so that contributors don't inadvertently make changes to the
diagnostic codes.

Soham Chowdhury authored 2 years ago and Marge Bot committed 2 years ago

This patch improves the uniformity of error message formatting by
printing constraints in quotes, as we do for types.

Fix #21167

sheaf authored 2 years ago and Marge Bot committed 2 years ago

This patch refactors hasFixedRuntimeRep_remainingValArgs, renaming it
to tcRemainingValArgs. The logic is moved to rebuildHsApps, which
ensures consistent behaviour across tcApp and quickLookArg1/tcEValArg.

This patch also refactors the treatment of stupid theta for data
constructors, changing the place we drop stupid theta arguments
from dsConLike to mkDataConRep (now the datacon wrapper drops these
arguments).

We decided not to implement PHASE 2 of the FixedRuntimeRep plan for
these remaining ValArgs. Future directions are outlined on the wiki:
  https://gitlab.haskell.org/ghc/ghc/-/wikis/Remaining-ValArgs

Fixes #21544 and #21650

Rodrigo Mesquita authored 3 years ago and Marge Bot committed 2 years ago

This commit redefines the structure of Splices in the AST.

We get rid of `HsSplice` which used to represent typed and untyped
splices, quasi quotes, and the result of splicing either an expression,
a type or a pattern.

Instead we have `HsUntypedSplice` which models an untyped splice or a
quasi quoter, which works in practice just like untyped splices.

The `HsExpr` constructor `HsSpliceE` which used to be constructed with
an `HsSplice` is split into `HsTypedSplice` and `HsUntypedSplice`. The
former is directly constructed with an `HsExpr` and the latter now takes
an `HsUntypedSplice`.

Both `HsType` and `Pat` constructors `HsSpliceTy` and `SplicePat` now
take an `HsUntypedSplice` instead of a `HsSplice` (remember only
/untyped splices/ can be spliced as types or patterns).

The result of splicing an expression, type, or pattern is now
comfortably stored in the extension fields `XSpliceTy`, `XSplicePat`,
`XUntypedSplice` as, respectively, `HsUntypedSpliceResult (HsType
GhcRn)`, `HsUntypedSpliceResult (Pat GhcRn)`, and `HsUntypedSpliceResult
(HsExpr GhcRn)`

Overall the TTG extension points are now better used to
make invalid states unrepresentable and model the progression between
stages better.

See Note [Lifecycle of an untyped splice, and PendingRnSplice]
and Note [Lifecycle of an typed splice, and PendingTcSplice] for more
details.

Updates haddock submodule

Fixes #21263

-------------------------
Metric Decrease:
    hard_hole_fits
-------------------------

sheaf authored 2 years ago and Marge Bot committed 2 years ago

This patch adds several tests relating to the eta-expansion of
data constructors, including UnliftedNewtypes and DataTypeContexts.

Simon Peyton Jones authored 2 years ago and Marge Bot committed 2 years ago

This fixes #21479

See Note [Unquantified tyvars in a pattern synonym]

While doing this, I found that some error messages pointed at the
pattern synonym /name/, rather than the /declaration/ so I widened the
SrcSpan to encompass the declaration.

sheaf authored 3 years ago and Marge Bot committed 3 years ago

PHASE 1: we never rewrite Concrete# evidence.

This patch migrates all the representation polymorphism checks to
the typechecker, using a new constraint form

  Concrete# :: forall k. k -> TupleRep '[]

Whenever a type `ty` must be representation-polymorphic
(e.g. it is the type of an argument to a function), we emit a new
`Concrete# ty` Wanted constraint. If this constraint goes
unsolved, we report a representation-polymorphism error to the user.
The 'FRROrigin' datatype keeps track of the context of the
representation-polymorphism check, for more informative error messages.

This paves the way for further improvements, such as
allowing type families in RuntimeReps and improving the soundness
of typed Template Haskell. This is left as future work (PHASE 2).

fixes #17907 #20277 #20330 #20423 #20426

updates haddock submodule

-------------------------
Metric Decrease:
    T5642
-------------------------

Krzysztof Gogolewski authored 3 years ago and Marge Bot committed 3 years ago

When determining whether to default a RuntimeRep or Multiplicity
variable, use isMetaTyVar to distinguish between metavariables
(which can be hidden) and skolems (which cannot).

Krzysztof Gogolewski authored 3 years ago and Marge Bot committed 3 years ago

The previous version did not substitute the type used in the scrutinee.

This commit adds proper hints to most diagnostic types in the
`GHC.Parser.Errors.Types` module. By "proper" we mean that previous to
this commit the hints were bundled together with the diagnostic message,
whereas now we moved most of them as proper `[GhcHint]` in the
implementation of `diagnosticHints`.

More specifically, this is the list of constructors which now has
proper hints:

* PsErrIllegalBangPattern
* PsWarnOperatorWhitespaceExtConflict
* PsErrLambdaCase
* PsErrIllegalPatSynExport
* PsWarnOperatorWhitespace
* PsErrMultiWayIf
* PsErrIllegalQualifiedDo
* PsErrNumUnderscores
* PsErrLinearFunction
* PsErrIllegalTraditionalRecordSyntax
* PsErrIllegalExplicitNamespace
* PsErrOverloadedRecordUpdateNotEnabled
* PsErrIllegalDataTypeContext
* PsErrSemiColonsInCondExpr
* PsErrSemiColonsInCondCmd
* PsWarnStarIsType
* PsWarnImportPreQualified
* PsErrImportPostQualified
* PsErrEmptyDoubleQuotes
* PsErrIllegalRoleName
* PsWarnStarBinder

For some reason, this patch increases the peak_megabyte_allocated of
the T11545 test to 90 (from a baseline of 80) but that particular test
doesn't emit any parsing diagnostic or hint and the metric increase
happens only for the `aarch64-linux-deb10`.

Metric Increase:
    T11545

Krzysztof Gogolewski authored 3 years ago and Marge Bot committed 3 years ago

- Fix linearity error with incomplete MultiWayIf (#20023)
- Fix partial pattern binding error message (#20024)
- Remove obsolete test LinearPolyTest
  It tested the special typing rule for ($), which was removed
  during the implementation of Quick Look 97cff919.
- Fix ticket numbers in linear/*/all.T, they referred to linear types
  issue tracker

Krzysztof Gogolewski authored 3 years ago and Marge Bot committed 3 years ago

- Remove fstName, sndName, fstIdKey, sndIdKey - no longer used,
  removed from basicKnownKeyNames
- Remove breakpointId, breakpointCondId, opaqueTyCon, unknownTyCon -
  they were used in the old implementation of the GHCi debugger
- Fix typos in comments
- Remove outdated comment in Lint.hs
- Use 'LitRubbish' instead of 'RubbishLit' for consistency
- Remove comment about subkinding - superseded by
  Note [Kind Constraint and kind Type]
- Mention ticket ID in a linear types error message
- Fix formatting in using-warnings.rst and linear-types.rst
- Remove comment about 'Any' in Dynamic.hs - Dynamic
  now uses Typeable + existential instead of Any
- Remove codeGen/should_compile/T13233.hs
  This was added by accident, it is not used and T13233 is already in
  should_fail

Alan Zimmerman authored 4 years ago and Marge Bot committed 4 years ago

Metric Increase:
       T10370
       parsing001

Updates haddock submodule

Krzysztof Gogolewski authored 4 years ago and Marge Bot committed 4 years ago

This addresses points (1a) and (1b) of #19165.

- Move mkFailExpr to HsToCore/Utils, as it can be shared
- Desugar incomplete patterns and holes to an empty case,
  as in Note [Incompleteness and linearity]
- Enable linear linting of desugarer output
- Mark MultConstructor as broken. It fails Lint, but I'd like to fix this
  separately.

Metric Decrease:
    T6048

Krzysztof Gogolewski authored 4 years ago and Marge Bot committed 4 years ago

This is a first step towards #18738.

Krzysztof Gogolewski authored 4 years ago and Marge Bot committed 4 years ago

The previous code using TyCoMapper could promote the same metavar twice.
Use a set instead.

When implementing Quick Look I'd failed to remember that overloaded
labels, like #foo, should be treated as a "head", so that they can be
instantiated with Visible Type Application. This caused #19154.

A very similar ticket covers overloaded literals: #19167.

This patch fixes both problems, but (annoyingly, albeit temporarily)
in two different ways.

Overloaded labels

I dealt with overloaded labels by buying fully into the
Rebindable Syntax approach described in GHC.Hs.Expr
Note [Rebindable syntax and HsExpansion].

There is a good overview in GHC.Rename.Expr
Note [Handling overloaded and rebindable constructs].
That module contains much of the payload for this patch.

Specifically:

* Overloaded labels are expanded in the renamer, fixing #19154.
  See Note [Overloaded labels] in GHC.Rename.Expr.

* Left and right sections used to have special code paths in the
  typechecker and desugarer.  Now we just expand them in the
  renamer. This is harder than it sounds.  See GHC.Rename.Expr
  Note [Left and right sections].

* Infix operator applications are expanded in the typechecker,
  specifically in GHC.Tc.Gen.App.splitHsApps.  See
  Note [Desugar OpApp in the typechecker] in that module

* ExplicitLists are expanded in the renamer, when (and only when)
  OverloadedLists is on.

* HsIf is expanded in the renamer when (and only when) RebindableSyntax
  is on.  Reason: the coverage checker treats HsIf specially.  Maybe
  we could instead expand it unconditionally, and fix up the coverage
  checker, but I did not attempt that.

Overloaded literals

Overloaded literals, like numbers (3, 4.2) and strings with
OverloadedStrings, were not working correctly with explicit type
applications (see #19167).  Ideally I'd also expand them in the
renamer, like the stuff above, but I drew back on that because they
can occur in HsPat as well, and I did not want to to do the HsExpanded
thing for patterns.

But they *can* now be the "head" of an application in the typechecker,
and hence something like ("foo" @T) works now.  See
GHC.Tc.Gen.Head.tcInferOverLit.  It's also done a bit more elegantly,
rather than by constructing a new HsExpr and re-invoking the
typechecker. There is some refactoring around tcShortCutLit.

Ultimately there is more to do here, following the Rebindable Syntax
story.

There are a lot of knock-on effects:

* HsOverLabel and ExplicitList no longer need funny (Maybe SyntaxExpr)
  fields to support rebindable syntax -- good!

* HsOverLabel, OpApp, SectionL, SectionR all become impossible in the
  output of the typecheker, GhcTc; so we set their extension fields to
  Void. See GHC.Hs.Expr Note [Constructor cannot occur]

* Template Haskell quotes for HsExpanded is a bit tricky.  See
  Note [Quotation and rebindable syntax] in GHC.HsToCore.Quote.

* In GHC.HsToCore.Match.viewLExprEq, which groups equal HsExprs for the
  purpose of pattern-match overlap checking, I found that dictionary
  evidence for the same type could have two different names.  Easily
  fixed by comparing types not names.

* I did quite a bit of annoying fiddling around in GHC.Tc.Gen.Head and
  GHC.Tc.Gen.App to get error message locations and contexts right,
  esp in splitHsApps, and the HsExprArg type.  Tiresome and not very
  illuminating.  But at least the tricky, higher order, Rebuilder
  function is gone.

* Some refactoring in GHC.Tc.Utils.Monad around contexts and locations
  for rebindable syntax.

* Incidentally fixes #19346, because we now print renamed, rather than
  typechecked, syntax in error mesages about applications.

The commit removes the vestigial module GHC.Builtin.RebindableNames,
and thus triggers a 2.4% metric decrease for test MultiLayerModules
(#19293).

Metric Decrease:
    MultiLayerModules
    T12545

Krzysztof Gogolewski authored 4 years ago and Marge Bot committed 4 years ago

Commit 65721691 (Improve inference with linear types, !4632)
fixed the bug.

Closes #18736.

Krzysztof Gogolewski authored 4 years ago and Marge Bot committed 4 years ago

This fixes test Linear14. The code in Unify.hs was always using
multiplicity Many instead of a new metavariable.

Alan Zimmerman authored 4 years ago and Marge Bot committed 4 years ago

This disallows `a %001 -> b`, and makes sure the type literal is
printed from its SourceText so it is clear why.

Closes #18888

Krzysztof Gogolewski authored 4 years ago and Marge Bot committed 4 years ago

Patch taken from ghc/ghc#18624 (comment 300673)