polytropos-plugin (empty) → 0.1.0.2

raw patch · 8 files changed

+4231/−0 lines, 8 filesdep +basedep +directorydep +filepath

Dependencies added: base, directory, filepath, ghc, ghc-tcplugin-api, polytropos-core, polytropos-plugin, primitive, process, tasty, tasty-hunit

Files

• CHANGELOG.md +12/−0
• LICENSE +391/−0
• README.md +63/−0
• polytropos-plugin.cabal +75/−0
• src/Polytropos/Plugin.hs +2295/−0
• src/Polytropos/Plugin/Compat.hs +246/−0
• src/Polytropos/Plugin/Source.hs +610/−0
• tests/smoke/Main.hs +539/−0

@@ -0,0 +1,12 @@+# Changelog for polytropos-plugin++## 0.1.0.0 — Initial Release++- GHC typechecker plugin synthesizing literal dictionaries and $O(1)$ jump tables directly into Core AST+- Solves `FieldIndex` by emitting literal slot index integers+- Solves `ConstructorIndex` by emitting literal tag integers+- Solves `RowEq` and `RowShow` by synthesizing unrolled per-field comparison and formatting routines without inductive search+- Solves `RowEqSum` and `RowShowSum` by synthesizing Core pattern match expressions over constructor tags+- Solves `AllFields` by synthesizing dictionary arrays+- Human-centric compile-time `TypeError` diagnostics with Levenshtein-distance fuzzy field name suggestions+- Multi-GHC compatibility covering GHC 9.6 through GHC 9.14 via `Polytropos.Plugin.Compat`

@@ -0,0 +1,391 @@+Polytropos Dual Licensing++Copyright (c) 2026, Nadia Yvette Chambers <nadia.yvette.chambers@ik.me>+All rights reserved.++SPDX-License-Identifier: EUPL-1.2 OR Apache-2.0++Polytropos is dual-licensed: you may use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the software under the terms+of EITHER:++1. The European Union Public Licence, version 1.2 (EUPL-1.2), as published by+   the European Commission (available in 23 authentic language versions); OR+2. The Apache License, Version 2.0 (Apache-2.0).++You may choose whichever license best fits your requirements and compliance+environment.++Individual license files are available in the LICENSES/ directory:+- LICENSES/EUPL-1.2.txt+- LICENSES/Apache-2.0.txt++================================================================================+1. European Union Public Licence v. 1.2 (EUPL-1.2)+================================================================================++                      EUROPEAN UNION PUBLIC LICENCE v. 1.2+                      EUPL © the European Union 2007, 2016++This European Union Public Licence (the ‘EUPL’) applies to the Work (as defined+below) which is provided under the terms of this Licence. Any use of the Work,+other than as authorised under this Licence is prohibited (to the extent such+use is covered by a right of the copyright holder of the Work).++The Work is provided under the terms of this Licence when the Licensor (as+defined below) has placed the following notice immediately following the+copyright notice for the Work:++        Licensed under the EUPL++or has expressed by any other means his willingness to license under the EUPL.++1. Definitions++In this Licence, the following terms have the following meaning:++- ‘The Licence’: this Licence.++- ‘The Original Work’: the work or software distributed or communicated by the+  Licensor under this Licence, available as Source Code and also as Executable+  Code as the case may be.++- ‘Derivative Works’: the works or software that could be created by the+  Licensee, based upon the Original Work or modifications thereof. This Licence+  does not define the extent of modification or dependence on the Original Work+  required in order to classify a work as a Derivative Work; this extent is+  determined by copyright law applicable in the country mentioned in Article 15.++- ‘The Work’: the Original Work or its Derivative Works.++- ‘The Source Code’: the human-readable form of the Work which is the most+  convenient for people to study and modify.++- ‘The Executable Code’: any code which has generally been compiled and which is+  meant to be interpreted by a computer as a program.++- ‘The Licensor’: the natural or legal person that distributes or communicates+  the Work under the Licence.++- ‘Contributor(s)’: any natural or legal person who modifies the Work under the+  Licence, or otherwise contributes to the creation of a Derivative Work.++- ‘The Licensee’ or ‘You’: any natural or legal person who makes any usage of+  the Work under the terms of the Licence.++- ‘Distribution’ or ‘Communication’: any act of selling, giving, lending,+  renting, distributing, communicating, transmitting, or otherwise making+  available, online or offline, copies of the Work or providing access to its+  essential functionalities at the disposal of any other natural or legal+  person.++2. Scope of the rights granted by the Licence++The Licensor hereby grants You a worldwide, royalty-free, non-exclusive,+sublicensable licence to do the following, for the duration of copyright vested+in the Original Work:++- use the Work in any circumstance and for all usage,+- reproduce the Work,+- modify the Work, and make Derivative Works based upon the Work,+- communicate to the public, including the right to make available or display+  the Work or copies thereof to the public and perform publicly, as the case may+  be, the Work,+- distribute the Work or copies thereof,+- lend and rent the Work or copies thereof,+- sublicense rights in the Work or copies thereof.++Those rights can be exercised on any media, supports and formats, whether now+known or later invented, as far as the applicable law permits so.++In the countries where moral rights apply, the Licensor waives his right to+exercise his moral right to the extent allowed by law in order to make effective+the licence of the economic rights here above listed.++The Licensor grants to the Licensee royalty-free, non-exclusive usage rights to+any patents held by the Licensor, to the extent necessary to make use of the+rights granted on the Work under this Licence.++3. Communication of the Source Code++The Licensor may provide the Work either in its Source Code form, or as+Executable Code. If the Work is provided as Executable Code, the Licensor+provides in addition a machine-readable copy of the Source Code of the Work+along with each copy of the Work that the Licensor distributes or indicates, in+a notice following the copyright notice attached to the Work, a repository where+the Source Code is easily and freely accessible for as long as the Licensor+continues to distribute or communicate the Work.++4. Limitations on copyright++Nothing in this Licence is intended to deprive the Licensee of the benefits from+any exception or limitation to the exclusive rights of the rights owners in the+Work, of the exhaustion of those rights or of other applicable limitations+thereto.++5. Obligations of the Licensee++The grant of the rights mentioned above is subject to some restrictions and+obligations imposed on the Licensee. Those obligations are the following:++Attribution right: The Licensee shall keep intact all copyright, patent or+trademarks notices and all notices that refer to the Licence and to the+disclaimer of warranties. The Licensee must include a copy of such notices and a+copy of the Licence with every copy of the Work he/she distributes or+communicates. The Licensee must cause any Derivative Work to carry prominent+notices stating that the Work has been modified and the date of modification.++Copyleft clause: If the Licensee distributes or communicates copies of the+Original Works or Derivative Works, this Distribution or Communication will be+done under the terms of this Licence or of a later version of this Licence+unless the Original Work is expressly distributed only under this version of the+Licence — for example by communicating ‘EUPL v. 1.2 only’. The Licensee+(becoming Licensor) cannot offer or impose any additional terms or conditions on+the Work or Derivative Work that alter or restrict the terms of the Licence.++Compatibility clause: If the Licensee Distributes or Communicates Derivative+Works or copies thereof based upon both the Work and another work licensed under+a Compatible Licence, this Distribution or Communication can be done under the+terms of this Compatible Licence. For the sake of this clause, ‘Compatible+Licence’ refers to the licences listed in the appendix attached to this Licence.+Should the Licensee's obligations under the Compatible Licence conflict with+his/her obligations under this Licence, the obligations of the Compatible+Licence shall prevail.++Provision of Source Code: When distributing or communicating copies of the Work,+the Licensee will provide a machine-readable copy of the Source Code or indicate+a repository where this Source will be easily and freely available for as long+as the Licensee continues to distribute or communicate the Work.++Legal Protection: This Licence does not grant permission to use the trade names,+trademarks, service marks, or names of the Licensor, except as required for+reasonable and customary use in describing the origin of the Work and+reproducing the content of the copyright notice.++6. Chain of Authorship++The original Licensor warrants that the copyright in the Original Work granted+hereunder is owned by him/her or licensed to him/her and that he/she has the+power and authority to grant the Licence.++Each Contributor warrants that the copyright in the modifications he/she brings+to the Work are owned by him/her or licensed to him/her and that he/she has the+power and authority to grant the Licence.++Each time You accept the Licence, the original Licensor and subsequent+Contributors grant You a licence to their contributions to the Work, under the+terms of this Licence.++7. Disclaimer of Warranty++The Work is a work in progress, which is continuously improved by numerous+Contributors. It is not a finished work and may therefore contain defects or+‘bugs’ inherent to this type of development.++For the above reason, the Work is provided under the Licence on an ‘as is’ basis+and without warranties of any kind concerning the Work, including without+limitation merchantability, fitness for a particular purpose, absence of defects+or errors, accuracy, non-infringement of intellectual property rights other than+copyright as stated in Article 6 of this Licence.++This disclaimer of warranty is an essential part of the Licence and a condition+for the grant of any rights to the Work.++8. Disclaimer of Liability++Except in the cases of wilful misconduct or damages directly caused to natural+persons, the Licensor will in no event be liable for any direct or indirect,+material or moral, damages of any kind, arising out of the Licence or of the use+of the Work, including without limitation, damages for loss of goodwill, work+stoppage, computer failure or malfunction, loss of data or any commercial+damage, even if the Licensor has been advised of the possibility of such damage.+However, the Licensor will be liable under statutory product liability laws as+far such laws apply to the Work.++9. Additional agreements++While distributing the Work, You may choose to conclude an additional agreement,+defining obligations or services consistent with this Licence. However, if+accepting obligations, You may act only on your own behalf and on your sole+responsibility, not on behalf of the original Licensor or any other Contributor,+and only if You agree to indemnify, defend, and hold each Contributor harmless+for any liability incurred by, or claims asserted against such Contributor by+the fact You have accepted any warranty or additional liability.++10. Acceptance of the Licence++The provisions of this Licence can be accepted by clicking on an icon ‘I agree’+placed under the bottom of a window displaying the text of this Licence or by+affirming consent in any other similar way, in accordance with the rules of+applicable law. Clicking on that icon indicates your clear and irrevocable+acceptance of this Licence and all of its terms and conditions.++Similarly, you irrevocably accept this Licence and all of its terms and+conditions by exercising any rights granted to You by Article 2 of this Licence,+such as the use of the Work, the creation by You of a Derivative Work or the+Distribution or Communication by You of the Work or copies thereof.++11. Information to the public++In case of any Distribution or Communication of the Work by means of electronic+communication by You (for example, by offering to download the Work from a+remote location) the distribution channel or media (for example, a website) must+at least provide to the public the information requested by the applicable law+regarding the Licensor, the Licence and the way it may be accessible, concluded,+stored and reproduced by the Licensee.++12. Termination of the Licence++The Licence and the rights granted hereunder will terminate automatically upon+any breach by the Licensee of the terms of the Licence.++Such a termination will not terminate the licences of any person who has+received the Work from the Licensee under the Licence, provided such persons+remain in full compliance with the Licence.++13. Miscellaneous++Without prejudice of Article 9 above, the Licence represents the complete+agreement between the Parties as to the Work.++If any provision of the Licence is invalid or unenforceable under applicable+law, this will not affect the validity or enforceability of the Licence as a+whole. Such provision will be construed or reformed so as necessary to make it+valid and enforceable.++The European Commission may publish other linguistic versions or new versions of+this Licence or updated versions of the Appendix, so far this is required and+reasonable, without reducing the scope of the rights granted by the Licence. New+versions of the Licence will be published with a unique version number.++All linguistic versions of this Licence, approved by the European Commission,+have identical value. Parties can take advantage of the linguistic version of+their choice.++14. Jurisdiction++Without prejudice to specific agreement between parties,++- any litigation resulting from the interpretation of this License, arising+  between the European Union institutions, bodies, offices or agencies, as a+  Licensor, and any Licensee, will be subject to the jurisdiction of the Court+  of Justice of the European Union, as laid down in article 272 of the Treaty on+  the Functioning of the European Union,++- any litigation arising between other parties and resulting from the+  interpretation of this License, will be subject to the exclusive jurisdiction+  of the competent court where the Licensor resides or conducts its primary+  business.++15. Applicable Law++Without prejudice to specific agreement between parties,++- this Licence shall be governed by the law of the European Union Member State+  where the Licensor has his seat, resides or has his registered office,++- this licence shall be governed by Belgian law if the Licensor has no seat,+  residence or registered office inside a European Union Member State.++Appendix++‘Compatible Licences’ according to Article 5 EUPL are:++- GNU General Public License (GPL) v. 2, v. 3+- GNU Affero General Public License (AGPL) v. 3+- Open Software License (OSL) v. 2.1, v. 3.0+- Eclipse Public License (EPL) v. 1.0+- CeCILL v. 2.0, v. 2.1+- Mozilla Public Licence (MPL) v. 2+- GNU Lesser General Public Licence (LGPL) v. 2.1, v. 3+- Creative Commons Attribution-ShareAlike v. 3.0 Unported (CC BY-SA 3.0) for+  works other than software+- European Union Public Licence (EUPL) v. 1.1, v. 1.2+- Québec Free and Open-Source Licence — Reciprocity (LiLiQ-R) or Strong+  Reciprocity (LiLiQ-R+).++The European Commission may update this Appendix to later versions of the above+licences without producing a new version of the EUPL, as long as they provide+the rights granted in Article 2 of this Licence and protect the covered Source+Code from exclusive appropriation.++All other changes or additions to this Appendix require the production of a new+EUPL version.++================================================================================+2. Apache License, Version 2.0 (Apache-2.0)+================================================================================++Apache License+Version 2.0, January 2004+http://www.apache.org/licenses/++TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION++1. Definitions.++"License" shall mean the terms and conditions for use, reproduction, and distribution as defined by Sections 1 through 9 of this document.++"Licensor" shall mean the copyright owner or entity authorized by the copyright owner that is granting the License.++"Legal Entity" shall mean the union of the acting entity and all other entities that control, are controlled by, or are under common control with that entity. For the purposes of this definition, "control" means (i) the power, direct or indirect, to cause the direction or management of such entity, whether by contract or otherwise, or (ii) ownership of fifty percent (50%) or more of the outstanding shares, or (iii) beneficial ownership of such entity.++"You" (or "Your") shall mean an individual or Legal Entity exercising permissions granted by this License.++"Source" form shall mean the preferred form for making modifications, including but not limited to software source code, documentation source, and configuration files.++"Object" form shall mean any form resulting from mechanical transformation or translation of a Source form, including but not limited to compiled object code, generated documentation, and conversions to other media types.++"Work" shall mean the work of authorship, whether in Source or Object form, made available under the License, as indicated by a copyright notice that is included in or attached to the work (an example is provided in the Appendix below).++"Derivative Works" shall mean any work, whether in Source or Object form, that is based on (or derived from) the Work and for which the editorial revisions, annotations, elaborations, or other modifications represent, as a whole, an original work of authorship. For the purposes of this License, Derivative Works shall not include works that remain separable from, or merely link (or bind by name) to the interfaces of, the Work and Derivative Works thereof.++"Contribution" shall mean any work of authorship, including the original version of the Work and any modifications or additions to that Work or Derivative Works thereof, that is intentionally submitted to Licensor for inclusion in the Work by the copyright owner or by an individual or Legal Entity authorized to submit on behalf of the copyright owner. For the purposes of this definition, "submitted" means any form of electronic, verbal, or written communication sent to the Licensor or its representatives, including but not limited to communication on electronic mailing lists, source code control systems, and issue tracking systems that are managed by, or on behalf of, the Licensor for the purpose of discussing and improving the Work, but excluding communication that is conspicuously marked or otherwise designated in writing by the copyright owner as "Not a Contribution."++"Contributor" shall mean Licensor and any individual or Legal Entity on behalf of whom a Contribution has been received by Licensor and subsequently incorporated within the Work.++2. Grant of Copyright License. Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable copyright license to reproduce, prepare Derivative Works of, publicly display, publicly perform, sublicense, and distribute the Work and such Derivative Works in Source or Object form.++3. Grant of Patent License. Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable (except as stated in this section) patent license to make, have made, use, offer to sell, sell, import, and otherwise transfer the Work, where such license applies only to those patent claims licensable by such Contributor that are necessarily infringed by their Contribution(s) alone or by combination of their Contribution(s) with the Work to which such Contribution(s) was submitted. If You institute patent litigation against any entity (including a cross-claim or counterclaim in a lawsuit) alleging that the Work or a Contribution incorporated within the Work constitutes direct or contributory patent infringement, then any patent licenses granted to You under this License for that Work shall terminate as of the date such litigation is filed.++4. Redistribution. You may reproduce and distribute copies of the Work or Derivative Works thereof in any medium, with or without modifications, and in Source or Object form, provided that You meet the following conditions:++     (a) You must give any other recipients of the Work or Derivative Works a copy of this License; and++     (b) You must cause any modified files to carry prominent notices stating that You changed the files; and++     (c) You must retain, in the Source form of any Derivative Works that You distribute, all copyright, patent, trademark, and attribution notices from the Source form of the Work, excluding those notices that do not pertain to any part of the Derivative Works; and++     (d) If the Work includes a "NOTICE" text file as part of its distribution, then any Derivative Works that You distribute must include a readable copy of the attribution notices contained within such NOTICE file, excluding those notices that do not pertain to any part of the Derivative Works, in at least one of the following places: within a NOTICE text file distributed as part of the Derivative Works; within the Source form or documentation, if provided along with the Derivative Works; or, within a display generated by the Derivative Works, if and wherever such third-party notices normally appear. The contents of the NOTICE file are for informational purposes only and do not modify the License. You may add Your own attribution notices within Derivative Works that You distribute, alongside or as an addendum to the NOTICE text from the Work, provided that such additional attribution notices cannot be construed as modifying the License.++     You may add Your own copyright statement to Your modifications and may provide additional or different license terms and conditions for use, reproduction, or distribution of Your modifications, or for any such Derivative Works as a whole, provided Your use, reproduction, and distribution of the Work otherwise complies with the conditions stated in this License.++5. Submission of Contributions. Unless You explicitly state otherwise, any Contribution intentionally submitted for inclusion in the Work by You to the Licensor shall be under the terms and conditions of this License, without any additional terms or conditions. Notwithstanding the above, nothing herein shall supersede or modify the terms of any separate license agreement you may have executed with Licensor regarding such Contributions.++6. Trademarks. This License does not grant permission to use the trade names, trademarks, service marks, or product names of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and reproducing the content of the NOTICE file.++7. Disclaimer of Warranty. Unless required by applicable law or agreed to in writing, Licensor provides the Work (and each Contributor provides its Contributions) on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied, including, without limitation, any warranties or conditions of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A PARTICULAR PURPOSE. You are solely responsible for determining the appropriateness of using or redistributing the Work and assume any risks associated with Your exercise of permissions under this License.++8. Limitation of Liability. In no event and under no legal theory, whether in tort (including negligence), contract, or otherwise, unless required by applicable law (such as deliberate and grossly negligent acts) or agreed to in writing, shall any Contributor be liable to You for damages, including any direct, indirect, special, incidental, or consequential damages of any character arising as a result of this License or out of the use or inability to use the Work (including but not limited to damages for loss of goodwill, work stoppage, computer failure or malfunction, or any and all other commercial damages or losses), even if such Contributor has been advised of the possibility of such damages.++9. Accepting Warranty or Additional Liability. While redistributing the Work or Derivative Works thereof, You may choose to offer, and charge a fee for, acceptance of support, warranty, indemnity, or other liability obligations and/or rights consistent with this License. However, in accepting such obligations, You may act only on Your own behalf and on Your sole responsibility, not on behalf of any other Contributor, and only if You agree to indemnify, defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against, such Contributor by reason of your accepting any such warranty or additional liability.++END OF TERMS AND CONDITIONS++APPENDIX: How to apply the Apache License to your work.++To apply the Apache License to your work, attach the following boilerplate notice, with the fields enclosed by brackets "[]" replaced with your own identifying information. (Don't include the brackets!)  The text should be enclosed in the appropriate comment syntax for the file format. We also recommend that a file or class name and description of purpose be included on the same "printed page" as the copyright notice for easier identification within third-party archives.++Copyright [yyyy] [name of copyright owner]++Licensed under the Apache License, Version 2.0 (the "License");+you may not use this file except in compliance with the License.+You may obtain a copy of the License at++http://www.apache.org/licenses/LICENSE-2.0++Unless required by applicable law or agreed to in writing, software+distributed under the License is distributed on an "AS IS" BASIS,+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+See the License for the specific language governing permissions and+limitations under the License.

@@ -0,0 +1,63 @@+# polytropos-plugin++GHC typechecker plugin synthesizing literal dictionaries and $O(1)$ jump tables directly into Core AST for [polytropos](https://github.com/NadiaYvette/polytropos).++## Overview++In traditional Haskell row libraries, solving field offsets or dictionary instances involves either:+1. Recursive type-level search ($O(N)$ or $O(N^2)$ compile-time scaling).+2. Runtime dictionary passing and pointer chasing.++`polytropos-plugin` solves evidence constraints (`FieldIndex`, `ConstructorIndex`, `RowEq`, `RowShow`, `RowEqSum`, `RowShowSum`, `AllFields`) by inspecting the row at compile time and emitting literal slot indices, tags, and dictionary vectors directly into GHC Core AST.++## Usage++Enable the plugin in your `.cabal` file or module:++```cabal+build-depends:+    polytropos-core >= 0.1 && < 0.2+  , polytropos-plugin >= 0.1 && < 0.2++ghc-options: -fplugin=Polytropos.Plugin+```++## Quick Example++```haskell+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE OverloadedRecordDot #-}+{-# OPTIONS_GHC -fplugin=Polytropos.Plugin #-}++import Polytropos++type User = Record '[ "name" := String, "score" := Int ]++main :: IO ()+main = do+  -- The plugin lowers REC into flat array construction:+  let user = REC { name = "Alice", score = 100 }+  putStrLn ("User: " ++ user.name)++  -- The plugin solves REC_UPD into O(1) setField without parentheses:+  let updated = REC_UPD user { score = 150 }+  print updated.score+```++## Features++- **Literal Offset Resolution**: Solves `FieldIndex @"foo" r` directly to integer slot literals.+- **Literal Tag Resolution**: Solves `ConstructorIndex @"Bar" s` directly to integer constructor tags.+- **Unrolled Core Synthesis**: Direct code generation for record equality (`RowEq`) and formatting (`RowShow`).+- **Human-Centric Error Diagnostics**: Custom `TypeError` reporting with Levenshtein-distance fuzzy field name suggestions when fields or constructors are missing.+- **Cross-GHC Support**: Supports GHC 9.6 through GHC 9.14 via internal compatibility shims.++## Documentation & Repository++- **Main Repository**: [https://github.com/NadiaYvette/polytropos](https://github.com/NadiaYvette/polytropos)+- **Plugin Architecture**: [PLUGIN_INVARIANTS.md](https://github.com/NadiaYvette/polytropos/blob/master/.agents/rules/plugin-invariants.md)++## License++Dual-licensed under `EUPL-1.2 OR Apache-2.0`.

@@ -0,0 +1,75 @@+cabal-version:      3.0+name:               polytropos-plugin+version: 0.1.0.2+synopsis:           TcPlugin that emits literal evidence for Polytropos row classes+description:+  A GHC typechecker plugin for <https://hackage.haskell.org/package/polytropos polytropos>+  that solves the evidence-class constraints ('Polytropos.Core.FieldIndex',+  'Polytropos.Core.ConstructorIndex', 'Polytropos.Core.RowEq', 'Polytropos.Core.RowShow',+  'Polytropos.Core.RowEqSum', 'Polytropos.Core.RowShowSum', 'Polytropos.Core.AllFields')+  by inspecting the row carried in a 'Polytropos.Core.RowRep''s type and emitting literal+  slot indices, tags, and dictionary vectors directly into GHC Core AST — eliminating+  inductive type-level search and pointer-chasing runtime overhead entirely.++  Uses the <https://hackage.haskell.org/package/ghc-tcplugin-api ghc-tcplugin-api> library+  for a streamlined interface to GHC's typechecker plugin API across compiler versions.++  Start at the front door module "Polytropos.Plugin" for complete usage+  instructions and worked examples. Enable in consuming packages via:+  @ghc-options: -fplugin=Polytropos.Plugin@.+license:            EUPL-1.2 OR Apache-2.0+license-file:       LICENSE+author:             Nadia Yvette Chambers+maintainer:         nadia.yvette.chambers@ik.me+category:           Compiler Plugin+homepage:           https://github.com/NadiaYvette/polytropos+bug-reports:        https://github.com/NadiaYvette/polytropos/issues+extra-doc-files:    README.md+                  , CHANGELOG.md++source-repository head+  type:     git+  location: https://github.com/NadiaYvette/polytropos+  subdir:   packages/polytropos-plugin++common warnings+  ghc-options:+      -Wall+      -Wcompat+      -Widentities+      -Wincomplete-record-updates+      -Wincomplete-uni-patterns+      -Wredundant-constraints+      -Wunused-packages++library+  import:           warnings+  exposed-modules:  Polytropos.Plugin+                  , Polytropos.Plugin.Source+  other-modules:    Polytropos.Plugin.Compat+  hs-source-dirs:   src+  default-language: GHC2021+  build-depends:+      base       >= 4.18 && < 4.23+    , ghc         >= 9.6  && < 9.15+    , ghc-tcplugin-api >= 0.1 && < 0.21++test-suite polytropos-plugin-smoke+  import:           warnings+  type:             exitcode-stdio-1.0+  hs-source-dirs:   tests/smoke+  main-is:          Main.hs+  default-language: GHC2021+  build-depends:+      base       >= 4.18 && < 4.23+    , polytropos-core+    , primitive+    , tasty         >= 1.4  && < 1.6+    , tasty-hunit   >= 0.10 && < 0.11+    , polytropos-plugin+    , process+    , filepath+    , directory++  ghc-options:+      -fplugin=Polytropos.Plugin

