{-# 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(..)
  , 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 :: Plugin
plugin = Plugin
defaultPlugin
  { tcPlugin           = const $ Just $ mkTcPlugin polytroposPlugin
  , parsedResultAction = \[String]
opts ModSummary
_modSummary -> [String] -> ParsedResult -> Hsc ParsedResult
sourcePlugin [String]
opts
  }

polytroposPlugin :: TcPlugin
polytroposPlugin :: TcPlugin
polytroposPlugin = TcPlugin
  { tcPluginInit :: TcPluginM 'Init PluginState
tcPluginInit     = TcPluginM 'Init PluginState
polytroposInit
  , tcPluginSolve :: PluginState -> TcPluginSolver
tcPluginSolve    = PluginState -> TcPluginSolver
polytroposSolve
  , tcPluginRewrite :: PluginState -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite  = PluginState -> UniqFM TyCon TcPluginRewriter
polytroposRewrite
  , tcPluginPostTc :: PluginState -> TcPluginM 'PostTc ()
tcPluginPostTc   = TcPluginM 'PostTc () -> PluginState -> TcPluginM 'PostTc ()
forall a b. a -> b -> a
const (() -> TcPluginM 'PostTc ()
forall a. a -> TcPluginM 'PostTc a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  , tcPluginShutdown :: PluginState -> IO ()
tcPluginShutdown = IO () -> PluginState -> IO ()
forall a b. a -> b -> a
const (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  }

--------------------------------------------------------------------------------- Plugin state
-------------------------------------------------------------------------------

data PluginState = PluginState

  { PluginState -> Var
psRepTag        :: !Var    -- ^ repTag :: Rep f a -> Word
  , PluginState -> Var
psRepArity      :: !Var    -- ^ repArity :: Rep f a -> Int
  , PluginState -> Var
psFieldAt       :: !Var    -- ^ fieldAt :: Int -> Rep f a -> f x
  , PluginState -> Var
psUnRowRep      :: !Var    -- ^ unRowRep :: RowRep f r row a -> Rep f a
  , PluginState -> Var
psNoInlineCo    :: !Var    -- ^ noInlineUnsafeCo :: a -> b
  , PluginState -> Var
psAnd           :: !Var    -- ^ GHC.Internal.Classes.&&
  , PluginState -> Var
psComp          :: !Var    -- ^ GHC.Internal.Base.(.)
  , PluginState -> Var
psEqClass       :: !Var    -- ^ GHC.Internal.Classes.== (method)
  , PluginState -> Var
psShowsPrecMeth :: !Var    -- ^ GHC.Internal.Show.showsPrec (method)
  , PluginState -> Var
psShowString    :: !Var    -- ^ GHC.Internal.Show.showString
  , PluginState -> Var
psShowChar      :: !Var    -- ^ GHC.Internal.Show.showChar
  , PluginState -> Var
psFEqInt        :: !Var    -- ^ $fEqInt
  , PluginState -> Var
psFEqBool       :: !Var    -- ^ $fEqBool
  , PluginState -> Var
psFEqWord       :: !Var    -- ^ $fEqWord
  , PluginState -> Var
psFShowInt      :: !Var    -- ^ $fShowInt
  , PluginState -> Var
psFShowBool     :: !Var    -- ^ $fShowBool
  , PluginState -> Class
psEqCls         :: !Class  -- ^ GHC.Classes.Eq class
  , PluginState -> Class
psShowCls       :: !Class  -- ^ GHC.Show.Show class
  , PluginState -> Class
psRowFlavourCls   :: !Class  -- ^ RowFlavour class
  , PluginState -> Class
psHasFieldCls     :: !Class  -- ^ GHC.Records.HasField class
  , PluginState -> TyCon
psDictAnyTyCon    :: !TyCon  -- ^ Polytropos.Core.DictAny
  , PluginState -> Var
psMkDictAny       :: !Var    -- ^ Polytropos.Core.mkDictAny
  , PluginState -> Var
psEvidenceAllFields :: !Var  -- ^ Polytropos.Core.evidenceAllFields
  , PluginState -> TyCon
psFieldTypesTyCon       :: !TyCon -- ^ Polytropos.Core.FieldTypes
  , PluginState -> TyCon
psSimpleFieldTypesTyCon :: !TyCon -- ^ Polytropos.Core.SimpleFieldTypes
  , PluginState -> TyCon
psFieldNamesTyCon       :: !TyCon -- ^ Polytropos.Core.FieldNames
  , PluginState -> TyCon
psTypeErrorTyCon        :: !TyCon -- ^ GHC.Internal.TypeError.TypeError
  , PluginState -> TyCon
psPromotedText          :: !TyCon -- ^ promoted 'Text
  , PluginState -> TyCon
psPromotedVcat          :: !TyCon -- ^ promoted ':$$:
  }

-------------------------------------------------------------------------------
-- Plugin initialisation
-------------------------------------------------------------------------------

polytroposInit :: TcPluginM 'Init PluginState
polytroposInit :: TcPluginM 'Init PluginState
polytroposInit = do
  coreMod <- TcPluginM 'Init Module
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 = DataCon -> TyCon
promoteDataCon DataCon
textDataCon
      psPromotedVcat = DataCon -> TyCon
promoteDataCon DataCon
vcatDataCon

  pure PluginState{..}

findModule :: String -> Maybe String -> TcPluginM 'Init Module
findModule :: String -> Maybe String -> TcPluginM 'Init Module
findModule String
modName Maybe String
mPkg = do
  let modName' :: ModuleName
modName' = String -> ModuleName
mkModuleName String
modName
  pkgQual <- ModuleName -> Maybe FastString -> TcPluginM 'Init PkgQual
forall (m :: * -> *).
MonadTcPlugin m =>
ModuleName -> Maybe FastString -> m PkgQual
resolveImport ModuleName
modName' (String -> FastString
fsLit (String -> FastString) -> Maybe String -> Maybe FastString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
mPkg)
  result <- findImportedModule modName' pkgQual
  case result of
    Found ModLocation
_ Module
mod' -> Module -> TcPluginM 'Init Module
forall a. a -> TcPluginM 'Init a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Module
mod'
    FindResult
_           -> String -> TcPluginM 'Init Module
forall a. HasCallStack => String -> a
error (String -> TcPluginM 'Init Module)
-> String -> TcPluginM 'Init Module
forall a b. (a -> b) -> a -> b
$ String
"polytropos: could not find module " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
modName

findPolytroposCoreModule :: TcPluginM 'Init Module
findPolytroposCoreModule :: TcPluginM 'Init Module
findPolytroposCoreModule = String -> Maybe String -> TcPluginM 'Init Module
findModule String
"Polytropos.Core" (String -> Maybe String
forall a. a -> Maybe a
Just String
"polytropos-core")

lookupIdInModule :: Module -> String -> TcPluginM 'Init Var
lookupIdInModule :: Module -> String -> TcPluginM 'Init Var
lookupIdInModule Module
modName String
occStr = do
  let occ :: OccName
occ = String -> OccName
mkVarOcc String
occStr
  name <- Module -> OccName -> TcPluginM 'Init Name
forall (m :: * -> *).
MonadTcPlugin m =>
Module -> OccName -> m Name
lookupOrig Module
modName OccName
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 :: PluginState -> UniqFM TyCon TcPluginRewriter
polytroposRewrite PluginState
state = [(TyCon, TcPluginRewriter)] -> UniqFM TyCon TcPluginRewriter
forall key elt. Uniquable key => [(key, elt)] -> UniqFM key elt
listToUFM
  [ (PluginState -> TyCon
psFieldTypesTyCon PluginState
state, TyCon -> TcPluginRewriter
rewriteFieldTypes (PluginState -> TyCon
psFieldTypesTyCon PluginState
state))
  , (PluginState -> TyCon
psSimpleFieldTypesTyCon PluginState
state, TyCon -> TcPluginRewriter
rewriteSimpleFieldTypes (PluginState -> TyCon
psSimpleFieldTypesTyCon PluginState
state))
  , (PluginState -> TyCon
psFieldNamesTyCon PluginState
state, TyCon -> TcPluginRewriter
rewriteFieldNames (PluginState -> TyCon
psFieldNamesTyCon PluginState
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 :: Type -> Maybe [(FastString, Type)]
walkRowFields_maybe Type
rowTy = do
  elems <- Type -> Maybe [Type]
myExtractPromotedList (Type -> Type
unwrapSynonyms Type
rowTy)
  mapM extractField elems
  where
    extractField :: Type -> Maybe (FastString, Type)
extractField Type
elemTy =
      case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Type
unwrapSynonyms Type
elemTy) of
        Just (TyCon
_, [Type]
args)
          | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
          , let nameTy :: Type
nameTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
          , let fieldTy :: Type
fieldTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
          , Just FastString
n <- Type -> Maybe FastString
isStrLitTy (Type -> Type
unwrapSynonyms Type
nameTy)
          -> (FastString, Type) -> Maybe (FastString, Type)
forall a. a -> Maybe a
Just (FastString
n, Type
fieldTy)
        Maybe (TyCon, [Type])
_ -> Maybe (FastString, Type)
forall a. Maybe a
Nothing

rewriteFieldNames :: TyCon -> [Ct] -> [Type] -> TcPluginM 'Rewrite TcPluginRewriteResult
rewriteFieldNames :: TyCon -> TcPluginRewriter
rewriteFieldNames TyCon
tyCon [Ct]
_givens [Type]
args
  | Bool -> Bool
not ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args)
  , let rowTy :: Type
rowTy = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
args
  , Just [(FastString, Type)]
fields <- Type -> Maybe [(FastString, Type)]
walkRowFields_maybe Type
rowTy
  = do
      let names :: [Type]
names = ((FastString, Type) -> Type) -> [(FastString, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (FastString -> Type
mkStrLitTy (FastString -> Type)
-> ((FastString, Type) -> FastString) -> (FastString, Type) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FastString, Type) -> FastString
forall a b. (a, b) -> a
fst) [(FastString, Type)]
fields
          reducedTy :: Type
reducedTy = Type -> [Type] -> Type
mkPromotedListTy Type
typeSymbolKind [Type]
names
      TcPluginRewriteResult -> TcPluginM 'Rewrite TcPluginRewriteResult
forall a. a -> TcPluginM 'Rewrite a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginRewriteResult -> TcPluginM 'Rewrite TcPluginRewriteResult)
-> TcPluginRewriteResult
-> TcPluginM 'Rewrite TcPluginRewriteResult
forall a b. (a -> b) -> a -> b
$ TcPluginRewriteTo
        { tcRewriterNewWanteds :: [Ct]
tcRewriterNewWanteds = []
        , tcPluginReduction :: Reduction
tcPluginReduction    =
            String
-> Role -> [Coercion] -> TyCon -> [Type] -> Type -> Reduction
mkTyFamAppReduction String
"polytropos" Role
Nominal [] TyCon
tyCon [Type]
args Type
reducedTy
        }
  | Bool
otherwise = TcPluginRewriteResult -> TcPluginM 'Rewrite TcPluginRewriteResult
forall a. a -> TcPluginM 'Rewrite a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TcPluginNoRewrite

rewriteSimpleFieldTypes :: TyCon -> [Ct] -> [Type] -> TcPluginM 'Rewrite TcPluginRewriteResult
rewriteSimpleFieldTypes :: TyCon -> TcPluginRewriter
rewriteSimpleFieldTypes TyCon
tyCon [Ct]
_givens [Type]
args
  | Bool -> Bool
not ([Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args)
  , let rowTy :: Type
rowTy = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
args
  , Just [(FastString, Type)]
fields <- Type -> Maybe [(FastString, Type)]
walkRowFields_maybe Type
rowTy
  = do
      let pairKind :: Type
pairKind = Boxity -> [Type] -> Type
mkTupleTy Boxity
Boxed [Type
typeSymbolKind, Type
liftedTypeKind]
          pairs :: [Type]
pairs = [ Type -> Type -> Type -> Type -> Type
mkPromotedPairTy Type
typeSymbolKind Type
liftedTypeKind (FastString -> Type
mkStrLitTy FastString
name) Type
ty
                  | (FastString
name, Type
ty) <- [(FastString, Type)]
fields
                  ]
          reducedTy :: Type
reducedTy = Type -> [Type] -> Type
mkPromotedListTy Type
pairKind [Type]
pairs
      TcPluginRewriteResult -> TcPluginM 'Rewrite TcPluginRewriteResult
forall a. a -> TcPluginM 'Rewrite a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginRewriteResult -> TcPluginM 'Rewrite TcPluginRewriteResult)
-> TcPluginRewriteResult
-> TcPluginM 'Rewrite TcPluginRewriteResult
forall a b. (a -> b) -> a -> b
$ TcPluginRewriteTo
        { tcRewriterNewWanteds :: [Ct]
tcRewriterNewWanteds = []
        , tcPluginReduction :: Reduction
tcPluginReduction    =
            String
-> Role -> [Coercion] -> TyCon -> [Type] -> Type -> Reduction
mkTyFamAppReduction String
"polytropos" Role
Nominal [] TyCon
tyCon [Type]
args Type
reducedTy
        }
  | Bool
otherwise = TcPluginRewriteResult -> TcPluginM 'Rewrite TcPluginRewriteResult
forall a. a -> TcPluginM 'Rewrite a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TcPluginNoRewrite

rewriteFieldTypes :: TyCon -> [Ct] -> [Type] -> TcPluginM 'Rewrite TcPluginRewriteResult
rewriteFieldTypes :: TyCon -> TcPluginRewriter
rewriteFieldTypes TyCon
tyCon [Ct]
_givens [Type]
args
  | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
  , let rowTy :: Type
rowTy = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
args
  , let fTy :: Type
fTy   = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
  , Just [(FastString, Type)]
fields <- Type -> Maybe [(FastString, Type)]
walkRowFields_maybe Type
rowTy
  = do
      let pairKind :: Type
pairKind = Boxity -> [Type] -> Type
mkTupleTy Boxity
Boxed [Type
typeSymbolKind, Type
liftedTypeKind]
          pairs :: [Type]
pairs = [ Type -> Type -> Type -> Type -> Type
mkPromotedPairTy Type
typeSymbolKind Type
liftedTypeKind (FastString -> Type
mkStrLitTy FastString
name) (Type -> Type -> Type
mkAppTy Type
fTy Type
ty)
                  | (FastString
name, Type
ty) <- [(FastString, Type)]
fields
                  ]
          reducedTy :: Type
reducedTy = Type -> [Type] -> Type
mkPromotedListTy Type
pairKind [Type]
pairs
      TcPluginRewriteResult -> TcPluginM 'Rewrite TcPluginRewriteResult
forall a. a -> TcPluginM 'Rewrite a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginRewriteResult -> TcPluginM 'Rewrite TcPluginRewriteResult)
-> TcPluginRewriteResult
-> TcPluginM 'Rewrite TcPluginRewriteResult
forall a b. (a -> b) -> a -> b
$ TcPluginRewriteTo
        { tcRewriterNewWanteds :: [Ct]
tcRewriterNewWanteds = []
        , tcPluginReduction :: Reduction
tcPluginReduction    =
            String
-> Role -> [Coercion] -> TyCon -> [Type] -> Type -> Reduction
mkTyFamAppReduction String
"polytropos" Role
Nominal [] TyCon
tyCon [Type]
args Type
reducedTy
        }
  | Bool
otherwise = TcPluginRewriteResult -> TcPluginM 'Rewrite TcPluginRewriteResult
forall a. a -> TcPluginM 'Rewrite a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
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 :: String -> String -> Int
levenshtein String
s1 String
s2 =
  let n :: Int
n = String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s1
      initRow :: [Int]
initRow = [Int
0 .. Int
n]
      stepRow :: [Int] -> Char -> [Int]
stepRow [Int]
row Char
c2 = case [Int]
row of
        [] -> []
        Int
d : [Int]
ds -> (Int -> (Char, Int, Int) -> Int)
-> Int -> [(Char, Int, Int)] -> [Int]
forall b a. (b -> a -> b) -> b -> [a] -> [b]
scanl (\Int
left (Char
c1, Int
diag, Int
above) ->
                           let cost :: Int
cost = if Char
c1 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c2 then Int
0 else Int
1
                           in Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Int
diag Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
cost) (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Int
left Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
above Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)))
                        (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                        (String -> [Int] -> [Int] -> [(Char, Int, Int)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 String
s1 [Int]
row [Int]
ds)
  in case ([Int] -> Char -> [Int]) -> [Int] -> String -> [Int]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' [Int] -> Char -> [Int]
stepRow [Int]
initRow String
s2 of
       [] -> Int
0
       [Int]
res -> [Int] -> Int
forall a. HasCallStack => [a] -> a
last [Int]
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 :: String -> [String] -> [String]
suggestSimilar String
target [String]
candidates =
  let scored :: [(String, Int)]
scored = [ (String
c, Int
d) | String
c <- [String]
candidates, let d :: Int
d = String -> String -> Int
levenshtein String
target String
c, Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
2 ]
  in ((String, Int) -> String) -> [(String, Int)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Int) -> String
forall a b. (a, b) -> a
fst (((String, Int) -> Int) -> [(String, Int)] -> [(String, Int)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (String, Int) -> Int
forall a b. (a, b) -> b
snd [(String, Int)]
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 :: [(Int, FastString, Type)] -> String
formatRecordRow [(Int, FastString, Type)]
fields =
  String
"{ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [ FastString -> String
unpackFS FastString
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) | (Int
_, FastString
n, Type
ty) <- [(Int, FastString, Type)]
fields ] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" }"

-- | 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 :: [(Int, FastString, Type)] -> String
formatVariantRow [(Int, FastString, Type)]
ctors =
  String
"< " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" | " (((Int, FastString, Type) -> String)
-> [(Int, FastString, Type)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, FastString, Type) -> String
forall {a}. (a, FastString, Type) -> String
formatCtor [(Int, FastString, Type)]
ctors) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" >"
  where
    formatCtor :: (a, FastString, Type) -> String
formatCtor (a
_, FastString
n, Type
conRowTy) =
      case Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
conRowTy of
        [] -> FastString -> String
unpackFS FastString
n
        [(Int
_, FastString
fn, Type
ty)] | FastString -> Bool
nullFS FastString
fn -> FastString -> String
unpackFS FastString
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
        [(Int, FastString, Type)]
fs -> FastString -> String
unpackFS FastString
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, FastString, Type)] -> String
formatRecordRow [(Int, FastString, Type)]
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 :: String -> [String] -> String
formatSuggestion String
target [String]
candidates =
  case String -> [String] -> [String]
suggestSimilar String
target [String]
candidates of
    [] -> case [String]
candidates of
      [] -> String
"(no fields in record)"
      [String]
_  -> String
"Available fields: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
c -> String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'") [String]
candidates)
    [String]
