<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN" "http://www.w3.org/TR/REC-html40/loose.dtd">
<html lang="en" style='--code-editor-font: var(--default-mono-font, "GitLab Mono"), JetBrains Mono, Menlo, DejaVu Sans Mono, Liberation Mono, Consolas, Ubuntu Mono, Courier New, andale mono, lucida console, monospace;'>
<head>
<meta content="text/html; charset=US-ASCII" http-equiv="Content-Type">
<title>
GitLab
</title>
<style data-premailer="ignore" type="text/css">
a { color: #1068bf; }
</style>
<style>img {
max-width: 100%; height: auto;
}
body {
font-size: .875rem;
}
body {
-webkit-text-shadow: rgba(255,255,255,.01) 0 0 1px;
}
body {
font-family: "GitLab Sans",-apple-system,BlinkMacSystemFont,"Segoe UI",Roboto,"Noto Sans",Ubuntu,Cantarell,"Helvetica Neue",sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol","Noto Color Emoji"; font-size: inherit;
}
</style>
</head>
<body style='font-size: inherit; -webkit-text-shadow: rgba(255,255,255,.01) 0 0 1px; font-family: "GitLab Sans",-apple-system,BlinkMacSystemFont,"Segoe UI",Roboto,"Noto Sans",Ubuntu,Cantarell,"Helvetica Neue",sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol","Noto Color Emoji";'>
<div class="content">
<h3 style="margin-top: 20px; margin-bottom: 10px;">
Simon Peyton Jones pushed to branch wip/T24978 at <a href="https://gitlab.haskell.org/ghc/ghc">Glasgow Haskell Compiler / GHC</a>
</h3>
<h4 style="margin-top: 10px; margin-bottom: 10px;">
Commits:
</h4>
<ul>
<li>
<strong style="font-weight: 600;"><a href="https://gitlab.haskell.org/ghc/ghc/-/commit/f7054f5ceff24877a89982e5131cdaa9f510e3e5">f7054f5c</a></strong>
<div>
<span> by Simon Peyton Jones </span> <i> at 2024-09-21T23:03:54+01:00 </i>
</div>
<pre class="commit-message" style='white-space: pre-wrap; display: block; font-size: 14px; color: #28272d; position: relative; font-family: "GitLab Mono","JetBrains Mono","Menlo","DejaVu Sans Mono","Liberation Mono","Consolas","Ubuntu Mono","Courier New","andale mono","lucida console",monospace; word-break: break-all; word-wrap: break-word; background-color: #fbfafd; border-radius: 2px; margin: 0; padding: 8px 12px; border: 1px solid #dcdcde;'>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
</pre>
</li>
</ul>
<h4 style="margin-top: 10px; margin-bottom: 10px;">
10 changed files:
</h4>
<ul>
<li class="file-stats">
<a href="#02362b473a022fb921814e97a6beba08107d38b1">
compiler/GHC/Builtin/Types/Literals.hs
</a>
</li>
<li class="file-stats">
<a href="#783e5dae6e86931f06700fc088fb7d48c8a07386">
compiler/GHC/Core/Coercion.hs
</a>
</li>
<li class="file-stats">
<a href="#b0ab2032bd0c006bb9cda1e5433173de35930f53">
compiler/GHC/Core/Coercion.hs-boot
</a>
</li>
<li class="file-stats">
<a href="#f10ed7a2470454dfdd8691a08beba67d8b78ee70">
compiler/GHC/Core/Coercion/Axiom.hs
</a>
</li>
<li class="file-stats">
<a href="#975dc08a8e7942b32d621f617d5a9c1b668601dd">
compiler/GHC/Core/Coercion/Opt.hs
</a>
</li>
<li class="file-stats">
<a href="#6fcf64907fb5bdd93082d2d1eb94e4566e735865">
compiler/GHC/Core/DataCon.hs
</a>
</li>
<li class="file-stats">
<a href="#448d7f6e0151c2014de38dead3a902f511c45b75">
compiler/GHC/Core/FVs.hs
</a>
</li>
<li class="file-stats">
<a href="#91648438362e5a35363d2bb7abb04016dedd7d7e">
compiler/GHC/Core/FamInstEnv.hs
</a>
</li>
<li class="file-stats">
<a href="#36a42448a83a9d1f6df8475f03ead2eed199dd8e">
compiler/GHC/Core/Lint.hs
</a>
</li>
<li class="file-stats">
<a href="#d01de95d8c71d4dec6a9a59146186e29a5b3fd38">
compiler/GHC/Core/Rules.hs
</a>
</li>
</ul>
<h5 style="margin-top: 10px; margin-bottom: 10px; font-size: .875rem;">
The diff was not included because it is too large.
</h5>
</div>
<div class="footer" style="margin-top: 10px;">
<p style="font-size: small; color: #737278;">
—
<br>
<a href="https://gitlab.haskell.org/ghc/ghc/-/commit/f7054f5ceff24877a89982e5131cdaa9f510e3e5">View it on GitLab</a>.
<br>
You're receiving this email because of your account on <a target="_blank" rel="noopener noreferrer" href="https://gitlab.haskell.org">gitlab.haskell.org</a>. <a href="https://gitlab.haskell.org/-/profile/notifications" target="_blank" rel="noopener noreferrer" class="mng-notif-link">Manage all notifications</a> · <a href="https://gitlab.haskell.org/help" target="_blank" rel="noopener noreferrer" class="help-link">Help</a>
<script type="application/ld+json">{"@context":"http://schema.org","@type":"EmailMessage","action":{"@type":"ViewAction","name":"View Commit","url":"https://gitlab.haskell.org/ghc/ghc/-/commit/f7054f5ceff24877a89982e5131cdaa9f510e3e5"}}</script>
</p>
</div>
</body>
</html>