@@ -0,0 +1,2295 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-}++{-|+Module      : Polytropos.Plugin+Description : GHC typechecker plugin synthesizing literal row evidence for Polytropos+Copyright   : (c) 2026 The Polytropos Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC Typechecker Plugin API)++GHC typechecker plugin for @polytropos@.++This plugin is the operational heart of the @polytropos@ compile-time engine.+It inspects the row types carried in @RowRep@ and synthesizes literal evidence+dictionaries directly into GHC Core during typechecking.++= Architectural Overview & Rationale++== Zero Type-Level Search at Runtime++In conventional type-level row libraries, projecting a field from a record+requires an inductive type-level search (e.g. via @KnownNat@ or recursive class instances)+that produces \(O(N)\) or \(O(N^2)\) Core dictionary trees and compiles to pointer-chasing+loops.++@polytropos-plugin@ eliminates this entire cost:+1. It intercepts wanted constraints for the evidence classes:+   * @FieldIndex@: computes the zero-based literal slot index for a field symbol+   * @ConstructorIndex@: computes the zero-based constructor tag for a variant symbol+   * @RowEq@ and @RowEqSum@: synthesizes unrolled structural equality checks+   * @RowShow@ and @RowShowSum@: synthesizes string formatting routines+   * @AllFields@: synthesizes literal vectors of dictionary witnesses ('Data.Primitive.SmallArray.SmallArray')+2. It solves these constraints immediately by emitting literal Core expressions with+   exact numeric literals (e.g. @0#@, @1#@, @2#@).+3. The resulting code compiles to direct array indexing into contiguous memory with+   zero intermediate allocations.++= How to Use This Plugin++In your consuming project's @.cabal@ file, add @polytropos-plugin@ to @build-depends@+and enable the plugin via @ghc-options@:++@+library+  build-depends:+      base >= 4.18+    , polytropos-core+    , polytropos-plugin+  ghc-options:+    -fplugin=Polytropos.Plugin+@++= Worked Example++Once the plugin is enabled in your @.cabal@ file, field projections and constructor+injections work seamlessly without manual instance declarations:++> {-# LANGUAGE DataKinds #-}+> {-# LANGUAGE OverloadedRecordDot #-}+>+> import Polytropos+>+> -- The plugin computes literal index 0 for "name" and 1 for "age"+> type User = Record '["name" ':= String, "age" ':= Int]+>+> -- Idiomatic record construction via REC syntax:+> mkUser :: String -> Int -> User+> mkUser n a = REC { name = n, age = a }+>+> -- Reading fields is compiled to direct O(1) array index lookup:+> userName :: User -> String+> userName u = u.name+>+> -- Functional record updates desugar to setField:+> updateUser :: User -> User+> updateUser u = REC_UPD u { age = 31 }+-}+module Polytropos.Plugin+  ( -- * GHC Plugin Entry Point+    plugin+  ) where++import Prelude++import Data.Either+  ( partitionEithers+  )++import Data.List+  ( intercalate+  , sortOn+#if !MIN_VERSION_base(4,20,0)+  , foldl'+#endif+  )++import Data.Bits+  ( xor+  )++import Data.Char+  ( ord+  )++import Data.Word+  ( Word64+  )++import Control.Monad+  ( forM+  , zipWithM+  )++import GHC.Core.DataCon+  ( promoteDataCon+  )++import GHC.Core.Make+  ( mkCoreApps+  , mkCoreConApps+  , mkCoreLams+  , mkCharExpr+  , mkStringExpr+  , mkIfThenElse+  , mkListExpr+  )++import GHC.Plugins+  ( Plugin (..)+  , defaultPlugin+  , tcPlugin+  , CoreExpr+  , Expr(..)+  , Type+  , mkTcOcc+  , nameOccName+  , mkTyConTy+  , mkTyConApp+  , splitTyConApp_maybe+  , isStrLitTy+  , mkStrLitTy+  , intDataCon+  , wordDataCon+  , FastString+  , unpackFS+  , Literal(..)+  , LitNumType(..)+  , wordTyCon+  , Var(..)+  , varType+  , intTy+  , stringTy+  , mkVarOcc+  , Module+  , mkModuleName+  , coreView+  , splitFunTy+  , splitFunTys+  , splitForAllTyCoVars+  , piResultTys+  , typeKind+  , mkTyVarTy+  , mkAppTy+  , getOccName+  , occNameString+  , fsLit+  , nullFS+  , nilFS+  , TyCon+  , showSDocUnsafe+  , ppr+  , isEmptyVarSet+  , tyCoVarsOfType+  )++import GHC.Core.Class+  ( classMethods+  , classTyCon+  )++import GHC.Core.Multiplicity+  ( scaledThing+  , scaledMult+  )++import GHC.Core.TyCo.Compare+  ( eqType+  )++import GHC.Builtin.Types+  ( trueDataCon+  , falseDataCon+  , maybeTyCon+  , nothingDataCon+  , justDataCon+  , unitTyCon+  , unitDataCon+  , constraintKind+  , typeSymbolKind+  , liftedTypeKind+  , mkPromotedPairTy+  , mkPromotedListTy+  , mkTupleTy+  )++import Language.Haskell.Syntax.Basic+  ( Boxity(..)+  )++import GHC.Builtin.Names+  ( gHC_CLASSES+  , eqClassName+  , showClassName+  , errorMessageTypeErrorFamName+  , typeErrorTextDataConName+  , typeErrorVAppendDataConName+  )++import Polytropos.Plugin.Compat+  ( modBase+  , modShow+  , modRecords+  )++import GHC.TcPlugin.API+  ( TcPlugin (..)+  , TcPluginSolveResult(..)+  , TcPluginM+  , classifyPredType+  , Pred(..)+  , ctPred+  , ctEvidence+  , isWanted+  , className+  , EvTerm (..)+  , Ct+  , CtLoc+  , TcPluginStage(..)+  , mkTcPlugin+  , listToUFM+  , UniqFM+  , lookupOrig+  , tcLookupId+  , tcLookupTyCon+  , tcLookupDataCon+  , findImportedModule+  , resolveImport+  , FindResult(..)+  , Class+  , classDataCon+  , tcLookupClass+  , evDataConApp+  , newName+  , mkLocalId+  , newWanted+  , ctEvExpr+  , mkNonCanonical+  , ctLoc+  , Role(..)+  , mkEqPredRole+  , splitAppTy_maybe+  , TcPluginRewriteResult(..)+  , mkTyFamAppReduction+  )++import GHC.TcPlugin.API.Internal+  ( unsafeLiftTcM+  , TcPluginRewriter+  )++import Polytropos.Plugin.Source+  ( sourcePlugin+  )++{-+================================================================================+                                GHC NOTES ARCHITECTURE+================================================================================++This module follows GHC's commentary convention:+  https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/coding-style#2-using-notes++Complex design decisions, theoretical invariants, and row algebra concepts are+explained in self-contained Notes below. Specific solver and rewrite sites in the+code carry cross-references (e.g. "-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]").++Notes defined in this module:+  * Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+  * Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+  * Note [SubRow and SubSum Projection and Narrowing Evidence] [ref:note-subrow-subsum]+  * Note [Type-Level Metadata Rewriting and Defunctionalization] [ref:note-metadata-rewriting]+  * Note [Human-Centric TypeError Diagnostics & Fuzzy Matching] [ref:note-typeerror-diagnostics]+  * Note [OCaml Subtype/Unify Correlation and Row Tail Algebra] [ref:note-ocaml-row-algebra]+  * Note [Solving Pipeline: Wanteds, Givens, and Staged Evidence Synthesis] [ref:note-solving-pipeline]+  * Note [SubRow and SubSum Interior Mechanics: Matchers and Witness Generation] [ref:note-subrow-subsum-mechanics]+  * Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]++External Canonical Design References:+  * docs/notes/POLYTROPOS_DESIGN.md (decisions D1–D10, open questions)+  * docs/notes/OCAML_ROW_TAIL_SUBTYPE_MECHANISM.md (Rémy row calculus & OCaml tails)+  * docs/notes/ROW_ROLE_DEFNS_DRAFT.ott & REVIEWER_WFU_ARGUMENT.md+  * plans/2026-10-09-plugin-gap-roadmap.md & 2026-10-09-plugin-gap-spec.md+================================================================================+-}++{- Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [tag:note-row-anatomy]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+In Didier Rémy's row calculus (and in OCaml's polymorphic variants / object types),+a row type is not merely a static list of fields; it is a structural sequence with+a tail:++    Row ::= '[]                       -- Closed empty row (Tnil in OCaml)+          | (label ':= ty) ': tail    -- Cons cell (Tfield in OCaml)+          | rho                       -- Row variable (Tvar in OCaml)++In Haskell's type system (via DataKinds and TypeOperators), we encode rows as+promoted type-level lists of pairs: `'[ "x" ':= Int, "y" ':= Bool]`.++1. Open vs. Closed Rows:+   - A *closed row* is one that syntactically terminates with `'[]`. Its complete+     field complement and exact arity N are known statically.+   - An *open row* is one whose tail is an uninstantiated type variable `rho`+     (e.g., `( "x" ':= Int ) ': rho`). The row is open because further type+     inference may discover additional fields that unify with `rho`.++2. Fixed vs. Unfixed Tails:+   Following OCaml's subtype/unification algebra (see docs/notes/OCAML_ROW_TAIL_SUBTYPE_MECHANISM.md):+   - An *unfixed tail* is a flexible unification variable (a meta-tyvar) that has+     not yet been pinned down. It can accept fresh fields through unification.+   - A *fixed tail* is a tail that cannot accept further fields without contradiction:+     either it is closed (`'[]`), or it is a universally quantified skolem tyvar,+     or it is an abstract/existential row constructor (`Tconstr`).++3. Solver Implications in Polytropos.Plugin:+   When `Polytropos.Plugin` solves evidence classes:+   - Single-field queries (`FieldIndex "x" r a`, `HasField "x" r a`): If `"x"` occurs+     in the known prefix of an open row, its slot offset from the head is fixed,+     so we can solve immediately. However, if `"x"` is NOT in the prefix and the tail+     is unfixed, we MUST NOT emit a missing-field error! We must defer (leave the wanted+     constraint unsolved), because `"x"` might appear when the unfixed tail is later+     instantiated.+   - Whole-row queries (`RowEq`, `RowShow`, `AllFields`, `SubRow`): These operations+     iterate over or project across the ENTIRE row payload. They fundamentally require+     the row tail to be fixed and closed (`walkRowWithTypes_maybe` returning `Just fields`).+     If the tail is unfixed (`walkRowWithTypes_maybe` returning `Nothing`), the solver+     defers, waiting for GHC's typechecker to complete row inference.+-}++{- Note [Literal Evidence Synthesis vs Type-Level Search] [tag:note-literal-evidence]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Traditional extensible record and variant libraries in Haskell (such as `vinyl`,+`sop-core`, or naive type-level lists) implement evidence resolution through+recursive type-class instances. For a row of N fields:+  * The class dictionary is a recursive chain of pairs: DictCons d1 (DictCons d2 ...)+  * Looking up a field at index k traverses k dictionary steps at runtime (O(N) access).+  * GHC's simplifier must unroll and optimize N nested dictionary applications,+    leading to O(N^2) Core size and severe compilation slowdowns on records with+    30+ fields (see benchmark/variants/README.md).++Polytropos solves this by collapsing products and sums into a single generic runtime+representation:+    data Rep = Rep {-# UNPACK #-} !Word {-# UNPACK #-} !(SmallArray Any)++`Polytropos.Plugin` is a GHC typechecker plugin that intercepts evidence constraints:+  - `FieldIndex label row a`: Computes the 0-based integer slot offset `i`.+  - `ConstructorIndex con row`: Computes the 0-based constructor tag `t` (Word).+  - `RowEq` / `RowShow` / `RowEqSum` / `RowShowSum`: Directly synthesizes unrolled+    Core expressions comparing or showing each slot in sequence, using literal `Int`+    and `Word` constants (see `mkIntExpr` and `mkWordExpr`).+  - `SubRow sub super`: Emits an array of literal integer slot indices mapping+    sub-record slots directly to super-record slots in O(1) jump steps.+  - `KnownHash label`: Emits the compile-time 64-bit FNV-1a hash of the label as+    a literal `Word`.++Zero recursive dictionaries exist in Core. Compiling a 100-field record scales in+strictly O(N) linear time, identical to hand-written nominal Haskell data types.+-}++{- Note [SubRow and SubSum Projection and Narrowing Evidence] [tag:note-subrow-subsum]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Polytropos provides width subtyping for records and coproduct subsumption for variants:+  * `SubRow sub super`: Evidence that every field `(n ':= a)` in `sub` is present in+    `super` with the exact same type `a`.+  * `SubSum sub super`: Evidence that every constructor `(c ':= fs)` in `sub` is+    present in `super` with identical field payload types `fs`.++1. SubRow Index Mapping:+   In `solveSubRow`, for each field in `sub`, the plugin locates its 0-based slot index+   in `super`. It synthesizes an array of literal indices:+       projectionIndices = [idx_super_0, idx_super_1, ..., idx_super_{K-1}]+   At runtime, `projectRecord` uses this index array to copy slots directly from+   the super-record into the sub-record payload using block copy operations.++2. SubSum Injection & Narrowing:+   In `solveSubSum`, the plugin synthesizes two arrays:+   - `injectIndices`: Maps each constructor tag in `sub` to its corresponding tag in `super`.+     Used by `widenVariant` to upcast a variant in O(1).+   - `narrowIndices`: An array indexed by `super` constructor tags, containing `Just subTag`+     if the constructor belongs to `sub`, or `Nothing` if absent.+     Used by `narrowVariant` to downcast a variant in O(1) tag lookup.++Both operations require closed rows (see Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]).+If either row has an unfixed tail, solving is deferred.+-}++{- Note [Type-Level Metadata Rewriting and Defunctionalization] [tag:note-metadata-rewriting]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+GHC provides type families for row reflection:+  * `FieldNames r`: Computes `[Symbol]` of field names in row order.+  * `SimpleFieldTypes r`: Computes `[Type]` of field values.+  * `FieldTypes r f`: Computes `[Type]` under higher-kinded functor `f`.++Normally, closed type families are evaluated via recursive axioms in GHC's constraint+solver, taking O(N) rewrite steps and cluttering solver traces.++`polytroposRewrite` intercepts type family applications during GHC's rewriting phase+(`TcPluginRewrite`). It inspects the row type directly, verifies that the row tail is+closed, constructs the reified promoted list `[Symbol]` or `[Type]`, and returns an+exact `Refl` coercion (`mkPluginCoercion`). This reduces row metadata queries to+O(1) rewrite steps without generating intermediate type family equations.+-}++{- Note [Human-Centric TypeError Diagnostics & Fuzzy Matching] [tag:note-typeerror-diagnostics]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+When a developer writes `rec.nmae` instead of `rec.name`, standard GHC type inference+either leaves an unexplained stuck constraint `HasField "nmae" (Record r) a` or emits+a confusing type mismatch error.++In `solveHasField` and `solveFieldIndex`:+1. When a field `n` is absent from a closed row `r`:+   - We extract all available field names in `r`.+   - We calculate Levenshtein edit distances between `n` and every field name in `r`.+   - If candidates with edit distance <= 2 exist, we format a fuzzy suggestion:+       "Did you mean: ‘name’?"+   - We construct a multi-line formatted schema showing available fields:+       "Available record fields:+          • id :: Int+          • name :: String+          • email :: String"+2. We synthesize a structured GHC `TypeError` constraint (`mkTypeErrorCt`), which GHC+   displays prominently to the user.+3. Crucially, we also emit a dummy dictionary (`mkDummyHasFieldDict`) solving the wanted+   constraint! This prevents cascading secondary errors (e.g. "could not deduce HasField",+   "ambiguous type variable a"), ensuring the user only sees the clean, actionable+   typo diagnostic with fuzzy suggestion.+-}++{- Note [OCaml Subtype/Unify Correlation and Row Tail Algebra] [tag:note-ocaml-row-algebra]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+In OCaml's typechecker (`typecore.ml` and `btype.ml`):+- `subtype_row` filters fields and, upon encountering an unfixed tail (`Tvar`), does NOT+  blindly instantiate or unify it. It emits a deferred constraint, preserving principal+  typing until more context arrives.+- `unify_row` takes two rows and computes the merged fields and the surviving tail.++In Polytropos:+- `walkRowWithTypes_maybe` acts as our `row_repr`: it traverses the cons cells. If the+  tail reaches `Tnil` (`[]`), it succeeds with `Just fields`. If the tail is an+  unfixed type variable, it aborts to `Nothing`.+- Solvers for subtyping (`SubRow`, `SubSum`) behave like OCaml's `subtype_row`: they+  only solve when tails are fixed, and leave wanted constraints deferred when tails+  are unfixed.+-}++{- Note [Solving Pipeline: Wanteds, Givens, and Staged Evidence Synthesis] [tag:note-solving-pipeline]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+GHC's typechecker plugin architecture (via `ghc-tcplugin-api`) invokes `polytroposSolve`+during constraint simplification with two lists of constraints:+  * `givens`: constraints assumed to hold in the current lexical scope (e.g. from an+    enclosing type signature `(RowEq r) => ...`).+  * `wanteds`: constraints that GHC needs evidence for in order to typecheck the program.++The polytropos constraint solving pipeline operates in five deterministic stages:++1. Classification and Target Isolation (`solveOne`):+   - We inspect each constraint's predicate type via `classifyPredType (ctPred ct)`.+   - If the predicate is a class constraint `ClassPred cls tys`, we match the unqualified+     OccName of `className cls` against our known evidence classes:+     `FieldIndex`, `ConstructorIndex`, `RowEq`, `RowShow`, `RowEqSum`, `RowShowSum`,+     `HasField`, `AllFields`, `SubRow`, `SubSum`, and `KnownHash`.+   - Non-polytropos constraints are immediately bypassed (`Right ()`), returning control+     to GHC's default solver.++2. Given Bypassing:+   - Givens are assumptions, not proof obligations. While givens can inform type inference,+     evidence classes in polytropos are defined over closed structural rows where evidence+     is a direct, deterministic property of the type itself. We therefore filter for+     `isWanted (ctEvidence ct)` and avoid re-solving givens.++3. Staged Solving and Deferral (Open vs Closed Rows):+   - Each individual solver inspects the row arguments.+   - If a row is still open with an unfixed tail (see Note [Row Type Anatomy: Open vs Closed+     Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]), the solver CANNOT make a closed-world+     judgement. It returns `Right ()` (deferral), leaving the constraint in GHC's worklist.+     As subsequent unification steps instantiate type variables, GHC will re-invoke the+     plugin with more concrete rows.++4. Direct Evidence Construction:+   - When a row is closed, the solver evaluates the query and synthesizes Core AST+     evidence directly (see Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]).+   - For `FieldIndex`: emits literal Int offset `mkIntExpr idx`.+   - For `ConstructorIndex`: emits literal Word tag `mkWordExpr tag`.+   - For `RowEq`/`RowShow`/`RowEqSum`/`RowShowSum`: builds complete method lambdas in Core AST.+   - For `HasField`: synthesizes selector lambda `\r -> fieldAt idx (unRowRep r)`.+   - For `AllFields`: packs runtime dictionaries into a `SmallArray (DictAny c)` and emits+     new wanted constraints for each field type so GHC resolves underlying field instances.+   - For `SubRow`/`SubSum`: generates projection slot index lists and narrowing maps+     (see Note [SubRow and SubSum Interior Mechanics: Matchers and Witness Generation] [ref:note-subrow-subsum-mechanics]).+   - For `KnownHash`: computes literal 64-bit FNV-1a hash constant.++5. Result Assembly and Worklist Emission:+   - `polytroposSolve` partitions the results into:+     * `tcPluginSolvedCts`: constraints successfully discharged by our synthesized evidence terms.+     * `tcPluginNewCts`: newly spawned proof obligations (e.g. `TypeError` diagnostics or+       per-field wanted constraints for `AllFields`).+     * `tcPluginInsolubleCts`: explicitly failed constraints (kept empty; see Note [Diagnostic+       Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]).+-}++{- Note [SubRow and SubSum Interior Mechanics: Matchers and Witness Generation] [tag:note-subrow-subsum-mechanics]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+The `SubRow` and `SubSum` evidence classes form the structural subtyping backbone of polytropos.+Their solvers (`solveSubRow` and `solveSubSum`) transform high-level type inclusion checks into+efficient, zero-overhead runtime witness arrays:++1. `SubRow sub super` (Width Subtyping for Records):+   - Mathematical Intuition: `sub` is a sub-record of `super` if EVERY field `(name, fieldTy)`+     in `sub` also exists in `super` with an identical type.+   - Directionality: A smaller record schema can be projected *out of* a larger record schema:+     `projectRecord :: SubRow sub super => Record super -> Record sub`.+   - Interior Matching (`matchFields`):+     * Walks each field in `sub` in target order.+     * Searches `super` for a field with matching name (or matches anonymously if either name is null)+       and checks type equality with `eqType`.+     * Records the 0-based offset `j` of that field in `super`.+     * Produces `indices :: [Int]`, specifying which slots in `super` correspond to each slot in `sub`.+   - Evidence Emission:+     * Constructs Core AST: `DictSubRow [Int]`.+     * At runtime, `projectRecord` uses this list to slice the source `SmallArray` directly into+       the pre-sized destination `SmallArray` in a single pass without searching.++2. `SubSum sub super` (Widening and Narrowing for Variants):+   - Mathematical Intuition: `sub` is a sub-variant of `super` if EVERY constructor `(conName, payloadRow)`+     in `sub` also exists in `super` with an identical payload schema.+   - Directionality:+     * Widening (Injection): A smaller variant can be injected *into* a larger variant totally:+       `widenVariant :: SubSum sub super => Variant sub -> Variant super`.+     * Narrowing (Projection): A larger variant can be projected *down to* a smaller variant partially:+       `narrowVariant :: SubSum sub super => Variant super -> Maybe (Variant sub)`.+   - Interior Matching (`matchCons` and `narrowIndices`):+     * `matchCons`: Maps each constructor in `sub` to its 0-based tag `j` in `super`, producing+       `injectIndices :: [Word]`.+     * `narrowIndices`: Walks all constructors in `super`. For each `super` constructor, checks if it+       exists in `sub`. If yes, records `Just subTag`; if no, records `Nothing`.+     * Produces `narrowIndices :: [Maybe Word]`.+   - Nested Payload Equivalence (`sameRow`):+     * Verifies that the payload product rows of matching constructors are structurally identical:+       same number of fields, matching field names, and pairwise `eqType` equality.+   - Evidence Emission:+     * Constructs Core AST: `DictSubSum [Word] [Maybe Word]`.+     * At runtime:+       - `widenVariant` looks up the source tag in the `injectIndices` array to rewrite the tag in O(1).+       - `narrowVariant` looks up the source tag in the `narrowIndices` array: if `Just t'`, replaces+         the tag with `t'`; if `Nothing`, returns `Nothing` in O(1) without branch trees.+-}++{- Note [Diagnostic Recovery and Cascading Error Prevention] [tag:note-diagnostic-prevention]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+A notorious weakness of extensible record libraries in Haskell is diagnostic cascading.+When a developer makes a typo (e.g. `user.nmae`), standard GHC behavior is catastrophic:+1. GHC fails to solve `HasField "nmae" User a`.+2. GHC reports: "No instance for (HasField "nmae" User a) arising from selection 'user.nmae'".+3. Because the type variable `a` cannot be deduced, downstream expressions fail to typecheck:+   "Could not deduce (Show a) from use of 'print'", "Ambiguous type variable 'a'", etc.+4. The developer is inundated with 10–20 irrelevant compiler errors, obscuring the simple typo.++`Polytropos.Plugin` employs a sophisticated two-pronged diagnostic recovery architecture:++1. Custom Diagnostic Synthesis (`mkTypeErrorCt`):+   When a field or constructor lookup fails on a closed row:+   - We construct an actionable, human-centric error message explaining exactly what failed.+   - We format a Levenshtein-distance fuzzy typo suggestion ("Did you mean: 'name'?") using+     our Wagner-Fischer algorithm (edit distance <= 2).+   - We print the entire actual record or variant schema so the developer has immediate context.+   - We package this into a `TypeError` constraint from `GHC.TypeLits` / `GHC.Internal.TypeError`+     and emit it as a new wanted constraint (`tcPluginNewCts`).++2. Safe Dummy Evidence Emission (`mkDummyHasFieldDict`, dummy `EvExpr`):+   - Alongside the newly emitted `TypeError` constraint, we **SOLVE** the original wanted constraint+     with a safe dummy dictionary!+   - For `HasField`: `mkDummyHasFieldDict` synthesizes a Core lambda `\r -> noInlineUnsafeCo ()`.+   - For `FieldIndex` / `ConstructorIndex`: we emit literal dummy offset 0.+   - For `SubRow` / `SubSum`: we emit empty dummy index lists.++Why solve the original constraint if it was invalid?+Because by discharging the original constraint:+- GHC considers the type of `user.nmae` to be successfully solved (instantiating `a` to the expected type).+- Downstream functions, typeclasses, and expressions typecheck without a single secondary error!+- When compilation reaches the reporting phase, GHC encounters the newly emitted `TypeError` wanted+  constraint and halts with **ONLY** our clean, focused, actionable diagnostic.+-}++-------------------------------------------------------------------------------+-- Plugin entry point+-------------------------------------------------------------------------------++-- | The polytropos GHC plugin entry point.+plugin :: Plugin+plugin = defaultPlugin+  { tcPlugin           = const $ Just $ mkTcPlugin polytroposPlugin+  , parsedResultAction = \opts _modSummary -> sourcePlugin opts+  }++polytroposPlugin :: TcPlugin+polytroposPlugin = TcPlugin+  { tcPluginInit     = polytroposInit+  , tcPluginSolve    = polytroposSolve+  , tcPluginRewrite  = polytroposRewrite+  , tcPluginPostTc   = const (return ())+  , tcPluginShutdown = const (return ())+  }++--------------------------------------------------------------------------------- Plugin state+-------------------------------------------------------------------------------++data PluginState = PluginState++  { psRepTag        :: !Var    -- ^ repTag :: Rep f a -> Word+  , psRepArity      :: !Var    -- ^ repArity :: Rep f a -> Int+  , psFieldAt       :: !Var    -- ^ fieldAt :: Int -> Rep f a -> f x+  , psUnRowRep      :: !Var    -- ^ unRowRep :: RowRep f r row a -> Rep f a+  , psNoInlineCo    :: !Var    -- ^ noInlineUnsafeCo :: a -> b+  , psAnd           :: !Var    -- ^ GHC.Internal.Classes.&&+  , psComp          :: !Var    -- ^ GHC.Internal.Base.(.)+  , psEqClass       :: !Var    -- ^ GHC.Internal.Classes.== (method)+  , psShowsPrecMeth :: !Var    -- ^ GHC.Internal.Show.showsPrec (method)+  , psShowString    :: !Var    -- ^ GHC.Internal.Show.showString+  , psShowChar      :: !Var    -- ^ GHC.Internal.Show.showChar+  , psFEqInt        :: !Var    -- ^ $fEqInt+  , psFEqBool       :: !Var    -- ^ $fEqBool+  , psFEqWord       :: !Var    -- ^ $fEqWord+  , psFShowInt      :: !Var    -- ^ $fShowInt+  , psFShowBool     :: !Var    -- ^ $fShowBool+  , psEqCls         :: !Class  -- ^ GHC.Classes.Eq class+  , psShowCls       :: !Class  -- ^ GHC.Show.Show class+  , psRowFlavourCls   :: !Class  -- ^ RowFlavour class+  , psHasFieldCls     :: !Class  -- ^ GHC.Records.HasField class+  , psDictAnyTyCon    :: !TyCon  -- ^ Polytropos.Core.DictAny+  , psMkDictAny       :: !Var    -- ^ Polytropos.Core.mkDictAny+  , psEvidenceAllFields :: !Var  -- ^ Polytropos.Core.evidenceAllFields+  , psFieldTypesTyCon       :: !TyCon -- ^ Polytropos.Core.FieldTypes+  , psSimpleFieldTypesTyCon :: !TyCon -- ^ Polytropos.Core.SimpleFieldTypes+  , psFieldNamesTyCon       :: !TyCon -- ^ Polytropos.Core.FieldNames+  , psTypeErrorTyCon        :: !TyCon -- ^ GHC.Internal.TypeError.TypeError+  , psPromotedText          :: !TyCon -- ^ promoted 'Text+  , psPromotedVcat          :: !TyCon -- ^ promoted ':$$:+  }++-------------------------------------------------------------------------------+-- Plugin initialisation+-------------------------------------------------------------------------------++polytroposInit :: TcPluginM 'Init PluginState+polytroposInit = do+  coreMod <- findPolytroposCoreModule+  psRepTag     <- lookupIdInModule coreMod "repTag"+  psRepArity   <- lookupIdInModule coreMod "repArity"+  psFieldAt    <- lookupIdInModule coreMod "fieldAt"+  psUnRowRep   <- lookupIdInModule coreMod "unRowRep"+  psNoInlineCo <- lookupIdInModule coreMod "noInlineUnsafeCo"++  psEqClass    <- lookupIdInModule gHC_CLASSES "=="+  psAnd        <- lookupIdInModule gHC_CLASSES "&&"+  psFEqInt     <- lookupIdInModule gHC_CLASSES "$fEqInt"+  psFEqBool    <- lookupIdInModule gHC_CLASSES "$fEqBool"+  psFEqWord    <- lookupIdInModule gHC_CLASSES "$fEqWord"++  psShowsPrecMeth <- lookupIdInModule modShow "showsPrec"+  psShowString    <- lookupIdInModule modShow "showString"+  psShowChar      <- lookupIdInModule modShow "showChar"+  psFShowInt      <- lookupIdInModule modShow "$fShowInt"+  psFShowBool     <- lookupIdInModule modShow "$fShowBool"++  psEqCls   <- tcLookupClass eqClassName+  psShowCls <- tcLookupClass showClassName++  psComp <- lookupIdInModule modBase "."++  rowFlavourName <- lookupOrig coreMod (mkTcOcc "RowFlavour")+  psRowFlavourCls <- tcLookupClass rowFlavourName++  hasFieldOcc <- lookupOrig modRecords (mkTcOcc "HasField")+  psHasFieldCls <- tcLookupClass hasFieldOcc++  dictAnyOcc <- lookupOrig coreMod (mkTcOcc "DictAny")+  psDictAnyTyCon <- tcLookupTyCon dictAnyOcc++  psMkDictAny <- lookupIdInModule coreMod "mkDictAny"+  psEvidenceAllFields <- lookupIdInModule coreMod "evidenceAllFields"++  fieldTypesOcc <- lookupOrig coreMod (mkTcOcc "FieldTypes")+  psFieldTypesTyCon <- tcLookupTyCon fieldTypesOcc++  simpleFieldTypesOcc <- lookupOrig coreMod (mkTcOcc "SimpleFieldTypes")+  psSimpleFieldTypesTyCon <- tcLookupTyCon simpleFieldTypesOcc++  fieldNamesOcc <- lookupOrig coreMod (mkTcOcc "FieldNames")+  psFieldNamesTyCon <- tcLookupTyCon fieldNamesOcc++  psTypeErrorTyCon <- tcLookupTyCon errorMessageTypeErrorFamName+  textDataCon      <- tcLookupDataCon typeErrorTextDataConName+  vcatDataCon      <- tcLookupDataCon typeErrorVAppendDataConName++  let psPromotedText = promoteDataCon textDataCon+      psPromotedVcat = promoteDataCon vcatDataCon++  pure PluginState{..}++findModule :: String -> Maybe String -> TcPluginM 'Init Module+findModule modName mPkg = do+  let modName' = mkModuleName modName+  pkgQual <- resolveImport modName' (fsLit <$> mPkg)+  result <- findImportedModule modName' pkgQual+  case result of+    Found _ mod' -> pure mod'+    _           -> error $ "polytropos: could not find module " ++ modName++findPolytroposCoreModule :: TcPluginM 'Init Module+findPolytroposCoreModule = findModule "Polytropos.Core" (Just "polytropos-core")++lookupIdInModule :: Module -> String -> TcPluginM 'Init Var+lookupIdInModule modName occStr = do+  let occ = mkVarOcc occStr+  name <- lookupOrig modName occ+  tcLookupId name++-------------------------------------------------------------------------------+-- Type family rewriting (FieldNames, SimpleFieldTypes, FieldTypes)+-------------------------------------------------------------------------------++-- | Type family rewriter for FieldNames, SimpleFieldTypes, and FieldTypes.+-- Evaluates closed row reflection queries in O(1) during GHC's type rewriting stage.+-- See Note [Type-Level Metadata Rewriting and Defunctionalization] [ref:note-metadata-rewriting]+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+polytroposRewrite :: PluginState -> UniqFM TyCon TcPluginRewriter+polytroposRewrite state = listToUFM+  [ (psFieldTypesTyCon state, rewriteFieldTypes (psFieldTypesTyCon state))+  , (psSimpleFieldTypesTyCon state, rewriteSimpleFieldTypes (psSimpleFieldTypesTyCon state))+  , (psFieldNamesTyCon state, rewriteFieldNames (psFieldNamesTyCon state))+  ]++-- | Extracts fields from a row type. Fails (returns Nothing) if the tail is unfixed or open.+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+-- See Note [OCaml Subtype/Unify Correlation and Row Tail Algebra] [ref:note-ocaml-row-algebra]+walkRowFields_maybe :: Type -> Maybe [(FastString, Type)]+walkRowFields_maybe rowTy = do+  elems <- myExtractPromotedList (unwrapSynonyms rowTy)+  mapM extractField elems+  where+    extractField elemTy =+      case splitTyConApp_maybe (unwrapSynonyms elemTy) of+        Just (_, args)+          | length args >= 2+          , let nameTy = args !! (length args - 2)+          , let fieldTy = args !! (length args - 1)+          , Just n <- isStrLitTy (unwrapSynonyms nameTy)+          -> Just (n, fieldTy)+        _ -> Nothing++rewriteFieldNames :: TyCon -> [Ct] -> [Type] -> TcPluginM 'Rewrite TcPluginRewriteResult+rewriteFieldNames tyCon _givens args+  | not (null args)+  , let rowTy = last args+  , Just fields <- walkRowFields_maybe rowTy+  = do+      let names = map (mkStrLitTy . fst) fields+          reducedTy = mkPromotedListTy typeSymbolKind names+      pure $ TcPluginRewriteTo+        { tcRewriterNewWanteds = []+        , tcPluginReduction    =+            mkTyFamAppReduction "polytropos" Nominal [] tyCon args reducedTy+        }+  | otherwise = pure TcPluginNoRewrite++rewriteSimpleFieldTypes :: TyCon -> [Ct] -> [Type] -> TcPluginM 'Rewrite TcPluginRewriteResult+rewriteSimpleFieldTypes tyCon _givens args+  | not (null args)+  , let rowTy = last args+  , Just fields <- walkRowFields_maybe rowTy+  = do+      let pairKind = mkTupleTy Boxed [typeSymbolKind, liftedTypeKind]+          pairs = [ mkPromotedPairTy typeSymbolKind liftedTypeKind (mkStrLitTy name) ty+                  | (name, ty) <- fields+                  ]+          reducedTy = mkPromotedListTy pairKind pairs+      pure $ TcPluginRewriteTo+        { tcRewriterNewWanteds = []+        , tcPluginReduction    =+            mkTyFamAppReduction "polytropos" Nominal [] tyCon args reducedTy+        }+  | otherwise = pure TcPluginNoRewrite++rewriteFieldTypes :: TyCon -> [Ct] -> [Type] -> TcPluginM 'Rewrite TcPluginRewriteResult+rewriteFieldTypes tyCon _givens args+  | length args >= 2+  , let rowTy = last args+  , let fTy   = args !! (length args - 2)+  , Just fields <- walkRowFields_maybe rowTy+  = do+      let pairKind = mkTupleTy Boxed [typeSymbolKind, liftedTypeKind]+          pairs = [ mkPromotedPairTy typeSymbolKind liftedTypeKind (mkStrLitTy name) (mkAppTy fTy ty)+                  | (name, ty) <- fields+                  ]+          reducedTy = mkPromotedListTy pairKind pairs+      pure $ TcPluginRewriteTo+        { tcRewriterNewWanteds = []+        , tcPluginReduction    =+            mkTyFamAppReduction "polytropos" Nominal [] tyCon args reducedTy+        }+  | otherwise = pure TcPluginNoRewrite++-------------------------------------------------------------------------------+-- Human-Centric TypeError Diagnostics Helpers+--+-- See Note [Human-Centric TypeError Diagnostics & Fuzzy Matching] [ref:note-typeerror-diagnostics]+-- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+-------------------------------------------------------------------------------++-- | Computes the Levenshtein edit distance between two strings using dynamic+-- programming. Used to rank fuzzy typo suggestions when a requested field or+-- constructor label is not found in a closed row.+--+-- Implementation details:+-- - Uses the standard Wagner-Fischer algorithm with row-by-row DP optimization.+-- - Rather than allocating an (M x N) matrix on the heap, it maintains only two+--   rows of distance integers: the previous row ('row') and the current row being+--   computed via 'scanl'.+-- - In 'stepRow':+--   * 'left' is the distance for the cell directly to the left (insertion: left + 1).+--   * 'above' is the distance for the cell directly above (deletion: above + 1).+--   * 'diag' is the diagonal distance (substitution: diag + (if c1 == c2 then 0 else 1)).+--   * The cell takes the minimum of all three edit costs.+-- - Complexity: O(M * N) time and O(min(M, N)) space, running in microseconds for+--   typical identifier lengths (<30 characters).+levenshtein :: String -> String -> Int+levenshtein s1 s2 =+  let n = length s1+      initRow = [0 .. n]+      stepRow row c2 = case row of+        [] -> []+        d : ds -> scanl (\left (c1, diag, above) ->+                           let cost = if c1 == c2 then 0 else 1+                           in min (diag + cost) (min (left + 1) (above + 1)))+                        (d + 1)+                        (zip3 s1 row ds)+  in case foldl' stepRow initRow s2 of+       [] -> 0+       res -> last res++-- | Filters and ranks candidate field/constructor names against a target typo.+--+-- Policy:+-- - Candidates with edit distance <= 2 are retained. Distance 2 is the empirical+--   sweet spot in compiler ergonomics: it catches transposed letters ("nmae"),+--   dropped characters ("nam"), and single-character substitutions ("nane"),+--   while rejecting false positives on short labels.+-- - Results are sorted ascending by edit distance (closest match first).+suggestSimilar :: String -> [String] -> [String]+suggestSimilar target candidates =+  let scored = [ (c, d) | c <- candidates, let d = levenshtein target c, d <= 2 ]+  in map fst (sortOn snd scored)++-- | Formats a product row's schema for display in compiler diagnostics:+-- "{ field1 :: Type1, field2 :: Type2, ... }"+--+-- Unrolls GHC Core Types to human-readable strings via 'ppr' and 'showSDocUnsafe'.+formatRecordRow :: [(Int, FastString, Type)] -> String+formatRecordRow fields =+  "{ " ++ intercalate ", " [ unpackFS n ++ " :: " ++ showSDocUnsafe (ppr ty) | (_, n, ty) <- fields ] ++ " }"++-- | Formats a sum row's schema for display in compiler diagnostics:+-- "< Con1 RecordPayload | Con2 TypePayload | Con3 >"+--+-- Handles empty constructors, single-field bare constructors, and multi-field+-- record constructors, printing a clean structural variant signature.+formatVariantRow :: [(Int, FastString, Type)] -> String+formatVariantRow ctors =+  "< " ++ intercalate " | " (map formatCtor ctors) ++ " >"+  where+    formatCtor (_, n, conRowTy) =+      case walkRowWithTypes conRowTy of+        [] -> unpackFS n+        [(_, fn, ty)] | nullFS fn -> unpackFS n ++ " :: " ++ showSDocUnsafe (ppr ty)+        fs -> unpackFS n ++ " " ++ formatRecordRow fs++-- | Formats a field suggestion clause:+-- - If close matches exist: "Did you mean: 'name' or 'age'?"+-- - If no close matches: lists all available fields in the record.+-- - If the record is empty: reports "(no fields in record)".+formatSuggestion :: String -> [String] -> String+formatSuggestion target candidates =+  case suggestSimilar target candidates of+    [] -> case candidates of+      [] -> "(no fields in record)"+      _  -> "Available fields: " ++ intercalate ", " (map (\c -> "'" ++ c ++ "'") candidates)+    suggs -> "Did you mean: " ++ intercalate " or " (map (\s -> "'" ++ s ++ "'") suggs) ++ "?"++-- | Formats a constructor suggestion clause for variants.+formatCtorSuggestion :: String -> [String] -> String+formatCtorSuggestion target candidates =+  case suggestSimilar target candidates of+    [] -> case candidates of+      [] -> "(no constructors in variant)"+      _  -> "Available constructors: " ++ intercalate ", " (map (\c -> "'" ++ c ++ "'") candidates)+    suggs -> "Did you mean: " ++ intercalate " or " (map (\s -> "'" ++ s ++ "'") suggs) ++ "?"++-- | Checks whether a Type contains no free type or coercion variables.+-- A closed type is fully grounded and ready for terminal diagnostic reporting.+isClosedType :: Type -> Bool+isClosedType ty = isEmptyVarSet (tyCoVarsOfType (unwrapSynonyms ty))++-- | Wraps a Haskell string into GHC's promoted 'Text constructor for type-level ErrorMessage.+mkTextMsg :: PluginState -> String -> Type+mkTextMsg state s = mkTyConApp (psPromotedText state) [mkStrLitTy (fsLit s)]++-- | Combines multiple promoted 'Text messages vertically using ':$$: (promoted Vcat).+mkVcatMsgs :: PluginState -> [Type] -> Type+mkVcatMsgs _ [] = error "mkVcatMsgs: empty list"+mkVcatMsgs _ [m] = m+mkVcatMsgs state (m : ms) = mkTyConApp (psPromotedVcat state) [m, mkVcatMsgs state ms]++-- | Synthesizes a new wanted GHC 'TypeError' constraint from a list of diagnostic strings.+--+-- Mechanics:+-- 1. Promotes each string into an 'ErrorMessage ('Text ...)'.+-- 2. Combines lines vertically with ':$$:'.+-- 3. Constructs the predicate type 'TypeError Constraint fullMsg'.+-- 4. Allocates a fresh wanted evidence variable with the original constraint's 'CtLoc'.+-- 5. Wraps the evidence in 'mkNonCanonical' so GHC's solver processes it as an unsolved+--    wanted constraint that halts compilation with the specified error message.+--+-- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+mkTypeErrorCt :: PluginState -> CtLoc -> [String] -> TcPluginM 'Solve Ct+mkTypeErrorCt state loc msgLines = do+  let msgTys = map (mkTextMsg state) msgLines+      fullMsg = mkVcatMsgs state msgTys+      predTy = mkTyConApp (psTypeErrorTyCon state) [constraintKind, fullMsg]+  ev <- newWanted loc predTy+  pure (mkNonCanonical ev)++-- | Synthesizes a dummy dictionary for GHC.Records.HasField that produces a safe bottom+-- value at runtime via 'noInlineUnsafeCo ()'.+--+-- Why dummy dictionaries are necessary:+-- When a user accesses an invalid field ('rec.nonexistent'), we emit a custom 'TypeError'+-- wanted constraint. If we leave the original 'HasField' wanted constraint unsolved, GHC+-- reports a confusing "No instance for HasField" error AND marks downstream expressions+-- as untypeable, triggering a cascade of secondary compiler errors. By discharging the+-- 'HasField' constraint with this dummy dictionary, downstream code typechecks cleanly,+-- and GHC halts with ONLY our custom typo diagnostic!+--+-- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+mkDummyHasFieldDict :: PluginState -> Class -> [Type] -> TcPluginM 'Solve EvTerm+mkDummyHasFieldDict state cls tys = do+  let getFieldId = case classMethods cls of+        (m : _) -> m+        [] -> error "Polytropos.Plugin: HasField has no methods"+      methodFullTy = piResultTys (varType getFieldId) tys+      (_, _, methodInDictTy) = splitFunTy methodFullTy+      (tyVars, tauTy) = splitForAllTyCoVars methodInDictTy+      (argTys, _) = splitFunTys tauTy+      scaledRTy = argTys !! 0+      fieldTy = last tys+  rName <- unsafeLiftTcM $ newName (mkVarOcc "rec")+  let rVar = mkLocalId rName (scaledMult scaledRTy) (scaledThing scaledRTy)+      -- dummyVal = noInlineUnsafeCo () :: fieldTy+      dummyVal = mkCoreApps (Var (psNoInlineCo state))+                   [ Type (mkTyConTy unitTyCon)+                   , Type fieldTy+                   , mkCoreConApps unitDataCon []+                   ]+      -- getFieldExpr = \rec -> dummyVal+      getFieldExpr = mkCoreLams (tyVars ++ [rVar]) dummyVal+  pure $ EvExpr (evDataConApp (classDataCon cls) tys [getFieldExpr])++-------------------------------------------------------------------------------+-- Constraint solving+-------------------------------------------------------------------------------++-- | Top-level constraint solver entry point for @Polytropos.Plugin@.+--+-- Invoked by GHC during constraint simplification with 'givens' and 'wanteds'.+-- See Note [Solving Pipeline: Wanteds, Givens, and Staged Evidence Synthesis] [ref:note-solving-pipeline]+--+-- Execution Flow:+-- 1. Evaluates all active constraints through 'solveOne'.+-- 2. Partitions results into solved evidence pairs and newly spawned wanted constraints.+-- 3. Returns 'TcPluginSolveResult' to GHC.+polytroposSolve+  :: PluginState+  -> [Ct]+  -> [Ct]+  -> TcPluginM 'Solve TcPluginSolveResult+polytroposSolve state givens wanteds = do+  let allCts = givens ++ wanteds+  results <- mapM (solveOne state) allCts+  let (solvedPairs, _) = partitionEithers results+      solvedCts = map fst solvedPairs+      newCts = concatMap snd solvedPairs+  pure $ TcPluginSolveResult+    { tcPluginInsolubleCts = []+    , tcPluginSolvedCts = solvedCts+    , tcPluginNewCts = newCts+    }++solveOne :: PluginState -> Ct -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveOne state ct+  | not (isWanted (ctEvidence ct))+  = pure $ Right ()+  | otherwise+  = do+    let predTy = ctPred ct+    case classifyPredType predTy of+      ClassPred cls tys -> do+        case className cls of+          name+            | nameOccName name == mkTcOcc "FieldIndex"+            -> solveFieldIndex state ct cls tys+            | nameOccName name == mkTcOcc "ConstructorIndex"+            -> solveConstructorIndex state ct cls tys+            | nameOccName name == mkTcOcc "RowEq"+            -> solveRowEq state ct cls tys+            | nameOccName name == mkTcOcc "RowShow"+            -> solveRowShow state ct cls tys+            | nameOccName name == mkTcOcc "RowEqSum"+            -> solveRowEqSum state ct cls tys+            | nameOccName name == mkTcOcc "RowShowSum"+            -> solveRowShowSum state ct cls tys+            | nameOccName name == mkTcOcc "HasField"+            -> solveHasField state ct cls tys+            | nameOccName name == mkTcOcc "AllFields"+            -> solveAllFields state ct cls tys+            | nameOccName name == mkTcOcc "SubRow"+            -> solveSubRow state ct cls tys+            | nameOccName name == mkTcOcc "SubSum"+            -> solveSubSum state ct cls tys+            | nameOccName name == mkTcOcc "KnownHash"+            -> noNew <$> solveKnownHash ct cls tys+            | otherwise+            -> pure $ Right ()+      _ -> pure $ Right ()+  where+    noNew (Left res) = Left (res, [])+    noNew (Right ()) = Right ()++-------------------------------------------------------------------------------+-- FieldIndex solver+-------------------------------------------------------------------------------++-- | Solves the 'FieldIndex' constraint by statically locating the field's 0-based+-- offset in the row and returning literal Int evidence.+--+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+-- See Note [Human-Centric TypeError Diagnostics & Fuzzy Matching] [ref:note-typeerror-diagnostics]+-- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+--+-- Execution Phases:+-- 1. Deconstruct Predicate Types:+--    Extracts the field identifier type 'nTy', the enclosing row 'rowTy', and the+--    expected field type 'expectedATy'.+-- 2. Label Discrimination (Named vs. Anonymous):+--    - Case A (Named Symbol): If 'nTy' is a type-level string literal (e.g. @"name"@),+--      locates the field via 'findFieldType'.+--    - Case B (Anonymous / Positional): If 'nTy' is an arbitrary type without a symbol+--      label, locates the first field possessing that exact type via 'findFieldIndexByType'.+-- 3. Verification & Evidence Synthesis:+--    - On Match: Verifies that 'actualTy' matches 'expectedATy' (or that 'expectedATy'+--      contains free type variables awaiting downstream unification). Emits 'mkIntExpr i'+--      wrapped in the 'FieldIndex' class dictionary.+--    - On Type Discrepancy: Synthesizes a human-readable 'TypeError' detailing the actual+--      vs expected type, and discharges the wanted with dummy evidence (index 0) to+--      prevent GHC from halting with cascading secondary errors.+--    - On Missing Field: Inspects the closed row schema, computes fuzzy Levenshtein+--      suggestions via 'formatSuggestion', emits a custom 'TypeError', and discharges+--      with dummy evidence.+solveFieldIndex+  :: PluginState+  -> Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveFieldIndex state ct cls tys+  | length tys >= 3 = do+      let nTy         = tys !! (length tys - 3)+          rowTy       = tys !! (length tys - 2)+          expectedATy = last tys+          unwrapN     = unwrapSynonyms nTy+          loc         = ctLoc ct+      case isStrLitTy unwrapN of+        Just fieldName -> do+          -- Named field lookup by type-level Symbol+          case findFieldType fieldName rowTy of+            Just (i, actualTy)+              -- Accept exact type match+              | actualTy `eqType` expectedATy -> do+                  let iExpr = mkIntExpr i+                      dictExpr = evDataConApp (classDataCon cls) tys [iExpr]+                  pure $ Left ((EvExpr dictExpr, ct), [])+              -- If either type is open / uninstantiated, emit nominal equality constraint to unify them+              | not (isClosedType expectedATy) || not (isClosedType actualTy) -> do+                  let iExpr = mkIntExpr i+                      dictExpr = evDataConApp (classDataCon cls) tys [iExpr]+                  eqEv <- newWanted loc (mkEqPredRole Nominal expectedATy actualTy)+                  pure $ Left ((EvExpr dictExpr, ct), [mkNonCanonical eqEv])+              -- Terminal type discrepancy: emit diagnostic and safe dummy evidence+              | otherwise -> do+                  let dummyExpr = mkIntExpr 0+                      dummyDict = evDataConApp (classDataCon cls) tys [dummyExpr]+                      diagLines =+                        [ "Polytropos Record Error:"+                        , "  Field '" ++ unpackFS fieldName ++ "' in record has type:"+                        , "    " ++ showSDocUnsafe (ppr actualTy)+                        , "  but expected:"+                        , "    " ++ showSDocUnsafe (ppr expectedATy)+                        ]+                  errCt <- mkTypeErrorCt state loc diagLines+                  pure $ Left ((EvExpr dummyDict, ct), [errCt])+            Nothing -> do+              -- Field not found: format schema and compute fuzzy typo suggestions+              case walkRowWithTypes_maybe rowTy of+                Just fields -> do+                  let dummyExpr = mkIntExpr 0+                      dummyDict = evDataConApp (classDataCon cls) tys [dummyExpr]+                      fNames = [ unpackFS n | (_, n, _) <- fields, not (nullFS n) ]+                      diagLines =+                        [ "Polytropos Record Error:"+                        , "  Field '" ++ unpackFS fieldName ++ "' does not exist in record:"+                        , "    " ++ formatRecordRow fields+                        , "  " ++ formatSuggestion (unpackFS fieldName) fNames+                        ]+                  errCt <- mkTypeErrorCt state loc diagLines+                  pure $ Left ((EvExpr dummyDict, ct), [errCt])+                Nothing -> pure $ Right () -- Row tail is still open/unfixed: defer solving+        Nothing -> do+          -- Anonymous/positional field lookup by payload Type+          case findFieldIndexByType unwrapN rowTy of+            Just i -> do+              let iExpr = mkIntExpr i+                  dictExpr = evDataConApp (classDataCon cls) tys [iExpr]+              pure $ Left ((EvExpr dictExpr, ct), [])+            Nothing -> do+              case walkRowWithTypes_maybe rowTy of+                Just fields -> do+                  let dummyExpr = mkIntExpr 0+                      dummyDict = evDataConApp (classDataCon cls) tys [dummyExpr]+                      diagLines =+                        [ "Polytropos Record Error:"+                        , "  Type '" ++ showSDocUnsafe (ppr unwrapN) ++ "' is not a field in record:"+                        , "    " ++ formatRecordRow fields+                        ]+                  errCt <- mkTypeErrorCt state loc diagLines+                  pure $ Left ((EvExpr dummyDict, ct), [errCt])+                Nothing -> pure $ Right ()+  | otherwise = pure $ Right ()++-------------------------------------------------------------------------------+-- ConstructorIndex solver+-------------------------------------------------------------------------------++-- | Solves the 'ConstructorIndex' constraint by statically locating the constructor's+-- 0-based tag in the sum row and returning literal Word evidence.+--+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+-- See Note [Human-Centric TypeError Diagnostics & Fuzzy Matching] [ref:note-typeerror-diagnostics]+-- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+--+-- Execution Phases:+-- 1. Deconstruct Constructor Predicate:+--    Extracts constructor identifier type 'nTy' and sum row 'rowTy'.+-- 2. Constructor Tag Lookup:+--    - Named Symbol: Locates constructor tag 'w' via 'findConstructorIndex'.+--    - Type-Indexed: Locates constructor possessing matching payload type via 'findConstructorIndexByType'.+-- 3. Evidence Synthesis & Recovery:+--    - Success: Emits literal 'mkWordExpr w' wrapped in 'ConstructorIndex' dictionary.+--    - Failure: Formats variant schema via 'formatVariantRow', ranks constructor typo+--      suggestions via 'formatCtorSuggestion', emits 'TypeError', and returns dummy evidence (tag 0).+solveConstructorIndex+  :: PluginState+  -> Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveConstructorIndex state ct cls tys+  | length tys >= 2 = do+      let nTy   = tys !! (length tys - 2)+          rowTy = tys !! (length tys - 1)+          unwrapN = unwrapSynonyms nTy+          loc = ctLoc ct+      case isStrLitTy unwrapN of+        Just conName -> do+          -- Named constructor lookup by type-level Symbol+          case findConstructorIndex conName rowTy of+            Just w -> do+              let wExpr = mkWordExpr w+                  dictExpr = evDataConApp (classDataCon cls) tys [wExpr]+              pure $ Left ((EvExpr dictExpr, ct), [])+            Nothing -> do+              -- Missing constructor: format variant schema and fuzzy suggestions+              case walkSumRowWithTypes_maybe rowTy of+                Just ctors -> do+                  let dummyExpr = mkWordExpr 0+                      dummyDict = evDataConApp (classDataCon cls) tys [dummyExpr]+                      cNames = [ unpackFS n | (_, n, _) <- ctors, not (nullFS n) ]+                      diagLines =+                        [ "Polytropos Variant Error:"+                        , "  Constructor '" ++ unpackFS conName ++ "' is not a member of variant:"+                        , "    " ++ formatVariantRow ctors+                        , "  " ++ formatCtorSuggestion (unpackFS conName) cNames+                        ]+                  errCt <- mkTypeErrorCt state loc diagLines+                  pure $ Left ((EvExpr dummyDict, ct), [errCt])+                Nothing -> pure $ Right () -- Open sum tail: defer solving+        Nothing -> do+          -- Anonymous constructor lookup by payload Type+          case findConstructorIndexByType unwrapN rowTy of+            Just w -> do+              let wExpr = mkWordExpr w+                  dictExpr = evDataConApp (classDataCon cls) tys [wExpr]+              pure $ Left ((EvExpr dictExpr, ct), [])+            Nothing -> do+              case walkSumRowWithTypes_maybe rowTy of+                Just ctors -> do+                  let dummyExpr = mkWordExpr 0+                      dummyDict = evDataConApp (classDataCon cls) tys [dummyExpr]+                      diagLines =+                        [ "Polytropos Variant Error:"+                        , "  Type '" ++ showSDocUnsafe (ppr unwrapN) ++ "' is not a payload type in variant:"+                        , "    " ++ formatVariantRow ctors+                        ]+                  errCt <- mkTypeErrorCt state loc diagLines+                  pure $ Left ((EvExpr dummyDict, ct), [errCt])+                Nothing -> pure $ Right ()+  | otherwise = pure $ Right ()++-------------------------------------------------------------------------------+-- RowEq solver+-------------------------------------------------------------------------------++-- | Solves the 'RowEq' constraint by synthesizing an unrolled comparison expression over all fields.+--+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+--+-- Architectural Blueprint:+-- 1. Unrolls Product Schema:+--    Traverses the row using 'walkRowWithTypes', collecting (index, name, fieldType) for every slot.+-- 2. Superclass Evidence Synthesis:+--    Emits trivial evidence for 'RowFlavour r' superclass constraint.+-- 3. Core Lambda Construction:+--    Extracts method signature for 'repEq' and allocates local variables 'r1' and 'r2'.+-- 4. Tag & Arity Checks:+--    Builds 'eqTag' ('repTag rep1 == repTag rep2') and 'eqArity' ('repArity rep1 == repArity rep2').+--    Note: In products, tag is statically 0 and arity is statically N, so GHC's simplifier folds+--    these comparisons into 'True' at compile time!+-- 5. Field Comparison Unrolling:+--    - Spawns fresh wanted 'Eq fieldTy' constraints for each field.+--    - Reads slot 'i' using 'fieldAt @i rep1' and 'fieldAt @i rep2'.+--    - Coerces payload pointers via 'noInlineUnsafeCo'.+--    - Invokes '==' from the corresponding 'Eq' dictionary.+-- 6. Boolean Short-Circuiting Conjunction:+--    Chains all comparisons using GHC's Boolean '(&&)' operator into a single flat Core expression:+--    @eqTag && eqArity && (field0_1 == field0_2) && (field1_1 == field1_2) && ...@+solveRowEq+  :: PluginState+  -> Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveRowEq state ct cls tys = do+  let rowTy  = last tys+      rTy    = tys !! (length tys - 2)+      fields = walkRowWithTypes rowTy+      loc    = ctLoc ct++      -- Superclass evidence for RowFlavour r+      scEvidence = evDataConApp (classDataCon (psRowFlavourCls state)) [rTy] []++      -- Extract repEq method type and bind lambda arguments: \r1 r2 -> ...+      repEqId = case classMethods cls of+        (m : _) -> m+        []      -> error "Polytropos.Plugin: RowEq class has no methods"+      methodFullTy = piResultTys (varType repEqId) tys+      (_, _, methodInDictTy) = splitFunTy methodFullTy+      (tyVars, tauTy) = splitForAllTyCoVars methodInDictTy+      (argTys, _) = splitFunTys tauTy+      scaledR1Ty = argTys !! 0+      scaledR2Ty = argTys !! 1++  r1Name <- unsafeLiftTcM $ newName (mkVarOcc "r1")+  r2Name <- unsafeLiftTcM $ newName (mkVarOcc "r2")+  let r1Var = mkLocalId r1Name (scaledMult scaledR1Ty) (scaledThing scaledR1Ty)+      r2Var = mkLocalId r2Name (scaledMult scaledR2Ty) (scaledThing scaledR2Ty)++      kATy   = mkTyVarTy (tyVars !! 0)+      fTy    = mkTyVarTy (tyVars !! 1)+      aTy    = mkTyVarTy (tyVars !! 2)+      kRowTy = typeKind rowTy++      -- Unpack RowRep wrappers: unRowRep r1, unRowRep r2+      unRowRepTypeArgs = [Type kRowTy, Type kATy, Type fTy, Type rTy, Type rowTy, Type aTy]+      rep1 = mkCoreApps (Var (psUnRowRep state)) (unRowRepTypeArgs ++ [Var r1Var])+      rep2 = mkCoreApps (Var (psUnRowRep state)) (unRowRepTypeArgs ++ [Var r2Var])++      -- Structural header checks: repTag and repArity+      repTypeArgs = [Type kATy, Type fTy, Type aTy]+      tag1 = mkCoreApps (Var (psRepTag state)) (repTypeArgs ++ [rep1])+      tag2 = mkCoreApps (Var (psRepTag state)) (repTypeArgs ++ [rep2])+      eqTag = mkCoreApps (Var (psEqClass state)) [Type (mkTyConTy wordTyCon), Var (psFEqWord state), tag1, tag2]++      arity1 = mkCoreApps (Var (psRepArity state)) (repTypeArgs ++ [rep1])+      arity2 = mkCoreApps (Var (psRepArity state)) (repTypeArgs ++ [rep2])+      eqArity = mkCoreApps (Var (psEqClass state)) [Type intTy, Var (psFEqInt state), arity1, arity2]++  -- Spawn wanted Eq constraints for every field type in the row+  wanteds <- forM fields $ \(i, _nameFS, fieldTy) -> do+    ev <- newWanted loc (mkAppTy (mkTyConTy (classTyCon (psEqCls state))) fieldTy)+    pure (i, fieldTy, ev)++  -- Synthesize comparison expression for slot i:+  -- (==) @fieldTy eqDict (noInlineUnsafeCo (fieldAt @i rep1)) (noInlineUnsafeCo (fieldAt @i rep2))+  let compareField (i, fieldTy, ev) =+        let fieldAtTypeArgs = [Type kATy, Type fTy, Type aTy, Type fieldTy]+            idxExpr = mkIntExpr i+            raw1 = mkCoreApps (Var (psFieldAt state)) (fieldAtTypeArgs ++ [idxExpr, rep1])+            raw2 = mkCoreApps (Var (psFieldAt state)) (fieldAtTypeArgs ++ [idxExpr, rep2])+            fFieldTy = mkAppTy fTy fieldTy+            val1 = mkCoreApps (Var (psNoInlineCo state)) [Type fFieldTy, Type fieldTy, raw1]+            val2 = mkCoreApps (Var (psNoInlineCo state)) [Type fFieldTy, Type fieldTy, raw2]+            eqDict = ctEvExpr ev+        in mkCoreApps (Var (psEqClass state)) [Type fieldTy, eqDict, val1, val2]++      fieldComps = map compareField wanteds++      -- Fold all comparisons left-to-right with short-circuiting Boolean (&&)+      andFn e1 e2 = mkCoreApps (Var (psAnd state)) [e1, e2]+      bodyExpr = foldl andFn (andFn eqTag eqArity) fieldComps+      repEqExpr = mkCoreLams (tyVars ++ [r1Var, r2Var]) bodyExpr++      dictExpr = evDataConApp (classDataCon cls) tys [scEvidence, repEqExpr]+      newWanteds = [mkNonCanonical ev | (_, _, ev) <- wanteds]+  pure $ Left ((EvExpr dictExpr, ct), newWanteds)++-------------------------------------------------------------------------------+-- RowShow solver+-------------------------------------------------------------------------------++-- | Solves the 'RowShow' constraint by synthesizing an unrolled showsPrec expression over all fields.+--+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+--+-- Architectural Blueprint:+-- 1. Format Prefix:+--    Extracts row name prefix (e.g. "R2 " or nominal alias).+-- 2. Core Lambda Construction:+--    Binds lambda arguments for precedence 'p' and record 'r': @\p r -> ...@.+-- 3. Field Rendering Unrolling:+--    - Spawns fresh wanted 'Show fieldTy' constraints for each field.+--    - Reads slot 'i' using 'fieldAt @i rep' and invokes 'showsPrec 0 val' from the dictionary.+-- 4. Alloc-Free ShowS Composition:+--    Composes all 'ShowS' functions using function composition '(.)', completely avoiding+--    intermediate heap-allocated string buffers during serialization.+solveRowShow+  :: PluginState+  -> Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveRowShow state ct cls tys = do+  let rowTy  = last tys+      rTy    = tys !! (length tys - 2)+      fields = walkRowWithTypes rowTy+      loc    = ctLoc ct++      -- Superclass evidence for RowFlavour r+      scEvidence = evDataConApp (classDataCon (psRowFlavourCls state)) [rTy] []++      -- Extract repShowsPrec method type and bind lambda arguments: \p r -> ...+      repShowsPrecId = case classMethods cls of+        (m : _) -> m+        []      -> error "Polytropos.Plugin: RowShow class has no methods"+      methodFullTy = piResultTys (varType repShowsPrecId) tys+      (_, _, methodInDictTy) = splitFunTy methodFullTy+      (tyVars, tauTy) = splitForAllTyCoVars methodInDictTy+      (argTys, _) = splitFunTys tauTy+      scaledPrecTy = argTys !! 0+      scaledRTy    = argTys !! 1++  precName <- unsafeLiftTcM $ newName (mkVarOcc "p")+  rName <- unsafeLiftTcM $ newName (mkVarOcc "r")+  let precVar = mkLocalId precName (scaledMult scaledPrecTy) (scaledThing scaledPrecTy)+      rVar    = mkLocalId rName (scaledMult scaledRTy) (scaledThing scaledRTy)++      kATy   = mkTyVarTy (tyVars !! 0)+      fTy    = mkTyVarTy (tyVars !! 1)+      aTy    = mkTyVarTy (tyVars !! 2)+      kRowTy = typeKind rowTy++      -- Unpack RowRep wrapper: unRowRep r+      unRowRepTypeArgs = [Type kRowTy, Type kATy, Type fTy, Type rTy, Type rowTy, Type aTy]+      rep = mkCoreApps (Var (psUnRowRep state)) (unRowRepTypeArgs ++ [Var rVar])++      -- Determine record display prefix+      rowName = case splitTyConApp_maybe rowTy of+        Just (tc, _)+          | let name = occNameString (getOccName tc)+          , name /= ":" && name /= "[]" && name /= "''[]"+          -> name+        _ -> "R" ++ show (length fields)++  prefixExpr <- unsafeLiftTcM $ mkStringExpr (rowName ++ " ")+  let prefixShowS = mkCoreApps (Var (psShowString state)) [prefixExpr]+      spaceShowS  = mkCoreApps (Var (psShowChar state)) [mkCharExpr ' ']++  -- Spawn wanted Show constraints for every field type in the row+  wanteds <- forM fields $ \(i, _nameFS, fieldTy) -> do+    ev <- newWanted loc (mkAppTy (mkTyConTy (classTyCon (psShowCls state))) fieldTy)+    pure (i, fieldTy, ev)++  -- Synthesize ShowS expression for slot i:+  -- showsPrec @fieldTy showDict 0 (noInlineUnsafeCo (fieldAt @i rep))+  let showField (i, fieldTy, ev) =+        let fieldAtTypeArgs = [Type kATy, Type fTy, Type aTy, Type fieldTy]+            idxExpr = mkIntExpr i+            raw = mkCoreApps (Var (psFieldAt state)) (fieldAtTypeArgs ++ [idxExpr, rep])+            fFieldTy = mkAppTy fTy fieldTy+            val = mkCoreApps (Var (psNoInlineCo state)) [Type fFieldTy, Type fieldTy, raw]+            showDict = ctEvExpr ev+            zeroPrec = mkIntExpr 0+        in mkCoreApps (Var (psShowsPrecMeth state)) [Type fieldTy, showDict, zeroPrec, val]++      fieldShows = map showField wanteds+      showParts = case fieldShows of+        [] -> [prefixShowS]+        (f0 : fs) -> prefixShowS : f0 : concatMap (\f -> [spaceShowS, f]) fs++      -- Chain all ShowS functions via (.) function composition+      compFn f g = mkCoreApps (Var (psComp state)) [Type stringTy, Type stringTy, Type stringTy, f, g]+      bodyExpr = foldr1 compFn showParts+      repShowsPrecExpr = mkCoreLams (tyVars ++ [precVar, rVar]) bodyExpr++      dictExpr = evDataConApp (classDataCon cls) tys [scEvidence, repShowsPrecExpr]+      newWanteds = [mkNonCanonical ev | (_, _, ev) <- wanteds]+  pure $ Left ((EvExpr dictExpr, ct), newWanteds)++-------------------------------------------------------------------------------+-- RowEqSum / RowShowSum solvers+-------------------------------------------------------------------------------++-- | Solves the 'RowEqSum' constraint by synthesizing constructor branch comparison Core trees.+--+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+--+-- Architectural Blueprint:+-- 1. Unrolls Variant Sum Schema:+--    Traverses the sum row with 'walkSumRowWithTypes', collecting (tag, constructorName, conRowTy)+--    for every constructor branch.+-- 2. Fast-Path Tag Inequality:+--    Verifies 'tag1 == tag2'. If two variant values have different active constructor tags,+--    they are structurally unequal immediately, requiring zero payload inspections.+-- 3. Branching Decision Tree ('buildTree'):+--    If 'tag1 == tag2', constructs a cascading if-then-else Core expression matching on the tag:+--    @if tag1 == 0 then (compare payload of Con0) else if tag1 == 1 then (compare payload of Con1) ... else False@+-- 4. Payload Equality Conjunction:+--    Inside each constructor branch, compares the payload fields using 'fieldAt' and the+--    corresponding 'Eq' dictionary, chained with short-circuiting Boolean '(&&)'.+solveRowEqSum+  :: PluginState+  -> Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveRowEqSum state ct cls tys = do+  let rowTy  = last tys+      rTy    = tys !! (length tys - 2)+      constructors = walkSumRowWithTypes rowTy+      loc    = ctLoc ct++      -- Superclass evidence for RowFlavour r+      scEvidence = evDataConApp (classDataCon (psRowFlavourCls state)) [rTy] []++      -- Extract repEqSum method type and bind lambda arguments: \r1 r2 -> ...+      repEqSumId = case classMethods cls of+        (m : _) -> m+        []      -> error "Polytropos.Plugin: RowEqSum class has no methods"+      methodFullTy = piResultTys (varType repEqSumId) tys+      (_, _, methodInDictTy) = splitFunTy methodFullTy+      (tyVars, tauTy) = splitForAllTyCoVars methodInDictTy+      (argTys, _) = splitFunTys tauTy+      scaledR1Ty = argTys !! 0+      scaledR2Ty = argTys !! 1++  r1Name <- unsafeLiftTcM $ newName (mkVarOcc "r1")+  r2Name <- unsafeLiftTcM $ newName (mkVarOcc "r2")+  let r1Var = mkLocalId r1Name (scaledMult scaledR1Ty) (scaledThing scaledR1Ty)+      r2Var = mkLocalId r2Name (scaledMult scaledR2Ty) (scaledThing scaledR2Ty)++      kATy   = mkTyVarTy (tyVars !! 0)+      fTy    = mkTyVarTy (tyVars !! 1)+      aTy    = mkTyVarTy (tyVars !! 2)+      kRowTy = typeKind rowTy++      -- Unpack RowRep wrappers: unRowRep r1, unRowRep r2+      unRowRepTypeArgs = [Type kRowTy, Type kATy, Type fTy, Type rTy, Type rowTy, Type aTy]+      rep1 = mkCoreApps (Var (psUnRowRep state)) (unRowRepTypeArgs ++ [Var r1Var])+      rep2 = mkCoreApps (Var (psUnRowRep state)) (unRowRepTypeArgs ++ [Var r2Var])++      -- Extract and compare constructor tags: repTag rep1 == repTag rep2+      repTypeArgs = [Type kATy, Type fTy, Type aTy]+      tag1 = mkCoreApps (Var (psRepTag state)) (repTypeArgs ++ [rep1])+      tag2 = mkCoreApps (Var (psRepTag state)) (repTypeArgs ++ [rep2])+      eqTag = mkCoreApps (Var (psEqClass state)) [Type (mkTyConTy wordTyCon), Var (psFEqWord state), tag1, tag2]++      falseExpr = mkCoreConApps falseDataCon []+      trueExpr  = mkCoreConApps trueDataCon []+      andFn e1 e2 = mkCoreApps (Var (psAnd state)) [e1, e2]++  -- Spawn wanted Eq constraints for all fields of all constructors+  ctorWanteds <- forM constructors $ \(i, conName, conRowTy) -> do+    let fields = walkRowWithTypes conRowTy+    fWanteds <- forM fields $ \(fi, _nameFS, fieldTy) -> do+      ev <- newWanted loc (mkAppTy (mkTyConTy (classTyCon (psEqCls state))) fieldTy)+      pure (fi, fieldTy, ev)+    pure (i, conName, fWanteds)++  -- Compare fields within an active constructor payload+  let compareConFields fWanteds =+        let fieldComps = [ compareField fi fieldTy ev | (fi, fieldTy, ev) <- fWanteds ]+        in foldl andFn trueExpr fieldComps++      compareField fi fieldTy ev =+        let fieldAtTypeArgs = [Type kATy, Type fTy, Type aTy, Type fieldTy]+            idxExpr = mkIntExpr fi+            raw1 = mkCoreApps (Var (psFieldAt state)) (fieldAtTypeArgs ++ [idxExpr, rep1])+            raw2 = mkCoreApps (Var (psFieldAt state)) (fieldAtTypeArgs ++ [idxExpr, rep2])+            fFieldTy = mkAppTy fTy fieldTy+            val1 = mkCoreApps (Var (psNoInlineCo state)) [Type fFieldTy, Type fieldTy, raw1]+            val2 = mkCoreApps (Var (psNoInlineCo state)) [Type fFieldTy, Type fieldTy, raw2]+            eqDict = ctEvExpr ev+        in mkCoreApps (Var (psEqClass state)) [Type fieldTy, eqDict, val1, val2]++      -- Synthesize recursive branch test: if tag == i then compareConFields else buildTree (rest)+      buildTree _ [] = falseExpr+      buildTree tagExpr ((i, _conName, fWanteds) : rest) =+        let iLit = mkWordExpr (fromIntegral i)+            cond = mkCoreApps (Var (psEqClass state)) [Type (mkTyConTy wordTyCon), Var (psFEqWord state), tagExpr, iLit]+        in mkIfThenElse cond (compareConFields fWanteds) (buildTree tagExpr rest)++      -- Top-level check: only inspect payload if constructor tags are equal+      bodyExpr = mkIfThenElse eqTag (buildTree tag1 ctorWanteds) falseExpr+      repEqSumExpr = mkCoreLams (tyVars ++ [r1Var, r2Var]) bodyExpr++      dictExpr = evDataConApp (classDataCon cls) tys [scEvidence, repEqSumExpr]+      allNewWanteds = [ mkNonCanonical ev | (_, _, fWanteds) <- ctorWanteds, (_, _, ev) <- fWanteds ]++  pure $ Left ((EvExpr dictExpr, ct), allNewWanteds)++-- | Solves the 'RowShowSum' constraint by synthesizing constructor branch showsPrec Core trees.+--+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+--+-- Architectural Blueprint:+-- 1. Extract Tag & Constructors:+--    Reads runtime tag via 'repTag rep' and unrolls all constructors in 'rowTy'.+-- 2. Constructor Dispatch Tree:+--    Builds a cascading branch dispatcher testing @tag == 0@, @tag == 1@, etc.+-- 3. In-Branch Payload Formatting:+--    For the active constructor:+--    - Emits constructor name string prefix (e.g. @"Just "@).+--    - Emits wanted 'Show' constraints for all payload fields.+--    - Formats each field with 'showsPrec 0 val'.+--    - Composes all segments using alloc-free '(.)' 'ShowS' composition.+solveRowShowSum+  :: PluginState+  -> Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveRowShowSum state ct cls tys = do+  let rowTy  = last tys+      rTy    = tys !! (length tys - 2)+      constructors = walkSumRowWithTypes rowTy+      loc    = ctLoc ct++      -- Superclass evidence for RowFlavour r+      scEvidence = evDataConApp (classDataCon (psRowFlavourCls state)) [rTy] []++      -- Extract repShowsPrecSum method type and bind lambda arguments: \p r -> ...+      repShowsPrecSumId = case classMethods cls of+        (m : _) -> m+        []      -> error "Polytropos.Plugin: RowShowSum class has no methods"+      methodFullTy = piResultTys (varType repShowsPrecSumId) tys+      (_, _, methodInDictTy) = splitFunTy methodFullTy+      (tyVars, tauTy) = splitForAllTyCoVars methodInDictTy+      (argTys, _) = splitFunTys tauTy+      scaledPrecTy = argTys !! 0+      scaledRTy    = argTys !! 1++  precName <- unsafeLiftTcM $ newName (mkVarOcc "p")+  rName <- unsafeLiftTcM $ newName (mkVarOcc "r")+  let precVar = mkLocalId precName (scaledMult scaledPrecTy) (scaledThing scaledPrecTy)+      rVar    = mkLocalId rName (scaledMult scaledRTy) (scaledThing scaledRTy)++      kATy   = mkTyVarTy (tyVars !! 0)+      fTy    = mkTyVarTy (tyVars !! 1)+      aTy    = mkTyVarTy (tyVars !! 2)+      kRowTy = typeKind rowTy++      -- Unpack RowRep wrapper: unRowRep r+      unRowRepTypeArgs = [Type kRowTy, Type kATy, Type fTy, Type rTy, Type rowTy, Type aTy]+      rep = mkCoreApps (Var (psUnRowRep state)) (unRowRepTypeArgs ++ [Var rVar])++      repTypeArgs = [Type kATy, Type fTy, Type aTy]+      tag = mkCoreApps (Var (psRepTag state)) (repTypeArgs ++ [rep])++      spaceShowS  = mkCoreApps (Var (psShowChar state)) [mkCharExpr ' ']+      compFn f g = mkCoreApps (Var (psComp state)) [Type stringTy, Type stringTy, Type stringTy, f, g]++  -- Spawn wanted Show constraints for every field of every constructor+  ctorWanteds <- forM constructors $ \(i, conNameFS, conRowTy) -> do+    let fields = walkRowWithTypes conRowTy+    fWanteds <- forM fields $ \(fi, _nameFS, fieldTy) -> do+      ev <- newWanted loc (mkAppTy (mkTyConTy (classTyCon (psShowCls state))) fieldTy)+      pure (fi, fieldTy, ev)+    pure (i, conNameFS, fWanteds)++  let showField fi fieldTy ev =+        let fieldAtTypeArgs = [Type kATy, Type fTy, Type aTy, Type fieldTy]+            idxExpr = mkIntExpr fi+            raw = mkCoreApps (Var (psFieldAt state)) (fieldAtTypeArgs ++ [idxExpr, rep])+            fFieldTy = mkAppTy fTy fieldTy+            val = mkCoreApps (Var (psNoInlineCo state)) [Type fFieldTy, Type fieldTy, raw]+            showDict = ctEvExpr ev+            zeroPrec = mkIntExpr 0+        in mkCoreApps (Var (psShowsPrecMeth state)) [Type fieldTy, showDict, zeroPrec, val]++      showConFields conNameFS fWanteds = do+        let conName = unpackFS conNameFS+        prefixExpr <- unsafeLiftTcM $ mkStringExpr (conName ++ " ")+        let prefixShowS = mkCoreApps (Var (psShowString state)) [prefixExpr]+            fieldShows = [ showField fi fieldTy ev | (fi, fieldTy, ev) <- fWanteds ]+            showParts = case fieldShows of+              [] -> [prefixShowS]+              (f0 : fs) -> prefixShowS : f0 : concatMap (\f -> [spaceShowS, f]) fs+        pure $ foldr1 compFn showParts++  -- Synthesize recursive branch dispatcher: if tag == i then showConFields else buildTree (rest)+  let buildTree _tagExpr [] = do+        errorPrefix <- unsafeLiftTcM $ mkStringExpr "??? "+        pure $ mkCoreApps (Var (psShowString state)) [errorPrefix]+      buildTree tagExpr ((i, conNameFS, fWanteds) : rest) = do+        let iLit = mkWordExpr (fromIntegral i)+            cond = mkCoreApps (Var (psEqClass state)) [Type (mkTyConTy wordTyCon), Var (psFEqWord state), tagExpr, iLit]+        trueBranch <- showConFields conNameFS fWanteds+        falseBranch <- buildTree tagExpr rest+        pure $ mkIfThenElse cond trueBranch falseBranch++  bodyExpr <- buildTree tag ctorWanteds+  let repShowsPrecSumExpr = mkCoreLams (tyVars ++ [precVar, rVar]) bodyExpr++      dictExpr = evDataConApp (classDataCon cls) tys [scEvidence, repShowsPrecSumExpr]+      allNewWanteds = [ mkNonCanonical ev | (_, _, fWanteds) <- ctorWanteds, (_, _, ev) <- fWanteds ]++  pure $ Left ((EvExpr dictExpr, ct), allNewWanteds)++-------------------------------------------------------------------------------+-- HasField solver+-------------------------------------------------------------------------------++-- | Solves GHC's 'HasField' class for records, enabling standard dot-syntax selection+-- (@rec.fieldName@) via literal slot offsets without runtime hash lookups.+--+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+-- See Note [Human-Centric TypeError Diagnostics & Fuzzy Matching] [ref:note-typeerror-diagnostics]+-- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+--+-- Architectural Blueprint:+-- 1. Structural Verification:+--    Ensures the target record is a 'RowRep' with flavour 'ProductRowT' or 'ProductRowHKDT'.+-- 2. Slot Offset Lookup:+--    Finds 0-based index 'i' and field type 'actualFieldTy' from 'rowTy'.+-- 3. Selector Lambda Synthesis:+--    Synthesizes the Core selector lambda:+--    @getField = \rec -> noInlineUnsafeCo (fieldAt @i (unRowRep rec))@+-- 4. Functor Transparency:+--    Accepts both bare field types and functor-wrapped field types ('fFieldTy'), allowing+--    'HasField' to operate transparently on both standard 'Record' and higher-kinded 'RecordF'.+-- 5. Diagnostic Recovery & Dummy Dictionary:+--    If the field is missing or has a type mismatch, emits a custom 'TypeError' and returns+--    a safe dummy dictionary ('mkDummyHasFieldDict') to prevent downstream cascading errors.+solveHasField+  :: PluginState+  -> Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveHasField state ct cls tys = do+  let len = length tys+  if len >= 3 then do+    let fieldTy = last tys+        recTy   = tys !! (len - 2)+        nTy     = tys !! (len - 3)+        loc     = ctLoc ct+    case isStrLitTy (unwrapSynonyms nTy) of+      Just fieldName -> do+        case splitTyConApp_maybe (unwrapSynonyms recTy) of+          Just (tc, args)+            | occNameString (getOccName tc) == "RowRep"+            , length args >= 4 -> do+              let aTy   = last args+                  rowTy = args !! (length args - 2)+                  rTy   = args !! (length args - 3)+                  fTy   = args !! (length args - 4)+                  kATy  = typeKind aTy+                  kRowTy = typeKind rowTy+              case splitTyConApp_maybe (unwrapSynonyms rTy) of+                Just (tcR, []) | occNameString (getOccName tcR) `elem` ["ProductRowT", "ProductRowHKDT"] -> do+                  case findFieldType fieldName rowTy of+                    Just (i, actualFieldTy) -> do+                      -- Locate getField method and bind record argument: \rec -> ...+                      let getFieldId = case classMethods cls of+                            (m : _) -> m+                            [] -> error "Polytropos.Plugin: HasField has no methods"+                          methodFullTy = piResultTys (varType getFieldId) tys+                          (_, _, methodInDictTy) = splitFunTy methodFullTy+                          (tyVars, tauTy) = splitForAllTyCoVars methodInDictTy+                          (argTys, _) = splitFunTys tauTy+                          scaledRTy = argTys !! 0++                      rName <- unsafeLiftTcM $ newName (mkVarOcc "rec")+                      let rVar = mkLocalId rName (scaledMult scaledRTy) (scaledThing scaledRTy)++                          unRowRepTypeArgs = [Type kRowTy, Type kATy, Type fTy, Type rTy, Type rowTy, Type aTy]+                          rep = mkCoreApps (Var (psUnRowRep state)) (unRowRepTypeArgs ++ [Var rVar])++                          fieldAtTypeArgs = [Type kATy, Type fTy, Type aTy, Type actualFieldTy]+                          idxExpr = mkIntExpr i+                          raw = mkCoreApps (Var (psFieldAt state)) (fieldAtTypeArgs ++ [idxExpr, rep])++                          -- Verify type compatibility (bare or wrapped in field functor f)+                          fFieldTy = mkAppTy fTy actualFieldTy+                          validTy  = fieldTy `eqType` actualFieldTy+                                  || fieldTy `eqType` fFieldTy+                          val = mkCoreApps (Var (psNoInlineCo state)) [Type fFieldTy, Type fieldTy, raw]++                          getFieldExpr = mkCoreLams (tyVars ++ [rVar]) val+                          dictExpr = evDataConApp (classDataCon cls) tys [getFieldExpr]++                      if validTy+                        then+                          pure $ Left ((EvExpr dictExpr, ct), [])+                        else if isClosedType fieldTy+                          then do+                            -- Field exists but context requested incompatible type: emit diagnostic+                            let diagLines =+                                  [ "Polytropos Record Error:"+                                  , "  Field '" ++ unpackFS fieldName ++ "' in record has type:"+                                  , "    " ++ showSDocUnsafe (ppr actualFieldTy)+                                  , "  but context expected:"+                                  , "    " ++ showSDocUnsafe (ppr fieldTy)+                                  ]+                            errCt <- mkTypeErrorCt state loc diagLines+                            pure $ Left ((EvExpr dictExpr, ct), [errCt])+                          else do+                            -- Context type is not closed (e.g. unbound type variable alpha in GHCi):+                            -- Emit nominal equality constraint to determine the result type+                            -- and prevent GHCi defaulting alpha to ().+                            let targetTy = case splitAppTy_maybe fieldTy of+                                  Just (h, _) | h `eqType` fTy -> fFieldTy+                                  _                            -> actualFieldTy+                            eqEv <- newWanted loc (mkEqPredRole Nominal fieldTy targetTy)+                            pure $ Left ((EvExpr dictExpr, ct), [mkNonCanonical eqEv])+                    Nothing -> do+                      -- Field not found: emit fuzzy typo suggestions and dummy HasField dictionary+                      case walkRowWithTypes_maybe rowTy of+                        Just fields -> do+                          dummyDict <- mkDummyHasFieldDict state cls tys+                          let fNames = [ unpackFS n | (_, n, _) <- fields, not (nullFS n) ]+                              diagLines =+                                [ "Polytropos Record Error:"+                                , "  Field '" ++ unpackFS fieldName ++ "' does not exist in record:"+                                , "    " ++ formatRecordRow fields+                                , "  " ++ formatSuggestion (unpackFS fieldName) fNames+                                ]+                          errCt <- mkTypeErrorCt state loc diagLines+                          pure $ Left ((dummyDict, ct), [errCt])+                        Nothing -> pure $ Right () -- Open row tail: defer solving+                _ -> pure $ Right ()+          _ -> pure $ Right ()+      Nothing -> pure $ Right ()+  else pure $ Right ()++-------------------------------------------------------------------------------+-- AllFields solver (generic field-class dictionary supply)+-------------------------------------------------------------------------------++-- | Solves 'AllFields' by synthesizing a flat array of type-erased 'DictAny' dictionaries.+--+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+--+-- Architectural Blueprint:+-- 1. Row Schema Inspection:+--    Verifies the row is closed and extracts all field types.+-- 2. Per-Field Wanted Dicts:+--    Spawns a wanted constraint @c fieldTy@ for every field in the row.+-- 3. Type Erasure & Packing:+--    Wraps each evidence dictionary in 'mkDictAny @c @fieldTy dict', casting each heterogeneous+--    instance to the uniform type-erased carrier @DictAny c@.+-- 4. Contiguous Array Construction:+--    Constructs a Core list of type-erased dictionaries and wraps it via 'evidenceAllFields',+--    producing a flat 'SmallArray (DictAny c)' at runtime. This allows combinators like+--    'cmapRecord' and 'cfoldMapRecord' to iterate over fields in O(N) time with zero+--    typeclass overhead!+solveAllFields+  :: PluginState+  -> Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveAllFields state ct cls tys+  | length tys >= 3+  , let rowTy = tys !! (length tys - 2)+  , Just _ <- myExtractPromotedList (unwrapSynonyms rowTy)+  = do+      let cTy    = last tys+          rTy    = tys !! (length tys - 3)+          fields = walkRowWithTypes rowTy+          loc    = ctLoc ct+          dictAnyTy = mkAppTy (mkTyConTy (psDictAnyTyCon state)) cTy++      -- For each field, create a new wanted constraint for (c fieldTy)+      wanteds <- forM fields $ \(_i, _nameFS, fieldTy) -> do+        ev <- newWanted loc (mkAppTy cTy fieldTy)+        pure (fieldTy, ev)++      -- For each field, construct: mkDictAny @c @fieldTy dict+      let dictAnys = [ mkCoreApps (Var (psMkDictAny state))+                                  [Type cTy, Type fieldTy, ctEvExpr ev]+                     | (fieldTy, ev) <- wanteds+                     ]++      -- Construct: evidenceAllFields @c [dictAny_0, dictAny_1, ...]+      let listExpr = mkListExpr dictAnyTy dictAnys+          arrExpr  = mkCoreApps (Var (psEvidenceAllFields state)) [Type cTy, listExpr]++      -- Superclass evidence for RowFlavour r+      let scEvidence = evDataConApp (classDataCon (psRowFlavourCls state)) [rTy] []++      -- Class dictionary: AllFields r row c+      let dictExpr = evDataConApp (classDataCon cls) tys [scEvidence, arrExpr]+          newWanteds = [mkNonCanonical ev | (_fieldTy, ev) <- wanteds]++      pure $ Left ((EvExpr dictExpr, ct), newWanteds)+  | otherwise = pure $ Right ()++-------------------------------------------------------------------------------+-- SubRow and SubSum solvers+--+-- See Note [SubRow and SubSum Projection and Narrowing Evidence] [ref:note-subrow-subsum]+-- See Note [SubRow and SubSum Interior Mechanics: Matchers and Witness Generation] [ref:note-subrow-subsum-mechanics]+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+-- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+-------------------------------------------------------------------------------++-- | Solves the 'SubRow sub super' constraint by synthesizing literal index projection lists.+--+-- Intuition:+-- A sub-record 'sub' can be projected out of a super-record 'super' if every field+-- declared in 'sub' also exists in 'super' with an identical type.+--+-- Implementation Phases:+-- 1. Extract and unwrap the row types 'subTy' and 'superTy'.+-- 2. Traverse both rows using 'walkRowWithTypes_maybe'. If either row has an unfixed tail,+--    we return 'Right ()' (defer) because full field complements are not yet known.+-- 3. Run 'matchFields' to find the 0-based offset of each sub-field in the super-record.+-- 4. If all match: synthesize a literal Core list '[Int]' containing the projection indices.+-- 5. If matching fails: invoke 'findSubRowMismatch' to pinpoint whether a field is missing+--    or has a type discrepancy, synthesize a custom 'TypeError' wanted constraint, and+--    discharge the original constraint with dummy evidence to stop error cascading.+solveSubRow+  :: PluginState+  -> Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveSubRow state ct cls tys+  | length tys >= 2+  , let subTy   = tys !! (length tys - 2)+  , let superTy = last tys+  , let loc     = ctLoc ct+  , Just subFields   <- walkRowWithTypes_maybe subTy+  , Just superFields <- walkRowWithTypes_maybe superTy+  = case matchFields subFields superFields of+      Just indices -> do+        -- Successful match: compile literal index list [Int] into Core AST:+        -- evidenceSubRow :: [Int] -> DictSubRow k sub super+        let indicesExpr = mkListExpr intTy (map mkIntExpr indices)+            dictExpr    = evDataConApp (classDataCon cls) tys [indicesExpr]+        pure $ Left ((EvExpr dictExpr, ct), [])+      Nothing -> do+        -- Structural mismatch: diagnose failure and synthesize custom TypeError.+        -- We emit a dummy dictionary so GHC does not cascade secondary errors.+        let dummyDict = evDataConApp (classDataCon cls) tys [mkListExpr intTy []]+            mismatchDiag = findSubRowMismatch subFields superFields+        errCt <- mkTypeErrorCt state loc mismatchDiag+        pure $ Left ((EvExpr dummyDict, ct), [errCt])+  | otherwise = pure $ Right ()+  where+    -- | Recursive field matcher:+    -- For each field '(name, fieldTy)' in the sub-record:+    -- 1. Look for a field '(j, sName, sFieldTy)' in 'superFields'.+    -- 2. Names match if they are equal, or if either is anonymous ('nullFS', for positional tuples).+    -- 3. Field types must be strictly equal under GHC's 'eqType'.+    -- 4. If found, record index 'j' and continue for the remainder of 'subFields'.+    -- 5. If any sub-field is missing or has a type mismatch, return 'Nothing'.+    matchFields :: [(Int, FastString, Type)] -> [(Int, FastString, Type)] -> Maybe [Int]+    matchFields [] _ = Just []+    matchFields ((_, name, fieldTy) : rest) sFields =+      case [ j | (j, sName, sFieldTy) <- sFields+               , (if nullFS name || nullFS sName then True else sName == name)+               , fieldTy `eqType` sFieldTy ] of+        (j : _) -> (j :) <$> matchFields rest sFields+        []      -> Nothing++    -- | Diagnostic generator for SubRow failure:+    -- Pinpoints the exact reason why sub-record projection failed:+    -- - Case A: A required field is missing in the super-record. We list the available fields+    --   and format fuzzy Levenshtein suggestions ("Did you mean: 'name'?").+    -- - Case B: The field name exists, but its type does not match. We print both types side-by-side.+    findSubRowMismatch :: [(Int, FastString, Type)] -> [(Int, FastString, Type)] -> [String]+    findSubRowMismatch [] _ =+      [ "Polytropos SubRow Error:"+      , "  Sub-record row does not match super-record row."+      ]+    findSubRowMismatch ((_, name, fieldTy) : rest) sFields =+      case [ sFieldTy | (_, sName, sFieldTy) <- sFields+                      , if nullFS name || nullFS sName then True else sName == name ] of+        [] ->+          let sNames = [ unpackFS n | (_, n, _) <- sFields, not (nullFS n) ]+          in [ "Polytropos SubRow Error:"+             , "  Cannot project record: field '" ++ unpackFS name ++ "' from sub-record is missing in super-record:"+             , "    " ++ formatRecordRow sFields+             , "  " ++ formatSuggestion (unpackFS name) sNames+             ]+        (sFieldTy : _)+          | not (fieldTy `eqType` sFieldTy) ->+              [ "Polytropos SubRow Error:"+              , "  Cannot project record: field '" ++ unpackFS name ++ "' has type:"+              , "    " ++ showSDocUnsafe (ppr fieldTy)+              , "  in sub-record, but has type:"+              , "    " ++ showSDocUnsafe (ppr sFieldTy)+              , "  in super-record."+              ]+          | otherwise -> findSubRowMismatch rest sFields++-- | Solves the 'SubSum sub super' constraint by synthesizing literal injection and narrowing arrays.+--+-- Intuition:+-- A sub-variant 'sub' can be widened into a super-variant 'super' if every constructor+-- declared in 'sub' also exists in 'super' with an identical payload schema.+--+-- Dual Operations Synthesized in a Single Witness:+-- 1. Widening (Injection): maps each constructor tag in 'sub' to its corresponding tag in 'super'.+--    This mapping is total: 'injectIndices :: [Word]'.+-- 2. Narrowing (Projection): maps each constructor tag in 'super' back to its tag in 'sub'+--    (or 'Nothing' if the active constructor is not present in 'sub').+--    This mapping is partial: 'narrowIndices :: [Maybe Word]'.+solveSubSum+  :: PluginState+  -> Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveSubSum state ct cls tys+  | length tys >= 2+  , let subTy   = tys !! (length tys - 2)+  , let superTy = last tys+  , let loc     = ctLoc ct+  , Just subCons   <- walkSumRowWithTypes_maybe subTy+  , Just superCons <- walkSumRowWithTypes_maybe superTy+  = case matchCons subCons superCons of+      Just injectIndices -> do+        let wordTy = mkTyConTy wordTyCon+            -- Core list of Word: [Word]+            injectExpr = mkListExpr wordTy (map mkWordExpr injectIndices)++            -- Build the narrowing table: for every constructor in 'superCons',+            -- check if it exists in 'subCons'. If yes -> Just subIdx; if no -> Nothing.+            narrowIndices =+              [ case [ fromIntegral i :: Word+                     | (i, sName, sConRowTy) <- subCons+                     , (if nullFS sName || nullFS superName then True else sName == superName)+                     , sameRow sConRowTy superConRowTy+                     ] of+                  (subIdx : _) -> Just subIdx+                  []           -> Nothing+              | (_j, superName, superConRowTy) <- superCons+              ]++            -- Core list of Maybe Word: [Maybe Word]+            maybeWordTy = mkAppTy (mkTyConTy maybeTyCon) wordTy+            narrowDataExpr Nothing = mkCoreConApps nothingDataCon [Type wordTy]+            narrowDataExpr (Just w) = mkCoreConApps justDataCon [Type wordTy, mkWordExpr w]+            narrowExpr = mkListExpr maybeWordTy (map narrowDataExpr narrowIndices)++            -- Evidence term: DictSubSum [Word] [Maybe Word]+            dictExpr = evDataConApp (classDataCon cls) tys [injectExpr, narrowExpr]+        pure $ Left ((EvExpr dictExpr, ct), [])+      Nothing -> do+        -- Constructor mismatch: generate custom diagnostic and return dummy dictionary.+        let wordTy = mkTyConTy wordTyCon+            maybeWordTy = mkAppTy (mkTyConTy maybeTyCon) wordTy+            dummyDict = evDataConApp (classDataCon cls) tys [mkListExpr wordTy [], mkListExpr maybeWordTy []]+            mismatchDiag = findSubSumMismatch subCons superCons+        errCt <- mkTypeErrorCt state loc mismatchDiag+        pure $ Left ((EvExpr dummyDict, ct), [errCt])+  | otherwise = pure $ Right ()+  where+    -- | Constructor matcher:+    -- Verifies that every constructor in 'subCons' exists in 'sCons' with an identical+    -- payload row (checked via 'sameRow'), and collects the super-variant tag 'j'.+    matchCons :: [(Int, FastString, Type)] -> [(Int, FastString, Type)] -> Maybe [Word]+    matchCons [] _ = Just []+    matchCons ((_, conName, conRowTy) : rest) sCons =+      case [ j | (j, sName, sRowTy) <- sCons+               , (if nullFS conName || nullFS sName then True else sName == conName)+               , sameRow conRowTy sRowTy ] of+        (j : _) -> (fromIntegral j :) <$> matchCons rest sCons+        []      -> Nothing++    -- | Deep structural comparison of constructor payload rows:+    -- 1. Fast path: check syntactic equality via 'eqType'.+    -- 2. Slow path: unroll both rows via 'walkRowWithTypes_maybe'. Assert identical arity,+    --    matching field names, and pairwise 'eqType' equality on every payload slot.+    sameRow r1 r2+      | r1 `eqType` r2 = True+      | Just fs1 <- walkRowWithTypes_maybe r1+      , Just fs2 <- walkRowWithTypes_maybe r2+      = length fs1 == length fs2 &&+        and [ (if nullFS n1 || nullFS n2 then True else n1 == n2) && t1 `eqType` t2 | ((_, n1, t1), (_, n2, t2)) <- zip fs1 fs2 ]+      | otherwise = False++    -- | Diagnostic generator for SubSum failure:+    -- Distinguishes between:+    -- - Missing constructor in super-variant (with fuzzy typo suggestions).+    -- - Payload row mismatch (displaying both constructor payload schemas).+    findSubSumMismatch :: [(Int, FastString, Type)] -> [(Int, FastString, Type)] -> [String]+    findSubSumMismatch [] _ =+      [ "Polytropos SubSum Error:"+      , "  Sub-variant row does not match super-variant row."+      ]+    findSubSumMismatch ((_, conName, conRowTy) : rest) sCons =+      case [ sRowTy | (_, sName, sRowTy) <- sCons+                    , if nullFS conName || nullFS sName then True else sName == conName ] of+        [] ->+          let sNames = [ unpackFS n | (_, n, _) <- sCons, not (nullFS n) ]+          in [ "Polytropos SubSum Error:"+             , "  Cannot widen variant: constructor '" ++ unpackFS conName ++ "' from sub-variant is missing in super-variant:"+             , "    " ++ formatVariantRow sCons+             , "  " ++ formatCtorSuggestion (unpackFS conName) sNames+             ]+        (sRowTy : _)+          | not (sameRow conRowTy sRowTy) ->+              let subFs   = walkRowWithTypes conRowTy+                  superFs = walkRowWithTypes sRowTy+              in [ "Polytropos SubSum Error:"+                 , "  Cannot widen variant: constructor '" ++ unpackFS conName ++ "' has different payload rows:"+                 , "    sub-variant payload:   " ++ formatRecordRow subFs+                 , "    super-variant payload: " ++ formatRecordRow superFs+                 ]+          | otherwise -> findSubSumMismatch rest sCons++-------------------------------------------------------------------------------+-- KnownHash solver+-------------------------------------------------------------------------------++-- | FNV-1a 64-bit hash for a type-level label symbol.+--+-- Algorithmic Details:+-- - Uses the standard Fowler-Noll-Vo 64-bit non-cryptographic hash algorithm (FNV-1a).+-- - Constants:+--   * offset_basis = 14695981039346656037 (0xcbf29ce484222325)+--   * prime        = 1099511628211        (0x100000001b3)+-- - Executes in microsecond compile-time: folds over characters in 'fs', XORing with the+--   accumulator and multiplying by the 64-bit prime modulo \(2^{64}\).+-- - Yields uniform distribution with effectively zero collision probability across+--   domain record labels.+fnv1a64FS :: FastString -> Word+fnv1a64FS fs = fromIntegral (foldl' step (14695981039346656037 :: Word64) (unpackFS fs))+  where+    step !h !c = (h `xor` fromIntegral (ord c)) * 1099511628211++-- | Solves the 'KnownHash' constraint by computing the compile-time 64-bit FNV-1a hash+-- of a type-level Symbol and emitting literal Word evidence.+--+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+--+-- Mechanics:+-- 1. Extracts the type-level symbol 'sTy'.+-- 2. Evaluates its string value via 'isStrLitTy' on the synonym-unwrapped type.+-- 3. Computes the 64-bit FNV-1a hash at compile time via 'fnv1a64FS'.+-- 4. Emits a literal Word expression 'mkWordExpr h' wrapped in the 'KnownHash' dictionary.+-- 5. Enables users to perform O(1) integer branch dispatch and HAMT indexing without+--    paying for runtime string hashing or KnownSymbol reflection.+solveKnownHash+  :: Ct+  -> Class+  -> [Type]+  -> TcPluginM 'Solve (Either (EvTerm, Ct) ())+solveKnownHash ct cls tys = do+  let mSTy = case tys of+        [s]    -> Just s+        [_, s] -> Just s+        _      -> Nothing+  case mSTy of+    Just sTy -> case isStrLitTy (unwrapSynonyms sTy) of+      Just fs -> do+        let h = fnv1a64FS fs+            wExpr = mkWordExpr h+            dictExpr = evDataConApp (classDataCon cls) tys [wExpr]+        pure $ Left (EvExpr dictExpr, ct)+      Nothing -> pure $ Right ()+    Nothing -> pure $ Right ()++-------------------------------------------------------------------------------+-- Row walking & schema extraction helpers+-------------------------------------------------------------------------------++-- | Walks a record row type to extract its field schema.+-- Returns 'Nothing' if the row tail is unfixed or open (deferring solving until+-- the row tail is unified by downstream inference).+--+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+-- See Note [OCaml Subtype/Unify Correlation and Row Tail Algebra] [ref:note-ocaml-row-algebra]+walkRowWithTypes_maybe :: Type -> Maybe [(Int, FastString, Type)]+walkRowWithTypes_maybe rowTy = do+  xs <- myExtractPromotedList (unwrapSynonyms rowTy)+  zipWithM extractField [0..] xs+  where+    extractField i elemTy =+      case splitTyConApp_maybe (unwrapSynonyms elemTy) of+        Just (_, args)+          | length args >= 2+          , let nameTy = args !! (length args - 2)+          , let fieldTy = args !! (length args - 1)+          , Just n <- isStrLitTy (unwrapSynonyms nameTy)+          -> Just (i, n, fieldTy)+        _ -> Just (i, nilFS, elemTy)++-- | Walks a variant sum row type to extract its constructor schema.+-- Returns 'Nothing' if the row tail is unfixed or open.+--+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+-- See Note [OCaml Subtype/Unify Correlation and Row Tail Algebra] [ref:note-ocaml-row-algebra]+walkSumRowWithTypes_maybe :: Type -> Maybe [(Int, FastString, Type)]+walkSumRowWithTypes_maybe rowTy = do+  xs <- myExtractPromotedList (unwrapSynonyms rowTy)+  zipWithM extractCon [0..] xs+  where+    extractCon i elemTy =+      case splitTyConApp_maybe (unwrapSynonyms elemTy) of+        Just (_, args)+          | length args >= 2+          , let nameTy = args !! (length args - 2)+          , let conRowTy = args !! (length args - 1)+          , Just n <- isStrLitTy (unwrapSynonyms nameTy)+          -> Just (i, n, conRowTy)+        _ -> Just (i, nilFS, elemTy)++-- | Fully unrolls GHC type synonyms to expose the underlying type constructor.+-- Uses 'coreView' recursively until no further synonyms can be stripped.+unwrapSynonyms :: Type -> Type+unwrapSynonyms ty = case coreView ty of+  Just ty' -> unwrapSynonyms ty'+  Nothing  -> ty++-- | Extracts elements from a promoted type-level list (@'[a, b, c]@).+--+-- Invariants:+-- - Returns 'Just [a, b, c]' for closed lists terminating in @'[]@.+-- - Returns 'Nothing' if the list terminates in a type variable (an open row tail)+--   or an unreduced type family application. This signals to TcPlugin solvers that+--   the row is still open, prompting them to defer solving safely.+--+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+-- See Note [OCaml Subtype/Unify Correlation and Row Tail Algebra] [ref:note-ocaml-row-algebra]+myExtractPromotedList :: Type -> Maybe [Type]+myExtractPromotedList ty = case splitTyConApp_maybe (unwrapSynonyms ty) of+  Just (tc, [_, x, xs]) | occNameString (getOccName tc) == ":" -> do+    rest <- myExtractPromotedList xs+    return (x : rest)+  Just (tc, [_]) | occNameString (getOccName tc) == "[]" -> Just []+  _ -> Nothing++-- | Pure version of 'walkRowWithTypes_maybe' that defaults open tails to '[]'.+walkRowWithTypes :: Type -> [(Int, FastString, Type)]+walkRowWithTypes rowTy =+  case myExtractPromotedList (unwrapSynonyms rowTy) of { Just xs -> zipWith extractField [0..] xs; Nothing -> [] }+  where+    extractField i elemTy =+      case splitTyConApp_maybe (unwrapSynonyms elemTy) of+        Just (_, args)+          | length args >= 2+          , let nameTy = args !! (length args - 2)+          , let fieldTy = args !! (length args - 1)+          , Just n <- isStrLitTy (unwrapSynonyms nameTy)+          -> (i, n, fieldTy)+        _ -> (i, nilFS, elemTy)++-- | Pure version of 'walkSumRowWithTypes_maybe' that defaults open tails to '[]'.+walkSumRowWithTypes :: Type -> [(Int, FastString, Type)]+walkSumRowWithTypes rowTy =+  case myExtractPromotedList (unwrapSynonyms rowTy) of { Just xs -> zipWith extractCon [0..] xs; Nothing -> [] }+  where+    extractCon i elemTy =+      case splitTyConApp_maybe (unwrapSynonyms elemTy) of+        Just (_, args)+          | length args >= 2+          , let nameTy = args !! (length args - 2)+          , let conRowTy = args !! (length args - 1)+          , Just n <- isStrLitTy (unwrapSynonyms nameTy)+          -> (i, n, conRowTy)+        _ -> (i, nilFS, elemTy)++-- | Find 0-based constructor tag by name in a sum row.+findConstructorIndex :: FastString -> Type -> Maybe Word+findConstructorIndex conName rowTy =+  case [fromIntegral i | (i, n, _) <- walkSumRowWithTypes rowTy, n == conName] of+    (w : _) -> Just w+    []      -> Nothing++-- | Find 0-based field index by matching field payload type.+findFieldIndexByType :: Type -> Type -> Maybe Int+findFieldIndexByType targetTy rowTy =+  case [i | (i, _, ty) <- walkRowWithTypes rowTy, targetTy `eqType` ty] of+    (i : _) -> Just i+    []      -> Nothing++-- | Find 0-based constructor tag by matching constructor payload type.+findConstructorIndexByType :: Type -> Type -> Maybe Word+findConstructorIndexByType targetTy rowTy =+  case [fromIntegral i | (i, _, ty) <- walkSumRowWithTypes rowTy, targetTy `eqType` ty] of+    (w : _) -> Just w+    []      -> Nothing++-- | Find 0-based field index and field type by name in a product row.+findFieldType :: FastString -> Type -> Maybe (Int, Type)+findFieldType fieldName rowTy =+  case [(i, ty) | (i, n, ty) <- walkRowWithTypes rowTy, n == fieldName] of+    (res : _) -> Just res+    []      -> Nothing++-------------------------------------------------------------------------------+-- Utilities+-------------------------------------------------------------------------------++-- | Construct a boxed Int Core expression from an Int value.+--+-- Generates: 'GHC.Types.I# <literal>'+-- Used by TcPlugin to emit literal 0-based slot offsets into dictionary evidence.+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+mkIntExpr :: Int -> CoreExpr+mkIntExpr i = mkCoreConApps intDataCon [Lit (LitNumber LitNumInt (toInteger i))]++-- | Construct a boxed Word Core expression from a Word value.+--+-- Generates: 'GHC.Types.W# <literal>'+-- Used by TcPlugin to emit literal 0-based constructor tags into dictionary evidence.+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+mkWordExpr :: Word -> CoreExpr+mkWordExpr w = mkCoreConApps wordDataCon [Lit (LitNumber LitNumWord (toInteger w))]

@@ -0,0 +1,246 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-}++#if __GLASGOW_HASKELL__ >= 914+{-# OPTIONS_GHC -Wno-pattern-namespace-specifier #-}+#endif++-- | Compatibility layer for GHC 9.6 through 9.14.+--+-- Isolates all compiler AST and builtin namespace churn behind a uniform+-- interface, keeping the solver and source desugaring logic clean.+module Polytropos.Plugin.Compat+  ( modBase+  , modShow+  , modRecords+  , CompatRecUpdField+  , matchRecordUpd+  , extractRecUpdField+  , pattern PrefixConPat+  , stripHsPar+  , polyLabel+  , mkPolytroposImportDecl+  , mkHsApp+  , mkTupArg+  , mkLambda+  ) where++import GHC.Unit.Types+  ( mkModule+  , moduleUnit+  )++import GHC.Plugins+  ( Module+  , FastString+  , unLoc+  , mkModuleName+  , rdrNameOcc+  , occNameFS+  , RawPkgQual(..)+  )++import GHC.Hs.Extension+  ( GhcPs+  )++import GHC.Hs+  ( LHsExpr+  , LHsRecUpdField+  , LImportDecl+  , ImportDecl(..)+  , ImportDeclQualifiedStyle(..)+  , IsBootInterface(..)+  , noAnn+  , noLocA+#if __GLASGOW_HASKELL__ >= 910+  , noExtField+#endif+  , HsExpr(..)+  , HsFieldBind(..)+  , HsConDetails(..)+  , LPat+  , mkHsLam+#if __GLASGOW_HASKELL__ >= 908+  , LHsRecUpdFields(..)+#endif+#if __GLASGOW_HASKELL__ >= 914+  , ImportDeclLevelStyle(..)+#endif+#if __GLASGOW_HASKELL__ >= 912+  , FieldOcc(..)+#else+  , AmbiguousFieldOcc(..)+#endif+  )++import Language.Haskell.Syntax.Expr+  ( HsTupArg(..)+  )++import GHC.Hs.ImpExp+  ( XImportDeclPass(..)+  )++import GHC.Types.SourceText+  ( SourceText(..)+  )++#if __GLASGOW_HASKELL__ >= 910+import GHC.Builtin.Names+  ( gHC_INTERNAL_BASE+  , gHC_INTERNAL_SHOW+  )+#else+import GHC.Builtin.Names+  ( gHC_BASE+  , gHC_SHOW+  )+#endif++-------------------------------------------------------------------------------+-- Module locations for base / show / records+-------------------------------------------------------------------------------++-- | Location of GHC.Base (or GHC.Internal.Base in 9.10+)+modBase :: Module+#if __GLASGOW_HASKELL__ >= 910+modBase = gHC_INTERNAL_BASE+#else+modBase = gHC_BASE+#endif++-- | Location of GHC.Show (or GHC.Internal.Show in 9.10+)+modShow :: Module+#if __GLASGOW_HASKELL__ >= 910+modShow = gHC_INTERNAL_SHOW+#else+modShow = gHC_SHOW+#endif++-- | Location of GHC.Records (or GHC.Internal.Records in 9.10+)+modRecords :: Module+#if __GLASGOW_HASKELL__ >= 910+modRecords = mkModule (moduleUnit modBase) (mkModuleName "GHC.Internal.Records")+#else+modRecords = mkModule (moduleUnit modBase) (mkModuleName "GHC.Records")+#endif++-------------------------------------------------------------------------------+-- Record Update Compatibility (GHC 9.6 vs 9.8 vs 9.14)+-------------------------------------------------------------------------------++#if __GLASGOW_HASKELL__ >= 908+type CompatRecUpdField = LHsRecUpdField GhcPs GhcPs+#else+type CompatRecUpdField = LHsRecUpdField GhcPs+#endif++-- | Extract the updated record expression and fields from RecordUpd.+matchRecordUpd :: HsExpr GhcPs -> Maybe (LHsExpr GhcPs, [CompatRecUpdField])+#if __GLASGOW_HASKELL__ >= 908+matchRecordUpd (RecordUpd _ r (RegularRecUpdFields _ flds)) = Just (r, flds)+matchRecordUpd _ = Nothing+#else+matchRecordUpd (RecordUpd _ r (Left flds)) = Just (r, flds)+matchRecordUpd _ = Nothing+#endif++-- | Extract the label FastString and value expression from a record update field.+extractRecUpdField :: CompatRecUpdField -> (FastString, LHsExpr GhcPs)+#if __GLASGOW_HASKELL__ >= 912+extractRecUpdField (unLoc -> HsFieldBind _ (unLoc -> FieldOcc _ (unLoc -> lbl)) arg _) =+  (occNameFS (rdrNameOcc lbl), arg)+#else+extractRecUpdField (unLoc -> HsFieldBind _ (unLoc -> ambOcc) arg _) =+  let lbl = case ambOcc of+        Unambiguous _ (unLoc -> rdr) -> rdr+        Ambiguous _ (unLoc -> rdr)   -> rdr+  in (occNameFS (rdrNameOcc lbl), arg)+#endif++-------------------------------------------------------------------------------+-- Pattern & Expression AST Compatibility+-------------------------------------------------------------------------------++-- | Pattern synonym matching PrefixCon constructor details across GHC versions.+#if __GLASGOW_HASKELL__ >= 914+pattern PrefixConPat :: [arg] -> HsConDetails arg rec+pattern PrefixConPat args = PrefixCon args+#else+pattern PrefixConPat :: [arg] -> HsConDetails tyarg arg rec+pattern PrefixConPat args <- PrefixCon _ args+  where PrefixConPat args = PrefixCon [] args+#endif++-- | Strip enclosing parenthesis expressions across GHC versions.+stripHsPar :: LHsExpr GhcPs -> LHsExpr GhcPs+#if __GLASGOW_HASKELL__ >= 910+stripHsPar (unLoc -> HsPar _ e) = stripHsPar e+#else+stripHsPar (unLoc -> HsPar _ _ e _) = stripHsPar e+#endif+stripHsPar e = e++-- | Construct an overloaded label expression across GHC 9.6-9.14.+polyLabel :: FastString -> LHsExpr GhcPs+#if __GLASGOW_HASKELL__ >= 912+polyLabel fs = noLocA (HsOverLabel NoSourceText fs)+#elif __GLASGOW_HASKELL__ >= 910+polyLabel fs = noLocA (HsOverLabel noExtField NoSourceText fs)+#else+polyLabel fs = noLocA (HsOverLabel noAnn NoSourceText fs)+#endif++-- | Construct the 'import qualified Polytropos as Polytropos' declaration.+mkPolytroposImportDecl :: LImportDecl GhcPs+#if __GLASGOW_HASKELL__ >= 914+mkPolytroposImportDecl = noLocA $ ImportDecl+  { ideclExt       = XImportDeclPass noAnn NoSourceText False+  , ideclName      = noLocA (mkModuleName "Polytropos")+  , ideclPkgQual   = NoRawPkgQual+  , ideclSource    = NotBoot+  , ideclLevelSpec = NotLevelled+  , ideclSafe      = False+  , ideclQualified = QualifiedPre+  , ideclAs        = Just (noLocA (mkModuleName "Polytropos"))+  , ideclImportList = Nothing+  }+#else+mkPolytroposImportDecl = noLocA $ ImportDecl+  { ideclExt       = XImportDeclPass noAnn NoSourceText False+  , ideclName      = noLocA (mkModuleName "Polytropos")+  , ideclPkgQual   = NoRawPkgQual+  , ideclSource    = NotBoot+  , ideclSafe      = False+  , ideclQualified = QualifiedPre+  , ideclAs        = Just (noLocA (mkModuleName "Polytropos"))+  , ideclImportList = Nothing+  }+#endif++-- | Construct a function application expression across GHC 9.6-9.14.+mkHsApp :: LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs+#if __GLASGOW_HASKELL__ >= 910+mkHsApp f x = noLocA (HsApp noExtField f x)+#else+mkHsApp f x = noLocA (HsApp noAnn f x)+#endif++-- | Construct a tuple present argument across GHC 9.6-9.14.+mkTupArg :: LHsExpr GhcPs -> HsTupArg GhcPs+#if __GLASGOW_HASKELL__ >= 910+mkTupArg e = Present noExtField e+#else+mkTupArg e = Present noAnn e+#endif++-- | Construct a lambda expression across GHC 9.6-9.14.+mkLambda :: [LPat GhcPs] -> LHsExpr GhcPs -> LHsExpr GhcPs+#if __GLASGOW_HASKELL__ >= 912+mkLambda pats body = mkHsLam (noLocA pats) body+#else+mkLambda pats body = mkHsLam pats body+#endif