suggs -> String
"Did you mean: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" or " ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'") [String]
suggs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"?"

-- | Formats a constructor suggestion clause for variants.
formatCtorSuggestion :: String -> [String] -> String
formatCtorSuggestion :: String -> [String] -> String
formatCtorSuggestion String
target [String]
candidates =
  case String -> [String] -> [String]
suggestSimilar String
target [String]
candidates of
    [] -> case [String]
candidates of
      [] -> String
"(no constructors in variant)"
      [String]
_  -> String
"Available constructors: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
c -> String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'") [String]
candidates)
    [String]
suggs -> String
"Did you mean: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" or " ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'") [String]
suggs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"?"

-- | 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 :: Type -> Bool
isClosedType Type
ty = VarSet -> Bool
isEmptyVarSet (Type -> VarSet
tyCoVarsOfType (Type -> Type
unwrapSynonyms Type
ty))

-- | Wraps a Haskell string into GHC's promoted 'Text constructor for type-level ErrorMessage.
mkTextMsg :: PluginState -> String -> Type
mkTextMsg :: PluginState -> String -> Type
mkTextMsg PluginState
state String
s = TyCon -> [Type] -> Type
mkTyConApp (PluginState -> TyCon
psPromotedText PluginState
state) [FastString -> Type
mkStrLitTy (String -> FastString
fsLit String
s)]

-- | Combines multiple promoted 'Text messages vertically using ':$$: (promoted Vcat).
mkVcatMsgs :: PluginState -> [Type] -> Type
mkVcatMsgs :: PluginState -> [Type] -> Type
mkVcatMsgs PluginState
_ [] = String -> Type
forall a. HasCallStack => String -> a
error String
"mkVcatMsgs: empty list"
mkVcatMsgs PluginState
_ [Type
m] = Type
m
mkVcatMsgs PluginState
state (Type
m : [Type]
ms) = TyCon -> [Type] -> Type
mkTyConApp (PluginState -> TyCon
psPromotedVcat PluginState
state) [Type
m, PluginState -> [Type] -> Type
mkVcatMsgs PluginState
state [Type]
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 :: PluginState -> CtLoc -> [String] -> TcPluginM 'Solve Ct
mkTypeErrorCt PluginState
state CtLoc
loc [String]
msgLines = do
  let msgTys :: [Type]
msgTys = (String -> Type) -> [String] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (PluginState -> String -> Type
mkTextMsg PluginState
state) [String]
msgLines
      fullMsg :: Type
fullMsg = PluginState -> [Type] -> Type
mkVcatMsgs PluginState
state [Type]
msgTys
      predTy :: Type
predTy = TyCon -> [Type] -> Type
mkTyConApp (PluginState -> TyCon
psTypeErrorTyCon PluginState
state) [Type
constraintKind, Type
fullMsg]
  ev <- CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted CtLoc
loc Type
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 :: PluginState -> Class -> [Type] -> TcPluginM 'Solve EvTerm
mkDummyHasFieldDict PluginState
state Class
cls [Type]
tys = do
  let getFieldId :: Var
getFieldId = case Class -> [Var]
classMethods Class
cls of
        (Var
m : [Var]
_) -> Var
m
        [] -> String -> Var
forall a. HasCallStack => String -> a
error String
"Polytropos.Plugin: HasField has no methods"
      methodFullTy :: Type
methodFullTy = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (Var -> Type
varType Var
getFieldId) [Type]
tys
      (Type
_, Type
_, Type
methodInDictTy) = Type -> (Type, Type, Type)
splitFunTy Type
methodFullTy
      ([Var]
tyVars, Type
tauTy) = Type -> ([Var], Type)
splitForAllTyCoVars Type
methodInDictTy
      ([Scaled Type]
argTys, Type
_) = Type -> ([Scaled Type], Type)
splitFunTys Type
tauTy
      scaledRTy :: Scaled Type
scaledRTy = [Scaled Type]
argTys [Scaled Type] -> Int -> Scaled Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
0
      fieldTy :: Type
fieldTy = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
tys
  rName <- TcM Name -> TcPluginM 'Solve Name
forall a. TcM a -> TcPluginM 'Solve a
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM Name -> TcPluginM 'Solve Name)
-> TcM Name -> TcPluginM 'Solve Name
forall a b. (a -> b) -> a -> b
$ OccName -> TcM Name
newName (String -> OccName
mkVarOcc String
"rec")
  let rVar = HasDebugCallStack => Name -> Type -> Type -> Var
Name -> Type -> Type -> Var
mkLocalId Name
rName (Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult Scaled Type
scaledRTy) (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
scaledRTy)
      -- dummyVal = noInlineUnsafeCo () :: fieldTy
      dummyVal = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psNoInlineCo PluginState
state))
                   [ Type -> CoreExpr
forall b. Type -> Expr b
Type (TyCon -> Type
mkTyConTy TyCon
unitTyCon)
                   , Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy
                   , DataCon -> [CoreExpr] -> CoreExpr
mkCoreConApps DataCon
unitDataCon []
                   ]
      -- getFieldExpr = \rec -> dummyVal
      getFieldExpr = [Var] -> CoreExpr -> CoreExpr
mkCoreLams ([Var]
tyVars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var
rVar]) CoreExpr
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 :: PluginState -> TcPluginSolver
polytroposSolve PluginState
state [Ct]
givens [Ct]
wanteds = do
  let allCts :: [Ct]
allCts = [Ct]
givens [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
wanteds
  results <- (Ct -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> [Ct] -> TcPluginM 'Solve [Either ((EvTerm, Ct), [Ct]) ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (PluginState
-> Ct -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveOne PluginState
state) [Ct]
allCts
  let (solvedPairs, _) = partitionEithers results
      solvedCts = (((EvTerm, Ct), [Ct]) -> (EvTerm, Ct))
-> [((EvTerm, Ct), [Ct])] -> [(EvTerm, Ct)]
forall a b. (a -> b) -> [a] -> [b]
map ((EvTerm, Ct), [Ct]) -> (EvTerm, Ct)
forall a b. (a, b) -> a
fst [((EvTerm, Ct), [Ct])]
solvedPairs
      newCts = (((EvTerm, Ct), [Ct]) -> [Ct]) -> [((EvTerm, Ct), [Ct])] -> [Ct]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((EvTerm, Ct), [Ct]) -> [Ct]
forall a b. (a, b) -> b
snd [((EvTerm, Ct), [Ct])]
solvedPairs
  pure $ TcPluginSolveResult
    { tcPluginInsolubleCts = []
    , tcPluginSolvedCts = solvedCts
    , tcPluginNewCts = newCts
    }

solveOne :: PluginState -> Ct -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveOne :: PluginState
-> Ct -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveOne PluginState
state Ct
ct
  | Bool -> Bool
not (CtEvidence -> Bool
isWanted (Ct -> CtEvidence
ctEvidence Ct
ct))
  = Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise
  = do
    let predTy :: Type
predTy = Ct -> Type
ctPred Ct
ct
    case HasDebugCallStack => Type -> Pred
Type -> Pred
classifyPredType Type
predTy of
      ClassPred Class
cls [Type]
tys -> do
        case Class -> Name
className Class
cls of
          Name
name
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"FieldIndex"
            -> PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveFieldIndex PluginState
state Ct
ct Class
cls [Type]
tys
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"ConstructorIndex"
            -> PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveConstructorIndex PluginState
state Ct
ct Class
cls [Type]
tys
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"RowEq"
            -> PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveRowEq PluginState
state Ct
ct Class
cls [Type]
tys
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"RowShow"
            -> PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveRowShow PluginState
state Ct
ct Class
cls [Type]
tys
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"RowEqSum"
            -> PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveRowEqSum PluginState
state Ct
ct Class
cls [Type]
tys
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"RowShowSum"
            -> PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveRowShowSum PluginState
state Ct
ct Class
cls [Type]
tys
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"HasField"
            -> PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveHasField PluginState
state Ct
ct Class
cls [Type]
tys
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"AllFields"
            -> PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveAllFields PluginState
state Ct
ct Class
cls [Type]
tys
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"SubRow"
            -> PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveSubRow PluginState
state Ct
ct Class
cls [Type]
tys
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"SubSum"
            -> PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveSubSum PluginState
state Ct
ct Class
cls [Type]
tys
            | Name -> OccName
nameOccName Name
name OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== String -> OccName
mkTcOcc String
"KnownHash"
            -> Either (EvTerm, Ct) () -> Either ((EvTerm, Ct), [Ct]) ()
forall {a} {a}. Either a () -> Either (a, [a]) ()
noNew (Either (EvTerm, Ct) () -> Either ((EvTerm, Ct), [Ct]) ())
-> TcPluginM 'Solve (Either (EvTerm, Ct) ())
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct -> Class -> [Type] -> TcPluginM 'Solve (Either (EvTerm, Ct) ())
solveKnownHash Ct
ct Class
cls [Type]
tys
            | Bool
otherwise
            -> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right ()
      Pred
_ -> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right ()
  where
    noNew :: Either a () -> Either (a, [a]) ()
noNew (Left a
res) = (a, [a]) -> Either (a, [a]) ()
forall a b. a -> Either a b
Left (a
res, [])
    noNew (Right ()) = () -> Either (a, [a]) ()
forall a b. b -> Either a b
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 :: PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveFieldIndex PluginState
state Ct
ct Class
cls [Type]
tys
  | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3 = do
      let nTy :: Type
nTy         = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
3)
          rowTy :: Type
