[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 7 commits: Add Given injectivity for built-in type families

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Wed Sep 25 10:27:41 UTC 2024 


Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC


Commits:
a948ae4f by Simon Peyton Jones at 2024-09-25T06:27:10-04:00
Add Given injectivity for built-in type families

Ticket #24845 asks (reasonably enough) that if we have
   [G] a+b ~ 0
then we also know
   [G] a ~ 0, b ~ 0
and similar injectivity-like facts for other built-in type
families.  The status quo was that we never generate evidence for
injectivity among Givens -- but it is quite reasonnable to do so.
All we need is to have /evidence/ for the new constraints

This MR implements that goal.  I also took the opportunity to
* Address #24978: refactoring UnivCo
* Fix #25248, which was a consequences of the previous formulation of UnivCo

As a result this MR touches a lot of code.  The big things are:

* Coercion constructor UnivCo now takes a [Coercion] as argument to
  express the coercions on which the UnivCo depends. A nice consequence
  is that UnivCoProvenance now has no free variables, simpler in a number
  of places.

* Coercion constructors AxiomInstCo and AxiomRuleCo are combined into
  AxiomCo.  The new AxiomCo, carries a (slightly oddly named)
  CoAxiomRule, which itself is a sum type of the various forms of
  built-in axiom.  See Note [CoAxiomRule] in GHC.Core.Coercion.Axiom

  A merit of this is that we can separate the case of open and closed
  type families, and eliminate the redundant `BranchIndex` in the former
  case.

* Much better representation for data BuiltInSynFamily, which means we
  no longer need to enumerate built-in axioms as well as built-in tycons.

* There is a massive refactor in GHC.Builtin.Types.Literals, which contains all
  the built-in axioms for type-level operations (arithmetic, append, cons etc).

  A big change is that instead of redundantly having (a) a hand-written
  matcher, and (b) a template-based "proves" function, which were hard to
  keep in sync, the two are derive from one set of human-supplied info.
  See GHC.Builtin.Types.Literals.mkRewriteAxiom, and friends.

* Significant changes in GHC.Tc.Solver.Equality to account for the new
  opportunity for Given/Given equalities.

Smaller things

* Improve pretty-printing to avoid parens around atomic coercions.

* Do proper eqType in findMatchingIrreds, not `eqTypeNoKindCheck`.
  Looks like a bug, Richard agrees.

* coercionLKind and coercionRKind are hot functions.  I refactored the
  implementation (which I had to change anyway) to increase sharing.
  See Note [coercionKind performance] in GHC.Core.Coercion

* I wrote a new Note [Finding orphan names] in GHC.Core.FVs about orphan
  names

* I improved the `is_concrete` flag in GHC.Core.Type.buildSynTyCon, to avoid
  calling tyConsOfType.  I forget exactly why I did this, but it's definitely
  better now.

* I moved some code from GHC.Tc.Types.Constraint into GHC.Tc.Types.CtLocEnv
  and I renamed the module GHC.Tc.Types.CtLocEnv to GHC.Tc.Types.CtLoc

- - - - -
c615193c by Ryan Scott at 2024-09-25T06:27:11-04:00
Resolve ambiguous method-bound type variables in vanilla defaults and GND

When defining an instance of a class with a "vanilla" default, such as in the
following example (from #14266):

```hs
class A t where
  f :: forall x m. Monoid x => t m -> m
  f = <blah>

instance A []
```

We have to reckon with the fact that the type of `x` (bound by the type
signature for the `f` method) is ambiguous. If we don't deal with the ambiguity
somehow, then when we generate the following code:

```hs
instance A [] where
  f = $dmf @[] -- NB: the type of `x` is still ambiguous
```

Then the generated code will not typecheck. (Issue #25148 is a more recent
example of the same problem.)

To fix this, we bind the type variables from the method's original type
signature using `TypeAbstractions` and instantiate `$dmf` with them using
`TypeApplications`:

```hs
instance A [] where
  f @x @m = $dmf @[] @x @m -- `x` is no longer ambiguous
```

Note that we only do this for vanilla defaults and not for generic defaults
(i.e., defaults using `DefaultSignatures`). For the full details, see `Note
[Default methods in instances] (Wrinkle: Ambiguous types from vanilla method
type signatures)`.

The same problem arose in the code generated by `GeneralizedNewtypeDeriving`,
as we also fix it here using the same technique. This time, we can take
advantage of the fact that `GeneralizedNewtypeDeriving`-generated code
_already_ brings method-bound type variables into scope via `TypeAbstractions`
(after !13190), so it is very straightforward to visibly apply the type
variables on the right-hand sides of equations. See `Note [GND and ambiguity]`.

Fixes #14266. Fixes #25148.

- - - - -
8f238895 by ARATA Mizuki at 2024-09-25T06:27:14-04:00
Document primitive string literals and desugaring of string literals

Fixes #17474 and #17974

Co-authored-by: Matthew Craven <5086-clyring at users.noreply.gitlab.haskell.org>

- - - - -
2ec0e30e by Zubin Duggal at 2024-09-25T06:27:15-04:00
rts: Fix segfault when using non-moving GC with profiling

`nonMovingCollect()` swaps out the `static_flag` value used as a
sentinel for `gct->scavenged_static_objects`, but the subsequent call
`resetStaticObjectForProfiling()` sees the old value of `static_flag` used as
the sentinel and segfaults. So we must call `resetStaticObjectForProfiling()`
before calling `nonMovingCollect()` as otherwise it looks for the incorrect
sentinel value

Fixes #25232 and #23958

Also teach the testsuite driver about nonmoving profiling ways
and stop disabling metric collection when nonmoving GC is enabled.

- - - - -
3e379148 by Sylvain Henry at 2024-09-25T06:27:28-04:00
Fix interaction between fork and kqueue (#24672)

A kqueue file descriptor isn't inherited by a child created with fork.
As such we mustn't try to close this file descriptor as we would close a
random one, e.g. the one used by timerfd.

Fix #24672

- - - - -
fff2dcdd by Simon Peyton Jones at 2024-09-25T06:27:29-04:00
Improve GHC.Tc.Solver.defaultEquality

This MR improves GHC.Tc.Solver.defaultEquality to solve #25251.

The main change is to use checkTyEqRhs to check the equality, so
that we do promotion properly.

But within that we needed a small enhancement to LC_Promote.  See
Note [Defaulting equalites] (DE4) and (DE5)

The tricky case is (alas) hard to trigger, so I have not added a
regression test.

- - - - -
48700abd by Sylvain Henry at 2024-09-25T06:27:33-04:00
JS: fix h$withCStringOnHeap helper (#25288)

strlen returns the length of the string without the \0 terminating byte,
hence CString weren't properly allocated on the heap (ending \0 byte was
missing).

- - - - -


10 changed files:

- compiler/GHC/Builtin/Types/Literals.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/FVs.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Rules.hs


The diff was not included because it is too large.


View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3b086110f4e28cec1189eefa54fa250c579e3eb7...48700abd54735d941ed4dc130eca15b6b91d610c

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3b086110f4e28cec1189eefa54fa250c579e3eb7...48700abd54735d941ed4dc130eca15b6b91d610c
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240925/89e6c721/attachment.html>

More information about the ghc-commits mailing list