@@ -0,0 +1,610 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns #-}++#if __GLASGOW_HASKELL__ >= 914+{-# OPTIONS_GHC -Wno-pattern-namespace-specifier #-}+#endif++-- | Source plugin for @polytropos@.+--+-- Desugars ergonomic syntax for row-polymorphic records, open variants,+-- and declaration forms into standard @Polytropos@ runtime combinators+-- before renaming and typechecking:+--+-- 1. __Record Construction:__+--    @REC { x = 1, y = True }@ (bare) and @REC_F { x = Just 1 }@ (HKD)+--    with field punning support.+-- 2. __Variant Injection:__+--    @VAR { Ok = 200 }@ or @VARIANT { Err = "fail" }@.+-- 3. __Record Updates:__+--    @REC_UPD r { x = 42 }@ into 'Polytropos.setField' chains.+-- 4. __Pattern Matching:__+--    @REC { x, y }@ into record view patterns, and+--    @VAR { Tag = pat }@ into variant projection view patterns.+-- 5. __Open Declarations:__+--    @data Person = Person { name :: String, age :: Int } deriving OpenRecord@+--    and @data Status = Active | Inactive String deriving OpenVariant@.+module Polytropos.Plugin.Source+  ( sourcePlugin+  ) where++import Prelude++import Data.Data+  ( Data+  , gmapT+  , Typeable+  , cast+  )+import Data.List+  ( nub+  )+import Data.List.NonEmpty+  ( NonEmpty(..)+  )++import GHC.Plugins+  ( CommandLineOption+  , FastString+  , fsLit+  , Hsc+  , GenLocated(..)+  , unLoc+  , mkRdrQual+  , mkRdrUnqual+  , mkVarOcc+  , mkDataOcc+  , mkModuleName+  , rdrNameOcc+  , occNameString+  , occNameFS+  , moduleNameString+  )++import GHC.Hs.Extension+  ( GhcPs+  )++import GHC.Hs+  ( HsParsedModule(..)+  , HsModule(..)+  , HsExpr(..)+  , Pat(..)+  , HsRecFields(..)+  , HsFieldBind(..)+  , FieldOcc(..)+  , LHsExpr+  , LHsRecField+  , LPat+  , LHsDecl+  , noLocA+  , HsConDetails(..)+  , LImportDecl+  , ImportDecl(..)+  , noAnn+  , noExtField+  , HsDecl(..)+  , TyClDecl(..)+  , HsDataDefn(..)+  , ConDecl(..)+  , DataDefnCons(..)+  , HsDerivingClause(..)+  , DerivClauseTys(..)+  , HsSigType(..)+  , HsType(..)+  )++import Language.Haskell.Syntax.Basic+  ( Boxity(..)+  )++import GHC.Driver.Plugins+  ( ParsedResult(..)+  )++import Polytropos.Plugin.Compat+  ( CompatRecUpdField+  , matchRecordUpd+  , extractRecUpdField+  , pattern PrefixConPat+  , stripHsPar+  , polyLabel+  , mkPolytroposImportDecl+  , mkHsApp+  , mkTupArg+  , mkLambda+  )++{-------------------------------------------------------------------------------+  GHC Notes: Source Plugin Architecture and Rewriting Mechanics+-------------------------------------------------------------------------------++Note [Source Plugin Desugaring Architecture: Syntactic Sugar Before Typechecking]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-source-plugin-arch]+GHC's source plugin hook ('parsedResultAction') operates directly on the untyped,+unrenamed abstract syntax tree ('HsParsedModule') immediately after the parser completes,+prior to the Renamer ('rnExpr') and Typechecker ('tcExpr').++Why desugar at the parsed AST level:+1. Native Syntax Feel:+   Developers write natural record syntax:+     @REC { name = "Alice", age = 30 }@+     @VAR { Ok = 200 }@+     @REC_UPD user { age = 31 }@+   without requiring language extensions that modify the lexical grammar or external+   preprocessors (like CPP or Template Haskell quotes).+2. Elimination of Downstream Complexity:+   By lowering syntactic forms to standard Polytropos combinators ('emptyRecord',+   'insertField', 'setField', 'injectVariant', 'projectVariant', 'recordField') before+   renaming, the GHC Typechecker receives standard Haskell function applications+   and view patterns. The typechecker plugin ('Polytropos.Plugin') can then solve+   the resulting 'FieldIndex', 'ConstructorIndex', and 'SubRow' constraints with+   exact literal evidence.+3. Import Injection:+   Source transformation automatically injects 'import qualified Polytropos as Polytropos'+   into the module's import list ('ensurePolytroposImport'), guaranteeing that all+   generated combinators and types resolve without requiring manual boilerplate imports+   by the user.+4. Source Span Preservation:+   Whenever AST nodes are transformed, annotations and source spans are maintained+   where possible, ensuring that compiler diagnostics and IDE hovers pinpoint the exact+   source locations written by the author.++Note [Open Declarations: Lowering Nominal Declarations to Open Rows]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-open-declarations]+Haskell developers frequently want the ergonomic benefits of declaring a named type+with field names or constructors, but want the resulting values to participate in open,+row-polymorphic operations without boilerplate conversion:++  @data Person = Person { name :: String, age :: Int } deriving OpenRecord@+  @data Status = Active | Inactive String deriving OpenVariant@++GHC's built-in deriving engine would reject 'OpenRecord' and 'OpenVariant' because they+are not built-in deriving strategies. The source plugin solves this via a two-stage process:++Stage 1 (Declaration Harvesting & Scrubbing):+- Scans 'hsmodDecls' for 'DataDecl's containing deriving clauses referencing 'OpenRecord'+  or 'OpenVariant'.+- Extracts the type name and constructor names into 'knownRecs' and 'knownVars'.+- Scrubs (filters out) the 'OpenRecord' and 'OpenVariant' deriving clauses from the AST,+  so GHC's stock deriving engine never sees them.++Stage 2 (Expression and Pattern Interception):+- Expressions:+  * Application of a known record constructor:+    @Person { name = "Alice", age = 30 }@+    is lowered into an open record construction chain:+    @insertField #name "Alice" (insertField #age 30 emptyRecord)@+  * Application of a known variant constructor:+    @Active@ or @Inactive "timeout"@+    is lowered into an open variant injection:+    @injectVariant #Active emptyRecord@+    @injectVariant #Inactive (insertField #_1 "timeout" emptyRecord)@+- Patterns:+  * Pattern matching on @Person { name, age }@ is lowered into a record view pattern.+  * Pattern matching on @Active@ or @Inactive err@ is lowered into a variant view pattern.++Note [Record Update and View Pattern Translation]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+[tag:note-view-patterns]+1. Record Updates:+   Haskell's standard record update syntax @r { x = 42 }@ is notoriously problematic:+   it requires nominal field ownership and cannot change field types.+   Polytropos provides @REC_UPD r { x = 42, y = True }@.+   The plugin intercepts 'RecordUpd' (and its compat variants across GHC versions)+   and folds the updates right-to-left:+     @setField #x 42 (setField #y True r)@+   For HKD records, @REC_UPD_F@ desugars into 'setFieldF' chains.++2. Record Patterns & View Pattern Bundling:+   A pattern like @REC { name = p1, age = p2 }@ cannot be matched with standard data constructors+   because 'Record' is backed by a flat 'SmallArray'.+   The plugin desugars this into GHC View Patterns ('ViewPat'):+   - Single-field match:+     @REC { name = p1 }@  ==>  @(recordField #name -> p1)@+   - Multi-field match:+     Naively creating nested view patterns would inspect the record multiple times.+     The plugin bundles multi-field matches into a single tuple projection lambda:+     @REC { name = p1, age = p2 }@  ==>+     @(\_r -> (recordField #name _r, recordField #age _r)) -> (p1, p2)@+     This projects all requested fields in a single step matching against an unboxed tuple.++3. Variant Patterns:+   @VAR { Ok = p }@ is desugared into:+     @(projectVariant #Ok -> Just p)@+   If the variant's active tag matches '#Ok', 'projectVariant' yields 'Just payload' and+   matching proceeds against 'p'. If the tag does not match, 'projectVariant' yields+   'Nothing', causing GHC to fall through to the next pattern match branch.+-}++{-------------------------------------------------------------------------------+  Top-Level Source Plugin Entry Point+-------------------------------------------------------------------------------}++-- | Top-level entry point for GHC's @parsedResultAction@.+-- Invoked immediately after GHC's parser completes on each source file.+-- See Note [Source Plugin Desugaring Architecture: Syntactic Sugar Before Typechecking] [ref:note-source-plugin-arch]+sourcePlugin :: [CommandLineOption] -> ParsedResult -> Hsc ParsedResult+sourcePlugin _opts res = do+  let pm = parsedResultModule res+  let pm' = transformParsedModule pm+  pure res { parsedResultModule = pm' }++-- | Transforms a parsed module AST through three sequential compiler passes:+-- 1. Declaration Harvesting & Scrubbing: discovers 'OpenRecord' and 'OpenVariant' deriving+--    clauses, registers their nominal constructors, and strips the clauses.+--    See Note [Open Declarations: Lowering Nominal Declarations to Open Rows] [ref:note-open-declarations]+-- 2. Expression Transformation: rewrites 'REC', 'VAR', 'REC_UPD', and nominal constructors+--    into Polytropos runtime function application chains.+-- 3. Pattern Transformation: rewrites 'REC' and 'VAR' patterns into view patterns.+--    See Note [Record Update and View Pattern Translation] [ref:note-view-patterns]+-- 4. Import Management: ensures 'import qualified Polytropos as Polytropos' is present.+transformParsedModule :: HsParsedModule -> HsParsedModule+transformParsedModule pm@HsParsedModule{ hpm_module = L modLoc hsmod } =+  let decls0 = hsmodDecls hsmod+      (knownRecs, knownVars, decls1) = extractAndCleanDeclarations decls0+      decls2 = everywhere (mkT (transformExpr knownRecs knownVars)) decls1+      decls3 = everywhere (mkT (transformPat knownRecs knownVars)) decls2+      hsmod' = hsmod+        { hsmodDecls   = decls3+        , hsmodImports = ensurePolytroposImport (hsmodImports hsmod)+        }+  in pm { hpm_module = L modLoc hsmod' }++{-------------------------------------------------------------------------------+  SYB Combinators (Self-contained Data.Data helpers)+-------------------------------------------------------------------------------}++-- | Casts a transformation function 'b -> b' over any type 'a' satisfying 'Typeable'.+-- Provides lightweight Scrap Your Boilerplate traversal without external library dependencies.+mkT :: (Typeable a, Typeable b) => (b -> b) -> a -> a+mkT f x = case cast x of+  Just y -> case cast (f y) of+    Just x' -> x'+    Nothing -> x+  Nothing -> x++-- | Bottom-up traversal over all subtrees of a data term.+everywhere :: (forall a. Data a => a -> a) -> (forall a. Data a => a -> a)+everywhere f x = f (gmapT (everywhere f) x)++{-------------------------------------------------------------------------------+  Declaration Analysis (OpenRecord & OpenVariant discovery)+-------------------------------------------------------------------------------}++-- | Scans top-level declarations for @OpenRecord@ and @OpenVariant@ deriving clauses,+-- records their names, and strips the clauses so GHC's stock deriving engine does+-- not halt with "Cannot derive OpenRecord" errors.+--+-- See Note [Open Declarations: Lowering Nominal Declarations to Open Rows] [ref:note-open-declarations]+extractAndCleanDeclarations :: [LHsDecl GhcPs] -> ([String], [String], [LHsDecl GhcPs])+extractAndCleanDeclarations decls =+  let (recs, vars, cleanedDecls) = foldr step ([], [], []) decls+  in (nub recs, nub vars, cleanedDecls)+  where+    step (L loc (TyClD x decl)) (rAcc, vAcc, dAcc)+      | DataDecl ext (L _ name) tyvars fixity (HsDataDefn defnExt ctxt mtype mkind cons derivs) <- decl+      , let hasOpenRec = any isDerivingOpenRecord derivs+      , let hasOpenVar = any isDerivingOpenVariant derivs+      = let typeNameStr = occNameString (rdrNameOcc name)+            rAcc' = if hasOpenRec then typeNameStr : rAcc else rAcc+            vCons = if hasOpenVar then extractConNames cons else []+            vAcc' = if hasOpenVar then vCons ++ vAcc else vAcc+            cleanedDerivs = filter (\c -> not (isDerivingOpenRecord c || isDerivingOpenVariant c)) derivs+            defn' = HsDataDefn defnExt ctxt mtype mkind cons cleanedDerivs+            decl' = DataDecl ext (noLocA name) tyvars fixity defn'+        in (rAcc', vAcc', L loc (TyClD x decl') : dAcc)+    step d (rAcc, vAcc, dAcc) =+      (rAcc, vAcc, d : dAcc)++    -- Detects 'deriving OpenRecord' or 'deriving (..., OpenRecord, ...)'+    isDerivingOpenRecord (L _ (HsDerivingClause _ _ (L _ dtys))) =+      hasSigNamed "OpenRecord" dtys+    isDerivingOpenRecord _ = False++    -- Detects 'deriving OpenVariant' or 'deriving (..., OpenVariant, ...)'+    isDerivingOpenVariant (L _ (HsDerivingClause _ _ (L _ dtys))) =+      hasSigNamed "OpenVariant" dtys+    isDerivingOpenVariant _ = False++    hasSigNamed target (DctSingle _ sig) = sigMatches target sig+    hasSigNamed target (DctMulti _ sigs) = any (sigMatches target) sigs+    hasSigNamed _ _ = False++    sigMatches target (L _ (HsSig _ _ (L _ hty))) =+      case hty of+        HsTyVar _ _ (L _ rdr) -> occNameString (rdrNameOcc rdr) == target+        HsAppTy _ (L _ (HsTyVar _ _ (L _ rdr))) _ -> occNameString (rdrNameOcc rdr) == target+        _ -> False+    sigMatches _ _ = False++    -- Extract constructor names from data definition+    extractConNames cons =+      [ occNameString (rdrNameOcc (unLoc conName))+      | L _ cdecl <- case cons of+          DataTypeCons _ cs -> cs+          NewTypeCon c      -> [c]+      , let conName = case cdecl of+              ConDeclH98 { con_name = n } -> n+              ConDeclGADT { con_names = (n :| _) } -> n+              _ -> noLocA (mkRdrUnqual (mkDataOcc "Unknown"))+      ]++{-------------------------------------------------------------------------------+  Expression Rewriting+-------------------------------------------------------------------------------}++-- | Rewrites expressions matching syntactic sugar markers ('REC', 'VAR', 'REC_UPD',+-- 'REC_UPD_F', and nominal constructors deriving 'OpenRecord' / 'OpenVariant') into+-- standard Polytropos library combinator expressions.+--+-- Supported Syntactic Forms:+-- 1. Bare Record Construction:+--    @REC { x = 1, y = True }@ or @Person { name = "Alice", age = 30 }@+--    Lowered into a chain of 'insertField' calls ending in 'emptyRecord'.+-- 2. HKD Record Construction:+--    @REC_F { x = Just 1 }@+--    Lowered into a chain of 'insertFieldF' calls ending in 'emptyRecordF'.+-- 3. Variant Injection:+--    @VAR { Ok = 200 }@ or @VARIANT { Err = "msg" }@+--    Lowered into @injectVariant #Tag val@.+-- 4. Functional Record Update:+--    @REC_UPD r { x = 42 }@ (or @REC_UPD (r { x = 42 })@ or @(REC_UPD r) { x = 42 }@)+--    Lowered into chained @setField #x 42 r@ calls.+-- 5. Open Variant Constructor Application:+--    - Record payload: @Success { val = 200 }@ ==> @injectVariant #Success (REC { val = 200 })@+--    - Prefix payload: @Success val@           ==> @injectVariant #Success val@+--    - Nullary:        @Loading@               ==> @injectVariant #Loading emptyRecord@+transformExpr :: [String] -> [String] -> HsExpr GhcPs -> HsExpr GhcPs+transformExpr knownRecs knownVars expr = case expr of+  -- 1. Record Construction: REC { x = 1, y = True } or Person { x = 1, y = True }+  RecordCon _ext (L _ nm) HsRecFields{ rec_flds = flds }+    | let conStr = occNameString (rdrNameOcc nm)+    , conStr == "REC" || conStr `elem` knownRecs+    -> desugarRecordCon False flds++  -- 2. HKD Record Construction: REC_F { x = Just 1 }+  RecordCon _ext (L _ nm) HsRecFields{ rec_flds = flds }+    | occNameString (rdrNameOcc nm) == "REC_F"+    -> desugarRecordCon True flds++  -- 3. Variant Injection: VAR { Ok = 200 } or VARIANT { Err = "msg" }+  RecordCon _ext (L _ nm) HsRecFields{ rec_flds = flds }+    | let conStr = occNameString (rdrNameOcc nm)+    , conStr == "VAR" || conStr == "VARIANT"+    -> desugarVariantCon flds++  -- 4. Record Update: REC_UPD r { x = 42 } or REC_UPD (r { x = 42 }) or (REC_UPD r) { x = 42 } or REC_UPD_F+  (matchRecordUpd -> Just (stripHsPar -> L _ (HsApp _ (stripHsPar -> L _ (HsVar _ (L _ nm))) r), flds))+    | let nmStr = occNameString (rdrNameOcc nm)+    , nmStr == "REC_UPD" || nmStr == "REC_UPD_F"+    -> desugarRecordUpd (nmStr == "REC_UPD_F") r flds++  HsApp _ (stripHsPar -> L _ (HsVar _ (L _ nm))) (stripHsPar -> L _ (matchRecordUpd -> Just (r, flds)))+    | let nmStr = occNameString (rdrNameOcc nm)+    , nmStr == "REC_UPD" || nmStr == "REC_UPD_F"+    -> desugarRecordUpd (nmStr == "REC_UPD_F") r flds++  -- 5. Open Variant Constructor Application (Lowering nominal forms to Variant)+  -- 5a. Record syntax payload: Success { val = 200 }+  RecordCon _ext (L _ nm) HsRecFields{ rec_flds = flds }+    | let conStr = occNameString (rdrNameOcc nm)+    , conStr `elem` knownVars+    -> let injFn = polyVar "injectVariant"+           lblExpr = polyLabel (fsLit conStr)+           recPayload = noLocA (desugarRecordCon False flds)+       in unLoc (mkHsApp (mkHsApp injFn lblExpr) recPayload)++  -- 5b. Prefix payload application: Success r+  HsApp appExt (L _ (HsVar _ (L _ nm))) arg+    | let conStr = occNameString (rdrNameOcc nm)+    , conStr `elem` knownVars+    -> let injFn = polyVar "injectVariant"+           lblExpr = polyLabel (fsLit conStr)+       in HsApp appExt (mkHsApp injFn lblExpr) arg++  -- 5c. Nullary constructor: Loading (payload is emptyRecord)+  HsVar _ (L _ nm)+    | let conStr = occNameString (rdrNameOcc nm)+    , conStr `elem` knownVars+    -> let injFn = polyVar "injectVariant"+           lblExpr = polyLabel (fsLit conStr)+           emptyFn = polyVar "emptyRecord"+       in unLoc (mkHsApp (mkHsApp injFn lblExpr) emptyFn)++  other -> other++-- | Desugars record construction into a nested fold of 'insertField' calls:+-- @REC { x = 1, y = True }@ ==> @insertField #x 1 (insertField #y True emptyRecord)@+--+-- When 'isHKD' is true, emits 'insertFieldF' and 'emptyRecordF' instead.+-- Supports field punning: @REC { x }@ extracts local variable 'x' as argument.+desugarRecordCon :: Bool -> [LHsRecField GhcPs (LHsExpr GhcPs)] -> HsExpr GhcPs+desugarRecordCon isHKD flds =+  let emptyFn = polyVar (if isHKD then "emptyRecordF" else "emptyRecord")+      insertFnName = if isHKD then "insertFieldF" else "insertField"+      foldStep :: LHsRecField GhcPs (LHsExpr GhcPs) -> LHsExpr GhcPs -> LHsExpr GhcPs+      foldStep fld acc =+        let (lbl, arg) = extractRecField fld+            insFn = polyVar insertFnName+            lblExpr = polyLabel lbl+        in mkHsApp (mkHsApp (mkHsApp insFn lblExpr) arg) acc+  in unLoc $ foldr foldStep emptyFn flds++-- | Desugars variant injection into @injectVariant #Tag val@:+-- @VAR { Ok = 200 }@ ==> @injectVariant #Ok 200@+desugarVariantCon :: [LHsRecField GhcPs (LHsExpr GhcPs)] -> HsExpr GhcPs+desugarVariantCon [] =+  error "Polytropos.Plugin.Source: VAR {} requires a constructor tag (e.g. VAR { Ok = 200 })"+desugarVariantCon (fld : _) =+  let (lbl, arg) = extractRecField fld+      injFn = polyVar "injectVariant"+      lblExpr = polyLabel lbl+  in unLoc (mkHsApp (mkHsApp injFn lblExpr) arg)++-- | Desugars functional record update into a fold of 'setField' calls:+-- @REC_UPD r { x = 42, y = False }@ ==> @setField #x 42 (setField #y False r)@+--+-- When 'isHKD' is true, emits 'setFieldF' instead.+desugarRecordUpd :: Bool -> LHsExpr GhcPs -> [CompatRecUpdField] -> HsExpr GhcPs+desugarRecordUpd isHKD r flds =+  let setFnName = if isHKD then "setFieldF" else "setField"+      foldStep :: CompatRecUpdField -> LHsExpr GhcPs -> LHsExpr GhcPs+      foldStep fld acc =+        let (fs, arg) = extractRecUpdField fld+            setFn = polyVar setFnName+            lblExpr = polyLabel fs+        in mkHsApp (mkHsApp (mkHsApp setFn lblExpr) arg) acc+  in unLoc $ foldr foldStep r flds++-- | Extracts the field label and value expression from a record field node.+-- Handles GHC field punning: if @pun@ flag is set, synthesizes a variable+-- expression referencing the field identifier in local scope.+extractRecField :: LHsRecField GhcPs (LHsExpr GhcPs) -> (FastString, LHsExpr GhcPs)+extractRecField (L _ (HsFieldBind _ (L _ (FieldOcc _ (L _ lbl))) arg pun)) =+  let fs = occNameFS (rdrNameOcc lbl)+      arg' = if pun then noLocA (HsVar noExtField (noLocA lbl)) else arg+  in (fs, arg')++{-------------------------------------------------------------------------------+  Pattern Rewriting+-------------------------------------------------------------------------------}++-- | Rewrites pattern matches on @REC@, @VAR@, and open nominal constructors into+-- GHC View Patterns ('ViewPat').+--+-- See Note [Record Update and View Pattern Translation] [ref:note-view-patterns]+--+-- Desugared Patterns:+-- 1. Record Pattern:+--    @REC { x, y }@ or @Person { name, age }@+--    Lowered into tuple-bundled view patterns via 'desugarRecordPat'.+-- 2. Variant Pattern:+--    @VAR { Ok = p }@+--    Lowered into @(projectVariant #Ok -> Just p)@.+-- 3. Open Variant Constructor Pattern:+--    - Record payload: @Success { val }@ ==> @(projectVariant #Success -> Just (val view pattern))@+--    - Prefix payload: @Success p@      ==> @(projectVariant #Success -> Just p)@+--    - Nullary:        @Loading@        ==> @(projectVariant #Loading -> Just _)@+transformPat :: [String] -> [String] -> Pat GhcPs -> Pat GhcPs+transformPat knownRecs knownVars pat = case pat of+  -- 1. Record Pattern: REC { x, y } or Person { x, y }+  ConPat _ext (L _ nm) (RecCon HsRecFields{ rec_flds = flds })+    | let conStr = occNameString (rdrNameOcc nm)+    , conStr == "REC" || conStr `elem` knownRecs+    -> desugarRecordPat flds++  -- 2. Variant Pattern: VAR { Ok = p } or VARIANT { Err = p }+  ConPat _ext (L _ nm) (RecCon HsRecFields{ rec_flds = flds })+    | let conStr = occNameString (rdrNameOcc nm)+    , conStr == "VAR" || conStr == "VARIANT"+    -> desugarVariantPat flds++  -- 3. Open Variant Constructor Pattern (Lowering nominal constructor patterns)+  -- 3a. Record syntax payload: Success { val }+  ConPat _ext (L _ nm) (RecCon HsRecFields{ rec_flds = flds })+    | let conStr = occNameString (rdrNameOcc nm)+    , conStr `elem` knownVars+    -> let viewExpr = mkHsApp (polyVar "projectVariant") (polyLabel (fsLit conStr))+           justCon  = noLocA (mkRdrUnqual (mkDataOcc "Just"))+           innerPat = noLocA (desugarRecordPat flds)+           justPat  = noLocA $ ConPat noAnn justCon (PrefixConPat [innerPat])+       in ViewPat noAnn viewExpr justPat++  -- 3b. 1-arg prefix pattern: Success r+  ConPat _ext (L _ nm) (PrefixConPat [argPat])+    | let conStr = occNameString (rdrNameOcc nm)+    , conStr `elem` knownVars+    -> let viewExpr = mkHsApp (polyVar "projectVariant") (polyLabel (fsLit conStr))+           justCon  = noLocA (mkRdrUnqual (mkDataOcc "Just"))+           justPat  = noLocA $ ConPat noAnn justCon (PrefixConPat [argPat])+       in ViewPat noAnn viewExpr justPat++  -- 3c. Nullary prefix pattern: Loading+  ConPat _ext (L _ nm) (PrefixConPat [])+    | let conStr = occNameString (rdrNameOcc nm)+    , conStr `elem` knownVars+    -> let viewExpr = mkHsApp (polyVar "projectVariant") (polyLabel (fsLit conStr))+           justCon  = noLocA (mkRdrUnqual (mkDataOcc "Just"))+           wildPat  = noLocA (WildPat noExtField)+           justPat  = noLocA $ ConPat noAnn justCon (PrefixConPat [wildPat])+       in ViewPat noAnn viewExpr justPat++  other -> other++-- | Desugars record pattern matching into GHC View Patterns ('ViewPat').+--+-- Optimization:+-- - Empty pattern @REC {}@ desugars to wildcard ('WildPat').+-- - Single field @REC { x = p }@ desugars to @(recordField #x -> p)@.+-- - Multi-field @REC { x = p1, y = p2 }@ bundles projections into a single tuple lambda:+--   @(\_r -> (recordField #x _r, recordField #y _r)) -> (p1, p2)@+--   This projects all fields in one evaluation pass rather than cascading multiple view patterns.+desugarRecordPat :: [LHsRecField GhcPs (LPat GhcPs)] -> Pat GhcPs+desugarRecordPat [] =+  WildPat noExtField+desugarRecordPat [fld] =+  let (lbl, p) = extractRecPatField fld+      viewExpr = mkHsApp (polyVar "recordField") (polyLabel lbl)+  in ViewPat noAnn viewExpr p+desugarRecordPat flds =+  let (lbls, pats) = unzip (map extractRecPatField flds)+      rVar         = mkRdrUnqual (mkVarOcc "_r")+      rExpr        = noLocA (HsVar noExtField (noLocA rVar))+      mkProj lbl   = mkHsApp (mkHsApp (polyVar "recordField") (polyLabel lbl)) rExpr+      tupExpr      = noLocA $ ExplicitTuple noAnn (map (mkTupArg . mkProj) lbls) Boxed+      rPat         = noLocA (VarPat noExtField (noLocA rVar))+      lamExpr      = mkLambda [rPat] tupExpr+      tupPat       = noLocA $ TuplePat noAnn pats Boxed+  in ViewPat noAnn lamExpr tupPat++-- | Desugars variant pattern matching into @(projectVariant #Tag -> Just p)@:+-- @VAR { Ok = p }@ ==> @(projectVariant #Ok -> Just p)@+--+-- If the runtime tag matches '#Ok', 'projectVariant' returns 'Just payload' and+-- succeeds; otherwise it returns 'Nothing' and pattern matching falls through.+desugarVariantPat :: [LHsRecField GhcPs (LPat GhcPs)] -> Pat GhcPs+desugarVariantPat [] =+  error "Polytropos.Plugin.Source: VAR {} pattern requires a constructor tag"+desugarVariantPat (fld : _) =+  let (lbl, p)   = extractRecPatField fld+      viewExpr   = mkHsApp (polyVar "projectVariant") (polyLabel lbl)+      justCon    = noLocA (mkRdrUnqual (mkDataOcc "Just"))+      justPat    = noLocA $ ConPat noAnn justCon (PrefixConPat [p])+  in ViewPat noAnn viewExpr justPat++-- | Extracts the field label and sub-pattern from a record pattern field node.+-- Supports field punning: @REC { x }@ binds to pattern variable 'x'.+extractRecPatField :: LHsRecField GhcPs (LPat GhcPs) -> (FastString, LPat GhcPs)+extractRecPatField (L _ (HsFieldBind _ (L _ (FieldOcc _ (L _ lbl))) p pun)) =+  let fs = occNameFS (rdrNameOcc lbl)+      p' = if pun then noLocA (VarPat noExtField (noLocA lbl)) else p+  in (fs, p')++{-------------------------------------------------------------------------------+  Helper Functions+-------------------------------------------------------------------------------}++-- | Synthesizes a qualified RdrName expression: @Polytropos.<identifier>@.+-- Ensures that transformed expressions reference canonical Polytropos symbols+-- regardless of userland import shadowing.+polyVar :: String -> LHsExpr GhcPs+polyVar occ = noLocA (HsVar noExtField (noLocA (mkRdrQual (mkModuleName "Polytropos") (mkVarOcc occ))))++-- | Ensures that @import qualified Polytropos as Polytropos@ is present in the module's imports.+-- Injected automatically during 'transformParsedModule' so generated combinators resolve cleanly.+ensurePolytroposImport :: [LImportDecl GhcPs] -> [LImportDecl GhcPs]+ensurePolytroposImport imps =+  if any isPolytroposImport imps+    then imps+    else mkPolytroposImportDecl : imps+  where+    isPolytroposImport (L _ ImportDecl{ ideclName = L _ modNm }) =+      moduleNameString modNm == "Polytropos"+    isPolytroposImport _ = False