rowTy       = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
          expectedATy :: Type
expectedATy = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
tys
          unwrapN :: Type
unwrapN     = Type -> Type
unwrapSynonyms Type
nTy
          loc :: CtLoc
loc         = Ct -> CtLoc
ctLoc Ct
ct
      case Type -> Maybe FastString
isStrLitTy Type
unwrapN of
        Just FastString
fieldName -> do
          -- Named field lookup by type-level Symbol
          case FastString -> Type -> Maybe (Int, Type)
findFieldType FastString
fieldName Type
rowTy of
            Just (Int
i, Type
actualTy)
              -- Accept exact type match, or uninstantiated type variable awaiting unification
              | Type
actualTy HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
expectedATy Bool -> Bool -> Bool
|| Bool -> Bool
not (Type -> Bool
isClosedType Type
expectedATy) -> do
                  let iExpr :: CoreExpr
iExpr = Int -> CoreExpr
mkIntExpr Int
i
                      dictExpr :: CoreExpr
dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
iExpr]
                  Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ ((EvTerm, Ct), [Ct]) -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. a -> Either a b
Left ((CoreExpr -> EvTerm
EvExpr CoreExpr
dictExpr, Ct
ct), [])
              -- Terminal type discrepancy: emit diagnostic and safe dummy evidence
              | Bool
otherwise -> do
                  let dummyExpr :: CoreExpr
dummyExpr = Int -> CoreExpr
mkIntExpr Int
0
                      dummyDict :: CoreExpr
dummyDict = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
dummyExpr]
                      diagLines :: [String]
diagLines =
                        [ String
"Polytropos Record Error:"
                        , String
"  Field '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FastString -> String
unpackFS FastString
fieldName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' in record has type:"
                        , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
actualTy)
                        , String
"  but expected:"
                        , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
expectedATy)
                        ]
                  errCt <- PluginState -> CtLoc -> [String] -> TcPluginM 'Solve Ct
mkTypeErrorCt PluginState
state CtLoc
loc [String]
diagLines
                  pure $ Left ((EvExpr dummyDict, ct), [errCt])
            Maybe (Int, Type)
Nothing -> do
              -- Field not found: format schema and compute fuzzy typo suggestions
              case Type -> Maybe [(Int, FastString, Type)]
walkRowWithTypes_maybe Type
rowTy of
                Just [(Int, FastString, Type)]
fields -> do
                  let dummyExpr :: CoreExpr
dummyExpr = Int -> CoreExpr
mkIntExpr Int
0
                      dummyDict :: CoreExpr
dummyDict = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
dummyExpr]
                      fNames :: [String]
fNames = [ FastString -> String
unpackFS FastString
n | (Int
_, FastString
n, Type
_) <- [(Int, FastString, Type)]
fields, Bool -> Bool
not (FastString -> Bool
nullFS FastString
n) ]
                      diagLines :: [String]
diagLines =
                        [ String
"Polytropos Record Error:"
                        , String
"  Field '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FastString -> String
unpackFS FastString
fieldName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' does not exist in record:"
                        , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, FastString, Type)] -> String
formatRecordRow [(Int, FastString, Type)]
fields
                        , String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
formatSuggestion (FastString -> String
unpackFS FastString
fieldName) [String]
fNames
                        ]
                  errCt <- PluginState -> CtLoc -> [String] -> TcPluginM 'Solve Ct
mkTypeErrorCt PluginState
state CtLoc
loc [String]
diagLines
                  pure $ Left ((EvExpr dummyDict, ct), [errCt])
                Maybe [(Int, FastString, Type)]
Nothing -> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right () -- Row tail is still open/unfixed: defer solving
        Maybe FastString
Nothing -> do
          -- Anonymous/positional field lookup by payload Type
          case Type -> Type -> Maybe Int
findFieldIndexByType Type
unwrapN Type
rowTy of
            Just Int
i -> do
              let iExpr :: CoreExpr
iExpr = Int -> CoreExpr
mkIntExpr Int
i
                  dictExpr :: CoreExpr
dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
iExpr]
              Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ ((EvTerm, Ct), [Ct]) -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. a -> Either a b
Left ((CoreExpr -> EvTerm
EvExpr CoreExpr
dictExpr, Ct
ct), [])
            Maybe Int
Nothing -> do
              case Type -> Maybe [(Int, FastString, Type)]
walkRowWithTypes_maybe Type
rowTy of
                Just [(Int, FastString, Type)]
fields -> do
                  let dummyExpr :: CoreExpr
dummyExpr = Int -> CoreExpr
mkIntExpr Int
0
                      dummyDict :: CoreExpr
dummyDict = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
dummyExpr]
                      diagLines :: [String]
diagLines =
                        [ String
"Polytropos Record Error:"
                        , String
"  Type '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
unwrapN) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' is not a field in record:"
                        , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, FastString, Type)] -> String
formatRecordRow [(Int, FastString, Type)]
fields
                        ]
                  errCt <- PluginState -> CtLoc -> [String] -> TcPluginM 'Solve Ct
mkTypeErrorCt PluginState
state CtLoc
loc [String]
diagLines
                  pure $ Left ((EvExpr dummyDict, ct), [errCt])
                Maybe [(Int, FastString, Type)]
Nothing -> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise = Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
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 :: PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveConstructorIndex PluginState
state Ct
ct Class
cls [Type]
tys
  | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2 = do
      let nTy :: Type
nTy   = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
          rowTy :: Type
rowTy = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
          unwrapN :: Type
unwrapN = Type -> Type
unwrapSynonyms Type
nTy
          loc :: CtLoc
loc = Ct -> CtLoc
ctLoc Ct
ct
      case Type -> Maybe FastString
isStrLitTy Type
unwrapN of
        Just FastString
conName -> do
          -- Named constructor lookup by type-level Symbol
          case FastString -> Type -> Maybe Word
findConstructorIndex FastString
conName Type
rowTy of
            Just Word
w -> do
              let wExpr :: CoreExpr
wExpr = Word -> CoreExpr
mkWordExpr Word
w
                  dictExpr :: CoreExpr
dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
wExpr]
              Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ ((EvTerm, Ct), [Ct]) -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. a -> Either a b
Left ((CoreExpr -> EvTerm
EvExpr CoreExpr
dictExpr, Ct
ct), [])
            Maybe Word
Nothing -> do
              -- Missing constructor: format variant schema and fuzzy suggestions
              case Type -> Maybe [(Int, FastString, Type)]
walkSumRowWithTypes_maybe Type
rowTy of
                Just [(Int, FastString, Type)]
ctors -> do
                  let dummyExpr :: CoreExpr
dummyExpr = Word -> CoreExpr
mkWordExpr Word
0
                      dummyDict :: CoreExpr
dummyDict = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
dummyExpr]
                      cNames :: [String]
cNames = [ FastString -> String
unpackFS FastString
n | (Int
_, FastString
n, Type
_) <- [(Int, FastString, Type)]
ctors, Bool -> Bool
not (FastString -> Bool
nullFS FastString
n) ]
                      diagLines :: [String]
diagLines =
                        [ String
"Polytropos Variant Error:"
                        , String
"  Constructor '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FastString -> String
unpackFS FastString
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' is not a member of variant:"
                        , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, FastString, Type)] -> String
formatVariantRow [(Int, FastString, Type)]
ctors
                        , String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
formatCtorSuggestion (FastString -> String
unpackFS FastString
conName) [String]
cNames
                        ]
                  errCt <- PluginState -> CtLoc -> [String] -> TcPluginM 'Solve Ct
mkTypeErrorCt PluginState
state CtLoc
loc [String]
diagLines
                  pure $ Left ((EvExpr dummyDict, ct), [errCt])
                Maybe [(Int, FastString, Type)]
Nothing -> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right () -- Open sum tail: defer solving
        Maybe FastString
Nothing -> do
          -- Anonymous constructor lookup by payload Type
          case Type -> Type -> Maybe Word
findConstructorIndexByType Type
unwrapN Type
rowTy of
            Just Word
w -> do
              let wExpr :: CoreExpr
wExpr = Word -> CoreExpr
mkWordExpr Word
w
                  dictExpr :: CoreExpr
dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
wExpr]
              Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ ((EvTerm, Ct), [Ct]) -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. a -> Either a b
Left ((CoreExpr -> EvTerm
EvExpr CoreExpr
dictExpr, Ct
ct), [])
            Maybe Word
Nothing -> do
              case Type -> Maybe [(Int, FastString, Type)]
walkSumRowWithTypes_maybe Type
rowTy of
                Just [(Int, FastString, Type)]
ctors -> do
                  let dummyExpr :: CoreExpr
dummyExpr = Word -> CoreExpr
mkWordExpr Word
0
                      dummyDict :: CoreExpr
dummyDict = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
dummyExpr]
                      diagLines :: [String]
diagLines =
                        [ String
"Polytropos Variant Error:"
                        , String
"  Type '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
unwrapN) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' is not a payload type in variant:"
                        , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, FastString, Type)] -> String
formatVariantRow [(Int, FastString, Type)]
ctors
                        ]
                  errCt <- PluginState -> CtLoc -> [String] -> TcPluginM 'Solve Ct
mkTypeErrorCt PluginState
state CtLoc
loc [String]
diagLines
                  pure $ Left ((EvExpr dummyDict, ct), [errCt])
                Maybe [(Int, FastString, Type)]
Nothing -> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise = Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
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 :: PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveRowEq PluginState
state Ct
ct Class
cls [Type]
tys = do
  let rowTy :: Type
rowTy  = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
tys
      rTy :: Type
rTy    = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
      fields :: [(Int, FastString, Type)]
fields = Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
rowTy
      loc :: CtLoc
loc    = Ct -> CtLoc
ctLoc Ct
ct

      -- Superclass evidence for RowFlavour r
      scEvidence :: CoreExpr
scEvidence = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon (PluginState -> Class
psRowFlavourCls PluginState
state)) [Type
rTy] []

      -- Extract repEq method type and bind lambda arguments: \r1 r2 -> ...
      repEqId :: Var
repEqId = case Class -> [Var]
classMethods Class
cls of
        (Var
m : [Var]
_) -> Var
m
        []      -> String -> Var
forall a. HasCallStack => String -> a
error String
"Polytropos.Plugin: RowEq class has no methods"
      methodFullTy :: Type
methodFullTy = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (Var -> Type
varType Var
repEqId) [Type]
tys
      (Type
_, Type
_, Type
methodInDictTy) = Type -> (Type, Type, Type)
splitFunTy Type
methodFullTy
      ([Var]
tyVars, Type
tauTy) = Type -> ([Var], Type)
splitForAllTyCoVars Type
methodInDictTy
      ([Scaled Type]
argTys, Type
_) = Type -> ([Scaled Type], Type)
splitFunTys Type
tauTy
      scaledR1Ty :: Scaled Type
scaledR1Ty = [Scaled Type]
argTys [Scaled Type] -> Int -> Scaled Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
0
      scaledR2Ty :: Scaled Type
scaledR2Ty = [Scaled Type]
argTys [Scaled Type] -> Int -> Scaled Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
1

  r1Name <- TcM Name -> TcPluginM 'Solve Name
forall a. TcM a -> TcPluginM 'Solve a
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM Name -> TcPluginM 'Solve Name)
-> TcM Name -> TcPluginM 'Solve Name
forall a b. (a -> b) -> a -> b
$ OccName -> TcM Name
newName (String -> OccName
mkVarOcc String
"r1")
  r2Name <- unsafeLiftTcM $ newName (mkVarOcc "r2")
  let r1Var = HasDebugCallStack => Name -> Type -> Type -> Var
Name -> Type -> Type -> Var
mkLocalId Name
r1Name (Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult Scaled Type
scaledR1Ty) (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
scaledR1Ty)
      r2Var = HasDebugCallStack => Name -> Type -> Type -> Var
Name -> Type -> Type -> Var
mkLocalId Name
r2Name (Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult Scaled Type
scaledR2Ty) (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
scaledR2Ty)

      kATy   = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
      fTy    = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
      aTy    = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
      kRowTy = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
rowTy

      -- Unpack RowRep wrappers: unRowRep r1, unRowRep r2
      unRowRepTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kRowTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
rTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
rowTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy]
      rep1 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psUnRowRep PluginState
state)) ([CoreExpr]
unRowRepTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [Var -> CoreExpr
forall b. Var -> Expr b
Var Var
r1Var])
      rep2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psUnRowRep PluginState
