packages feed

egison-5.1.0: hs-src/Language/Egison/Type/TypeClassExpand.hs

{- |
Module      : Language.Egison.Type.TypeClassExpand
Licence     : MIT

This module expands type class method calls using type information from TIExpr.
It transforms TIExpr to TIExpr, replacing type class method calls with
dictionary-based dispatch.

Pipeline: Phase 7 (TypedDesugar) - TypeClassExpand
This is executed after TensorMapInsertion.  TensorMapInsertion must see the
unexpanded qualified type first; this module then resolves type class methods
to concrete dictionary-based functions.

For example, if we have:
  class Eq a where (==) : a -> a -> Bool
  instance Eq Integer where (==) x y := x = y

Then a call like:
  autoEq 1 2  (with type constraint: Eq Integer)
becomes:
  eqIntegerEq 1 2  (dictionary-based dispatch)

This eliminates the need for runtime dispatch functions like resolveEq.
-}

module Language.Egison.Type.TypeClassExpand
  ( expandTypeClassMethodsT
  , expandTypeClassMethodsInPattern
  , addDictionaryParametersT
  , applyConcreteConstraintDictionaries
  , applyConcreteConstraintDictionariesInPattern
  , fixUnboundDictRefs
  ) where

import           Data.Char                  (toLower)
import           Data.List                  (isPrefixOf)
import           Data.Maybe                 (mapMaybe)
import           Data.Text                  (pack, unpack)
import           Control.Monad              (mplus)
import qualified Data.Set                   as Set

import           Language.Egison.AST        (ConstantExpr(..))
import           Language.Egison.Data       (EvalM)
import           Language.Egison.EvalState  (MonadEval(..))
import           Language.Egison.IExpr      (TIExpr(..), TIExprNode(..), stringToVar,
                                             Index(..), tiExprType, tiScheme, tiExprNode,
                                             TIPattern(..), TIPatternNode(..), TILoopRange(..),
                                             IPrimitiveDataPattern,
                                             mapTIExprChildren, Var(..))
import           Language.Egison.Type.Env  (ClassEnv(..), ClassInfo(..), InstanceInfo(..),
                                             lookupInstances, lookupClass, lookupEnv)
import           Language.Egison.Type.Types (Type(..), TyVar(..), TypeScheme(..), Constraint(..), constraintType, typeToName,
                                            sanitizeMethodName, freeTyVars, instType, classParam, mapType)
import           Language.Egison.Type.Instance (findMatchingInstanceForTypes,
                                                  findMostSpecificInstanceForTypes)

-- ============================================================================
-- Helper Functions (shared across the module)
-- ============================================================================

-- | Dispatch helper: prefer the most-specific instance via subtype partial
-- order; fall back to the first unifying instance if specificity returns
-- an ambiguity error or no match. This keeps backward compatibility while
-- enabling deterministic specialization (see design/runtime-type-dispatch.md
-- §4). Runs in EvalM to consult the declared CAS subtype order
-- (`declare cas-subtype` edges) alongside the structural skeleton.
findInstanceForDispatch :: [Type] -> [InstanceInfo] -> EvalM (Maybe InstanceInfo)
findInstanceForDispatch tys insts = do
  edges <- getCasSubtypeEdges
  return $ case findMostSpecificInstanceForTypes edges tys insts of
    Right inst -> Just inst
    Left _     -> findMatchingInstanceForTypes tys insts

-- | Build the candidate list for `TIRuntimeDispatch` from a class's
-- instance list. Each candidate is the instance's principal type paired
-- with the dictionary variable name that holds the instance dictionary.
-- The MathValue instance itself is filtered out so the runtime dispatcher
-- never selects "self" (which would loop). Single-param classes only —
-- multi-param dispatch keeps using static specificity.
runtimeDispatchCandidates :: [InstanceInfo] -> [(Type, String)]
runtimeDispatchCandidates instances =
  [ (instType inst, dictName)
  | inst <- instances
  , length (instTypes inst) == 1
  , instType inst /= TMathValue
  , let dictName = lowerFirst (instClass inst) ++
                   concatMap typeToName (instTypes inst)
  ]

-- | Extract type variable substitutions from instance type and actual type
-- Example: [a] -> [[Integer]] gives [(a, [Integer])]
extractTypeSubstitutions :: Type -> Type -> [(TyVar, Type)]
extractTypeSubstitutions instTy actualTy = go instTy actualTy
  where
    go (TVar v) actual = [(v, actual)]
    go (TCollection instElem) (TCollection actualElem) = go instElem actualElem
    go (TTuple instTypes) (TTuple actualTypes)
      | length instTypes == length actualTypes =
          concatMap (\(i, a) -> go i a) (zip instTypes actualTypes)
    go (TInductive _ instArgs) (TInductive _ actualArgs)
      | length instArgs == length actualArgs =
          concatMap (\(i, a) -> go i a) (zip instArgs actualArgs)
    go (TTensor instElem) (TTensor actualElem) = go instElem actualElem
    go (TFun instArg instRet) (TFun actualArg actualRet) =
      go instArg actualArg ++ go instRet actualRet
    go (THash instK instV) (THash actualK actualV) =
      go instK actualK ++ go instV actualV
    go (TMatcher instT) (TMatcher actualT) = go instT actualT
    go (TMatcherSlot instS instT) (TMatcherSlot actualS actualT) = go instS actualS ++ go instT actualT
    go (TIO instT) (TIO actualT) = go instT actualT
    go (TIORef instT) (TIORef actualT) = go instT actualT
    go TPort TPort = []
    go _ _ = []

-- | Apply type substitutions to a constraint
applySubstsToConstraint :: [(TyVar, Type)] -> Constraint -> Constraint
applySubstsToConstraint substs (Constraint cName cTypes) =
  Constraint cName (map (applySubstsToType substs) cTypes)


-- | Apply type substitutions to a type. Built on 'mapType', so the
-- recursion lives in one place; symbol sets contain atoms, not types, and
-- are left untouched.
applySubstsToType :: [(TyVar, Type)] -> Type -> Type
applySubstsToType substs = mapType replace
  where
    replace t@(TVar v) = case lookup v substs of
                           Just newType -> newType
                           Nothing      -> t
    replace t          = t

-- | Get the arity of a function type (number of parameters)
getMethodArity :: Type -> Int
getMethodArity (TFun _ t2) = 1 + getMethodArity t2
getMethodArity _ = 0

-- | Get parameter types from a function type
getParamTypes :: Type -> [Type]
getParamTypes (TFun t1 t2) = t1 : getParamTypes t2
getParamTypes _ = []

-- | Apply N parameters to a function type and get the result type
-- applyParamsToType (a -> b -> c) 2 = c
-- applyParamsToType (a -> b -> c) 1 = b -> c
applyParamsToType :: Type -> Int -> Type
applyParamsToType (TFun _ t2) n
  | n > 0 = applyParamsToType t2 (n - 1)
applyParamsToType t _ = t  -- n == 0 or no more function types

-- | Lowercase first character of a string
lowerFirst :: String -> String
lowerFirst [] = []
lowerFirst (c:cs) = toLower c : cs