@@ -0,0 +1,539 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE OverloadedRecordDot #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS_GHC -Wno-unused-top-binds #-}++-- | Smoke test: exercise RowEq / RowShow through the TcPlugin on R2.+--+-- This is the acceptance test for Option A: the plugin must emit literal+-- RowEq / RowShow bodies that actually work at runtime, not just compile.++module Main (main) where++import Control.Monad (forM_)+import Data.Functor.Identity (Identity(..))+import Data.Kind (Type)+import Data.List (isInfixOf)+import Data.Primitive.SmallArray (SmallArray, sizeofSmallArray, indexSmallArray)+import Data.Proxy (Proxy(..))+import Data.Type.Equality ((:~:)(Refl))+import GHC.Exts (Any)+import GHC.TypeLits (Symbol)+import System.Directory (getTemporaryDirectory, removeFile)+import System.Environment (lookupEnv)+import System.Exit (ExitCode(..))+import System.IO (hClose, hPutStr, openTempFile)+import System.Process (readProcessWithExitCode)+import Test.Tasty (defaultMain, testGroup)+import Test.Tasty.HUnit (testCase, (@?=), assertBool)++import Polytropos.Core+import Polytropos++-- | R2: a two-field product: a :: Int, b :: Bool.+type R2 = '[ "a" := Int, "b" := Bool ]++-- | Store a concrete value in a slot.+slot :: a -> Identity Any+slot = noInlineUnsafeCo++-- | The two values under test.+ab :: RowRep Identity ProductRowT R2 (Int, Bool)+ab = RowRep (productRep [slot (7 :: Int), slot True])++other :: RowRep Identity ProductRowT R2 (Int, Bool)+other = RowRep (productRep [slot (7 :: Int), slot False])++type RD = '[ "x" := Int, "y" := Bool ]+rDot :: RowRep Identity ProductRowT RD (Int, Bool)+rDot = RowRep (productRep [slot (42 :: Int), slot True])++data Person = Person { name :: String, age :: Int }+  deriving (Show, Eq, OpenRecord)++data Status = Success { val :: Int } | Failure { msg :: String }+  deriving (Show, Eq, OpenVariant)++main :: IO ()+main = defaultMain $ testGroup "plugin RowEq/RowShow smoke"+  [ testGroup "Products"+      [ testCase "repEq is reflexive" $+          repEq ab ab @?= True+      , testCase "repEq detects a differing slot" $+          repEq ab other @?= False+      , testCase "repShowsPrec renders both fields" $+          repShowsPrec 0 ab "" @?= "R2 7 True"+      ]+  , testGroup "Sums"+      [ testCase "repEqSum (RowEqSum) matches same constructor and same payload" $+          repEqSum sumC1 sumC1 @?= True+      , testCase "repEqSum (RowEqSum) rejects different payloads in same constructor" $+          repEqSum sumC1 sumC1diff @?= False+      , testCase "repEqSum (RowEqSum) rejects different constructors" $+          repEqSum sumC1 sumC2 @?= False+      , testCase "repShowsPrecSum (RowShowSum) renders C1 properly" $+          repShowsPrecSum 0 sumC1 "" @?= "C1 7"+      , testCase "repShowsPrecSum (RowShowSum) renders C2 properly" $+          repShowsPrecSum 0 sumC2 "" @?= "C2 True"+      ]+  , testGroup "OverloadedRecordDot"+      [ testCase "r.x == 42" $+          rDot.x @?= Identity (42 :: Int)+      , testCase "r.y == True" $+          rDot.y @?= Identity True+      , testCase "rHKD.msg == Just \"ok\" on RecordF Maybe" $+          rHKD.msg @?= Just ("ok" :: String)+      , testCase "rHKD.code == Nothing on RecordF Maybe" $+          rHKD.code @?= (Nothing :: Maybe Int)+      , testCase "bare Record dot projection with inferred type variable" $ do+          let u = insertField (Field @"name") ("Alice" :: String) emptyRecord+          show u.name @?= "\"Alice\""+      ]+  , testGroup "AllFields generic dictionary supply"+      [ testCase "supplies Show dictionaries for homogeneous product row" $+          let arr = fieldDicts @ProductRowT @TwoInts @Show+          in do+            sizeofSmallArray arr @?= 2+            showAllFields arr (repVals (unRowRep twoInts)) @?= "42 7"+      , testCase "supplies Show dictionaries for heterogeneous product row (String, Int, Bool)" $+          let arr = fieldDicts @ProductRowT @HeteroRow @Show+          in do+            sizeofSmallArray arr @?= 3+            showAllFields arr (repVals (unRowRep heteroVal)) @?= "\"hello\" 99 True"+      , testCase "supplies Show dictionaries for HKD product row (Maybe String, Maybe Int)" $+          let arr = fieldDicts @ProductRowHKDT @(HKDProductRow Maybe) @Show+          in do+            sizeofSmallArray arr @?= 2+            showAllFieldsHKD arr (repVals (unRowRep hkdVal)) @?= "Just \"ok\" Nothing"+      ]+  , testGroup "HKD Row Vocabulary"+      [ testCase "FieldIndex resolves on HKD product row" $ do+          fieldIndex @_ @"msg" @(HKDProductRow Maybe) @(Maybe String) @?= 0+          fieldIndex @_ @"code" @(HKDProductRow Maybe) @(Maybe Int) @?= 1+      , testCase "ConstructorIndex resolves on HKD sum row" $ do+          constructorIndex @_ @"Success" @(HKDSumRow Maybe) @?= 0+          constructorIndex @_ @"Failure" @(HKDSumRow Maybe) @?= 1+      ]+  , testGroup "Type-level row metadata rewriting"+      [ testCase "FieldNames reduces on TwoInts" $+          case namesTwoInts of+            Refl -> pure ()+      , testCase "FieldNames reduces on empty row" $+          case namesEmpty of+            Refl -> pure ()+      , testCase "SimpleFieldTypes reduces on TwoInts" $+          case simpleTypesTwoInts of+            Refl -> pure ()+      , testCase "SimpleFieldTypes reduces on empty row" $+          case simpleTypesEmpty of+            Refl -> pure ()+      , testCase "FieldTypes reduces on TwoInts with Maybe" $+          case fieldTypesTwoInts of+            Refl -> pure ()+      , testCase "FieldTypes reduces on HeteroRow with Identity" $+          case fieldTypesHetero of+            Refl -> pure ()+      , testCase "FieldTypes reduces on empty row" $+          case fieldTypesEmpty of+            Refl -> pure ()+      ]+  , testGroup "SubRow and SubSum evidence"+      [ testCase "SubRow emits projection indices" $ do+          subRowIndices @SmallProd @BigProd @?= [2, 0]+          subRowIndices @SmallProd @SmallProd @?= [0, 1]+      , testCase "projectRecord extracts sub-record fields" $ do+          let bigRec :: Record BigProd+              bigRec = insertField (Field @"a") (10 :: Int)+                     $ insertField (Field @"b") True+                     $ insertField (Field @"c") "hello"+                     $ emptyRecord+              smallRec :: Record SmallProd+              smallRec = projectRecord bigRec+          smallRec.c @?= Identity "hello"+          smallRec.a @?= Identity (10 :: Int)+      , testCase "SubSum emits inject and narrow indices" $ do+          subSumInjectIndices @SmallSum @BigSum @?= [0, 2]+          subSumNarrowIndices @SmallSum @BigSum @?= [Just 0, Nothing, Just 1]+      , testCase "widenVariant remaps constructor tag to super-row" $ do+          let vC_small :: Variant SmallSum+              vC_small = injectVariant (Field @"C") (insertField (Field @"y") True emptyRecord)+              vC_wide :: Variant BigSum+              vC_wide = widenVariant vC_small+          repTag (unRowRep vC_wide) @?= 2+          case projectVariant (Field @"C") vC_wide of+            Just (r :: Record '[ "y" := Bool ]) -> r.y @?= Identity True+            Nothing -> error "expected Just in widenVariant"+      , testCase "narrowVariant succeeds on matching constructor" $ do+          let vC_small :: Variant SmallSum+              vC_small = injectVariant (Field @"C") (insertField (Field @"y") True emptyRecord)+              vC_wide :: Variant BigSum+              vC_wide = widenVariant vC_small+          case narrowVariant @SmallSum vC_wide of+            Just vC' -> case projectVariant (Field @"C") vC' of+              Just (r :: Record '[ "y" := Bool ]) -> r.y @?= Identity True+              Nothing -> error "expected Just in narrowVariant"+            Nothing -> error "expected Just in narrowVariant"+      , testCase "narrowVariant returns Nothing for super constructor absent in sub" $ do+          let vB_big :: Variant BigSum+              vB_big = injectVariant (Field @"B") (insertField (Field @"x") (42 :: Int) emptyRecord)+              mNarrow = narrowVariant @SmallSum vB_big+          case mNarrow of+            Nothing -> pure ()+            Just _  -> error "expected Nothing in narrowVariant"+      ]+  , testGroup "Compile-time label hashing (KnownHash)"+      [ testCase "knownHash solves on literal symbols and matches fnv1a64" $ do+          knownHash @"x" @?= fnv1a64 "x"+          knownHash @"greeting" @?= fnv1a64 "greeting"+          knownHash @"a" @?= fnv1a64 "a"+          knownHash @"veryLongFieldNameForTestingCompileTimeHashing"+            @?= fnv1a64 "veryLongFieldNameForTestingCompileTimeHashing"+      , testCase "labelHash and hashVal proxies extract the literal hash" $ do+          labelHash (Field @"greeting") @?= fnv1a64 "greeting"+          hashVal (Field @"greeting") @?= fnv1a64 "greeting"+          labelHash (Proxy @"a") @?= fnv1a64 "a"+      , testCase "different labels yield distinct non-zero hashes" $ do+          knownHash @"x" /= 0 @?= True+          knownHash @"y" /= 0 @?= True+          knownHash @"x" /= knownHash @"y" @?= True+      ]+  , testGroup "Source Plugin Syntax (§1.6)"+      [ testCase "REC bare record construction" $ do+          let r = REC { a = (10 :: Int), b = True }+          r.a @?= Identity (10 :: Int)+          r.b @?= Identity True+      , testCase "REC with field punning" $ do+          let a = (99 :: Int)+              b = False+              r = REC { a, b }+          r.a @?= Identity (99 :: Int)+          r.b @?= Identity False+      , testCase "REC_F HKD record construction" $ do+          let r = REC_F { msg = Just ("hello" :: String), code = (Nothing :: Maybe Int) }+          r.msg @?= Just "hello"+          r.code @?= (Nothing :: Maybe Int)+      , testCase "VAR and VARIANT injection" $ do+          let v1 :: Variant '[ "ok" := '[ "val" := Int ] ]+              v1 = VAR { ok = REC { val = (200 :: Int) } }+          case projectVariant (Field @"ok") v1 of+            Just r -> r.val @?= Identity (200 :: Int)+            Nothing -> error "expected Just in projectVariant"+          let v2 :: Variant '[ "err" := '[ "msg" := String ] ]+              v2 = VARIANT { err = REC { msg = ("not found" :: String) } }+          case projectVariant (Field @"err") v2 of+            Just r -> r.msg @?= Identity "not found"+            Nothing -> error "expected Just in projectVariant"+      , testCase "REC_UPD bare record update" $ do+          let r1 = REC { a = (10 :: Int), b = True }+              r2 = REC_UPD r1 { a = (42 :: Int) }+          r2.a @?= Identity (42 :: Int)+          r2.b @?= Identity True+      , testCase "REC_UPD_F HKD record update" $ do+          let r1 = REC_F { msg = Just ("hi" :: String), code = (Nothing :: Maybe Int) }+              r2 = REC_UPD_F r1 { code = (Just 200 :: Maybe Int) }+          r2.msg @?= Just "hi"+          r2.code @?= Just (200 :: Int)+      , testCase "REC pattern matching (single and multiple fields)" $ do+          let r = REC { a = (10 :: Int), b = True }+              valA = case r of+                REC { a = vA } -> vA+              (x, y) = case r of+                REC { a, b } -> (a, b)+          valA @?= (10 :: Int)+          x @?= (10 :: Int)+          y @?= True+      , testCase "VAR pattern matching" $ do+          let v1 = VAR { ok = REC { val = (200 :: Int) } } :: Variant '[ "ok" := '[ "val" := Int ], "err" := '[ "msg" := String ] ]+              v2 = VAR { err = REC { msg = ("oops" :: String) } } :: Variant '[ "ok" := '[ "val" := Int ], "err" := '[ "msg" := String ] ]+              check :: Variant '[ "ok" := '[ "val" := Int ], "err" := '[ "msg" := String ] ] -> String+              check v = case v of+                VAR { ok = REC { val = n } } -> show n+                VAR { err = REC { msg = s } } -> s+                _                             -> error "unreachable"+          check v1 @?= "200"+          check v2 @?= "oops"+      , testCase "OpenRecord declaration form construction and matching" $ do+          let p = Person { name = "Alice", age = (30 :: Int) }+          p.name @?= Identity "Alice"+          p.age @?= Identity (30 :: Int)+          let (resName, resAge) = case p of+                Person { name, age } -> (name, age)+          resName @?= "Alice"+          resAge @?= (30 :: Int)+      , testCase "OpenVariant declaration form construction and matching" $ do+          let s1 = Success { val = (200 :: Int) } :: Variant '[ "Success" := '[ "val" := Int ], "Failure" := '[ "msg" := String ] ]+              s2 = Failure { msg = "bad request" } :: Variant '[ "Success" := '[ "val" := Int ], "Failure" := '[ "msg" := String ] ]+              eval :: Variant '[ "Success" := '[ "val" := Int ], "Failure" := '[ "msg" := String ] ] -> Int+              eval s = case s of+                Success { val } -> val+                Failure { msg } -> length msg+                _               -> error "unreachable"+          eval s1 @?= 200+          eval s2 @?= 11+      ]+  , testGroup "Eliminators and Peeling (§1.7)"+      [ testCase "eliminateUniform handles variants in O(1) with REC handlers" $ do+          let v1 = VAR { ok = REC { val = (42 :: Int) } } :: Variant '[ "ok" := '[ "val" := Int ], "err" := '[ "msg" := String ] ]+              v2 = VAR { err = REC { msg = ("error!" :: String) } } :: Variant '[ "ok" := '[ "val" := Int ], "err" := '[ "msg" := String ] ]+              handlers = REC+                { ok = \(REC { val }) -> "Success: " ++ show (val :: Int)+                , err = \(REC { msg }) -> "Failure: " ++ (msg :: String)+                }+          eliminateUniform handlers v1 @?= "Success: 42"+          eliminateUniform handlers v2 @?= "Failure: error!"+      , testCase "peel isolates single constructor and updates remaining variant tag" $ do+          let vOk = VAR { ok = REC { val = (100 :: Int) } } :: Variant '[ "ok" := '[ "val" := Int ], "err" := '[ "msg" := String ] ]+              vErr = VAR { err = REC { msg = ("oops" :: String) } } :: Variant '[ "ok" := '[ "val" := Int ], "err" := '[ "msg" := String ] ]+          case peel @"ok" vOk of+            Right (REC { val }) -> val @?= (100 :: Int)+            Left _ -> error "expected Right"+          case peel @"ok" vErr of+            Right _ -> error "expected Left"+            Left rest -> case projectVariant (Field @"err") rest of+              Just (REC { msg }) -> msg @?= "oops"+              Nothing -> error "expected err in rest"+      ]+  , testGroup "TypeError human-centric diagnostics"+      [ testCase "missing field diagnostic with available fields list" $+          checkGhcDiag+            (unlines+              [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+              , "module Test where"+              , "import Polytropos.Core"+              , "t = fieldIndex @_ @\"email\" @'[ \"name\" := String, \"age\" := Int ] @Int"+              ])+            [ "Polytropos Record Error:"+            , "Field 'email' does not exist in record:"+            , "{ name :: String, age :: Int }"+            , "Available fields: 'name', 'age'"+            ]+      , testCase "missing field diagnostic with fuzzy suggestion" $+          checkGhcDiag+            (unlines+              [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+              , "module Test where"+              , "import Polytropos.Core"+              , "t = fieldIndex @_ @\"naem\" @'[ \"name\" := String, \"age\" := Int ] @String"+              ])+            [ "Polytropos Record Error:"+            , "Field 'naem' does not exist in record:"+            , "Did you mean: 'name'?"+            ]+      , testCase "field type mismatch diagnostic" $+          checkGhcDiag+            (unlines+              [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+              , "module Test where"+              , "import Polytropos.Core"+              , "t = fieldIndex @_ @\"name\" @'[ \"name\" := String, \"age\" := Int ] @Int"+              ])+            [ "Polytropos Record Error:"+            , "Field 'name' in record has type:"+            , "String"+            , "but expected:"+            , "Int"+            ]+      , testCase "missing constructor diagnostic with available constructors list" $+          checkGhcDiag+            (unlines+              [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+              , "module Test where"+              , "import Polytropos.Core"+              , "t = constructorIndex @_ @\"Exit\" @'[ \"Start\" := '[ \"x\" := String ], \"Stop\" := '[ \"y\" := Int ] ]"+              ])+            [ "Polytropos Variant Error:"+            , "Constructor 'Exit' is not a member of variant:"+            , "< Start { x :: String } | Stop { y :: Int } >"+            , "Available constructors: 'Start', 'Stop'"+            ]+      , testCase "missing constructor diagnostic with fuzzy suggestion" $+          checkGhcDiag+            (unlines+              [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+              , "module Test where"+              , "import Polytropos.Core"+              , "t = constructorIndex @_ @\"Strt\" @'[ \"Start\" := '[ \"x\" := String ], \"Stop\" := '[ \"y\" := Int ] ]"+              ])+            [ "Polytropos Variant Error:"+            , "Constructor 'Strt' is not a member of variant:"+            , "Did you mean: 'Start' or 'Stop'?"+            ]+      , testCase "SubRow missing field diagnostic" $+          checkGhcDiag+            (unlines+              [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+              , "module Test where"+              , "import Polytropos.Core"+              , "t = subRowIndices @'[ \"z\" := Bool ] @'[ \"a\" := Int, \"b\" := Bool ]"+              ])+            [ "Polytropos SubRow Error:"+            , "Cannot project record: field 'z' from sub-record is missing in super-record:"+            , "{ a :: Int, b :: Bool }"+            ]+      , testCase "SubRow field type mismatch diagnostic" $+          checkGhcDiag+            (unlines+              [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+              , "module Test where"+              , "import Polytropos.Core"+              , "t = subRowIndices @'[ \"a\" := String ] @'[ \"a\" := Int, \"b\" := Bool ]"+              ])+            [ "Polytropos SubRow Error:"+            , "Cannot project record: field 'a' has type:"+            , "String"+            , "in sub-record, but has type:"+            , "Int"+            , "in super-record."+            ]+      , testCase "SubSum missing constructor diagnostic" $+          checkGhcDiag+            (unlines+              [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+              , "module Test where"+              , "import Polytropos.Core"+              , "t = subSumInjectIndices @'[ \"Missing\" := '[] ] @'[ \"A\" := '[], \"B\" := '[] ]"+              ])+            [ "Polytropos SubSum Error:"+            , "Cannot widen variant: constructor 'Missing' from sub-variant is missing in super-variant:"+            , "< A | B >"+            , "Available constructors: 'A', 'B'"+            ]+      , testCase "SubSum payload mismatch diagnostic" $+          checkGhcDiag+            (unlines+              [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+              , "module Test where"+              , "import Polytropos.Core"+              , "t = subSumInjectIndices @'[ \"A\" := '[ \"x\" := Int ] ] @'[ \"A\" := '[ \"x\" := String ] ]"+              ])+            [ "Polytropos SubSum Error:"+            , "Cannot widen variant: constructor 'A' has different payload rows:"+            , "sub-variant payload:   { x :: Int }"+            , "super-variant payload: { x :: String }"+            ]+      ]+  ]++checkGhcDiag :: String -> [String] -> IO ()+checkGhcDiag snippet expectedSubstrings = do+  tmpDir <- getTemporaryDirectory+  (tmpFile, h) <- openTempFile tmpDir "PolytroposDiagTest.hs"+  hPutStr h snippet+  hClose h+  extraFlags <- maybe [] words <$> lookupEnv "POLYTROPOS_TEST_GHC_FLAGS"+  (exitCode, _stdout, stderr) <- readProcessWithExitCode+    "ghc"+    ([ "-fno-code"+     , tmpFile+     , "-fplugin=Polytropos.Plugin"+     ] ++ extraFlags)+    ""+  removeFile tmpFile+  exitCode @?= ExitFailure 1+  forM_ expectedSubstrings $ \expected ->+    assertBool+      ("Expected diagnostic to contain: " ++ show expected ++ "\nActual stderr:\n" ++ stderr)+      (expected `isInfixOf` stderr)++-- | Use a supplied array of type-erased Show dictionaries to show every slot.+showAllFields :: DictAllFields Show+              -> SmallArray (Identity Any)+              -> String+showAllFields arr slots =+  go 0+  where+    n = sizeofSmallArray slots+    go i+      | i == n = ""+      | otherwise =+          case indexSmallArray arr i of+            DictAny ->+              let Identity x = indexSmallArray slots i+              in show x <> if i + 1 == n then "" else " " <> go (i + 1)++type TwoInts = '[ "x" := Int, "y" := Int ]+twoInts :: RowRep Identity ProductRowT TwoInts ()+twoInts = RowRep (productRep [slot (42 :: Int), slot (7 :: Int)])++type HeteroRow = '[ "greeting" := String, "count" := Int, "active" := Bool ]+heteroVal :: RowRep Identity ProductRowT HeteroRow ()+heteroVal = RowRep (productRep [slot ("hello" :: String), slot (99 :: Int), slot True])++namesTwoInts :: FieldNames TwoInts :~: '[ "x", "y" ]+namesTwoInts = Refl++namesEmpty :: FieldNames ('[] :: [(Symbol, Type)]) :~: '[]+namesEmpty = Refl++simpleTypesTwoInts :: SimpleFieldTypes TwoInts :~: '[ '("x", Int), '("y", Int) ]+simpleTypesTwoInts = Refl++simpleTypesEmpty :: SimpleFieldTypes ('[] :: [(Symbol, Type)]) :~: '[]+simpleTypesEmpty = Refl++fieldTypesTwoInts :: FieldTypes Maybe TwoInts :~: '[ '("x", Maybe Int), '("y", Maybe Int) ]+fieldTypesTwoInts = Refl++fieldTypesHetero :: FieldTypes Identity HeteroRow :~: '[ '("greeting", Identity String), '("count", Identity Int), '("active", Identity Bool) ]+fieldTypesHetero = Refl++fieldTypesEmpty :: FieldTypes Maybe ('[] :: [(Symbol, Type)]) :~: '[]+fieldTypesEmpty = Refl++-- | S2: a sum with two constructors+type S2 = '[ "C1" := '[ "x" := Int ], "C2" := '[ "y" := Bool ] ]++-- | Ensure the plugin solves these dictionaries (RowEqSum, RowShowSum) for S2.++sumC1 :: RowRep Identity SumRowT S2 a+sumC1 = RowRep (injectRep 0 [slot (7 :: Int)])++sumC1diff :: RowRep Identity SumRowT S2 a+sumC1diff = RowRep (injectRep 0 [slot (8 :: Int)])++sumC2 :: RowRep Identity SumRowT S2 a+sumC2 = RowRep (injectRep 1 [slot True])++type HKDProductRow (f :: Type -> Type) = '[ "msg" := f String, "code" := f Int ] :: ProductRow f++type HKDSumRow (f :: Type -> Type) = '[ "Success" := HKDProductRow f, "Failure" := '[] ] :: SumRowHKD f++slotMaybe :: Maybe a -> Maybe Any+slotMaybe = noInlineUnsafeCo++hkdVal :: RowRep Maybe ProductRowHKDT (HKDProductRow Maybe) ()+hkdVal = RowRep (productRep [slotMaybe (Just ("ok" :: String)), slotMaybe (Nothing :: Maybe Int)])++rHKD :: RowRep Maybe ProductRowHKDT (HKDProductRow Maybe) ()+rHKD = hkdVal++showAllFieldsHKD :: DictAllFields Show+                 -> SmallArray (Maybe Any)+                 -> String+showAllFieldsHKD arr slots =+  go 0+  where+    n = sizeofSmallArray slots+    go i+      | i == n = ""+      | otherwise =+          case indexSmallArray arr i of+            DictAny ->+              let x :: Any+                  x = noInlineUnsafeCo (indexSmallArray slots i)+              in show x <> if i + 1 == n then "" else " " <> go (i + 1)++-- | Big product and sub-product for testing SubRow evidence.+type BigProd = '[ "a" := Int, "b" := Bool, "c" := String ]+type SmallProd = '[ "c" := String, "a" := Int ]++-- | Big sum and sub-sum for testing SubSum evidence.+type BigSum = '[ "A" := '[], "B" := '[ "x" := Int ], "C" := '[ "y" := Bool ] ]+type SmallSum = '[ "A" := '[], "C" := '[ "y" := Bool ] ]