state)) ([CoreExpr]
unRowRepTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [Var -> CoreExpr
forall b. Var -> Expr b
Var Var
r2Var])

      -- Structural header checks: repTag and repArity
      repTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy]
      tag1 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psRepTag PluginState
state)) ([CoreExpr]
repTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
rep1])
      tag2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psRepTag PluginState
state)) ([CoreExpr]
repTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
rep2])
      eqTag = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psEqClass PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type (TyCon -> Type
mkTyConTy TyCon
wordTyCon), Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFEqWord PluginState
state), CoreExpr
tag1, CoreExpr
tag2]

      arity1 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psRepArity PluginState
state)) ([CoreExpr]
repTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
rep1])
      arity2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psRepArity PluginState
state)) ([CoreExpr]
repTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
rep2])
      eqArity = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psEqClass PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFEqInt PluginState
state), CoreExpr
arity1, CoreExpr
arity2]

  -- Spawn wanted Eq constraints for every field type in the row
  wanteds <- forM fields $ \(Int
i, FastString
_nameFS, Type
fieldTy) -> do
    ev <- CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted CtLoc
loc (Type -> Type -> Type
mkAppTy (TyCon -> Type
mkTyConTy (Class -> TyCon
classTyCon (PluginState -> Class
psEqCls PluginState
state))) Type
fieldTy)
    pure (i, fieldTy, ev)

  -- Synthesize comparison expression for slot i:
  -- (==) @fieldTy eqDict (noInlineUnsafeCo (fieldAt @i rep1)) (noInlineUnsafeCo (fieldAt @i rep2))
  let compareField (Int
i, Type
fieldTy, CtEvidence
ev) =
        let fieldAtTypeArgs :: [CoreExpr]
fieldAtTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy]
            idxExpr :: CoreExpr
idxExpr = Int -> CoreExpr
mkIntExpr Int
i
            raw1 :: CoreExpr
raw1 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFieldAt PluginState
state)) ([CoreExpr]
fieldAtTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
idxExpr, CoreExpr
rep1])
            raw2 :: CoreExpr
raw2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFieldAt PluginState
state)) ([CoreExpr]
fieldAtTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
idxExpr, CoreExpr
rep2])
            fFieldTy :: Type
fFieldTy = Type -> Type -> Type
mkAppTy Type
fTy Type
fieldTy
            val1 :: CoreExpr
val1 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psNoInlineCo PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fFieldTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
raw1]
            val2 :: CoreExpr
val2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psNoInlineCo PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fFieldTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
raw2]
            eqDict :: CoreExpr
eqDict = HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
ev
        in CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psEqClass PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
eqDict, CoreExpr
val1, CoreExpr
val2]

      fieldComps = ((Int, Type, CtEvidence) -> CoreExpr)
-> [(Int, Type, CtEvidence)] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Type, CtEvidence) -> CoreExpr
compareField [(Int, Type, CtEvidence)]
wanteds

      -- Fold all comparisons left-to-right with short-circuiting Boolean (&&)
      andFn CoreExpr
e1 CoreExpr
e2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psAnd PluginState
state)) [CoreExpr
e1, CoreExpr
e2]
      bodyExpr = (CoreExpr -> CoreExpr -> CoreExpr)
-> CoreExpr -> [CoreExpr] -> CoreExpr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CoreExpr -> CoreExpr -> CoreExpr
andFn (CoreExpr -> CoreExpr -> CoreExpr
andFn CoreExpr
eqTag CoreExpr
eqArity) [CoreExpr]
fieldComps
      repEqExpr = [Var] -> CoreExpr -> CoreExpr
mkCoreLams ([Var]
tyVars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var
r1Var, Var
r2Var]) CoreExpr
bodyExpr

      dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
scEvidence, CoreExpr
repEqExpr]
      newWanteds = [CtEvidence -> Ct
mkNonCanonical CtEvidence
ev | (Int
_, Type
_, CtEvidence
ev) <- [(Int, Type, CtEvidence)]
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 :: PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveRowShow PluginState
state Ct
ct Class
cls [Type]
tys = do
  let rowTy :: Type
rowTy  = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
tys
      rTy :: Type
rTy    = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
      fields :: [(Int, FastString, Type)]
fields = Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
rowTy
      loc :: CtLoc
loc    = Ct -> CtLoc
ctLoc Ct
ct

      -- Superclass evidence for RowFlavour r
      scEvidence :: CoreExpr
scEvidence = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon (PluginState -> Class
psRowFlavourCls PluginState
state)) [Type
rTy] []

      -- Extract repShowsPrec method type and bind lambda arguments: \p r -> ...
      repShowsPrecId :: Var
repShowsPrecId = case Class -> [Var]
classMethods Class
cls of
        (Var
m : [Var]
_) -> Var
m
        []      -> String -> Var
forall a. HasCallStack => String -> a
error String
"Polytropos.Plugin: RowShow class has no methods"
      methodFullTy :: Type
methodFullTy = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (Var -> Type
varType Var
repShowsPrecId) [Type]
tys
      (Type
_, Type
_, Type
methodInDictTy) = Type -> (Type, Type, Type)
splitFunTy Type
methodFullTy
      ([Var]
tyVars, Type
tauTy) = Type -> ([Var], Type)
splitForAllTyCoVars Type
methodInDictTy
      ([Scaled Type]
argTys, Type
_) = Type -> ([Scaled Type], Type)
splitFunTys Type
tauTy
      scaledPrecTy :: Scaled Type
scaledPrecTy = [Scaled Type]
argTys [Scaled Type] -> Int -> Scaled Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
0
      scaledRTy :: Scaled Type
scaledRTy    = [Scaled Type]
argTys [Scaled Type] -> Int -> Scaled Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
1

  precName <- TcM Name -> TcPluginM 'Solve Name
forall a. TcM a -> TcPluginM 'Solve a
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM Name -> TcPluginM 'Solve Name)
-> TcM Name -> TcPluginM 'Solve Name
forall a b. (a -> b) -> a -> b
$ OccName -> TcM Name
newName (String -> OccName
mkVarOcc String
"p")
  rName <- unsafeLiftTcM $ newName (mkVarOcc "r")
  let precVar = HasDebugCallStack => Name -> Type -> Type -> Var
Name -> Type -> Type -> Var
mkLocalId Name
precName (Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult Scaled Type
scaledPrecTy) (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
scaledPrecTy)
      rVar    = HasDebugCallStack => Name -> Type -> Type -> Var
Name -> Type -> Type -> Var
mkLocalId Name
rName (Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult Scaled Type
scaledRTy) (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
scaledRTy)

      kATy   = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
      fTy    = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
      aTy    = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
      kRowTy = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
rowTy

      -- Unpack RowRep wrapper: unRowRep r
      unRowRepTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kRowTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
rTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
rowTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy]
      rep = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psUnRowRep PluginState
state)) ([CoreExpr]
unRowRepTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [Var -> CoreExpr
forall b. Var -> Expr b
Var Var
rVar])

      -- Determine record display prefix
      rowName = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
rowTy of
        Just (TyCon
tc, [Type]
_)
          | let name :: String
name = OccName -> String
occNameString (TyCon -> OccName
forall a. NamedThing a => a -> OccName
getOccName TyCon
tc)
          , String
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
":" Bool -> Bool -> Bool
&& String
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"[]" Bool -> Bool -> Bool
&& String
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"''[]"
          -> String
name
        Maybe (TyCon, [Type])
_ -> String
"R" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([(Int, FastString, Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, FastString, Type)]
fields)

  prefixExpr <- unsafeLiftTcM $ mkStringExpr (rowName ++ " ")
  let prefixShowS = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psShowString PluginState
state)) [CoreExpr
prefixExpr]
      spaceShowS  = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psShowChar PluginState
state)) [Char -> CoreExpr
mkCharExpr Char
' ']

  -- Spawn wanted Show constraints for every field type in the row
  wanteds <- forM fields $ \(Int
i, FastString
_nameFS, Type
fieldTy) -> do
    ev <- CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted CtLoc
loc (Type -> Type -> Type
mkAppTy (TyCon -> Type
mkTyConTy (Class -> TyCon
classTyCon (PluginState -> Class
psShowCls PluginState
state))) Type
fieldTy)
    pure (i, fieldTy, ev)

  -- Synthesize ShowS expression for slot i:
  -- showsPrec @fieldTy showDict 0 (noInlineUnsafeCo (fieldAt @i rep))
  let showField (Int
i, Type
fieldTy, CtEvidence
ev) =
        let fieldAtTypeArgs :: [CoreExpr]
fieldAtTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy]
            idxExpr :: CoreExpr
idxExpr = Int -> CoreExpr
mkIntExpr Int
i
            raw :: CoreExpr
raw = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFieldAt PluginState
state)) ([CoreExpr]
fieldAtTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
idxExpr, CoreExpr
rep])
            fFieldTy :: Type
fFieldTy = Type -> Type -> Type
mkAppTy Type
fTy Type
fieldTy
            val :: CoreExpr
val = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psNoInlineCo PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fFieldTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
raw]
            showDict :: CoreExpr
showDict = HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
ev
            zeroPrec :: CoreExpr
zeroPrec = Int -> CoreExpr
mkIntExpr Int
0
        in CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psShowsPrecMeth PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
showDict, CoreExpr
zeroPrec, CoreExpr
val]

      fieldShows = ((Int, Type, CtEvidence) -> CoreExpr)
-> [(Int, Type, CtEvidence)] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Type, CtEvidence) -> CoreExpr
showField [(Int, Type, CtEvidence)]
wanteds
      showParts = case [CoreExpr]
fieldShows of
        [] -> [CoreExpr
prefixShowS]
        (CoreExpr
f0 : [CoreExpr]
fs) -> CoreExpr
prefixShowS CoreExpr -> [CoreExpr] -> [CoreExpr]
forall a. a -> [a] -> [a]
: CoreExpr
f0 CoreExpr -> [CoreExpr] -> [CoreExpr]
forall a. a -> [a] -> [a]
: (CoreExpr -> [CoreExpr]) -> [CoreExpr] -> [CoreExpr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\CoreExpr
f -> [CoreExpr
spaceShowS, CoreExpr
f]) [CoreExpr]
fs

      -- Chain all ShowS functions via (.) function composition
      compFn CoreExpr
f CoreExpr
g = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psComp PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
stringTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
stringTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
stringTy, CoreExpr
f, CoreExpr
g]
      bodyExpr = (CoreExpr -> CoreExpr -> CoreExpr) -> [CoreExpr] -> CoreExpr
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 CoreExpr -> CoreExpr -> CoreExpr
compFn [CoreExpr]
showParts
      repShowsPrecExpr = [Var] -> CoreExpr -> CoreExpr
mkCoreLams ([Var]
tyVars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var
precVar, Var
rVar]) CoreExpr
bodyExpr

      dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
scEvidence, CoreExpr
repShowsPrecExpr]
      newWanteds = [CtEvidence -> Ct
mkNonCanonical CtEvidence
ev | (Int
_, Type
_, CtEvidence
ev) <- [(Int, Type, CtEvidence)]
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 :: PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveRowEqSum PluginState
state Ct
ct Class
cls [Type]
tys = do
  let rowTy :: Type
rowTy  = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
tys
      rTy :: Type
rTy    = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
      constructors :: [(Int, FastString, Type)]
constructors = Type -> [(Int, FastString, Type)]
walkSumRowWithTypes Type
rowTy
      loc :: CtLoc
loc    = Ct -> CtLoc
ctLoc Ct
ct

      -- Superclass evidence for RowFlavour r
      scEvidence :: CoreExpr
scEvidence = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon (PluginState -> Class
psRowFlavourCls PluginState
state)) [Type
rTy] []

      -- Extract repEqSum method type and bind lambda arguments: \r1 r2 -> ...
      repEqSumId :: Var
repEqSumId = case Class -> [Var]
classMethods Class
cls of
        (Var
m : [Var]
_) -> Var
m
        []      -> String -> Var
forall a. HasCallStack => String -> a
error String
"Polytropos.Plugin: RowEqSum class has no methods"
      methodFullTy :: Type
methodFullTy = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (Var -> Type
varType Var
repEqSumId) [Type]
tys
      (Type
_, Type
_, Type
methodInDictTy) = Type -> (Type, Type, Type)
splitFunTy Type
methodFullTy
      ([Var]
tyVars, Type
tauTy) = Type -> ([Var], Type)
splitForAllTyCoVars Type
methodInDictTy
      ([Scaled Type]
argTys, Type
_) = Type -> ([Scaled Type], Type)
splitFunTys Type
tauTy
      scaledR1Ty :: Scaled Type
scaledR1Ty = [Scaled Type]
argTys [Scaled Type] -> Int -> Scaled Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
0
      scaledR2Ty :: Scaled Type
scaledR2Ty = [Scaled Type]
argTys [Scaled Type] -> Int -> Scaled Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
1

  r1Name <- TcM Name -> TcPluginM 'Solve Name
forall a. TcM a -> TcPluginM 'Solve a
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM Name -> TcPluginM 'Solve Name)
-> TcM Name -> TcPluginM 'Solve Name
forall a b. (a -> b) -> a -> b
$ OccName -> TcM Name
newName (String -> OccName
mkVarOcc String
"r1")
  r2Name <- unsafeLiftTcM $ newName (mkVarOcc "r2")
  let r1Var = HasDebugCallStack => Name -> Type -> Type -> Var
Name -> Type -> Type -> Var
mkLocalId Name
r1Name (Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult Scaled Type
scaledR1Ty) (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
scaledR1Ty)
      r2Var = HasDebugCallStack => Name -> Type -> Type -> Var