-- | Locally-bound variable names visible at an expression node. Local
-- binders always shadow top-level definitions, so names in this set must
-- never be treated as class methods or as references to constrained
-- top-level functions (e.g. a parameter named `count` must not receive
-- the dictionary arguments of lib's `count {Eq a}`).
type LocalScope = Set.Set String

-- | Names bound by a primitive-data pattern (let/letrec/do binders,
-- matcher primitive-data-match clauses). PDPatternBase is Foldable over
-- its variable slots (PDPatVar), so folding collects exactly the binders.
pdBoundNames :: IPrimitiveDataPattern -> [String]
pdBoundNames pd = [n | Var n _ <- foldr (:) [] pd]

-- | Find a constraint that provides the given method (checks superclass chain).
-- Returns the constraint, the class that owns the method, and the superclass path.
findConstraintForMethod :: ClassEnv -> String -> [Constraint] -> Maybe Constraint
findConstraintForMethod env methodName cs =
  case findConstraintForMethodWithPath env methodName cs of
    Just (constraint, _, _) -> Just constraint
    Nothing -> Nothing

-- | Like findConstraintForMethod but also returns the owning class and superclass path.
findConstraintForMethodWithPath :: ClassEnv -> String -> [Constraint]
                                -> Maybe (Constraint, String, [String])
findConstraintForMethodWithPath env methodName cs = go cs
  where
    go [] = Nothing
    go (c@(Constraint className _) : rest) =
      case findMethodInHierarchy env className methodName of
        Just (ownerClass, path) -> Just (c, ownerClass, path)
        Nothing -> go rest

-- | Search for a method in the class hierarchy starting from a given class.
-- Returns the class that owns the method and the path to it.
findMethodInHierarchy :: ClassEnv -> String -> String -> Maybe (String, [String])
findMethodInHierarchy env startClass methodName = bfs [(startClass, [])]
  where
    bfs [] = Nothing
    bfs ((current, path):queue) =
      case lookupClass current env of
        Nothing -> bfs queue
        Just info ->
          if methodName `elem` map fst (classMethods info)
          then Just (current, path)
          else let nexts = [(s, path ++ [s]) | s <- classSupers info]
               in bfs (queue ++ nexts)

-- ============================================================================
-- Main Type Class Expansion
-- ============================================================================

-- | Expand type class method calls in a typed expression (TIExpr)
-- This function recursively processes TIExpr and replaces type class method calls
-- with dictionary-based dispatch.
expandTypeClassMethodsT :: TIExpr -> EvalM TIExpr
expandTypeClassMethodsT tiExpr = do
  classEnv <- getClassEnv
  -- Use expandTIExprWithConstraints which handles constraint clearing
  expandTIExprWithConstraints classEnv Set.empty tiExpr
  where
    -- Expand TIExprNode without parent constraints
    -- Each child expression uses only its own constraints from type inference
    expandTIExprNode :: ClassEnv -> LocalScope -> TIExprNode -> EvalM TIExprNode
    expandTIExprNode classEnv' scope node = case node of
      -- Constants and variables: no expansion needed at node level
      -- (TIVarExpr expansion is handled at TIExpr level in expandTIExprWithConstraints)
      TIConstantExpr c -> return $ TIConstantExpr c
      TIVarExpr name -> return $ TIVarExpr name
      
      -- Lambda expressions: process body with its own constraints only
      TILambdaExpr mVar params body -> do
        -- Use only the body's own constraints (no parent constraints)
        -- Type inference has already assigned correct constraints to each expression
        let scope' = foldr Set.insert scope
                       ([n | Var n _ <- params] ++ [n | Just (Var n _) <- [mVar]])
        body' <- expandTIExprWithConstraints classEnv' scope' body
        return $ TILambdaExpr mVar params body'
      
      -- Application: check if it's a method call or constrained function call
      TIApplyExpr func args -> do
        -- First, expand the arguments (each uses its own constraints)
        args' <- mapM (expandTIExprWithConstraints classEnv' scope) args

        case tiExprNode func of
          TIVarExpr methodName -> do
            -- Try to resolve if func is a method call using func's own constraints
            let (Forall _ funcConstraints _) = tiScheme func
            resolved <- tryResolveMethodCall classEnv' scope funcConstraints methodName args'
            case resolved of
              Just result -> return result
              Nothing -> do
                -- Not a method call - process recursively
                -- Note: Dictionary application for constrained functions
                -- is handled in TIVarExpr case of expandTIExprWithConstraints
                func' <- expandTIExprWithConstraints classEnv' scope func
                return $ TIApplyExpr func' args'
          _ -> do
            -- Not a simple variable: process recursively
            func' <- expandTIExprWithConstraints classEnv' scope func
            return $ TIApplyExpr func' args'
      
      -- Collections
      TITupleExpr exprs -> do
        exprs' <- mapM (expandTIExprWithConstraints classEnv' scope) exprs
        return $ TITupleExpr exprs'

      TICollectionExpr exprs -> do
        exprs' <- mapM (expandTIExprWithConstraints classEnv' scope) exprs
        return $ TICollectionExpr exprs'

      -- Control flow
      TIIfExpr cond thenExpr elseExpr -> do
        cond' <- expandTIExprWithConstraints classEnv' scope cond
        thenExpr' <- expandTIExprWithConstraints classEnv' scope thenExpr
        elseExpr' <- expandTIExprWithConstraints classEnv' scope elseExpr
        return $ TIIfExpr cond' thenExpr' elseExpr'

      -- Let bindings. `let` is non-recursive (RHSs are evaluated in the
      -- outer environment); `letrec` binders are visible in every RHS.
      TILetExpr bindings body -> do
        bindings' <- mapM (\(v, e) -> do
          e' <- expandTIExprWithConstraints classEnv' scope e
          return (v, e')) bindings
        let scope' = foldr Set.insert scope (concatMap (pdBoundNames . fst) bindings)
        body' <- expandTIExprWithConstraints classEnv' scope' body
        return $ TILetExpr bindings' body'

      TILetRecExpr bindings body -> do
        let scope' = foldr Set.insert scope (concatMap (pdBoundNames . fst) bindings)
        bindings' <- mapM (\(v, e) -> do
          e' <- expandTIExprWithConstraints classEnv' scope' e
          return (v, e')) bindings
        body' <- expandTIExprWithConstraints classEnv' scope' body
        return $ TILetRecExpr bindings' body'

      TISeqExpr e1 e2 -> do
        e1' <- expandTIExprWithConstraints classEnv' scope e1
        e2' <- expandTIExprWithConstraints classEnv' scope e2
        return $ TISeqExpr e1' e2'

      -- Collections
      TIConsExpr h t -> do
        h' <- expandTIExprWithConstraints classEnv' scope h
        t' <- expandTIExprWithConstraints classEnv' scope t
        return $ TIConsExpr h' t'

      TIJoinExpr l r -> do
        l' <- expandTIExprWithConstraints classEnv' scope l
        r' <- expandTIExprWithConstraints classEnv' scope r
        return $ TIJoinExpr l' r'
      
      TIHashExpr pairs -> do
        -- Dictionary hashes: process keys but NOT values
        -- Values should remain as simple method references
        pairs' <- mapM (\(k, v) -> do
          k' <- expandTIExprWithConstraints classEnv' scope k
          -- Do NOT process v - dictionary values should not be expanded
          return (k', v)) pairs
        return $ TIHashExpr pairs'

      TIVectorExpr exprs -> do
        exprs' <- mapM (expandTIExprWithConstraints classEnv' scope) exprs
        return $ TIVectorExpr exprs'

      -- More lambda-like constructs
      TIMemoizedLambdaExpr vars body -> do
        let scope' = foldr Set.insert scope vars
        body' <- expandTIExprWithConstraints classEnv' scope' body
        return $ TIMemoizedLambdaExpr vars body'

      TICambdaExpr var body -> do
        body' <- expandTIExprWithConstraints classEnv' (Set.insert var scope) body
        return $ TICambdaExpr var body'

      TIWithSymbolsExpr syms body -> do
        let scope' = foldr Set.insert scope syms
        body' <- expandTIExprWithConstraints classEnv' scope' body
        return $ TIWithSymbolsExpr syms body'

      -- Do bindings are sequential: each RHS sees the binders of the
      -- previous bindings; the body sees them all.
      TIDoExpr bindings body -> do
        (bindingsRev, scope') <- foldl
          (\acc (v, e) -> do
            (done, sc) <- acc
            e' <- expandTIExprWithConstraints classEnv' sc e
            return ((v, e') : done, foldr Set.insert sc (pdBoundNames v)))
          (return ([], scope)) bindings
        body' <- expandTIExprWithConstraints classEnv' scope' body
        return $ TIDoExpr (reverse bindingsRev) body'

      -- Pattern matching. Pattern variables bind left-to-right: embedded
      -- expressions (value/predicate patterns, loop ranges) see the binders
      -- accumulated so far, and the clause body sees them all.
      TIMatchExpr mode target matcher clauses -> do
        target' <- expandTIExprWithConstraints classEnv' scope target
        matcher' <- expandTIExprWithConstraints classEnv' scope matcher
        clauses' <- mapM (\(pat, body) -> do
          (pat', clauseScope) <- expandTIPattern classEnv' scope pat
          body' <- expandTIExprWithConstraints classEnv' clauseScope body
          return (pat', body')) clauses
        return $ TIMatchExpr mode target' matcher' clauses'

      TIMatchAllExpr mode target matcher clauses -> do
        target' <- expandTIExprWithConstraints classEnv' scope target
        matcher' <- expandTIExprWithConstraints classEnv' scope matcher
        clauses' <- mapM (\(pat, body) -> do
          (pat', clauseScope) <- expandTIPattern classEnv' scope pat
          body' <- expandTIExprWithConstraints classEnv' clauseScope body
          return (pat', body')) clauses
        return $ TIMatchAllExpr mode target' matcher' clauses'

      -- Tensor operations
      TITensorMapExpr func tensor -> do
        func' <- expandTIExprWithConstraints classEnv' scope func
        tensor' <- expandTIExprWithConstraints classEnv' scope tensor
        return $ TITensorMapExpr func' tensor'

      TITensorMap2Expr func t1 t2 -> do
        func' <- expandTIExprWithConstraints classEnv' scope func
        t1' <- expandTIExprWithConstraints classEnv' scope t1
        t2' <- expandTIExprWithConstraints classEnv' scope t2
        return $ TITensorMap2Expr func' t1' t2'

      TITensorMap2WedgeExpr func t1 t2 -> do
        func' <- expandTIExprWithConstraints classEnv' scope func
        t1' <- expandTIExprWithConstraints classEnv' scope t1
        t2' <- expandTIExprWithConstraints classEnv' scope t2
        return $ TITensorMap2WedgeExpr func' t1' t2'

      TIGenerateTensorExpr func shape -> do
        func' <- expandTIExprWithConstraints classEnv' scope func
        shape' <- expandTIExprWithConstraints classEnv' scope shape
        return $ TIGenerateTensorExpr func' shape'

      TITensorExpr shape elems -> do
        shape' <- expandTIExprWithConstraints classEnv' scope shape
        elems' <- expandTIExprWithConstraints classEnv' scope elems
        return $ TITensorExpr shape' elems'

      TITensorContractExpr tensor -> do
        tensor' <- expandTIExprWithConstraints classEnv' scope tensor
        return $ TITensorContractExpr tensor'

      TITransposeExpr perm tensor -> do
        perm' <- expandTIExprWithConstraints classEnv' scope perm
        tensor' <- expandTIExprWithConstraints classEnv' scope tensor
        return $ TITransposeExpr perm' tensor'

      TIFlipIndicesExpr tensor -> do
        tensor' <- expandTIExprWithConstraints classEnv' scope tensor
        return $ TIFlipIndicesExpr tensor'

      -- Quote expressions
      TIQuoteExpr e -> do
        e' <- expandTIExprWithConstraints classEnv' scope e
        return $ TIQuoteExpr e'

      TIQuoteSymbolExpr e -> do
        e' <- expandTIExprWithConstraints classEnv' scope e
        return $ TIQuoteSymbolExpr e'

      -- Indexed expressions
      TISubrefsExpr b base ref -> do
        base' <- expandTIExprWithConstraints classEnv' scope base
        ref' <- expandTIExprWithConstraints classEnv' scope ref
        return $ TISubrefsExpr b base' ref'
      
      TISuprefsExpr b base ref -> do
        base' <- expandTIExprWithConstraints classEnv' scope base
        ref' <- expandTIExprWithConstraints classEnv' scope ref
        return $ TISuprefsExpr b base' ref'

      TIUserrefsExpr b base ref -> do
        base' <- expandTIExprWithConstraints classEnv' scope base
        ref' <- expandTIExprWithConstraints classEnv' scope ref
        return $ TIUserrefsExpr b base' ref'

      -- Other cases: return unchanged for now
      TIInductiveDataExpr name exprs -> do
        exprs' <- mapM (expandTIExprWithConstraints classEnv' scope) exprs
        return $ TIInductiveDataExpr name exprs'

      TIMatcherExpr patDefs -> do
        -- Expand expressions inside matcher definitions
        -- patDefs is a list of (PrimitivePatPattern, TIExpr, [TIBindingExpr])
        -- where TIBindingExpr is (IPrimitiveDataPattern, TIExpr)
        patDefs' <- mapM (\(pat, matcherExpr, bindings) -> do
          -- Expand the next-matcher expression
          matcherExpr' <- expandTIExprWithConstraints classEnv' scope matcherExpr
          -- Expand expressions in primitive-data-match clauses; the
          -- primitive-data pattern's variables are bound in its expression
          bindings' <- mapM (\(dp, expr) -> do
            let scope' = foldr Set.insert scope (pdBoundNames dp)
            expr' <- expandTIExprWithConstraints classEnv' scope' expr
            return (dp, expr')) bindings
          return (pat, matcherExpr', bindings')) patDefs
        return $ TIMatcherExpr patDefs'
      TIIndexedExpr override base indices -> do
        base' <- expandTIExprWithConstraints classEnv' scope base
        -- Expand indices (which are already typed as TIExpr)
        indices' <- mapM (traverse (\tiexpr -> expandTIExprWithConstraints classEnv' scope tiexpr)) indices
        return $ TIIndexedExpr override base' indices'

      TIWedgeApplyExpr func args -> do
        func' <- expandTIExprWithConstraints classEnv' scope func
        args' <- mapM (expandTIExprWithConstraints classEnv' scope) args
        return $ TIWedgeApplyExpr func' args'
      
      TIFunctionExpr names -> return $ TIFunctionExpr names  -- Built-in function, no expansion needed

      -- Runtime dispatch: traverse args; class/method/candidates are already resolved.
      TIRuntimeDispatch className methodName candidates args -> do
        args' <- mapM (expandTIExprWithConstraints classEnv' scope) args
        return $ TIRuntimeDispatch className methodName candidates args'

      -- Reshape: traverse the inner expression; type annotation is metadata.
      TIReshape ty inner -> do
        inner' <- expandTIExprWithConstraints classEnv' scope inner
        return $ TIReshape ty inner'

    -- Helper: expand a TIExpr using only its own constraints
    -- Parent constraints are not passed to avoid constraint accumulation
    expandTIExprWithConstraints :: ClassEnv -> LocalScope -> TIExpr -> EvalM TIExpr
    expandTIExprWithConstraints classEnv' scope expr = do
      let scheme@(Forall _ exprConstraints exprType) = tiScheme expr
          -- Use only the expression's own constraints
          -- Type inference has already assigned correct constraints to each expression
          allConstraints = exprConstraints

      -- Special handling for TIVarExpr: eta-expand methods or apply dictionaries
      expandedNode <- case tiExprNode expr of
        -- Locally bound names (lambda params, let/match binders, ...) always
        -- shadow top-level definitions: treat them as plain variables, never
        -- as class methods or constrained top-level functions.
        TIVarExpr varName | varName `Set.member` scope ->
          expandTIExprNode classEnv' scope (tiExprNode expr)
        TIVarExpr varName -> do
          -- Check if this is a type class method
          case findConstraintForMethod classEnv' varName allConstraints of
            Just constraint@(Constraint className tyArgs) -> do
              -- Principal type: head of tyArgs (the first class type parameter).
              -- For multi-param classes, additional types are in `tyArgs` and used
              -- by `findMatchingInstanceForTypes` for full dispatch.
              let tyArg = constraintType constraint
              -- Get method type to determine arity
              typeEnv <- getTypeEnv
              case lookupEnv (stringToVar varName) typeEnv of
                Just (Forall _ _ _ty) -> do
                  -- Use the expression's actual type (exprType) instead of the method's declared type (ty)
                  -- because eta-expansion should create parameters matching the expected usage context
                  let arity = getMethodArity exprType
                      paramTypes = getParamTypes exprType
                      paramNames = ["etaVar" ++ show i | i <- [1..arity]]
                      paramVars = map stringToVar paramNames
                      paramExprs = zipWith (\n t -> TIExpr (Forall [] [] t) (TIVarExpr n)) paramNames paramTypes
                      methodKey = sanitizeMethodName varName

                  -- Determine dictionary name based on type
                  case tyArg of
                    TVar (TyVar _v) -> do
                      -- Type variable: use dictionary parameter name (without type parameter)
                      typeEnv <- getTypeEnv
                      let dictParamName = "dict_" ++ className
                      -- Look up dictionary type from type environment
                      dictHashType <- case lookupEnv (stringToVar dictParamName) typeEnv of
                        Just (Forall _ _ dictType) -> return dictType
                        Nothing -> return $ THash TString TAny  -- Fallback
                      -- Get method type from ClassEnv instead of dictHashType
                      let methodType = getMethodTypeFromClass classEnv' className methodKey tyArg
                          methodConstraint = Constraint className tyArgs
                          methodScheme = Forall (Set.toList $ freeTyVars tyArg) [methodConstraint] methodType
                          dictExpr = TIExpr (Forall [] [] dictHashType) (TIVarExpr dictParamName)
                          indexExpr = TIExpr (Forall [] [] TString)
                                            (TIConstantExpr (StringExpr (pack methodKey)))
                          dictAccess = TIExpr methodScheme $
                                       TIIndexedExpr False dictExpr [Sub indexExpr]
                      -- 0-arity methods (constants like zero, one): return dict access directly
                      if null paramVars
                        then return $ TIIndexedExpr False dictExpr [Sub indexExpr]
                        else do
                          let resultType = applyParamsToType methodType (length paramExprs)
                              bodyScheme = case resultType of
                                             TFun _ _ -> methodScheme
                                             _ -> Forall [] [] resultType
                              body = TIExpr bodyScheme (TIApplyExpr dictAccess paramExprs)
                          return $ TILambdaExpr Nothing paramVars body
                    _ -> do
                      -- Concrete type: find matching instance using all
                      -- constraint types (single-param classes pass [t]).
                      let instances = lookupInstances className classEnv'
                      mInst <- findInstanceForDispatch tyArgs instances
                      case mInst of
                        Just inst -> do
                          -- Found instance: eta-expand with concrete dictionary
                          typeEnv <- getTypeEnv
                          let instTypeName = concatMap typeToName (instTypes inst)
                              dictName = lowerFirst className ++ instTypeName

                          -- Look up dictionary type from type environment
                          dictHashType <- case lookupEnv (stringToVar dictName) typeEnv of
                            Just (Forall _ _ dictType) -> return dictType
                            Nothing -> return $ THash TString TAny  -- Fallback

                          -- Get method type from ClassEnv instead of dictHashType
                          let methodType = getMethodTypeFromClass classEnv' className methodKey tyArg
                              methodConstraint = Constraint className tyArgs
                              methodScheme = Forall (Set.toList $ freeTyVars tyArg) [methodConstraint] methodType

                          -- Check if instance has nested constraints
                          dictExprBase <- if null (instContext inst)
                            then do
                              -- No constraints: dictionary is a simple hash
                              return $ TIExpr (Forall [] [] dictHashType) (TIVarExpr dictName)
                            else do
                              -- Has constraints: dictionary is a function that returns a hash
                              -- Get the result type (should be the hash type after applying arguments)
                              let dictFuncType = case dictHashType of
                                    TFun _ resultType -> TFun dictHashType resultType
                                    _ -> TFun (THash TString TAny) dictHashType
                                  dictFuncExpr = TIExpr (Forall [] [] dictFuncType) (TIVarExpr dictName)
                              dictArgs <- mapM (resolveDictionaryArg classEnv') (instContext inst)
                              return $ TIExpr (Forall [] [] dictHashType) (TIApplyExpr dictFuncExpr dictArgs)

                          let indexExpr = TIExpr (Forall [] [] TString)
                                               (TIConstantExpr (StringExpr (pack methodKey)))
                              dictAccess = TIExpr methodScheme $
                                           TIIndexedExpr False dictExprBase [Sub indexExpr]
                          -- 0-arity methods (constants like zero, one): return dict access directly
                          if null paramVars
                            then return $ TIIndexedExpr False dictExprBase [Sub indexExpr]
                            else do
                              let resultType = applyParamsToType methodType (length paramExprs)
                                  bodyScheme = case resultType of
                                                 TFun _ _ -> methodScheme
                                                 _ -> Forall [] [] resultType
                                  body = TIExpr bodyScheme (TIApplyExpr dictAccess paramExprs)
                              return $ TILambdaExpr Nothing paramVars body
                        Nothing -> checkConstrainedVariable
                Nothing -> checkConstrainedVariable
            Nothing -> checkConstrainedVariable
          where
            -- Check if this is a constrained variable (not a method)
            -- IMPORTANT: Only apply dictionaries if the variable was DEFINED with constraints,
            -- not just if the expression has propagated constraints from usage context.
            checkConstrainedVariable = do
              typeEnv <- getTypeEnv
              case lookupEnv (stringToVar varName) typeEnv of
                Just (Forall _ originalConstraints _)
                  | not (null originalConstraints) -> do
                      -- De-expand constraints to match the function's dict params
                      let minOrigCs = deExpandConstraints classEnv' originalConstraints
                          hasOnlyConcreteConstraints = all isConcreteConstraint exprConstraints
                      if null minOrigCs
                        then expandTIExprNode classEnv' scope (tiExprNode expr)
                        else if hasOnlyConcreteConstraints
                        then do
                          -- Concrete types: resolve dict args using de-expanded original
                          -- constraints with concrete type substituted
                          let concreteType = case exprConstraints of
                                (c : _) -> constraintType c
                                []      -> TAny
                              -- For TVar constraints (single-param), substitute the concrete type.
                              -- Multi-param constraints with all concrete types pass through unchanged.
                              resolveType c = case constraintTypes c of
                                [TVar _] -> Constraint (constraintClass c) [concreteType]
                                _        -> c
                          dictArgs <- mapM (resolveDictionaryArg classEnv') (map resolveType minOrigCs)
                          -- Clear constraints on the inner var ref to prevent
                          -- applyConcreteConstraintDictionaries from adding dicts again
                          let Forall vs _ ty = scheme
                              varExpr = TIExpr (Forall vs [] ty) (TIVarExpr varName)
                          return $ TIApplyExpr varExpr dictArgs
                        else do
                          -- Type variable: pass dict params for de-expanded constraints
                          let makeDict c =
                                let dictName = constraintToDictParam c
                                    dictType = TVar (TyVar "dict")
                                in TIExpr (Forall [] [] dictType) (TIVarExpr dictName)
                              dictArgs = map makeDict minOrigCs
                              varExpr = TIExpr scheme (TIVarExpr varName)
                          return $ TIApplyExpr varExpr dictArgs
                _ ->
                  expandTIExprNode classEnv' scope (tiExprNode expr)

            isConcreteConstraint c = all isConcreteType (constraintTypes c)
            isConcreteType (TVar _) = False
            isConcreteType _        = True
        _ -> expandTIExprNode classEnv' scope (tiExprNode expr)

      -- If concrete dictionaries were applied by checkConstrainedVariable,
      -- clear constraints from the scheme to prevent applyConcreteConstraintDictionaries
      -- from adding them again (avoiding double-application).
      --
      -- TIApplyExpr: dispatched (n-ary methods, e.g. `(+) x y` → resolved
      -- function applied to args).
      -- TIIndexedExpr: 0-arity method (e.g. `zero` → `dict["zero"]`). Without
      -- this clear, applyConcreteConstraintDictionaries would wrap the value
      -- in `TIApplyExpr value [dict]`, treating the resolved value as a
      -- function and producing "Expected function, but found: 0" at runtime.
      let isConcrete c = all isConcreteType' (constraintTypes c)
          isConcreteType' (TVar _) = False
          isConcreteType' _        = True
          shouldClear = not (null exprConstraints) && all isConcrete exprConstraints
          scheme' = case expandedNode of
            TIApplyExpr _ _    | shouldClear -> let Forall vs _ ty = scheme in Forall vs [] ty
            TIIndexedExpr {}   | shouldClear -> let Forall vs _ ty = scheme in Forall vs [] ty
            _                                -> scheme
      return $ TIExpr scheme' expandedNode

    -- Expand type class methods in patterns (no parent constraints).
    -- Pattern variables bind left-to-right: the returned scope accumulates
    -- the names bound so far, so embedded expressions (value/predicate
    -- patterns, loop ranges) and the clause body see the right binders.
    expandTIPattern :: ClassEnv -> LocalScope -> TIPattern -> EvalM (TIPattern, LocalScope)
    expandTIPattern classEnv' scope (TIPattern scheme node) = do
      (node', scope') <- expandTIPatternNode classEnv' scope node
      return (TIPattern scheme node', scope')

    -- Thread the scope through a list of subpatterns left-to-right.
    expandTIPatterns :: ClassEnv -> LocalScope -> [TIPattern] -> EvalM ([TIPattern], LocalScope)
    expandTIPatterns classEnv' scope pats = go scope [] pats
      where
        go sc acc []       = return (reverse acc, sc)
        go sc acc (p : ps) = do
          (p', sc') <- expandTIPattern classEnv' sc p
          go sc' (p' : acc) ps

    -- Expand pattern nodes recursively (no parent constraints)
    expandTIPatternNode :: ClassEnv -> LocalScope -> TIPatternNode -> EvalM (TIPatternNode, LocalScope)
    expandTIPatternNode classEnv' scope node = case node of
      -- Loop pattern: the loop variable is bound in the subpatterns
      TILoopPat var loopRange pat1 pat2 -> do
        loopRange' <- expandTILoopRange classEnv' scope loopRange
        let scopeV = Set.insert var scope
        (pat1', scope1) <- expandTIPattern classEnv' scopeV pat1
        (pat2', scope2) <- expandTIPattern classEnv' scope1 pat2
        return (TILoopPat var loopRange' pat1' pat2', scope2)

      -- Recursive pattern constructors
      TIAndPat pat1 pat2 -> do
        (pat1', scope1) <- expandTIPattern classEnv' scope pat1
        (pat2', scope2) <- expandTIPattern classEnv' scope1 pat2
        return (TIAndPat pat1' pat2', scope2)

      -- Or-pattern alternatives must bind the same variables; take the
      -- union so the body sees them whichever alternative matched.
      TIOrPat pat1 pat2 -> do
        (pat1', scope1) <- expandTIPattern classEnv' scope pat1
        (pat2', scope2) <- expandTIPattern classEnv' scope pat2
        return (TIOrPat pat1' pat2', Set.union scope1 scope2)

      TIForallPat pat1 pat2 -> do
        (pat1', scope1) <- expandTIPattern classEnv' scope pat1
        (pat2', scope2) <- expandTIPattern classEnv' scope1 pat2
        return (TIForallPat pat1' pat2', scope2)

      -- Not-pattern bindings never escape (a match produces no bindings)
      TINotPat pat -> do
        (pat', _) <- expandTIPattern classEnv' scope pat
        return (TINotPat pat', scope)

      TITuplePat pats -> do
        (pats', scope') <- expandTIPatterns classEnv' scope pats
        return (TITuplePat pats', scope')

      TIInductivePat name pats -> do
        (pats', scope') <- expandTIPatterns classEnv' scope pats
        return (TIInductivePat name pats', scope')

      TIIndexedPat pat exprs -> do
        (pat', scope') <- expandTIPattern classEnv' scope pat
        exprs' <- mapM (expandTIExprWithConstraints classEnv' scope') exprs
        return (TIIndexedPat pat' exprs', scope')

      TILetPat bindings pat -> do
        let scopeB = foldr Set.insert scope (concatMap (pdBoundNames . fst) bindings)
        (pat', scope') <- expandTIPattern classEnv' scopeB pat
        return (TILetPat bindings pat', scope')  -- TODO: Expand binding expressions

      TIPApplyPat funcExpr argPats -> do
        funcExpr' <- expandTIExprWithConstraints classEnv' scope funcExpr
        (argPats', scope') <- expandTIPatterns classEnv' scope argPats
        return (TIPApplyPat funcExpr' argPats', scope')

      TIDApplyPat pat pats -> do
        (pat', scope1) <- expandTIPattern classEnv' scope pat
        (pats', scope') <- expandTIPatterns classEnv' scope1 pats
        return (TIDApplyPat pat' pats', scope')

      TISeqConsPat pat1 pat2 -> do
        (pat1', scope1) <- expandTIPattern classEnv' scope pat1
        (pat2', scope2) <- expandTIPattern classEnv' scope1 pat2
        return (TISeqConsPat pat1' pat2', scope2)

      TISeqNilPat -> return (TISeqNilPat, scope)

      TIVarPat name -> return (TIVarPat name, scope)

      TIInductiveOrPApplyPat name pats -> do
        (pats', scope') <- expandTIPatterns classEnv' scope pats
        return (TIInductiveOrPApplyPat name pats', scope')

      -- Leaf patterns: no expansion needed
      TIWildCard -> return (TIWildCard, scope)
      TIPatVar name -> return (TIPatVar name, Set.insert name scope)
      TIValuePat expr -> do
        expr' <- expandTIExprWithConstraints classEnv' scope expr
        return (TIValuePat expr', scope)
      TIPredPat pred -> do
        pred' <- expandTIExprWithConstraints classEnv' scope pred
        return (TIPredPat pred', scope)
      TIContPat -> return (TIContPat, scope)
      TILaterPatVar -> return (TILaterPatVar, scope)

    -- Expand loop range expressions (no parent constraints)
    expandTILoopRange :: ClassEnv -> LocalScope -> TILoopRange -> EvalM TILoopRange
    expandTILoopRange classEnv' scope (TILoopRange start end rangePat) = do
      start' <- expandTIExprWithConstraints classEnv' scope start
      end' <- expandTIExprWithConstraints classEnv' scope end
      (rangePat', _) <- expandTIPattern classEnv' scope rangePat
      return $ TILoopRange start' end' rangePat'

    -- Try to resolve a method call using type class constraints.
    -- Uses superclass chain traversal to find methods in transitive superclasses.
    -- A locally-bound name is never a class method (local binders shadow).
    tryResolveMethodCall :: ClassEnv -> LocalScope -> [Constraint] -> String -> [TIExpr] -> EvalM (Maybe TIExprNode)
    tryResolveMethodCall _ scope _ methodName _
      | methodName `Set.member` scope = return Nothing
    tryResolveMethodCall classEnv' _ cs methodName expandedArgs = do
      -- De-expand constraints to get the minimal set (matching dict params)
      let minCs = deExpandConstraints classEnv' cs
      case findConstraintForMethodWithPath classEnv' methodName minCs of
        Nothing -> return Nothing
        Just (constraint@(Constraint constraintClass _), ownerClass, path) -> do
          let methodKey = sanitizeMethodName methodName
              dictHashType = THash TString TAny
              tyArg = constraintType constraint   -- principal (first) type
              tyArgs = constraintTypes constraint
          -- Determine the actual type for instance lookup. We refine the first
          -- type from the call's first argument if the constraint's first type
          -- is still a type variable; subsequent multi-param types are unchanged.
          let argTypes = map tiExprType expandedArgs
              actualType = case (tyArg, argTypes) of
                (TVar _, (t:_)) -> t
                _ -> tyArg
              actualTypes = case (tyArgs, argTypes) of
                (TVar _ : rest, t:_) -> t : rest
                _                     -> tyArgs
          case actualType of
            TVar _ -> do
              -- Type variable: use dictionary parameter with superclass chain
              let dictParamName = "dict_" ++ constraintClass
                  dictExpr = TIExpr (Forall [] [] dictHashType) (TIVarExpr dictParamName)
                  chainedDict = buildSuperclassChain dictExpr path
                  methodType = getMethodTypeFromClass classEnv' ownerClass methodKey actualType
                  methodScheme = Forall [] [] methodType
                  indexExpr = TIExpr (Forall [] [] TString)
                                    (TIConstantExpr (StringExpr (pack methodKey)))
                  dictAccess = TIExpr methodScheme $
                               TIIndexedExpr False chainedDict [Sub indexExpr]
              return $ Just $ TIApplyExpr dictAccess expandedArgs
            _ -> do
              -- Concrete type: find matching instance for the ownerClass.
              -- Use full-list dispatch (multi-param-aware).
              let instances = lookupInstances ownerClass classEnv'
              -- Phase 3: if the dispatch target is TMathValue and there is
              -- no explicit `instance Class MathValue`, defer to runtime
              -- dispatch via `TIRuntimeDispatch`. This lets users write only
              -- specific (Frac/Poly/Term/Factor) instances and have the
              -- compiler pick the right one based on the value's CAS shape.
              let mathValueInstanceExists =
                    any (\inst -> instTypes inst == [TMathValue]) instances
                  -- TInt is an alias for TMathValue in Egison's CAS layer
                  -- (see typeToName / typeConstructorName which map both to
                  -- "MathValue"). Treat TInt as MathValue for runtime
                  -- dispatch purposes so `declare symbol`-typed values
                  -- (which surface as TInt) trigger IRuntimeDispatch.
                  isMathValueLike t = t == TMathValue || t == TInt
                  shouldRuntimeDispatch =
                    isMathValueLike actualType
                      && not mathValueInstanceExists
                      && not (null (runtimeDispatchCandidates instances))
              if shouldRuntimeDispatch then do
                let candidates = runtimeDispatchCandidates instances
                return $ Just $
                  TIRuntimeDispatch ownerClass methodKey candidates expandedArgs
              else do
                mInst <- findInstanceForDispatch actualTypes instances
                case mInst of
                  Just inst -> do
                    let instTypeName = concatMap typeToName (instTypes inst)
                        dictName = lowerFirst ownerClass ++ instTypeName
                        methodType = getMethodTypeFromClass classEnv' ownerClass methodKey actualType
                        methodScheme = Forall [] [] methodType
                    dictExprBase <- if null (instContext inst)
                      then return $ TIExpr (Forall [] [] dictHashType) (TIVarExpr dictName)
                      else do
                        let dictFuncType = TFun (THash TString TAny) dictHashType
                            dictFuncExpr = TIExpr (Forall [] [] dictFuncType) (TIVarExpr dictName)
                            substitutedConstraints = substituteInstanceConstraints (instType inst) actualType (instContext inst)
                        dictArgs <- mapM (resolveDictionaryArg classEnv') substitutedConstraints
                        return $ TIExpr (Forall [] [] dictHashType) (TIApplyExpr dictFuncExpr dictArgs)
                    let indexExpr = TIExpr (Forall [] [] TString)
                                          (TIConstantExpr (StringExpr (pack methodKey)))
                        dictAccess = TIExpr methodScheme $
                                     TIIndexedExpr False dictExprBase [Sub indexExpr]
                    return $ Just $ TIApplyExpr dictAccess expandedArgs
                  Nothing -> return Nothing
    
    -- Substitute type variables in instance constraints based on actual type
    -- e.g., for instance {Eq a} Eq [a] matched with [[Integer]]
    -- instType = [a], actualType = [[Integer]]
    -- Extract: a -> [Integer], then apply to constraints {Eq a} -> {Eq [Integer]}
    substituteInstanceConstraints :: Type -> Type -> [Constraint] -> [Constraint]
    substituteInstanceConstraints instType actualType constraints =
      let substs = extractTypeSubstitutions instType actualType
      in map (applySubstsToConstraint substs) constraints

    -- Resolve a constraint to a dictionary argument (with depth limit to prevent infinite recursion)
    resolveDictionaryArg :: ClassEnv -> Constraint -> EvalM TIExpr
    resolveDictionaryArg classEnv constraint = resolveDictionaryArgWithDepth classEnv 50 constraint
    
    resolveDictionaryArgWithDepth :: ClassEnv -> Int -> Constraint -> EvalM TIExpr
    resolveDictionaryArgWithDepth _ 0 (Constraint className _) = do
      -- Depth limit reached, return error placeholder
      return $ TIExpr (Forall [] [] (TVar (TyVar "error"))) (TIVarExpr ("dict_" ++ className ++ "_TOO_DEEP"))
    
    resolveDictionaryArgWithDepth classEnv depth constraint@(Constraint className tyArgs) = do
      let tyArg = constraintType constraint  -- principal (first) type
      case tyArg of
        TVar (TyVar _v) -> do
          -- Type variable: use dictionary parameter name (without type parameter)
          -- e.g., for {Eq a}, return dict_Eq
          let dictParamName = "dict_" ++ className
              dictType = TVar (TyVar "dict")
          return $ TIExpr (Forall [] [] dictType) (TIVarExpr dictParamName)
        _ -> do
          -- Concrete type: find matching instance using all constraint types.
          let instances = lookupInstances className classEnv
          mInst <- findInstanceForDispatch tyArgs instances
          case mInst of
            Just inst -> do
              -- Found instance: generate dictionary name (e.g., "numInteger", "eqCollection")
              let instTypeName = concatMap typeToName (instTypes inst)
                  dictName = lowerFirst className ++ instTypeName
                  dictType = TVar (TyVar "dict")
                  dictExpr = TIExpr (Forall [] [] dictType) (TIVarExpr dictName)
              
              -- Check if this instance has nested constraints
              -- e.g., instance {Eq a} Eq [a] has constraint {Eq a}
              if null (instContext inst)
                then do
                  -- No constraints: return simple dictionary reference
                  return dictExpr
                else do
                  -- Has constraints: need to resolve them and apply to dictionary
                  -- e.g., for Eq [Integer], resolve {Eq Integer} -> eqInteger
                  -- then return: eqCollection eqInteger

                  -- Substitute type variables in constraints with actual types
                  -- e.g., for instance {Eq a} Eq [a] matched with [[Integer]]
                  -- instType inst = [a], tyArg = [[Integer]]
                  -- Extract: a -> [Integer]
                  -- Apply to constraints: {Eq a} -> {Eq [Integer]}
                  let substs = extractTypeSubstitutions (instType inst) tyArg
                      substitutedConstraints = map (applySubstsToConstraint substs) (instContext inst)

                  -- Recursively resolve each constraint with reduced depth
                  dictArgs <- mapM (resolveDictionaryArgWithDepth classEnv (depth - 1)) substitutedConstraints

                  -- Apply dictionary function to resolved dictionaries
                  -- e.g., eqCollection eqInteger (when resolving Eq [Integer])
                  --       eqCollection (eqCollection eqInteger) (when resolving Eq [[Integer]])
                  return $ TIExpr (Forall [] [] dictType) (TIApplyExpr dictExpr dictArgs)
            Nothing -> do
              -- No instance found - this is an error, but return a dummy for now
              return $ TIExpr (Forall [] [] (TVar (TyVar "error"))) (TIVarExpr "undefined")

-- | Generate dictionary parameter name from constraint
-- Used for both dictionary parameter generation and dictionary argument passing
-- Type parameters are not included in the dictionary parameter name
constraintToDictParam :: Constraint -> String
constraintToDictParam (Constraint className _constraintType) =
  "dict_" ++ className

-- | Remove constraints that are transitively implied by other constraints.
-- Given the expanded set {Field a, Ring a, AddGroup a, ...}, returns
-- only the "root" constraints: {Field a}.
deExpandConstraints :: ClassEnv -> [Constraint] -> [Constraint]
deExpandConstraints classEnv cs =
  filter (\c -> not (isSubsumedBy classEnv c cs)) cs
  where
    isSubsumedBy env (Constraint cn ty) allCs =
      any (\(Constraint cn' ty') ->
        cn /= cn' && ty == ty' && isTransitiveSuperclass env cn cn') allCs
    isTransitiveSuperclass env target start =
      case lookupClass start env of
        Nothing -> False
        Just info ->
          target `elem` classSupers info ||
          any (isTransitiveSuperclass env target) (classSupers info)

-- | Find a path through the superclass hierarchy from startClass to targetClass.
-- Returns the list of intermediate classes (excluding startClass, including targetClass).
-- Uses BFS to find the shortest path.
findSuperclassPath :: ClassEnv -> String -> String -> Maybe [String]
findSuperclassPath classEnv startClass targetClass
  | startClass == targetClass = Just []
  | otherwise = bfs [(startClass, [])]
  where
    bfs [] = Nothing
    bfs ((current, path):queue)
      | current == targetClass = Just path
      | otherwise =
          case lookupClass current classEnv of
            Nothing -> bfs queue
            Just info ->
              let nexts = [(s, path ++ [s]) | s <- classSupers info,
                           s `notElem` map fst queue, s `notElem` map fst [(current, path)]]
              in bfs (queue ++ nexts)

-- | Build a chain of superclass dictionary accesses as a TIExprNode.
-- Given dict_Field and path ["Ring", "MulMonoid", "MulSemigroup"],
-- generates: (dict_Field)_("__super_Ring")_("__super_MulMonoid")_("__super_MulSemigroup")
buildSuperclassChain :: TIExpr -> [String] -> TIExpr
buildSuperclassChain dictExpr [] = dictExpr
buildSuperclassChain dictExpr (step:rest) =
  let indexExpr = TIExpr (Forall [] [] TString)
                         (TIConstantExpr (StringExpr (pack ("__super_" ++ step))))
      accessed = TIExpr (Forall [] [] (THash TString TAny))
                        (TIIndexedExpr False dictExpr [Sub indexExpr])
  in buildSuperclassChain accessed rest

-- | Get method type from ClassEnv
-- This retrieves the method type from the class definition and substitutes type variables
-- Note: methodKey is the sanitized name (e.g., "plus"), but classMethods uses original names (e.g., "+")
-- We need to try both the sanitized and original names
getMethodTypeFromClass :: ClassEnv -> String -> String -> Type -> Type
getMethodTypeFromClass classEnv className methodKey constraintType =
  case lookupClass className classEnv of
    Just classInfo ->
      -- Try to find the method by sanitized name first, then try unsanitizing
      case lookup methodKey (classMethods classInfo) `mplus` lookupUnsanitized methodKey (classMethods classInfo) of
        Just classMethodType ->
          -- Substitute class type parameter with actual constraint type
          -- e.g., class Num a has plus : a -> a -> a
          --       constraint Num t0 → plus : t0 -> t0 -> t0
          applySubstsToType [(classParam classInfo, constraintType)] classMethodType
        Nothing -> TAny  -- Method not found in class
    Nothing -> TAny  -- Class not found
  where
    -- Lookup by unsanitizing the method key (reverse of sanitizeMethodName)
    -- e.g., "plus" -> "+", "times" -> "*"
    lookupUnsanitized :: String -> [(String, a)] -> Maybe a
    lookupUnsanitized key methods =
      case unsanitizeMethodName key of
        Just originalName -> lookup originalName methods
        Nothing -> Nothing

    -- Reverse of sanitizeMethodName
    unsanitizeMethodName :: String -> Maybe String
    unsanitizeMethodName "eq" = Just "=="
    unsanitizeMethodName "neq" = Just "/="
    unsanitizeMethodName "lt" = Just "<"
    unsanitizeMethodName "le" = Just "<="
    unsanitizeMethodName "gt" = Just ">"
    unsanitizeMethodName "ge" = Just ">="
    unsanitizeMethodName "plus" = Just "+"
    unsanitizeMethodName "minus" = Just "-"
    unsanitizeMethodName "times" = Just "*"
    unsanitizeMethodName "div" = Just "/"
    unsanitizeMethodName _ = Nothing

-- | Add dictionary parameters to a function based on its type scheme constraints
-- This transforms constrained functions into dictionary-passing style
addDictionaryParametersT :: TypeScheme -> TIExpr -> EvalM TIExpr
addDictionaryParametersT (Forall _vars constraints _ty) tiExpr
  | null constraints = return tiExpr  -- No constraints, no change
  | otherwise = do
      classEnv <- getClassEnv
      -- De-expand constraints to get the minimal set (e.g., {Field a} instead of
      -- {Field a, Ring a, AddGroup a, ...}).  Each root constraint gets one dict param.
      let cs = deExpandConstraints classEnv constraints
      if null cs then return tiExpr
                 else addDictParamsToTIExpr classEnv cs tiExpr
  where
    -- Add dictionary parameters to a TIExpr
    addDictParamsToTIExpr :: ClassEnv -> [Constraint] -> TIExpr -> EvalM TIExpr
    addDictParamsToTIExpr env cs expr = case tiExprNode expr of
      -- Lambda: add dictionary parameters before regular parameters
      TILambdaExpr mVar params body -> do
        let dictParams = map constraintToDictParam cs
            dictVars = map stringToVar dictParams
        -- Remap old expanded dict references (e.g., dict_MulSemigroup) in the body
        -- to superclass chain accesses from the new de-expanded params (e.g.,
        -- dict_Field -> __super_Ring -> __super_MulMonoid -> __super_MulSemigroup).
        -- expandTypeClassMethodsT (Step 1) already resolved methods using expanded
        -- dict names.  Now we remap those to chain accesses from minimal params.
        body' <- case tiExprNode body of
                   TIHashExpr _ -> return body
                   _ -> return $ remapDictRefsInBody env cs body
        let newNode = TILambdaExpr mVar (dictVars ++ params) body'
        return $ TIExpr (tiScheme expr) newNode
      
      -- Hash (dictionary definition): wrap in lambda AND apply dict params to methods
      -- Dictionary values are method references that need dictionary parameters
      TIHashExpr pairs -> do
        let dictParams = map constraintToDictParam cs
            dictVars = map stringToVar dictParams
            wrapperType = tiExprType expr
        
        -- For each value in the hash (which is a method reference),
        -- if it has constraints, apply dictionary parameters to it
        pairs' <- mapM (\(k, v) -> do
          -- Check if the value (method) has constraints
          typeEnv <- getTypeEnv
          let vNode = tiExprNode v
          case vNode of
            TIVarExpr methodName -> do
              case lookupEnv (stringToVar methodName) typeEnv of
                Just (Forall _ vConstraints _) | not (null vConstraints) -> do
                  -- Method has constraints, apply dictionary parameters
                  let dictArgExprs = map (\p -> TIExpr (Forall [] [] (TVar (TyVar "dict"))) (TIVarExpr p)) dictParams
                      vApplied = TIExpr (tiScheme v) (TIApplyExpr v dictArgExprs)
                  return (k, vApplied)
                _ -> return (k, v)  -- No constraints, keep as-is
            _ -> return (k, v)  -- Not a variable, keep as-is
          ) pairs
        
        let hashExpr' = TIExpr (tiScheme expr) (TIHashExpr pairs')
            newNode = TILambdaExpr Nothing dictVars hashExpr'
            newScheme = Forall [] [] wrapperType
        return $ TIExpr newScheme newNode
      
      -- Not a lambda: wrap in a lambda with dictionary parameters
      _ -> do
        let dictParams = map constraintToDictParam cs
            dictVars = map stringToVar dictParams
        -- Special handling for TIVarExpr: if it's a constrained variable, apply dictionaries
        expr' <- case tiExprNode expr of
          TIVarExpr varName -> do
            -- Check if this variable has constraints that match our constraints
            typeEnv <- getTypeEnv
            case lookupEnv (stringToVar varName) typeEnv of
              Just (Forall _ varConstraints _) | not (null varConstraints) -> do
                -- Check which constraints from varConstraints match parent constraints cs
                let (Forall _ exprConstraints _) = tiScheme expr
                    matchingConstraints = filter (\(Constraint eName eType) ->
                          any (\(Constraint pName pType) ->
                            eName == pName && eType == pType) cs) exprConstraints
                if null matchingConstraints
                  then replaceMethodCallsWithDictAccessT env cs expr
                  else do
                    -- Apply matching dictionary parameters
                    let dictArgExprs = map (\p -> TIExpr (Forall [] [] (TVar (TyVar "dict"))) (TIVarExpr p))
                                           (map constraintToDictParam matchingConstraints)
                        varExpr = TIExpr (tiScheme expr) (TIVarExpr varName)
                    return $ TIExpr (tiScheme expr) (TIApplyExpr varExpr dictArgExprs)
              _ -> replaceMethodCallsWithDictAccessT env cs expr
          _ -> replaceMethodCallsWithDictAccessT env cs expr
        let wrapperType = tiExprType expr
            newNode = TILambdaExpr Nothing dictVars expr'
            newScheme = Forall [] [] wrapperType
        return $ TIExpr newScheme newNode
    
    -- Remap old expanded dict references to superclass chain accesses.
    -- When expandTypeClassMethodsT resolved method * with {MulSemigroup a},
    -- it generated dict_MulSemigroup.  After de-expanding to {Field a},
    -- dict_MulSemigroup must become (dict_Field)_("__super_Ring")_(...).
    remapDictRefsInBody :: ClassEnv -> [Constraint] -> TIExpr -> TIExpr
    remapDictRefsInBody env cs tiExpr =
      let s = tiScheme tiExpr
          node' = remapNode (tiExprNode tiExpr)
      in TIExpr s node'
      where
        remapNode :: TIExprNode -> TIExprNode
        remapNode node = case node of
          TIVarExpr name
            | "dict_" `isPrefixOf` name ->
                let oldClass = drop 5 name  -- "dict_Foo" → "Foo"
                in case findDictChain env cs oldClass of
                     Just chainExpr -> tiExprNode chainExpr
                     Nothing -> node
          _ -> mapTIExprChildren (remapDictRefsInBody env cs) node

        findDictChain :: ClassEnv -> [Constraint] -> String -> Maybe TIExpr
        findDictChain classEnv minCs targetClass =
          -- For each de-expanded constraint, try to find a path to targetClass
          let tryConstraint (Constraint cn _ty) =
                case findSuperclassPath classEnv cn targetClass of
                  Just path ->
                    let dictExpr = TIExpr (Forall [] [] (THash TString TAny))
                                         (TIVarExpr ("dict_" ++ cn))
                    in Just (buildSuperclassChain dictExpr path)
                  Nothing -> Nothing
          in case mapMaybe tryConstraint minCs of
               (result:_) -> Just result
               [] -> Nothing

    -- Replace method calls with dictionary access in TIExpr
    replaceMethodCallsWithDictAccessT :: ClassEnv -> [Constraint] -> TIExpr -> EvalM TIExpr
    replaceMethodCallsWithDictAccessT env cs tiExpr = do
      let scheme@(Forall _ exprConstraints exprType) = tiScheme tiExpr
      newNode <- replaceMethodCallsInNode env cs exprConstraints exprType (tiExprNode tiExpr)
      return $ TIExpr scheme newNode
    
    -- Replace method calls in TIExprNode
    replaceMethodCallsInNode :: ClassEnv -> [Constraint] -> [Constraint] -> Type -> TIExprNode -> EvalM TIExprNode
    replaceMethodCallsInNode env cs _exprConstraints exprType node = case node of
      -- Standalone method reference: eta-expand with superclass chain access
      TIVarExpr methodName -> do
        case findConstraintForMethodWithPath env methodName cs of
          Just (constraint, ownerClass, path) -> do
            let tyArg = constraintType constraint
                dictParam = constraintToDictParam constraint
                arity = getMethodArity exprType
                paramTypes = getParamTypes exprType
                paramNames = ["etaVar" ++ show i | i <- [1..arity]]
                paramVars = map stringToVar paramNames
                paramExprs = zipWith (\n t -> TIExpr (Forall [] [] t) (TIVarExpr n)) paramNames paramTypes
                dictExpr = TIExpr (Forall [] [] (THash TString TAny)) (TIVarExpr dictParam)
                chainedDict = buildSuperclassChain dictExpr path
                methodType = getMethodTypeFromClass env ownerClass (sanitizeMethodName methodName) tyArg
                methodScheme = Forall [] [] methodType
                indexExpr = TIExpr (Forall [] [] TString)
                                  (TIConstantExpr (StringExpr (pack (sanitizeMethodName methodName))))
                dictAccess = TIExpr methodScheme $
                             TIIndexedExpr False chainedDict [Sub indexExpr]
            if null paramVars
              then return $ TIIndexedExpr False chainedDict [Sub indexExpr]
              else do
                let body = TIExpr methodScheme (TIApplyExpr dictAccess paramExprs)
                return $ TILambdaExpr Nothing paramVars body
          Nothing ->
            return $ TIVarExpr methodName
      
      -- Method call: replace with dictionary access via superclass chain
      TIApplyExpr func args -> do
        case tiExprNode func of
          TIVarExpr methodName -> do
            case findConstraintForMethodWithPath env methodName cs of
              Just (constraint, ownerClass, path) -> do
                let dictParam = constraintToDictParam constraint
                    tyArg = constraintType constraint
                    dictExpr = TIExpr (Forall [] [] (THash TString TAny)) (TIVarExpr dictParam)
                    chainedDict = buildSuperclassChain dictExpr path
                    methodType = getMethodTypeFromClass env ownerClass (sanitizeMethodName methodName) tyArg
                    methodScheme = Forall [] [] methodType
                    indexExpr = TIExpr (Forall [] [] TString) 
                                      (TIConstantExpr (StringExpr (pack (sanitizeMethodName methodName))))
                    dictAccess = TIExpr methodScheme $
                                 TIIndexedExpr False chainedDict [Sub indexExpr]
                args' <- mapM (replaceMethodCallsWithDictAccessT env cs) args
                return $ TIApplyExpr dictAccess args'
              Nothing -> do
                -- Not a method, process recursively
                func' <- replaceMethodCallsWithDictAccessT env cs func
                args' <- mapM (replaceMethodCallsWithDictAccessT env cs) args
                return $ TIApplyExpr func' args'
          _ -> do
            -- Not a simple variable, process recursively
            func' <- replaceMethodCallsWithDictAccessT env cs func
            args' <- mapM (replaceMethodCallsWithDictAccessT env cs) args
            return $ TIApplyExpr func' args'
      
      -- Lambda: recursively process body
      TILambdaExpr mVar params body -> do
        body' <- replaceMethodCallsWithDictAccessT env cs body
        return $ TILambdaExpr mVar params body'
      
      -- If: recursively process
      TIIfExpr cond thenExpr elseExpr -> do
        cond' <- replaceMethodCallsWithDictAccessT env cs cond
        thenExpr' <- replaceMethodCallsWithDictAccessT env cs thenExpr
        elseExpr' <- replaceMethodCallsWithDictAccessT env cs elseExpr
        return $ TIIfExpr cond' thenExpr' elseExpr'
      
      -- Let: recursively process
      TILetExpr bindings body -> do
        bindings' <- mapM (\(pat, e) -> do
          e' <- replaceMethodCallsWithDictAccessT env cs e
          return (pat, e')) bindings
        body' <- replaceMethodCallsWithDictAccessT env cs body
        return $ TILetExpr bindings' body'
      
      -- LetRec: recursively process
      TILetRecExpr bindings body -> do
        bindings' <- mapM (\(pat, e) -> do
          e' <- replaceMethodCallsWithDictAccessT env cs e
          return (pat, e')) bindings
        body' <- replaceMethodCallsWithDictAccessT env cs body
        return $ TILetRecExpr bindings' body'
      
      -- Hash: do NOT process values inside dictionary hashes
      -- Dictionary values should remain as simple references
      -- e.g., {| ("eq", eqCollectionEq), ... |} not {| ("eq", eqCollectionEq dict_Eq), ... |}
      -- We return the node as-is without recursively processing the pairs
      TIHashExpr pairs -> do
        -- Process only keys, not values (values should remain as method references)
        pairs' <- mapM (\(k, v) -> do
          k' <- replaceMethodCallsWithDictAccessT env cs k
          -- Do NOT process v - keep it as a simple reference
          return (k', v)) pairs
        return $ TIHashExpr pairs'
      
      -- Matcher: recursively process expressions inside matcher definitions
      TIMatcherExpr patDefs -> do
        patDefs' <- mapM (\(pat, matcherExpr, bindings) -> do
          -- Process the next-matcher expression
          matcherExpr' <- replaceMethodCallsWithDictAccessT env cs matcherExpr
          -- Process expressions in primitive-data-match clauses
          bindings' <- mapM (\(dp, expr) -> do
            expr' <- replaceMethodCallsWithDictAccessT env cs expr
            return (dp, expr')) bindings
          return (pat, matcherExpr', bindings')) patDefs
        return $ TIMatcherExpr patDefs'
      
      -- Other expressions: return as-is for now
      _ -> return node

-- | Apply dictionaries to expressions with concrete type constraints
-- This is used for top-level definitions like: def integer : Matcher Integer := eq
-- where the right-hand side (eq) has concrete type constraints {Eq Integer}
applyConcreteConstraintDictionaries :: TIExpr -> EvalM TIExpr
applyConcreteConstraintDictionaries expr = do
  classEnv <- getClassEnv
  let scheme@(Forall vars constraints _) = tiScheme expr

  -- First, recursively process sub-expressions
  expr' <- case tiExprNode expr of
    TIApplyExpr func args -> do
      func' <- applyConcreteConstraintDictionaries func
      args' <- mapM applyConcreteConstraintDictionaries args
      return $ TIExpr scheme (TIApplyExpr func' args')
    -- Indexed access (`R'_i_j_k~l` etc.) wraps a base expression that may
    -- itself need dict args applied. Without this recursion, a tensor-valued
    -- def whose body uses typeclass methods (e.g. `def R'_i_j_k~l :=
    -- generateTensor (\... -> Ring ops ...)`) keeps its `\dict_AddGroup ...
    -- ->` outer wrapper at the use-site, and the IIndexedExpr eval path
    -- (Core.hs `Value (Func ...)` arm) treats the lambda directly as a
    -- function-with-index, raising "Expected number, but found: <lambda>"
    -- when the lambda is later used in arithmetic.
    TIIndexedExpr override base indices -> do
      base' <- applyConcreteConstraintDictionaries base
      indices' <- mapM (traverse applyConcreteConstraintDictionaries) indices
      return $ TIExpr scheme (TIIndexedExpr override base' indices')
    _ -> return expr

  -- De-expand constraints to minimal set, then check if concrete
  let minConstraints = deExpandConstraints classEnv constraints
      isConcreteConstraint c = all isConcreteConstraintType (constraintTypes c)
      isConcreteConstraintType (TVar _) = False
      isConcreteConstraintType _        = True
      hasOnlyConcreteConstraints = not (null minConstraints) && all isConcreteConstraint minConstraints

  if hasOnlyConcreteConstraints
    then do
      dictArgs <- mapM (resolveDictionaryForConstraint classEnv) minConstraints
      let resultType = tiExprType expr'
          newScheme = Forall vars [] resultType
      -- Insert dict args between function and regular args
      case tiExprNode expr' of
        TIApplyExpr func args ->
          let funcWithDicts = TIExpr (tiScheme func) (TIApplyExpr func dictArgs)
          in return $ TIExpr newScheme (TIApplyExpr funcWithDicts args)
        _ ->
          return $ TIExpr newScheme (TIApplyExpr expr' dictArgs)
    else
      return expr'
  where
    -- Resolve dictionary for a concrete constraint.
    -- Multi-param classes use full-list dispatch; single-param falls back.
    resolveDictionaryForConstraint :: ClassEnv -> Constraint -> EvalM TIExpr
    resolveDictionaryForConstraint classEnv (Constraint className tyArgs) = do
      -- Normalize TInt to TMathValue for instance matching
      -- (Integer and MathValue share runtime representation in Egison).
      let normalizeType t = case t of
                              TInt -> TMathValue
                              _    -> t
          normalizedTypes = map normalizeType tyArgs
          instances = lookupInstances className classEnv
      mInst <- findInstanceForDispatch normalizedTypes instances
      case mInst of
        Just inst -> do
          -- Generate dictionary name (e.g., "eqInteger", "numInteger")
          let instTypeName = concatMap typeToName (instTypes inst)
              dictName = lowerFirst className ++ instTypeName
              dictType = TVar (TyVar "dict")
              dictExpr = TIExpr (Forall [] [] dictType) (TIVarExpr dictName)
          
          -- Check if instance has nested constraints
          if null (instContext inst)
            then do
              -- No constraints: return simple dictionary reference
              return dictExpr
            else do
              -- Has constraints: need to resolve them recursively
              nestedDictArgs <- mapM (resolveDictionaryForConstraint classEnv) (instContext inst)
              return $ TIExpr (Forall [] [] dictType) (TIApplyExpr dictExpr nestedDictArgs)
        Nothing -> do
          -- No instance found - return dummy dictionary
          let dictName = "dict_" ++ className ++ "_NOT_FOUND"
              dictType = TVar (TyVar "dict")
          return $ TIExpr (Forall [] [] dictType) (TIVarExpr dictName)

-- | Expand type class method calls in patterns
-- This is a public wrapper for expandTIPattern used by TypedDesugar
expandTypeClassMethodsInPattern :: TIPattern -> EvalM TIPattern
expandTypeClassMethodsInPattern tipat = do
  classEnv <- getClassEnv
  expandPatternWithClassEnv classEnv tipat
  where
    expandPatternWithClassEnv :: ClassEnv -> TIPattern -> EvalM TIPattern
    expandPatternWithClassEnv classEnv' (TIPattern scheme node) = do
      node' <- expandPatternNode classEnv' node
      return $ TIPattern scheme node'
    
    expandPatternNode :: ClassEnv -> TIPatternNode -> EvalM TIPatternNode
    expandPatternNode classEnv' node = case node of
      TILoopPat var loopRange pat1 pat2 -> do
        loopRange' <- expandLoopRange classEnv' loopRange
        pat1' <- expandPatternWithClassEnv classEnv' pat1
        pat2' <- expandPatternWithClassEnv classEnv' pat2
        return $ TILoopPat var loopRange' pat1' pat2'
      
      TIAndPat pat1 pat2 -> do
        pat1' <- expandPatternWithClassEnv classEnv' pat1
        pat2' <- expandPatternWithClassEnv classEnv' pat2
        return $ TIAndPat pat1' pat2'
      
      TIOrPat pat1 pat2 -> do
        pat1' <- expandPatternWithClassEnv classEnv' pat1
        pat2' <- expandPatternWithClassEnv classEnv' pat2
        return $ TIOrPat pat1' pat2'
      
      TIForallPat pat1 pat2 -> do
        pat1' <- expandPatternWithClassEnv classEnv' pat1
        pat2' <- expandPatternWithClassEnv classEnv' pat2
        return $ TIForallPat pat1' pat2'
      
      TINotPat pat -> do
        pat' <- expandPatternWithClassEnv classEnv' pat
        return $ TINotPat pat'
      
      TITuplePat pats -> do
        pats' <- mapM (expandPatternWithClassEnv classEnv') pats
        return $ TITuplePat pats'
      
      TIInductivePat name pats -> do
        pats' <- mapM (expandPatternWithClassEnv classEnv') pats
        return $ TIInductivePat name pats'
      
      TIIndexedPat pat exprs -> do
        pat' <- expandPatternWithClassEnv classEnv' pat
        exprs' <- mapM expandTypeClassMethodsT exprs
        return $ TIIndexedPat pat' exprs'
      
      TILetPat bindings pat -> do
        pat' <- expandPatternWithClassEnv classEnv' pat
        bindings' <- mapM (\(pd, e) -> do
          e' <- expandTypeClassMethodsT e
          return (pd, e')) bindings
        return $ TILetPat bindings' pat'
      
      TIPApplyPat funcExpr argPats -> do
        funcExpr' <- expandTypeClassMethodsT funcExpr
        argPats' <- mapM (expandPatternWithClassEnv classEnv') argPats
        return $ TIPApplyPat funcExpr' argPats'
      
      TIDApplyPat pat pats -> do
        pat' <- expandPatternWithClassEnv classEnv' pat
        pats' <- mapM (expandPatternWithClassEnv classEnv') pats
        return $ TIDApplyPat pat' pats'
      
      TISeqConsPat pat1 pat2 -> do
        pat1' <- expandPatternWithClassEnv classEnv' pat1
        pat2' <- expandPatternWithClassEnv classEnv' pat2
        return $ TISeqConsPat pat1' pat2'
      
      TIInductiveOrPApplyPat name pats -> do
        pats' <- mapM (expandPatternWithClassEnv classEnv') pats
        return $ TIInductiveOrPApplyPat name pats'
      
      TIValuePat expr -> do
        expr' <- expandTypeClassMethodsT expr
        expr'' <- applyConcreteConstraintDictionaries expr'
        return $ TIValuePat expr''
      
      TIPredPat pred -> do
        pred' <- expandTypeClassMethodsT pred
        pred'' <- applyConcreteConstraintDictionaries pred'
        return $ TIPredPat pred''
      
      -- Leaf patterns
      TISeqNilPat -> return TISeqNilPat
      TIVarPat name -> return $ TIVarPat name
      TIWildCard -> return TIWildCard
      TIPatVar name -> return $ TIPatVar name
      TIContPat -> return TIContPat
      TILaterPatVar -> return TILaterPatVar
    
    expandLoopRange :: ClassEnv -> TILoopRange -> EvalM TILoopRange
    expandLoopRange classEnv' (TILoopRange start end rangePat) = do
      start' <- expandTypeClassMethodsT start
      end' <- expandTypeClassMethodsT end
      rangePat' <- expandPatternWithClassEnv classEnv' rangePat
      return $ TILoopRange start' end' rangePat'

-- | Apply dictionaries to expressions with concrete constraints in patterns
-- This is used to apply dictionaries to value patterns like #(n + 1)
applyConcreteConstraintDictionariesInPattern :: TIPattern -> EvalM TIPattern
applyConcreteConstraintDictionariesInPattern (TIPattern scheme node) = do
  node' <- applyDictInPatternNode node
  return $ TIPattern scheme node'
  where
    applyDictInPatternNode :: TIPatternNode -> EvalM TIPatternNode
    applyDictInPatternNode pnode = case pnode of
      TIValuePat expr -> do
        expr' <- applyConcreteConstraintDictionaries expr
        return $ TIValuePat expr'
      
      TIPredPat expr -> do
        expr' <- applyConcreteConstraintDictionaries expr
        return $ TIPredPat expr'
      
      TIIndexedPat pat exprs -> do
        pat' <- applyConcreteConstraintDictionariesInPattern pat
        exprs' <- mapM applyConcreteConstraintDictionaries exprs
        return $ TIIndexedPat pat' exprs'
      
      TILetPat bindings pat -> do
        pat' <- applyConcreteConstraintDictionariesInPattern pat
        bindings' <- mapM (\(pd, e) -> do
          e' <- applyConcreteConstraintDictionaries e
          return (pd, e')) bindings
        return $ TILetPat bindings' pat'
      
      TILoopPat var loopRange pat1 pat2 -> do
        loopRange' <- applyDictInLoopRange loopRange
        pat1' <- applyConcreteConstraintDictionariesInPattern pat1
        pat2' <- applyConcreteConstraintDictionariesInPattern pat2
        return $ TILoopPat var loopRange' pat1' pat2'
      
      TIAndPat pat1 pat2 -> do
        pat1' <- applyConcreteConstraintDictionariesInPattern pat1
        pat2' <- applyConcreteConstraintDictionariesInPattern pat2
        return $ TIAndPat pat1' pat2'
      
      TIOrPat pat1 pat2 -> do
        pat1' <- applyConcreteConstraintDictionariesInPattern pat1
        pat2' <- applyConcreteConstraintDictionariesInPattern pat2
        return $ TIOrPat pat1' pat2'
      
      TIForallPat pat1 pat2 -> do
        pat1' <- applyConcreteConstraintDictionariesInPattern pat1
        pat2' <- applyConcreteConstraintDictionariesInPattern pat2
        return $ TIForallPat pat1' pat2'
      
      TINotPat pat -> do
        pat' <- applyConcreteConstraintDictionariesInPattern pat
        return $ TINotPat pat'
      
      TITuplePat pats -> do
        pats' <- mapM applyConcreteConstraintDictionariesInPattern pats
        return $ TITuplePat pats'
      
      TIInductivePat name pats -> do
        pats' <- mapM applyConcreteConstraintDictionariesInPattern pats
        return $ TIInductivePat name pats'
      
      TIPApplyPat funcExpr argPats -> do
        funcExpr' <- applyConcreteConstraintDictionaries funcExpr
        argPats' <- mapM applyConcreteConstraintDictionariesInPattern argPats
        return $ TIPApplyPat funcExpr' argPats'
      
      TIDApplyPat pat pats -> do
        pat' <- applyConcreteConstraintDictionariesInPattern pat
        pats' <- mapM applyConcreteConstraintDictionariesInPattern pats
        return $ TIDApplyPat pat' pats'
      
      TISeqConsPat pat1 pat2 -> do
        pat1' <- applyConcreteConstraintDictionariesInPattern pat1
        pat2' <- applyConcreteConstraintDictionariesInPattern pat2
        return $ TISeqConsPat pat1' pat2'
      
      TIInductiveOrPApplyPat name pats -> do
        pats' <- mapM applyConcreteConstraintDictionariesInPattern pats
        return $ TIInductiveOrPApplyPat name pats'
      
      -- Leaf patterns
      TISeqNilPat -> return TISeqNilPat
      TIVarPat name -> return $ TIVarPat name
      TIWildCard -> return TIWildCard
      TIPatVar name -> return $ TIPatVar name
      TIContPat -> return TIContPat
      TILaterPatVar -> return TILaterPatVar
    
    applyDictInLoopRange :: TILoopRange -> EvalM TILoopRange
    applyDictInLoopRange (TILoopRange start end rangePat) = do
      start' <- applyConcreteConstraintDictionaries start
      end' <- applyConcreteConstraintDictionaries end
      rangePat' <- applyConcreteConstraintDictionariesInPattern rangePat
      return $ TILoopRange start' end' rangePat'

-- ============================================================================
-- Unbound dictionary reference repair (post-pass)
-- ============================================================================

-- | Rewrite dictionary accesses whose dictionary PARAMETER is not lambda-bound
-- into 'TIRuntimeDispatch'.
--
-- The expansion above rewrites a class-method use whose constraint is still a
-- type variable into an access on the dictionary parameter @dict_<Class>@,
-- assuming the enclosing definition's scheme carries the constraint so that
-- 'addDictionaryParametersT' binds that parameter.  When constraint
-- information was lost (e.g. a definition whose signature is missing a
-- {Class a} it actually needs, or inference corners that drop node
-- substitutions), the reference stays UNBOUND: at runtime the variable
-- silently evaluates to a symbol, the string index (the sanitized method
-- name, e.g. "ge" for >=) ends up inside CAS data, and evaluation fails far
-- away with @Expected CASData, but found: "ge"@.
--
-- This pass runs AFTER 'addDictionaryParametersT' (so legitimate dictionary
-- parameters are visible as lambda binders) and rewrites any remaining
-- access through an unbound @dict_*@ root into a runtime-type dispatch on
-- the method's owner class — the same mechanism used for MathValue-like
-- dispatch — which resolves the instance from the first argument's runtime
-- type.  Accesses with no arguments (0-arity methods like @zero@) cannot be
-- dispatched at runtime and are left unchanged.
fixUnboundDictRefs :: ClassEnv -> TIExpr -> TIExpr
fixUnboundDictRefs classEnv = goE Set.empty
  where
    goE :: Set.Set String -> TIExpr -> TIExpr
    goE scope (TIExpr sch node) = TIExpr sch (goN scope node)

    goN :: Set.Set String -> TIExprNode -> TIExprNode
    goN scope node = case node of
      -- Lambda binders may introduce dictionary parameters (from
      -- addDictionaryParametersT or instance-dictionary functions).
      TILambdaExpr mVar params body ->
        let scope' = foldr Set.insert scope
                       [ n | Var n _ <- params, "dict_" `isPrefixOf` n ]
        in TILambdaExpr mVar params (goE scope' body)
      TIMemoizedLambdaExpr params body ->
        let scope' = foldr Set.insert scope
                       [ n | n <- params, "dict_" `isPrefixOf` n ]
        in TIMemoizedLambdaExpr params (goE scope' body)

      -- A method application through an unbound dictionary parameter:
      -- (dict_C[__super_X]...["m"]) args  ==>  runtime dispatch on the owner.
      TIApplyExpr fn args
        | Just (root, owner, methodKey) <- splitDictAccess fn
        , not (root `Set.member` scope)
        , candidates <- runtimeDispatchCandidates (lookupInstances owner classEnv)
        , not (null candidates)
        -> TIRuntimeDispatch owner methodKey candidates (map (goE scope) args)

      -- An unbound dictionary parameter used as a VALUE — typically passed
      -- as a dictionary ARGUMENT to a constrained function, e.g.
      -- `(sort dict_Ord) xs` inside a definition whose signature lacks
      -- {Ord a}.  Synthesize a dictionary whose every method dispatches on
      -- its first argument's runtime type, so the callee's dictionary
      -- accesses keep working.  (0-arity methods cannot be dispatched at
      -- runtime and are omitted; superclass entries are synthesized
      -- recursively.)
      TIVarExpr d
        | "dict_" `isPrefixOf` d
        , not (d `Set.member` scope)
        , let cls = drop (length ("dict_" :: String)) d
        , Just _ <- lookupClass cls classEnv
        -> tiExprNode (dispatchDictFor 3 cls)

      -- Patterns embed expressions (value patterns, predicate patterns,
      -- pattern-function applications, loop ranges); mapTIExprChildren does
      -- not descend into them, so handle the pattern-carrying nodes here.
      TIMatchExpr mode tgt mat clauses ->
        TIMatchExpr mode (goE scope tgt) (goE scope mat)
                    [ (goP scope p, goE scope b) | (p, b) <- clauses ]
      TIMatchAllExpr mode tgt mat clauses ->
        TIMatchAllExpr mode (goE scope tgt) (goE scope mat)
                       [ (goP scope p, goE scope b) | (p, b) <- clauses ]

      _ -> mapTIExprChildren (goE scope) node

    goP :: Set.Set String -> TIPattern -> TIPattern
    goP scope (TIPattern sch pnode) = TIPattern sch (goPN scope pnode)

    goPN :: Set.Set String -> TIPatternNode -> TIPatternNode
    goPN scope pnode = case pnode of
      TIValuePat e             -> TIValuePat (goE scope e)
      TIPredPat e              -> TIPredPat (goE scope e)
      TIIndexedPat p es        -> TIIndexedPat (goP scope p) (map (goE scope) es)
      TILetPat bs p            -> TILetPat [ (dp, goE scope e) | (dp, e) <- bs ] (goP scope p)
      TINotPat p               -> TINotPat (goP scope p)
      TIAndPat p1 p2           -> TIAndPat (goP scope p1) (goP scope p2)
      TIOrPat p1 p2            -> TIOrPat (goP scope p1) (goP scope p2)
      TIForallPat p1 p2        -> TIForallPat (goP scope p1) (goP scope p2)
      TITuplePat ps            -> TITuplePat (map (goP scope) ps)
      TIInductivePat n ps      -> TIInductivePat n (map (goP scope) ps)
      TILoopPat v (TILoopRange s e rp) p1 p2 ->
        TILoopPat v (TILoopRange (goE scope s) (goE scope e) (goP scope rp))
                  (goP scope p1) (goP scope p2)
      TIPApplyPat e ps         -> TIPApplyPat (goE scope e) (map (goP scope) ps)
      TIInductiveOrPApplyPat n ps -> TIInductiveOrPApplyPat n (map (goP scope) ps)
      TISeqConsPat p1 p2       -> TISeqConsPat (goP scope p1) (goP scope p2)
      TIDApplyPat p ps         -> TIDApplyPat (goP scope p) (map (goP scope) ps)
      TIWildCard               -> pnode
      TIPatVar _               -> pnode
      TIVarPat _               -> pnode
      TIContPat                -> pnode
      TISeqNilPat              -> pnode
      TILaterPatVar            -> pnode

    -- Recognize a dictionary access chain rooted at a dict_* variable:
    --   dict_C ["m"]                       -> (dict_C, C, m)
    --   dict_C ["__super_X"]... ["m"]      -> (dict_C, X-of-last-hop, m)
    splitDictAccess :: TIExpr -> Maybe (String, String, String)
    splitDictAccess (TIExpr _ (TIIndexedExpr _ base [Sub keyExpr])) = do
      key <- stringKeyOf keyExpr
      if "__super_" `isPrefixOf` key
        then Nothing  -- a bare superclass hop is not a method access
        else do
          (root, hops) <- dictRootOf base
          ownerFromChain root hops key
    splitDictAccess _ = Nothing

    ownerFromChain :: String -> [String] -> String -> Maybe (String, String, String)
    ownerFromChain root hops key =
      let owner = case hops of
                    [] -> drop (length ("dict_" :: String)) root
                    _  -> drop (length ("__super_" :: String)) (last hops)
      in if null owner then Nothing else Just (root, owner, key)

    -- Walk down nested __super_ accesses to the dict_* root.
    -- Returns (root variable name, super hops in outermost-last order).
    dictRootOf :: TIExpr -> Maybe (String, [String])
    dictRootOf (TIExpr _ (TIVarExpr n))
      | "dict_" `isPrefixOf` n = Just (n, [])
    dictRootOf (TIExpr _ (TIIndexedExpr _ base [Sub keyExpr])) = do
      key <- stringKeyOf keyExpr
      if "__super_" `isPrefixOf` key
        then do (root, hops) <- dictRootOf base
                return (root, hops ++ [key])
        else Nothing
    dictRootOf _ = Nothing

    stringKeyOf :: TIExpr -> Maybe String
    stringKeyOf (TIExpr _ (TIConstantExpr (StringExpr t))) = Just (unpack t)
    stringKeyOf _ = Nothing

    -- A dictionary value for class `cls` whose methods are runtime
    -- dispatchers.  Used as the stand-in for an unbound dict_<cls>.
    dispatchDictFor :: Int -> String -> TIExpr
    dispatchDictFor depth cls =
      let (methods, supers) = case lookupClass cls classEnv of
            Just ci -> (classMethods ci, classSupers ci)
            Nothing -> ([], [])
          candidates = runtimeDispatchCandidates (lookupInstances cls classEnv)
          anyScheme = Forall [] [] TAny
          strScheme = Forall [] [] TString
          strKey k = TIExpr strScheme (TIConstantExpr (StringExpr (pack k)))
          mkMethod (mname, mty) =
            let key = sanitizeMethodName mname
                arity = getMethodArity mty
                params = ["dispatchArg" ++ show i | i <- [1 .. arity]]
                argEs = [TIExpr anyScheme (TIVarExpr p) | p <- params]
                body = TIExpr anyScheme (TIRuntimeDispatch cls key candidates argEs)
            in if arity == 0 || null candidates
                 then Nothing
                 else Just (strKey key,
                            TIExpr anyScheme (TILambdaExpr Nothing (map stringToVar params) body))
          superEntries
            | depth <= 0 = []
            | otherwise =
                [ (strKey ("__super_" ++ s), dispatchDictFor (depth - 1) s)
                | s <- supers ]
      in TIExpr (Forall [] [] (THash TString TAny))
                (TIHashExpr (mapMaybe mkMethod methods ++ superEntries))