[Git][ghc/ghc][wip/T24978] Add Given injectivity for built-in type families

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/T24978 at Glasgow Haskell Compiler / GHC


Commits:
f7054f5c by Simon Peyton Jones at 2024-09-21T23:03:54+01: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

- - - - -


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/-/commit/f7054f5ceff24877a89982e5131cdaa9f510e3e5

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f7054f5ceff24877a89982e5131cdaa9f510e3e5
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/20240921/ea7735c6/attachment.html>