Name -> Type -> Type -> Var
mkLocalId Name
r2Name (Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult Scaled Type
scaledR2Ty) (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
scaledR2Ty)

      kATy   = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
      fTy    = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
      aTy    = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
      kRowTy = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
rowTy

      -- Unpack RowRep wrappers: unRowRep r1, unRowRep r2
      unRowRepTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kRowTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
rTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
rowTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy]
      rep1 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psUnRowRep PluginState
state)) ([CoreExpr]
unRowRepTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [Var -> CoreExpr
forall b. Var -> Expr b
Var Var
r1Var])
      rep2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psUnRowRep PluginState
state)) ([CoreExpr]
unRowRepTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [Var -> CoreExpr
forall b. Var -> Expr b
Var Var
r2Var])

      -- Extract and compare constructor tags: repTag rep1 == repTag rep2
      repTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy]
      tag1 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psRepTag PluginState
state)) ([CoreExpr]
repTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
rep1])
      tag2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psRepTag PluginState
state)) ([CoreExpr]
repTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
rep2])
      eqTag = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psEqClass PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type (TyCon -> Type
mkTyConTy TyCon
wordTyCon), Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFEqWord PluginState
state), CoreExpr
tag1, CoreExpr
tag2]

      falseExpr = DataCon -> [CoreExpr] -> CoreExpr
mkCoreConApps DataCon
falseDataCon []
      trueExpr  = DataCon -> [CoreExpr] -> CoreExpr
mkCoreConApps DataCon
trueDataCon []
      andFn CoreExpr
e1 CoreExpr
e2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psAnd PluginState
state)) [CoreExpr
e1, CoreExpr
e2]

  -- Spawn wanted Eq constraints for all fields of all constructors
  ctorWanteds <- forM constructors $ \(Int
i, FastString
conName, Type
conRowTy) -> do
    let fields :: [(Int, FastString, Type)]
fields = Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
conRowTy
    fWanteds <- [(Int, FastString, Type)]
-> ((Int, FastString, Type)
    -> TcPluginM 'Solve (Int, Type, CtEvidence))
-> TcPluginM 'Solve [(Int, Type, CtEvidence)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, FastString, Type)]
fields (((Int, FastString, Type)
  -> TcPluginM 'Solve (Int, Type, CtEvidence))
 -> TcPluginM 'Solve [(Int, Type, CtEvidence)])
-> ((Int, FastString, Type)
    -> TcPluginM 'Solve (Int, Type, CtEvidence))
-> TcPluginM 'Solve [(Int, Type, CtEvidence)]
forall a b. (a -> b) -> a -> b
$ \(Int
fi, FastString
_nameFS, Type
fieldTy) -> do
      ev <- CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted CtLoc
loc (Type -> Type -> Type
mkAppTy (TyCon -> Type
mkTyConTy (Class -> TyCon
classTyCon (PluginState -> Class
psEqCls PluginState
state))) Type
fieldTy)
      pure (fi, fieldTy, ev)
    pure (i, conName, fWanteds)

  -- Compare fields within an active constructor payload
  let compareConFields [(Int, Type, CtEvidence)]
fWanteds =
        let fieldComps :: [CoreExpr]
fieldComps = [ Int -> Type -> CtEvidence -> CoreExpr
compareField Int
fi Type
fieldTy CtEvidence
ev | (Int
fi, Type
fieldTy, CtEvidence
ev) <- [(Int, Type, CtEvidence)]
fWanteds ]
        in (CoreExpr -> CoreExpr -> CoreExpr)
-> CoreExpr -> [CoreExpr] -> CoreExpr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CoreExpr -> CoreExpr -> CoreExpr
andFn CoreExpr
trueExpr [CoreExpr]
fieldComps

      compareField Int
fi Type
fieldTy CtEvidence
ev =
        let fieldAtTypeArgs :: [CoreExpr]
fieldAtTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy]
            idxExpr :: CoreExpr
idxExpr = Int -> CoreExpr
mkIntExpr Int
fi
            raw1 :: CoreExpr
raw1 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFieldAt PluginState
state)) ([CoreExpr]
fieldAtTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
idxExpr, CoreExpr
rep1])
            raw2 :: CoreExpr
raw2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFieldAt PluginState
state)) ([CoreExpr]
fieldAtTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
idxExpr, CoreExpr
rep2])
            fFieldTy :: Type
fFieldTy = Type -> Type -> Type
mkAppTy Type
fTy Type
fieldTy
            val1 :: CoreExpr
val1 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psNoInlineCo PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fFieldTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
raw1]
            val2 :: CoreExpr
val2 = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psNoInlineCo PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fFieldTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
raw2]
            eqDict :: CoreExpr
eqDict = HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
ev
        in CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psEqClass PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
eqDict, CoreExpr
val1, CoreExpr
val2]

      -- Synthesize recursive branch test: if tag == i then compareConFields else buildTree (rest)
      buildTree CoreExpr
_ [] = CoreExpr
falseExpr
      buildTree CoreExpr
tagExpr ((Int
i, FastString
_conName, [(Int, Type, CtEvidence)]
fWanteds) : [(Int, FastString, [(Int, Type, CtEvidence)])]
rest) =
        let iLit :: CoreExpr
iLit = Word -> CoreExpr
mkWordExpr (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
            cond :: CoreExpr
cond = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psEqClass PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type (TyCon -> Type
mkTyConTy TyCon
wordTyCon), Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFEqWord PluginState
state), CoreExpr
tagExpr, CoreExpr
iLit]
        in CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
mkIfThenElse CoreExpr
cond ([(Int, Type, CtEvidence)] -> CoreExpr
compareConFields [(Int, Type, CtEvidence)]
fWanteds) (CoreExpr
-> [(Int, FastString, [(Int, Type, CtEvidence)])] -> CoreExpr
buildTree CoreExpr
tagExpr [(Int, FastString, [(Int, Type, CtEvidence)])]
rest)

      -- Top-level check: only inspect payload if constructor tags are equal
      bodyExpr = CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
mkIfThenElse CoreExpr
eqTag (CoreExpr
-> [(Int, FastString, [(Int, Type, CtEvidence)])] -> CoreExpr
buildTree CoreExpr
tag1 [(Int, FastString, [(Int, Type, CtEvidence)])]
ctorWanteds) CoreExpr
falseExpr
      repEqSumExpr = [Var] -> CoreExpr -> CoreExpr
mkCoreLams ([Var]
tyVars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var
r1Var, Var
r2Var]) CoreExpr
bodyExpr

      dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
scEvidence, CoreExpr
repEqSumExpr]
      allNewWanteds = [ CtEvidence -> Ct
mkNonCanonical CtEvidence
ev | (Int
_, FastString
_, [(Int, Type, CtEvidence)]
fWanteds) <- [(Int, FastString, [(Int, Type, CtEvidence)])]
ctorWanteds, (Int
_, Type
_, CtEvidence
ev) <- [(Int, Type, CtEvidence)]
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 :: PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveRowShowSum PluginState
state Ct
ct Class
cls [Type]
tys = do
  let rowTy :: Type
rowTy  = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
tys
      rTy :: Type
rTy    = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
      constructors :: [(Int, FastString, Type)]
constructors = Type -> [(Int, FastString, Type)]
walkSumRowWithTypes Type
rowTy
      loc :: CtLoc
loc    = Ct -> CtLoc
ctLoc Ct
ct

      -- Superclass evidence for RowFlavour r
      scEvidence :: CoreExpr
scEvidence = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon (PluginState -> Class
psRowFlavourCls PluginState
state)) [Type
rTy] []

      -- Extract repShowsPrecSum method type and bind lambda arguments: \p r -> ...
      repShowsPrecSumId :: Var
repShowsPrecSumId = case Class -> [Var]
classMethods Class
cls of
        (Var
m : [Var]
_) -> Var
m
        []      -> String -> Var
forall a. HasCallStack => String -> a
error String
"Polytropos.Plugin: RowShowSum class has no methods"
      methodFullTy :: Type
methodFullTy = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (Var -> Type
varType Var
repShowsPrecSumId) [Type]
tys
      (Type
_, Type
_, Type
methodInDictTy) = Type -> (Type, Type, Type)
splitFunTy Type
methodFullTy
      ([Var]
tyVars, Type
tauTy) = Type -> ([Var], Type)
splitForAllTyCoVars Type
methodInDictTy
      ([Scaled Type]
argTys, Type
_) = Type -> ([Scaled Type], Type)
splitFunTys Type
tauTy
      scaledPrecTy :: Scaled Type
scaledPrecTy = [Scaled Type]
argTys [Scaled Type] -> Int -> Scaled Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
0
      scaledRTy :: Scaled Type
scaledRTy    = [Scaled Type]
argTys [Scaled Type] -> Int -> Scaled Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
1

  precName <- TcM Name -> TcPluginM 'Solve Name
forall a. TcM a -> TcPluginM 'Solve a
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM Name -> TcPluginM 'Solve Name)
-> TcM Name -> TcPluginM 'Solve Name
forall a b. (a -> b) -> a -> b
$ OccName -> TcM Name
newName (String -> OccName
mkVarOcc String
"p")
  rName <- unsafeLiftTcM $ newName (mkVarOcc "r")
  let precVar = HasDebugCallStack => Name -> Type -> Type -> Var
Name -> Type -> Type -> Var
mkLocalId Name
precName (Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult Scaled Type
scaledPrecTy) (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
scaledPrecTy)
      rVar    = HasDebugCallStack => Name -> Type -> Type -> Var
Name -> Type -> Type -> Var
mkLocalId Name
rName (Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult Scaled Type
scaledRTy) (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
scaledRTy)

      kATy   = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
      fTy    = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
      aTy    = Var -> Type
mkTyVarTy ([Var]
tyVars [Var] -> Int -> Var
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
      kRowTy = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
rowTy

      -- Unpack RowRep wrapper: unRowRep r
      unRowRepTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kRowTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
rTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
rowTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy]
      rep = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psUnRowRep PluginState
state)) ([CoreExpr]
unRowRepTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [Var -> CoreExpr
forall b. Var -> Expr b
Var Var
rVar])

      repTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy]
      tag = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psRepTag PluginState
state)) ([CoreExpr]
repTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
rep])

      spaceShowS  = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psShowChar PluginState
state)) [Char -> CoreExpr
mkCharExpr Char
' ']
      compFn CoreExpr
f CoreExpr
g = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psComp PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
stringTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
stringTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
stringTy, CoreExpr
f, CoreExpr
g]

  -- Spawn wanted Show constraints for every field of every constructor
  ctorWanteds <- forM constructors $ \(Int
i, FastString
conNameFS, Type
conRowTy) -> do
    let fields :: [(Int, FastString, Type)]
fields = Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
conRowTy
    fWanteds <- [(Int, FastString, Type)]
-> ((Int, FastString, Type)
    -> TcPluginM 'Solve (Int, Type, CtEvidence))
-> TcPluginM 'Solve [(Int, Type, CtEvidence)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, FastString, Type)]
fields (((Int, FastString, Type)
  -> TcPluginM 'Solve (Int, Type, CtEvidence))
 -> TcPluginM 'Solve [(Int, Type, CtEvidence)])
-> ((Int, FastString, Type)
    -> TcPluginM 'Solve (Int, Type, CtEvidence))
-> TcPluginM 'Solve [(Int, Type, CtEvidence)]
forall a b. (a -> b) -> a -> b
$ \(Int
fi, FastString
_nameFS, Type
fieldTy) -> do
      ev <- CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted CtLoc
loc (Type -> Type -> Type
mkAppTy (TyCon -> Type
mkTyConTy (Class -> TyCon
classTyCon (PluginState -> Class
psShowCls PluginState
state))) Type
fieldTy)
      pure (fi, fieldTy, ev)
    pure (i, conNameFS, fWanteds)

  let showField Int
fi Type
fieldTy CtEvidence
ev =
        let fieldAtTypeArgs :: [CoreExpr]
fieldAtTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy]
            idxExpr :: CoreExpr
idxExpr = Int -> CoreExpr
mkIntExpr Int
fi
            raw :: CoreExpr
raw = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFieldAt PluginState
state)) ([CoreExpr]
fieldAtTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
idxExpr, CoreExpr
rep])
            fFieldTy :: Type
fFieldTy = Type -> Type -> Type
mkAppTy Type
fTy Type
fieldTy
            val :: CoreExpr
val = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psNoInlineCo PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fFieldTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
raw]
            showDict :: CoreExpr
showDict = HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
ev
            zeroPrec :: CoreExpr
zeroPrec = Int -> CoreExpr
mkIntExpr Int
0
        in CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psShowsPrecMeth PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
showDict, CoreExpr
zeroPrec, CoreExpr
val]

      showConFields FastString
conNameFS [(Int, Type, CtEvidence)]
fWanteds = do
        let conName :: String
conName = FastString -> String
unpackFS FastString
conNameFS
        prefixExpr <- TcM CoreExpr -> TcPluginM 'Solve CoreExpr
forall a. TcM a -> TcPluginM 'Solve a
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM CoreExpr -> TcPluginM 'Solve CoreExpr)
-> TcM CoreExpr -> TcPluginM 'Solve CoreExpr
forall a b. (a -> b) -> a -> b
$ String -> TcM CoreExpr
forall (m :: * -> *). MonadThings m => String -> m CoreExpr
mkStringExpr (String
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ")
        let prefixShowS = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psShowString PluginState
state)) [CoreExpr
prefixExpr]
            fieldShows = [ Int -> Type -> CtEvidence -> CoreExpr
showField Int
fi Type
fieldTy CtEvidence
ev | (Int
fi, Type
fieldTy, CtEvidence
ev) <- [(Int, Type, CtEvidence)]
fWanteds ]
            showParts = case [CoreExpr]
fieldShows of
              [] -> [CoreExpr
prefixShowS]
              (CoreExpr
f0 : [CoreExpr]
fs) -> CoreExpr
prefixShowS CoreExpr -> [CoreExpr] -> [CoreExpr]
forall a. a -> [a] -> [a]
: CoreExpr
f0 CoreExpr -> [CoreExpr] -> [CoreExpr]
forall a. a -> [a] -> [a]
: (CoreExpr -> [CoreExpr]) -> [CoreExpr] -> [CoreExpr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\CoreExpr
f -> [CoreExpr
spaceShowS, CoreExpr
f]) [CoreExpr]
fs
        pure $ foldr1 compFn showParts

  -- Synthesize recursive branch dispatcher: if tag == i then showConFields else buildTree (rest)
  let buildTree CoreExpr
_tagExpr [] = do
        errorPrefix <- TcM CoreExpr -> TcPluginM 'Solve CoreExpr
forall a. TcM a -> TcPluginM 'Solve a
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM CoreExpr -> TcPluginM 'Solve CoreExpr)
-> TcM CoreExpr -> TcPluginM 'Solve CoreExpr
forall a b. (a -> b) -> a -> b
$ String -> TcM CoreExpr
forall (m :: * -> *). MonadThings m => String -> m CoreExpr
mkStringExpr String
"??? "
        pure $ mkCoreApps (Var (psShowString state)) [errorPrefix]
      buildTree CoreExpr
tagExpr ((Int
i, FastString
conNameFS, [(Int, Type, CtEvidence)]
fWanteds) : [(Int, FastString, [(Int, Type, CtEvidence)])]
rest) = do
        let iLit :: CoreExpr
iLit = Word -> CoreExpr
mkWordExpr (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
            cond :: CoreExpr
cond = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psEqClass PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type (TyCon -> Type
mkTyConTy TyCon
wordTyCon), Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFEqWord PluginState
state), CoreExpr
tagExpr, CoreExpr
iLit]
        trueBranch <- FastString
-> [(Int, Type, CtEvidence)] -> TcPluginM 'Solve CoreExpr
showConFields FastString
conNameFS [(Int, Type, CtEvidence)]
fWanteds
        falseBranch <- buildTree tagExpr rest
        pure $ mkIfThenElse cond trueBranch falseBranch

  bodyExpr <- buildTree tag ctorWanteds
  let repShowsPrecSumExpr = [Var] -> CoreExpr -> CoreExpr
mkCoreLams ([Var]
tyVars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var
precVar, Var
rVar]) CoreExpr
bodyExpr

      dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
scEvidence, CoreExpr
repShowsPrecSumExpr]
      allNewWanteds = [ CtEvidence -> Ct
mkNonCanonical CtEvidence
ev | (Int
_, FastString
_, [(Int, Type, CtEvidence)]
fWanteds) <- [(Int, FastString, [(Int, Type, CtEvidence)])]
ctorWanteds, (Int
_, Type
_, CtEvidence
ev) <- [(Int, Type, CtEvidence)]
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 :: PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveHasField PluginState
state Ct
ct Class
cls [Type]
tys = do
  let len :: Int
len = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys
  if Int
len Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3 then do
    let fieldTy :: Type
fieldTy = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
tys
        recTy :: Type
recTy   = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
        nTy :: Type
nTy     = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
3)
        loc :: CtLoc
loc     = Ct -> CtLoc
ctLoc Ct
ct
    case Type -> Maybe FastString
isStrLitTy (Type -> Type
unwrapSynonyms Type
nTy) of
      Just FastString
fieldName -> do
        case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Type
unwrapSynonyms Type
recTy) of
          Just (TyCon
tc, [Type]
args)
            | OccName -> String
occNameString (TyCon -> OccName
forall a. NamedThing a => a -> OccName
getOccName TyCon
tc) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"RowRep"
            , [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
4 -> do
              let aTy :: Type
aTy   = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
args
                  rowTy :: Type
rowTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
                  rTy :: Type
rTy   = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
3)
                  fTy :: Type
fTy   = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
4)
                  kATy :: Type
kATy  = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
aTy
                  kRowTy :: Type
kRowTy = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
rowTy
              case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Type
unwrapSynonyms Type
rTy) of
                Just (TyCon
tcR, []) | OccName -> String
occNameString (TyCon -> OccName
forall a. NamedThing a => a -> OccName
getOccName TyCon
tcR) String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"ProductRowT", String
"ProductRowHKDT"] -> do
                  case FastString -> Type -> Maybe (Int, Type)
findFieldType FastString
fieldName Type
rowTy of
                    Just (Int
i, Type
actualFieldTy) -> do
                      -- Locate getField method and bind record argument: \rec -> ...
                      let getFieldId :: Var
getFieldId = case Class -> [Var]
classMethods Class
cls of
                            (Var
m : [Var]
_) -> Var
m
                            [] -> String -> Var
forall a. HasCallStack => String -> a
error String
"Polytropos.Plugin: HasField has no methods"
                          methodFullTy :: Type
methodFullTy = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (Var -> Type
varType Var
getFieldId) [Type]
tys
                          (Type
_, Type
_, Type
methodInDictTy) = Type -> (Type, Type, Type)
splitFunTy Type
methodFullTy
                          ([Var]
tyVars, Type
tauTy) = Type -> ([Var], Type)
splitForAllTyCoVars Type
methodInDictTy
                          ([Scaled Type]
argTys, Type
_) = Type -> ([Scaled Type], Type)
splitFunTys Type
tauTy
                          scaledRTy :: Scaled Type
scaledRTy = [Scaled Type]
argTys [Scaled Type] -> Int -> Scaled Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
0

                      rName <- TcM Name -> TcPluginM 'Solve Name
forall a. TcM a -> TcPluginM 'Solve a
forall (m :: * -> *) a. MonadTcPlugin m => TcM a -> m a
unsafeLiftTcM (TcM Name -> TcPluginM 'Solve Name)
-> TcM Name -> TcPluginM 'Solve Name
forall a b. (a -> b) -> a -> b
$ OccName -> TcM Name
newName (String -> OccName
mkVarOcc String
"rec")
                      let rVar = HasDebugCallStack => Name -> Type -> Type -> Var
Name -> Type -> Type -> Var
mkLocalId Name
rName (Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult Scaled Type
scaledRTy) (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
scaledRTy)

                          unRowRepTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kRowTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
rTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
rowTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy]
                          rep = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psUnRowRep PluginState
state)) ([CoreExpr]
unRowRepTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [Var -> CoreExpr
forall b. Var -> Expr b
Var Var
rVar])

                          fieldAtTypeArgs = [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
kATy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
aTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
actualFieldTy]
                          idxExpr = Int -> CoreExpr
mkIntExpr Int
i
                          raw = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psFieldAt PluginState
state)) ([CoreExpr]
fieldAtTypeArgs [CoreExpr] -> [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a] -> [a]
++ [CoreExpr
idxExpr, CoreExpr
rep])

                          -- Verify type compatibility (bare or wrapped in field functor f)
                          fFieldTy = Type -> Type -> Type
mkAppTy Type
fTy Type
actualFieldTy
                          validTy  = Type
fieldTy HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
actualFieldTy
                                  Bool -> Bool -> Bool
|| Type
fieldTy HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
fFieldTy
                          val = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psNoInlineCo PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fFieldTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, CoreExpr
raw]

                          getFieldExpr = [Var] -> CoreExpr -> CoreExpr
mkCoreLams ([Var]
tyVars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var
rVar]) CoreExpr
val
                          dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
getFieldExpr]

                      if isClosedType fieldTy && not validTy
                        then do
                          -- Field exists but context requested incompatible type: emit diagnostic
                          let diagLines =
                                [ String
"Polytropos Record Error:"
                                , String
"  Field '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FastString -> String
unpackFS FastString
fieldName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' in record has type:"
                                , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
actualFieldTy)
                                , String
"  but context expected:"
                                , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
fieldTy)
                                ]
                          errCt <- mkTypeErrorCt state loc diagLines
                          pure $ Left ((EvExpr dictExpr, ct), [errCt])
                        else
                          pure $ Left ((EvExpr dictExpr, ct), [])
                    Maybe (Int, Type)
Nothing -> do
                      -- Field not found: emit fuzzy typo suggestions and dummy HasField dictionary
                      case Type -> Maybe [(Int, FastString, Type)]
walkRowWithTypes_maybe Type
rowTy of
                        Just [(Int, FastString, Type)]
fields -> do
                          dummyDict <- PluginState -> Class -> [Type] -> TcPluginM 'Solve EvTerm
mkDummyHasFieldDict PluginState
state Class
cls [Type]
tys
                          let fNames = [ FastString -> String
unpackFS FastString
n | (Int
_, FastString
n, Type
_) <- [(Int, FastString, Type)]
fields, Bool -> Bool
not (FastString -> Bool
nullFS FastString
n) ]
                              diagLines =
                                [ String
"Polytropos Record Error:"
                                , String
"  Field '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FastString -> String
unpackFS FastString
fieldName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' does not exist in record:"
                                , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, FastString, Type)] -> String
formatRecordRow [(Int, FastString, Type)]
fields
                                , String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
formatSuggestion (FastString -> String
unpackFS FastString
fieldName) [String]
fNames
                                ]
                          errCt <- mkTypeErrorCt state loc diagLines
                          pure $ Left ((dummyDict, ct), [errCt])
                        Maybe [(Int, FastString, Type)]
Nothing -> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right () -- Open row tail: defer solving
                Maybe (TyCon, [Type])
_ -> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right ()
          Maybe (TyCon, [Type])
_ -> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right ()
      Maybe FastString
Nothing -> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
Right ()
  else Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
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 :: PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveAllFields PluginState
state Ct
ct Class
cls [Type]
tys
  | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3
  , let rowTy :: Type
rowTy = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
  , Just [Type]
_ <- Type -> Maybe [Type]
myExtractPromotedList (Type -> Type
unwrapSynonyms Type
rowTy)
  = do
      let cTy :: Type
cTy    = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
tys
          rTy :: Type
rTy    = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
3)
          fields :: [(Int, FastString, Type)]
fields = Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
rowTy
          loc :: CtLoc
loc    = Ct -> CtLoc
ctLoc Ct
ct
          dictAnyTy :: Type
dictAnyTy = Type -> Type -> Type
mkAppTy (TyCon -> Type
mkTyConTy (PluginState -> TyCon
psDictAnyTyCon PluginState
state)) Type
cTy

      -- For each field, create a new wanted constraint for (c fieldTy)
      wanteds <- [(Int, FastString, Type)]
-> ((Int, FastString, Type) -> TcPluginM 'Solve (Type, CtEvidence))
-> TcPluginM 'Solve [(Type, CtEvidence)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, FastString, Type)]
fields (((Int, FastString, Type) -> TcPluginM 'Solve (Type, CtEvidence))
 -> TcPluginM 'Solve [(Type, CtEvidence)])
-> ((Int, FastString, Type) -> TcPluginM 'Solve (Type, CtEvidence))
-> TcPluginM 'Solve [(Type, CtEvidence)]
forall a b. (a -> b) -> a -> b
$ \(Int
_i, FastString
_nameFS, Type
fieldTy) -> do
        ev <- CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted CtLoc
loc (Type -> Type -> Type
mkAppTy Type
cTy Type
fieldTy)
        pure (fieldTy, ev)

      -- For each field, construct: mkDictAny @c @fieldTy dict
      let dictAnys = [ CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psMkDictAny PluginState
state))
                                  [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
cTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
fieldTy, HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
ev]
                     | (Type
fieldTy, CtEvidence
ev) <- [(Type, CtEvidence)]
wanteds
                     ]

      -- Construct: evidenceAllFields @c [dictAny_0, dictAny_1, ...]
      let listExpr = Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
dictAnyTy [CoreExpr]
dictAnys
          arrExpr  = CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps (Var -> CoreExpr
forall b. Var -> Expr b
Var (PluginState -> Var
psEvidenceAllFields PluginState
state)) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
cTy, CoreExpr
listExpr]

      -- Superclass evidence for RowFlavour r
      let scEvidence = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon (PluginState -> Class
psRowFlavourCls PluginState
state)) [Type
rTy] []

      -- Class dictionary: AllFields r row c
      let dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
scEvidence, CoreExpr
arrExpr]
          newWanteds = [CtEvidence -> Ct
mkNonCanonical CtEvidence
ev | (Type
_fieldTy, CtEvidence
ev) <- [(Type, CtEvidence)]
wanteds]

      pure $ Left ((EvExpr dictExpr, ct), newWanteds)
  | Bool
otherwise = Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
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 :: PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveSubRow PluginState
state Ct
ct Class
cls [Type]
tys
  | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
  , let subTy :: Type
subTy   = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
  , let superTy :: Type
superTy = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
tys
  , let loc :: CtLoc
loc     = Ct -> CtLoc
ctLoc Ct
ct
  , Just [(Int, FastString, Type)]
subFields   <- Type -> Maybe [(Int, FastString, Type)]
walkRowWithTypes_maybe Type
subTy
  , Just [(Int, FastString, Type)]
superFields <- Type -> Maybe [(Int, FastString, Type)]
walkRowWithTypes_maybe Type
superTy
  = case [(Int, FastString, Type)]
-> [(Int, FastString, Type)] -> Maybe [Int]
matchFields [(Int, FastString, Type)]
subFields [(Int, FastString, Type)]
superFields of
      Just [Int]
indices -> do
        -- Successful match: compile literal index list [Int] into Core AST:
        -- evidenceSubRow :: [Int] -> DictSubRow k sub super
        let indicesExpr :: CoreExpr
indicesExpr = Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
intTy ((Int -> CoreExpr) -> [Int] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map Int -> CoreExpr
mkIntExpr [Int]
indices)
            dictExpr :: CoreExpr
dictExpr    = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
indicesExpr]
        Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ ((EvTerm, Ct), [Ct]) -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. a -> Either a b
Left ((CoreExpr -> EvTerm
EvExpr CoreExpr
dictExpr, Ct
ct), [])
      Maybe [Int]
Nothing -> do
        -- Structural mismatch: diagnose failure and synthesize custom TypeError.
        -- We emit a dummy dictionary so GHC does not cascade secondary errors.
        let dummyDict :: CoreExpr
dummyDict = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
intTy []]
            mismatchDiag :: [String]
mismatchDiag = [(Int, FastString, Type)] -> [(Int, FastString, Type)] -> [String]
findSubRowMismatch [(Int, FastString, Type)]
subFields [(Int, FastString, Type)]
superFields
        errCt <- PluginState -> CtLoc -> [String] -> TcPluginM 'Solve Ct
mkTypeErrorCt PluginState
state CtLoc
loc [String]
mismatchDiag
        pure $ Left ((EvExpr dummyDict, ct), [errCt])
  | Bool
otherwise = Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
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 :: [(Int, FastString, Type)]
-> [(Int, FastString, Type)] -> Maybe [Int]
matchFields [] [(Int, FastString, Type)]
_ = [Int] -> Maybe [Int]
forall a. a -> Maybe a
Just []
    matchFields ((Int
_, FastString
name, Type
fieldTy) : [(Int, FastString, Type)]
rest) [(Int, FastString, Type)]
sFields =
      case [ Int
j | (Int
j, FastString
sName, Type
sFieldTy) <- [(Int, FastString, Type)]
sFields
               , (if FastString -> Bool
nullFS FastString
name Bool -> Bool -> Bool
|| FastString -> Bool
nullFS FastString
sName then Bool
True else FastString
sName FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
name)
               , Type
fieldTy HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
sFieldTy ] of
        (Int
j : [Int]
_) -> (Int
j Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:) ([Int] -> [Int]) -> Maybe [Int] -> Maybe [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, FastString, Type)]
-> [(Int, FastString, Type)] -> Maybe [Int]
matchFields [(Int, FastString, Type)]
rest [(Int, FastString, Type)]
sFields
        []      -> Maybe [Int]
forall a. Maybe a
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 :: [(Int, FastString, Type)] -> [(Int, FastString, Type)] -> [String]
findSubRowMismatch [] [(Int, FastString, Type)]
_ =
      [ String
"Polytropos SubRow Error:"
      , String
"  Sub-record row does not match super-record row."
      ]
    findSubRowMismatch ((Int
_, FastString
name, Type
fieldTy) : [(Int, FastString, Type)]
rest) [(Int, FastString, Type)]
sFields =
      case [ Type
sFieldTy | (Int
_, FastString
sName, Type
sFieldTy) <- [(Int, FastString, Type)]
sFields
                      , if FastString -> Bool
nullFS FastString
name Bool -> Bool -> Bool
|| FastString -> Bool
nullFS FastString
sName then Bool
True else FastString
sName FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
name ] of
        [] ->
          let sNames :: [String]
sNames = [ FastString -> String
unpackFS FastString
n | (Int
_, FastString
n, Type
_) <- [(Int, FastString, Type)]
sFields, Bool -> Bool
not (FastString -> Bool
nullFS FastString
n) ]
          in [ String
"Polytropos SubRow Error:"
             , String
"  Cannot project record: field '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FastString -> String
unpackFS FastString
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' from sub-record is missing in super-record:"
             , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, FastString, Type)] -> String
formatRecordRow [(Int, FastString, Type)]
sFields
             , String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
formatSuggestion (FastString -> String
unpackFS FastString
name) [String]
sNames
             ]
        (Type
sFieldTy : [Type]
_)
          | Bool -> Bool
not (Type
fieldTy HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
sFieldTy) ->
              [ String
"Polytropos SubRow Error:"
              , String
"  Cannot project record: field '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FastString -> String
unpackFS FastString
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' has type:"
              , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
fieldTy)
              , String
"  in sub-record, but has type:"
              , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
sFieldTy)
              , String
"  in super-record."
              ]
          | Bool
otherwise -> [(Int, FastString, Type)] -> [(Int, FastString, Type)] -> [String]
findSubRowMismatch [(Int, FastString, Type)]
rest [(Int, FastString, Type)]
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 :: PluginState
-> Ct
-> Class
-> [Type]
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
solveSubSum PluginState
state Ct
ct Class
cls [Type]
tys
  | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
  , let subTy :: Type
subTy   = [Type]
tys [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
  , let superTy :: Type
superTy = [Type] -> Type
forall a. HasCallStack => [a] -> a
last [Type]
tys
  , let loc :: CtLoc
loc     = Ct -> CtLoc
ctLoc Ct
ct
  , Just [(Int, FastString, Type)]
subCons   <- Type -> Maybe [(Int, FastString, Type)]
walkSumRowWithTypes_maybe Type
subTy
  , Just [(Int, FastString, Type)]
superCons <- Type -> Maybe [(Int, FastString, Type)]
walkSumRowWithTypes_maybe Type
superTy
  = case [(Int, FastString, Type)]
-> [(Int, FastString, Type)] -> Maybe [Word]
matchCons [(Int, FastString, Type)]
subCons [(Int, FastString, Type)]
superCons of
      Just [Word]
injectIndices -> do
        let wordTy :: Type
wordTy = TyCon -> Type
mkTyConTy TyCon
wordTyCon
            -- Core list of Word: [Word]
            injectExpr :: CoreExpr
injectExpr = Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
wordTy ((Word -> CoreExpr) -> [Word] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map Word -> CoreExpr
mkWordExpr [Word]
injectIndices)

            -- Build the narrowing table: for every constructor in 'superCons',
            -- check if it exists in 'subCons'. If yes -> Just subIdx; if no -> Nothing.
            narrowIndices :: [Maybe Word]
narrowIndices =
              [ case [ Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i :: Word
                     | (Int
i, FastString
sName, Type
sConRowTy) <- [(Int, FastString, Type)]
subCons
                     , (if FastString -> Bool
nullFS FastString
sName Bool -> Bool -> Bool
|| FastString -> Bool
nullFS FastString
superName then Bool
True else FastString
sName FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
superName)
                     , Type -> Type -> Bool
sameRow Type
sConRowTy Type
superConRowTy
                     ] of
                  (Word
subIdx : [Word]
_) -> Word -> Maybe Word
forall a. a -> Maybe a
Just Word
subIdx
                  []           -> Maybe Word
forall a. Maybe a
Nothing
              | (Int
_j, FastString
superName, Type
superConRowTy) <- [(Int, FastString, Type)]
superCons
              ]

            -- Core list of Maybe Word: [Maybe Word]
            maybeWordTy :: Type
maybeWordTy = Type -> Type -> Type
mkAppTy (TyCon -> Type
mkTyConTy TyCon
maybeTyCon) Type
wordTy
            narrowDataExpr :: Maybe Word -> CoreExpr
narrowDataExpr Maybe Word
Nothing = DataCon -> [CoreExpr] -> CoreExpr
mkCoreConApps DataCon
nothingDataCon [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
wordTy]
            narrowDataExpr (Just Word
w) = DataCon -> [CoreExpr] -> CoreExpr
mkCoreConApps DataCon
justDataCon [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
wordTy, Word -> CoreExpr
mkWordExpr Word
w]
            narrowExpr :: CoreExpr
narrowExpr = Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
maybeWordTy ((Maybe Word -> CoreExpr) -> [Maybe Word] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map Maybe Word -> CoreExpr
narrowDataExpr [Maybe Word]
narrowIndices)

            -- Evidence term: DictSubSum [Word] [Maybe Word]
            dictExpr :: CoreExpr
dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
injectExpr, CoreExpr
narrowExpr]
        Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ ((EvTerm, Ct), [Ct]) -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. a -> Either a b
Left ((CoreExpr -> EvTerm
EvExpr CoreExpr
dictExpr, Ct
ct), [])
      Maybe [Word]
Nothing -> do
        -- Constructor mismatch: generate custom diagnostic and return dummy dictionary.
        let wordTy :: Type
wordTy = TyCon -> Type
mkTyConTy TyCon
wordTyCon
            maybeWordTy :: Type
maybeWordTy = Type -> Type -> Type
mkAppTy (TyCon -> Type
mkTyConTy TyCon
maybeTyCon) Type
wordTy
            dummyDict :: CoreExpr
dummyDict = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
wordTy [], Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
maybeWordTy []]
            mismatchDiag :: [String]
mismatchDiag = [(Int, FastString, Type)] -> [(Int, FastString, Type)] -> [String]
findSubSumMismatch [(Int, FastString, Type)]
subCons [(Int, FastString, Type)]
superCons
        errCt <- PluginState -> CtLoc -> [String] -> TcPluginM 'Solve Ct
mkTypeErrorCt PluginState
state CtLoc
loc [String]
mismatchDiag
        pure $ Left ((EvExpr dummyDict, ct), [errCt])
  | Bool
otherwise = Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ((EvTerm, Ct), [Ct]) ()
 -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ()))
-> Either ((EvTerm, Ct), [Ct]) ()
-> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())
forall a b. (a -> b) -> a -> b
$ () -> Either ((EvTerm, Ct), [Ct]) ()
forall a b. b -> Either a b
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 :: [(Int, FastString, Type)]
-> [(Int, FastString, Type)] -> Maybe [Word]
matchCons [] [(Int, FastString, Type)]
_ = [Word] -> Maybe [Word]
forall a. a -> Maybe a
Just []
    matchCons ((Int
_, FastString
conName, Type
conRowTy) : [(Int, FastString, Type)]
rest) [(Int, FastString, Type)]
sCons =
      case [ Int
j | (Int
j, FastString
sName, Type
sRowTy) <- [(Int, FastString, Type)]
sCons
               , (if FastString -> Bool
nullFS FastString
conName Bool -> Bool -> Bool
|| FastString -> Bool
nullFS FastString
sName then Bool
True else FastString
sName FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
conName)
               , Type -> Type -> Bool
sameRow Type
conRowTy Type
sRowTy ] of
        (Int
j : [Int]
_) -> (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
j Word -> [Word] -> [Word]
forall a. a -> [a] -> [a]
:) ([Word] -> [Word]) -> Maybe [Word] -> Maybe [Word]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, FastString, Type)]
-> [(Int, FastString, Type)] -> Maybe [Word]
matchCons [(Int, FastString, Type)]
rest [(Int, FastString, Type)]
sCons
        []      -> Maybe [Word]
forall a. Maybe a
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 :: Type -> Type -> Bool
sameRow Type
r1 Type
r2
      | Type
r1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
r2 = Bool
True
      | Just [(Int, FastString, Type)]
fs1 <- Type -> Maybe [(Int, FastString, Type)]
walkRowWithTypes_maybe Type
r1
      , Just [(Int, FastString, Type)]
fs2 <- Type -> Maybe [(Int, FastString, Type)]
walkRowWithTypes_maybe Type
r2
      = [(Int, FastString, Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, FastString, Type)]
fs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [(Int, FastString, Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, FastString, Type)]
fs2 Bool -> Bool -> Bool
&&
        [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ (if FastString -> Bool
nullFS FastString
n1 Bool -> Bool -> Bool
|| FastString -> Bool
nullFS FastString
n2 then Bool
True else FastString
n1 FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
n2) Bool -> Bool -> Bool
&& Type
t1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
t2 | ((Int
_, FastString
n1, Type
t1), (Int
_, FastString
n2, Type
t2)) <- [(Int, FastString, Type)]
-> [(Int, FastString, Type)]
-> [((Int, FastString, Type), (Int, FastString, Type))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int, FastString, Type)]
fs1 [(Int, FastString, Type)]
fs2 ]
      | Bool
otherwise = Bool
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 :: [(Int, FastString, Type)] -> [(Int, FastString, Type)] -> [String]
findSubSumMismatch [] [(Int, FastString, Type)]
_ =
      [ String
"Polytropos SubSum Error:"
      , String
"  Sub-variant row does not match super-variant row."
      ]
    findSubSumMismatch ((Int
_, FastString
conName, Type
conRowTy) : [(Int, FastString, Type)]
rest) [(Int, FastString, Type)]
sCons =
      case [ Type
sRowTy | (Int
_, FastString
sName, Type
sRowTy) <- [(Int, FastString, Type)]
sCons
                    , if FastString -> Bool
nullFS FastString
conName Bool -> Bool -> Bool
|| FastString -> Bool
nullFS FastString
sName then Bool
True else FastString
sName FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
conName ] of
        [] ->
          let sNames :: [String]
sNames = [ FastString -> String
unpackFS FastString
n | (Int
_, FastString
n, Type
_) <- [(Int, FastString, Type)]
sCons, Bool -> Bool
not (FastString -> Bool
nullFS FastString
n) ]
          in [ String
"Polytropos SubSum Error:"
             , String
"  Cannot widen variant: constructor '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FastString -> String
unpackFS FastString
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' from sub-variant is missing in super-variant:"
             , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, FastString, Type)] -> String
formatVariantRow [(Int, FastString, Type)]
sCons
             , String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
formatCtorSuggestion (FastString -> String
unpackFS FastString
conName) [String]
sNames
             ]
        (Type
sRowTy : [Type]
_)
          | Bool -> Bool
not (Type -> Type -> Bool
sameRow Type
conRowTy Type
sRowTy) ->
              let subFs :: [(Int, FastString, Type)]
subFs   = Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
conRowTy
                  superFs :: [(Int, FastString, Type)]
superFs = Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
sRowTy
              in [ String
"Polytropos SubSum Error:"
                 , String
"  Cannot widen variant: constructor '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FastString -> String
unpackFS FastString
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' has different payload rows:"
                 , String
"    sub-variant payload:   " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, FastString, Type)] -> String
formatRecordRow [(Int, FastString, Type)]
subFs
                 , String
"    super-variant payload: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, FastString, Type)] -> String
formatRecordRow [(Int, FastString, Type)]
superFs
                 ]
          | Bool
otherwise -> [(Int, FastString, Type)] -> [(Int, FastString, Type)] -> [String]
findSubSumMismatch [(Int, FastString, Type)]
rest [(Int, FastString, Type)]
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 :: FastString -> Word
fnv1a64FS FastString
fs = Word64 -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral ((Word64 -> Char -> Word64) -> Word64 -> String -> Word64
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Word64 -> Char -> Word64
forall {a}. (Bits a, Num a) => a -> Char -> a
step (Word64
14695981039346656037 :: Word64) (FastString -> String
unpackFS FastString
fs))
  where
    step :: a -> Char -> a
step !a
h !Char
c = (a
h a -> a -> a
forall a. Bits a => a -> a -> a
`xor` Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
ord Char
c)) a -> a -> a
forall a. Num a => a -> a -> a
* a
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 -> Class -> [Type] -> TcPluginM 'Solve (Either (EvTerm, Ct) ())
solveKnownHash Ct
ct Class
cls [Type]
tys = do
  let mSTy :: Maybe Type
mSTy = case [Type]
tys of
        [Type
s]    -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
s
        [Type
_, Type
s] -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
s
        [Type]
_      -> Maybe Type
forall a. Maybe a
Nothing
  case Maybe Type
mSTy of
    Just Type
sTy -> case Type -> Maybe FastString
isStrLitTy (Type -> Type
unwrapSynonyms Type
sTy) of
      Just FastString
fs -> do
        let h :: Word
h = FastString -> Word
fnv1a64FS FastString
fs
            wExpr :: CoreExpr
wExpr = Word -> CoreExpr
mkWordExpr Word
h
            dictExpr :: CoreExpr
dictExpr = DataCon -> [Type] -> [CoreExpr] -> CoreExpr
evDataConApp (Class -> DataCon
classDataCon Class
cls) [Type]
tys [CoreExpr
wExpr]
        Either (EvTerm, Ct) () -> TcPluginM 'Solve (Either (EvTerm, Ct) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (EvTerm, Ct) ()
 -> TcPluginM 'Solve (Either (EvTerm, Ct) ()))
-> Either (EvTerm, Ct) ()
-> TcPluginM 'Solve (Either (EvTerm, Ct) ())
forall a b. (a -> b) -> a -> b
$ (EvTerm, Ct) -> Either (EvTerm, Ct) ()
forall a b. a -> Either a b
Left (CoreExpr -> EvTerm
EvExpr CoreExpr
dictExpr, Ct
ct)
      Maybe FastString
Nothing -> Either (EvTerm, Ct) () -> TcPluginM 'Solve (Either (EvTerm, Ct) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (EvTerm, Ct) ()
 -> TcPluginM 'Solve (Either (EvTerm, Ct) ()))
-> Either (EvTerm, Ct) ()
-> TcPluginM 'Solve (Either (EvTerm, Ct) ())
forall a b. (a -> b) -> a -> b
$ () -> Either (EvTerm, Ct) ()
forall a b. b -> Either a b
Right ()
    Maybe Type
Nothing -> Either (EvTerm, Ct) () -> TcPluginM 'Solve (Either (EvTerm, Ct) ())
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (EvTerm, Ct) ()
 -> TcPluginM 'Solve (Either (EvTerm, Ct) ()))
-> Either (EvTerm, Ct) ()
-> TcPluginM 'Solve (Either (EvTerm, Ct) ())
forall a b. (a -> b) -> a -> b
$ () -> Either (EvTerm, Ct) ()
forall a b. b -> Either a b
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 :: Type -> Maybe [(Int, FastString, Type)]
walkRowWithTypes_maybe Type
rowTy = do
  xs <- Type -> Maybe [Type]
myExtractPromotedList (Type -> Type
unwrapSynonyms Type
rowTy)
  zipWithM extractField [0..] xs
  where
    extractField :: a -> Type -> Maybe (a, FastString, Type)
extractField a
i Type
elemTy =
      case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Type
unwrapSynonyms Type
elemTy) of
        Just (TyCon
_, [Type]
args)
          | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
          , let nameTy :: Type
nameTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
          , let fieldTy :: Type
fieldTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
          , Just FastString
n <- Type -> Maybe FastString
isStrLitTy (Type -> Type
unwrapSynonyms Type
nameTy)
          -> (a, FastString, Type) -> Maybe (a, FastString, Type)
forall a. a -> Maybe a
Just (a
i, FastString
n, Type
fieldTy)
        Maybe (TyCon, [Type])
_ -> (a, FastString, Type) -> Maybe (a, FastString, Type)
forall a. a -> Maybe a
Just (a
i, FastString
nilFS, Type
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 :: Type -> Maybe [(Int, FastString, Type)]
walkSumRowWithTypes_maybe Type
rowTy = do
  xs <- Type -> Maybe [Type]
myExtractPromotedList (Type -> Type
unwrapSynonyms Type
rowTy)
  zipWithM extractCon [0..] xs
  where
    extractCon :: a -> Type -> Maybe (a, FastString, Type)
extractCon a
i Type
elemTy =
      case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Type
unwrapSynonyms Type
elemTy) of
        Just (TyCon
_, [Type]
args)
          | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
          , let nameTy :: Type
nameTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
          , let conRowTy :: Type
conRowTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
          , Just FastString
n <- Type -> Maybe FastString
isStrLitTy (Type -> Type
unwrapSynonyms Type
nameTy)
          -> (a, FastString, Type) -> Maybe (a, FastString, Type)
forall a. a -> Maybe a
Just (a
i, FastString
n, Type
conRowTy)
        Maybe (TyCon, [Type])
_ -> (a, FastString, Type) -> Maybe (a, FastString, Type)
forall a. a -> Maybe a
Just (a
i, FastString
nilFS, Type
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 :: Type -> Type
unwrapSynonyms Type
ty = case Type -> Maybe Type
coreView Type
ty of
  Just Type
ty' -> Type -> Type
unwrapSynonyms Type
ty'
  Maybe Type
Nothing  -> Type
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 :: Type -> Maybe [Type]
myExtractPromotedList Type
ty = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Type
unwrapSynonyms Type
ty) of
  Just (TyCon
tc, [Type
_, Type
x, Type
xs]) | OccName -> String
occNameString (TyCon -> OccName
forall a. NamedThing a => a -> OccName
getOccName TyCon
tc) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
":" -> do
    rest <- Type -> Maybe [Type]
myExtractPromotedList Type
xs
    return (x : rest)
  Just (TyCon
tc, [Type
_]) | OccName -> String
occNameString (TyCon -> OccName
forall a. NamedThing a => a -> OccName
getOccName TyCon
tc) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"[]" -> [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just []
  Maybe (TyCon, [Type])
_ -> Maybe [Type]
forall a. Maybe a
Nothing

-- | Pure version of 'walkRowWithTypes_maybe' that defaults open tails to '[]'.
walkRowWithTypes :: Type -> [(Int, FastString, Type)]
walkRowWithTypes :: Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
rowTy =
  case Type -> Maybe [Type]
myExtractPromotedList (Type -> Type
unwrapSynonyms Type
rowTy) of { Just [Type]
xs -> (Int -> Type -> (Int, FastString, Type))
-> [Int] -> [Type] -> [(Int, FastString, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Type -> (Int, FastString, Type)
forall {a}. a -> Type -> (a, FastString, Type)
extractField [Int
0..] [Type]
xs; Maybe [Type]
Nothing -> [] }
  where
    extractField :: a -> Type -> (a, FastString, Type)
extractField a
i Type
elemTy =
      case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Type
unwrapSynonyms Type
elemTy) of
        Just (TyCon
_, [Type]
args)
          | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
          , let nameTy :: Type
nameTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
          , let fieldTy :: Type
fieldTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
          , Just FastString
n <- Type -> Maybe FastString
isStrLitTy (Type -> Type
unwrapSynonyms Type
nameTy)
          -> (a
i, FastString
n, Type
fieldTy)
        Maybe (TyCon, [Type])
_ -> (a
i, FastString
nilFS, Type
elemTy)

-- | Pure version of 'walkSumRowWithTypes_maybe' that defaults open tails to '[]'.
walkSumRowWithTypes :: Type -> [(Int, FastString, Type)]
walkSumRowWithTypes :: Type -> [(Int, FastString, Type)]
walkSumRowWithTypes Type
rowTy =
  case Type -> Maybe [Type]
myExtractPromotedList (Type -> Type
unwrapSynonyms Type
rowTy) of { Just [Type]
xs -> (Int -> Type -> (Int, FastString, Type))
-> [Int] -> [Type] -> [(Int, FastString, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Type -> (Int, FastString, Type)
forall {a}. a -> Type -> (a, FastString, Type)
extractCon [Int
0..] [Type]
xs; Maybe [Type]
Nothing -> [] }
  where
    extractCon :: a -> Type -> (a, FastString, Type)
extractCon a
i Type
elemTy =
      case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Type
unwrapSynonyms Type
elemTy) of
        Just (TyCon
_, [Type]
args)
          | [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
          , let nameTy :: Type
nameTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2)
          , let conRowTy :: Type
conRowTy = [Type]
args [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
          , Just FastString
n <- Type -> Maybe FastString
isStrLitTy (Type -> Type
unwrapSynonyms Type
nameTy)
          -> (a
i, FastString
n, Type
conRowTy)
        Maybe (TyCon, [Type])
_ -> (a
i, FastString
nilFS, Type
elemTy)

-- | Find 0-based constructor tag by name in a sum row.
findConstructorIndex :: FastString -> Type -> Maybe Word
findConstructorIndex :: FastString -> Type -> Maybe Word
findConstructorIndex FastString
conName Type
rowTy =
  case [Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i | (Int
i, FastString
n, Type
_) <- Type -> [(Int, FastString, Type)]
walkSumRowWithTypes Type
rowTy, FastString
n FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
conName] of
    (Word
w : [Word]
_) -> Word -> Maybe Word
forall a. a -> Maybe a
Just Word
w
    []      -> Maybe Word
forall a. Maybe a
Nothing

-- | Find 0-based field index by matching field payload type.
findFieldIndexByType :: Type -> Type -> Maybe Int
findFieldIndexByType :: Type -> Type -> Maybe Int
findFieldIndexByType Type
targetTy Type
rowTy =
  case [Int
i | (Int
i, FastString
_, Type
ty) <- Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
rowTy, Type
targetTy HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
ty] of
    (Int
i : [Int]
_) -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
    []      -> Maybe Int
forall a. Maybe a
Nothing

-- | Find 0-based constructor tag by matching constructor payload type.
findConstructorIndexByType :: Type -> Type -> Maybe Word
findConstructorIndexByType :: Type -> Type -> Maybe Word
findConstructorIndexByType Type
targetTy Type
rowTy =
  case [Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i | (Int
i, FastString
_, Type
ty) <- Type -> [(Int, FastString, Type)]
walkSumRowWithTypes Type
rowTy, Type
targetTy HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
ty] of
    (Word
w : [Word]
_) -> Word -> Maybe Word
forall a. a -> Maybe a
Just Word
w
    []      -> Maybe Word
forall a. Maybe a
Nothing

-- | Find 0-based field index and field type by name in a product row.
findFieldType :: FastString -> Type -> Maybe (Int, Type)
findFieldType :: FastString -> Type -> Maybe (Int, Type)
findFieldType FastString
fieldName Type
rowTy =
  case [(Int
i, Type
ty) | (Int
i, FastString
n, Type
ty) <- Type -> [(Int, FastString, Type)]
walkRowWithTypes Type
rowTy, FastString
n FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
fieldName] of
    ((Int, Type)
res : [(Int, Type)]
_) -> (Int, Type) -> Maybe (Int, Type)
forall a. a -> Maybe a
Just (Int, Type)
res
    []      -> Maybe (Int, Type)
forall a. Maybe a
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 :: Int -> CoreExpr
mkIntExpr Int
i = DataCon -> [CoreExpr] -> CoreExpr
mkCoreConApps DataCon
intDataCon [Literal -> CoreExpr
forall b. Literal -> Expr b
Lit (LitNumType -> Integer -> Literal
LitNumber LitNumType
LitNumInt (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
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 :: Word -> CoreExpr
mkWordExpr Word
w = DataCon -> [CoreExpr] -> CoreExpr
mkCoreConApps DataCon
wordDataCon [Literal -> CoreExpr
forall b. Literal -> Expr b
Lit (LitNumType -> Integer -> Literal
LitNumber LitNumType
LitNumWord (Word -> Integer
forall a. Integral a => a -> Integer
toInteger Word
w))]