{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}

-- | Shared type-checking support for term patterns.
module Aihc.Tc.Generate.Pattern
  ( PatternCheck (..),
    annotatePatternBindings,
    checkPattern,
    checkPatterns,
    checkPatternsWithGivens,
    checkedPattern,
    withPatternBindings,
  )
where

import Aihc.Parser.Syntax
  ( Literal (..),
    Name (..),
    NumericType (..),
    Pattern (..),
    RecordField (..),
    SourceSpan (..),
    TupleFlavor (..),
    UnqualifiedName (..),
    fromAnnotation,
    mkAnnotation,
    nameText,
    peelLiteralAnn,
    peelPatternAnn,
  )
import Aihc.Resolve (ResolutionAnnotation (..), ResolutionNamespace (..))
import Aihc.Tc.Annotations (PendingTcAnnotation, pendingAnnotation)
import Aihc.Tc.Constraint
import Aihc.Tc.Env (TyConInfo (..))
import Aihc.Tc.Error (TcErrorKind (..))
import Aihc.Tc.Evidence (EvTerm (..))
import Aihc.Tc.Instantiate (Instantiation (..), applySubst, instantiateWithArgs)
import Aihc.Tc.Monad
import Aihc.Tc.Types
import Data.Either (fromRight)
import Data.Map.Strict qualified as Map
import Data.Maybe (mapMaybe)
import Data.Set qualified as Set
import Data.Text (Text)
import Data.Text qualified as T

data PatternCheck = PatternCheck
  { pcBindings :: ![(UnqualifiedName, TcType)],
    pcWantedCts :: ![Ct],
    pcGivenCts :: ![Ct],
    pcSkolems :: ![TyVarId],
    pcPatterns :: ![Pattern]
  }
  deriving (Show)

instance Semigroup PatternCheck where
  left <> right =
    PatternCheck
      { pcBindings = pcBindings left <> pcBindings right,
        pcWantedCts = pcWantedCts left <> pcWantedCts right,
        pcGivenCts = pcGivenCts left <> pcGivenCts right,
        pcSkolems = pcSkolems left <> pcSkolems right,
        pcPatterns = pcPatterns left <> pcPatterns right
      }

instance Monoid PatternCheck where
  mempty = PatternCheck [] [] [] [] []

data GadtHandling
  = GadtAsWanted
  | GadtAsGiven
  deriving (Eq)

checkPatterns :: SourceSpan -> [(Pattern, TcType)] -> TcM PatternCheck
checkPatterns = checkPatternsWith GadtAsWanted

checkPatternsWithGivens :: SourceSpan -> [(Pattern, TcType)] -> TcM PatternCheck
checkPatternsWithGivens = checkPatternsWith GadtAsGiven

checkPatternsWith :: GadtHandling -> SourceSpan -> [(Pattern, TcType)] -> TcM PatternCheck
checkPatternsWith gadtHandling sp = fmap mconcat . mapM (uncurry (checkPatternWith gadtHandling sp))

checkPattern :: SourceSpan -> Pattern -> TcType -> TcM PatternCheck
checkPattern = checkPatternWith GadtAsWanted

checkPatternWith :: GadtHandling -> SourceSpan -> Pattern -> TcType -> TcM PatternCheck
checkPatternWith gadtHandling sp pat scrutTy =
  case overloadedIntegerPatternLiteral pat of
    Just isNegative -> checkOverloadedIntegerPattern sp pat isNegative scrutTy
    Nothing -> checkPatternCore gadtHandling sp pat scrutTy

checkPatternCore :: GadtHandling -> SourceSpan -> Pattern -> TcType -> TcM PatternCheck
checkPatternCore gadtHandling sp pat scrutTy =
  case pat of
    PVar name ->
      pure (checkedOnly pat) {pcBindings = [(name, scrutTy)]}
    PAnn ann inner -> do
      innerCheck <- checkPatternWith gadtHandling sp inner scrutTy
      pure innerCheck {pcPatterns = [PAnn ann (checkedPattern innerCheck)]}
    PParen inner -> do
      innerCheck <- checkPatternWith gadtHandling sp inner scrutTy
      pure innerCheck {pcPatterns = [PParen (checkedPattern innerCheck)]}
    PWildcard {} -> pure (checkedOnly pat)
    PLit lit -> do
      maybeLiteralTy <- charLiteralPatternType lit
      case maybeLiteralTy of
        Just literalTy -> do
          eqCt <- wantedEq sp scrutTy literalTy
          pure (checkedOnly (PLit (checkedLiteral scrutTy lit))) {pcWantedCts = [eqCt]}
        Nothing -> pure (checkedOnly (PLit (checkedLiteral scrutTy lit)))
    PNegLit {} -> pure (checkedOnly pat)
    PAs name inner -> do
      innerCheck <- checkPatternWith gadtHandling sp inner scrutTy
      pure innerCheck {pcBindings = (name, scrutTy) : pcBindings innerCheck, pcPatterns = [PAs name (checkedPattern innerCheck)]}
    PStrict inner -> do
      innerCheck <- checkPatternWith gadtHandling sp inner scrutTy
      pure innerCheck {pcPatterns = [PStrict (checkedPattern innerCheck)]}
    PIrrefutable inner -> do
      innerCheck <- checkPatternWith gadtHandling sp inner scrutTy
      pure innerCheck {pcPatterns = [PIrrefutable (checkedPattern innerCheck)]}
    PCon name _typeArgs subPats ->
      checkConPattern gadtHandling sp pat name subPats scrutTy
    PInfix lhs op rhs ->
      checkConPattern gadtHandling sp pat op [lhs, rhs] scrutTy
    PList items -> checkListPattern gadtHandling sp items scrutTy
    PTuple flavor items -> do
      elemTys <- mapM (const freshMetaTv) items
      let arity = length items
          typeName = tupleTyConText flavor arity
      maybeTyCon <- lookupTyCon typeName
      let fallbackKind =
            case flavor of
              Boxed -> foldr (KFun . typeKind) KType elemTys
              Unboxed -> foldr (KFun . typeKind) (KTYPE (TupleRep (map (fromRight liftedRuntimeRep . runtimeRepOfType) elemTys))) elemTys
      tupleTyCon <-
        case maybeTyCon of
          Just info -> pure (tciTyCon info)
          Nothing -> mkKnownTyCon (tupleTyConModule flavor) typeName arity fallbackKind
      let tupleTy = TcTyCon tupleTyCon elemTys
      eqCt <- wantedEq sp scrutTy tupleTy
      itemChecks <- checkPatternsWith gadtHandling sp (zip items elemTys)
      pure itemChecks {pcWantedCts = eqCt : pcWantedCts itemChecks, pcPatterns = [PTuple flavor (pcPatterns itemChecks)]}
    _ -> pure (checkedOnly pat)

checkedOnly :: Pattern -> PatternCheck
checkedOnly pat = mempty {pcPatterns = [pat]}

checkedLiteral :: TcType -> Literal -> Literal
checkedLiteral ty = LitAnn (mkAnnotation (pendingAnnotation ty [] [] []))

checkListPattern :: GadtHandling -> SourceSpan -> [Pattern] -> TcType -> TcM PatternCheck
checkListPattern gadtHandling sp items scrutTy =
  case items of
    [] -> do
      scheme <- listConstructorScheme "[]"
      (nilTy, _typeArgs, predicates, skolems) <- instantiateConstructorPattern scheme
      scrutCts <- constructorScrutineeCt gadtHandling sp "[]" scrutTy nilTy
      predicateGivens <- mapM (constructorGiven sp "[]") predicates
      pure
        mempty
          { pcWantedCts = fst scrutCts,
            pcGivenCts = predicateGivens <> snd scrutCts,
            pcSkolems = skolems,
            pcPatterns = [PList []]
          }
    item : rest -> do
      scheme <- listConstructorScheme ":"
      (consTy, _typeArgs, predicates, skolems) <- instantiateConstructorPattern scheme
      (argumentTypes, resultTy) <- splitConTy 2 consTy
      case argumentTypes of
        [itemTy, tailTy] -> do
          scrutCts <- constructorScrutineeCt gadtHandling sp ":" scrutTy resultTy
          itemCheck <- checkPatternWith gadtHandling sp item itemTy
          tailCheck <- checkListPattern gadtHandling sp rest tailTy
          predicateGivens <- mapM (constructorGiven sp ":") predicates
          let nestedCheck = itemCheck <> tailCheck
              checkedTailItems = case checkedPattern tailCheck of
                PAnn _ (PList patterns) -> patterns
                PList patterns -> patterns
                _ -> rest
              checkedItems = checkedPattern itemCheck : checkedTailItems
          pure
            nestedCheck
              { pcWantedCts = fst scrutCts <> pcWantedCts nestedCheck,
                pcGivenCts = predicateGivens <> snd scrutCts <> pcGivenCts nestedCheck,
                pcSkolems = skolems <> pcSkolems nestedCheck,
                pcPatterns = [PList checkedItems]
              }
        _ -> abortTc "GHC.Types list cons constructor has an invalid arity"

listConstructorScheme :: Text -> TcM TypeScheme
listConstructorScheme name = do
  sourceBinder <- lookupTerm name
  maybeBinder <- maybe (lookupKnownTerm "GHC.Types" name) (pure . Just) sourceBinder
  case maybeBinder of
    Just (TcIdBinder scheme _) -> pure scheme
    Just TcMonoIdBinder {} -> abortTc ("GHC.Types list constructor is monomorphic: " <> T.unpack name)
    Nothing -> abortTc ("GHC.Types list constructor is missing: " <> T.unpack name)

checkedPattern :: PatternCheck -> Pattern
checkedPattern check =
  case pcPatterns check of
    [pat] -> pat
    _ -> error "checkedPattern: expected exactly one checked pattern"

charLiteralPatternType :: Literal -> TcM (Maybe TcType)
charLiteralPatternType literal =
  case peelLiteralAnn literal of
    LitChar {} -> do
      maybeInfo <- lookupTyCon "Char"
      pure (Just (TcTyCon (maybe (mkTyCon "Char" 0 liftedTypeKind) tciTyCon maybeInfo) []))
    LitCharHash {} -> do
      tyCon <- mkKnownTyCon "GHC.Prim" "Char#" 0 liftedTypeKind
      pure (Just (TcTyCon tyCon []))
    _ -> pure Nothing

overloadedIntegerPatternLiteral :: Pattern -> Maybe Bool
overloadedIntegerPatternLiteral pat =
  case peelPatternAnn pat of
    PLit lit
      | isOverloadedIntegerLiteral lit -> Just False
    PNegLit lit
      | isOverloadedIntegerLiteral lit -> Just True
    _ -> Nothing

isOverloadedIntegerLiteral :: Literal -> Bool
isOverloadedIntegerLiteral lit =
  case peelLiteralAnn lit of
    LitInt _ TInteger _ -> True
    _ -> False

checkOverloadedIntegerPattern :: SourceSpan -> Pattern -> Bool -> TcType -> TcM PatternCheck
checkOverloadedIntegerPattern sp pat isNegative scrutTy = do
  (fromIntegerPending, fromIntegerCts) <-
    checkPatternMethodWithExpected sp pat "fromInteger" $ \case
      TcFunTy integerTy _ -> pure (scrutTy, TcFunTy integerTy scrutTy)
      _ -> abortTc "fromInteger does not have a function type"
  negateCheck <-
    if isNegative
      then Just <$> checkPatternMethod sp pat "negate" scrutTy (TcFunTy scrutTy scrutTy)
      else pure Nothing
  (eqPending, eqCts) <-
    checkPatternMethodWithExpected sp pat "==" $ \case
      TcFunTy _ (TcFunTy _ boolTy) ->
        let expectedTy = TcFunTy scrutTy (TcFunTy scrutTy boolTy)
         in pure (expectedTy, expectedTy)
      _ -> abortTc "== does not have a binary function type"
  let methodAnnotations =
        [("fromInteger", fromIntegerPending)]
          <> maybe [] (\(pending, _) -> [("negate", pending)]) negateCheck
          <> [("==", eqPending)]
      pat' = foldr (uncurry attachPendingPatternAnnotation) pat methodAnnotations
      negateCts = maybe [] snd negateCheck
  pure
    PatternCheck
      { pcBindings = [],
        pcWantedCts = fromIntegerCts <> negateCts <> eqCts,
        pcGivenCts = [],
        pcSkolems = [],
        pcPatterns = [pat']
      }

checkPatternMethod :: SourceSpan -> Pattern -> Text -> TcType -> TcType -> TcM (PendingTcAnnotation, [Ct])
checkPatternMethod sp pat name annotationTy expectedTy =
  checkPatternMethodWithExpected sp pat name (const (pure (annotationTy, expectedTy)))

checkPatternMethodWithExpected :: SourceSpan -> Pattern -> Text -> (TcType -> TcM (TcType, TcType)) -> TcM (PendingTcAnnotation, [Ct])
checkPatternMethodWithExpected sp pat name expectedTypes = do
  resolution <- requiredPatternResolution name pat
  (actualTy, typeArgs, methodCts) <- inferResolvedPatternMethod sp name resolution
  (annotationTy, expectedTy) <- expectedTypes actualTy
  methodEq <- wantedMethodEq sp name actualTy expectedTy
  pure
    ( pendingAnnotation
        annotationTy
        typeArgs
        (map ctEvVar methodCts)
        [],
      methodCts <> [methodEq]
    )

wantedMethodEq :: SourceSpan -> Text -> TcType -> TcType -> TcM Ct
wantedMethodEq sp method actual expected = do
  ev <- freshEvVar
  pure $
    mkWantedEqCt
      TypeTrace
        { typeTraceType = actual,
          typeTraceRole = ActualType,
          typeTraceOrigin = ConstraintTypeOrigin (OccurrenceOf method)
        }
      TypeTrace
        { typeTraceType = expected,
          typeTraceRole = ExpectedType,
          typeTraceOrigin = ConstraintTypeOrigin (LitOrigin sp)
        }
      ev
      (LitOrigin sp)
      sp

inferResolvedPatternMethod :: SourceSpan -> Text -> ResolutionAnnotation -> TcM (TcType, [TcType], [Ct])
inferResolvedPatternMethod sp displayName resolution = do
  mBinder <- lookupResolvedTerm displayName (resolutionTarget resolution)
  case mBinder of
    Just (TcIdBinder scheme _) -> do
      inst <- instantiateWithArgs scheme
      cts <- mapM (predToCt sp displayName) (instPreds inst)
      pure (instType inst, instTypeArgs inst, cts)
    Just (TcMonoIdBinder ty) ->
      pure (ty, [], [])
    Nothing ->
      abortTc ("resolved " <> T.unpack displayName <> " missing from type environment: " <> show (resolutionTarget resolution))

predToCt :: SourceSpan -> Text -> Pred -> TcM Ct
predToCt sp name pred' = do
  ev <- freshEvVar
  pure (mkWantedCt pred' ev (OccurrenceOf name) sp)

requiredPatternResolution :: Text -> Pattern -> TcM ResolutionAnnotation
requiredPatternResolution name pat =
  case [resolution | resolution <- patternResolutions pat, resolutionName resolution == name, resolutionNamespace resolution == ResolutionNamespaceTerm] of
    resolution : _ -> pure resolution
    [] -> do
      emitError NoSourceSpan (OtherError ("missing resolver annotation for overloaded pattern method " <> T.unpack name))
      abortTc ("missing resolver annotation for overloaded pattern method " <> T.unpack name)

patternResolutions :: Pattern -> [ResolutionAnnotation]
patternResolutions pat =
  case pat of
    PAnn ann inner -> mapMaybe fromAnnotation [ann] <> patternResolutions inner
    PParen inner -> patternResolutions inner
    PStrict inner -> patternResolutions inner
    PIrrefutable inner -> patternResolutions inner
    PAs _ inner -> patternResolutions inner
    PTypeSig inner _ -> patternResolutions inner
    _ -> []

attachPendingPatternAnnotation :: Text -> PendingTcAnnotation -> Pattern -> Pattern
attachPendingPatternAnnotation target pending pat =
  case pat of
    PAnn ann inner ->
      case fromAnnotation ann of
        Just resolution
          | resolutionName resolution == target,
            resolutionNamespace resolution == ResolutionNamespaceTerm ->
              PAnn (mkAnnotation pending) (PAnn ann inner)
        _ -> PAnn ann (attachPendingPatternAnnotation target pending inner)
    PParen inner -> PParen (attachPendingPatternAnnotation target pending inner)
    PStrict inner -> PStrict (attachPendingPatternAnnotation target pending inner)
    PIrrefutable inner -> PIrrefutable (attachPendingPatternAnnotation target pending inner)
    PAs name inner -> PAs name (attachPendingPatternAnnotation target pending inner)
    PTypeSig inner ty -> PTypeSig (attachPendingPatternAnnotation target pending inner) ty
    _ -> pat

annotatePatternBindings :: [(UnqualifiedName, TcType)] -> Pattern -> Pattern
annotatePatternBindings bindings =
  go
  where
    go pat =
      case pat of
        PAnn ann inner -> PAnn ann (go inner)
        PVar name -> PVar (annotateBinderName bindings name)
        PParen inner -> PParen (go inner)
        PAs name inner -> PAs (annotateBinderName bindings name) (go inner)
        PStrict inner -> PStrict (go inner)
        PIrrefutable inner -> PIrrefutable (go inner)
        PList items -> PList (map go items)
        PTuple flavor items -> PTuple flavor (map go items)
        PUnboxedSum alt arity inner -> PUnboxedSum alt arity (go inner)
        PInfix lhs op rhs -> PInfix (go lhs) op (go rhs)
        PView expr inner -> PView expr (go inner)
        PCon name typeArgs subPats -> PCon name typeArgs (map go subPats)
        PRecord name fields wildcard -> PRecord name (map annotateRecordField fields) wildcard
        PTypeSig inner type' -> PTypeSig (go inner) type'
        PSplice expr -> PSplice expr
        _ -> pat

    annotateRecordField :: RecordField Pattern -> RecordField Pattern
    annotateRecordField field =
      field {recordFieldValue = go (recordFieldValue field)}

annotateBinderName :: [(UnqualifiedName, TcType)] -> UnqualifiedName -> UnqualifiedName
annotateBinderName bindings name =
  case lookup name bindings of
    Nothing -> name
    Just ty -> name {unqualifiedNameAnns = unqualifiedNameAnns name <> [mkAnnotation (pendingAnnotation ty [] [] [])]}

checkConPattern :: GadtHandling -> SourceSpan -> Pattern -> Name -> [Pattern] -> TcType -> TcM PatternCheck
checkConPattern gadtHandling sp originalPat conSyntax subPats scrutTy = do
  let conName = patternNameText conSyntax
  target <- resolvedTermTarget conSyntax
  mBinder <- lookupResolvedTerm conName target
  case mBinder of
    Just (TcIdBinder scheme _) -> do
      (conTy, typeArgs, predicates, skolems) <- instantiateConstructorPattern scheme
      (argTys, conResTy) <- splitConTy (length subPats) conTy
      scrutCt <- constructorScrutineeCt gadtHandling sp conName scrutTy conResTy
      subCheck <- checkPatternsWith gadtHandling sp (zip subPats argTys)
      predicateGivens <- mapM (constructorGiven sp conName) predicates
      let rebuiltPattern = replaceConstructorSubpatterns originalPat (pcPatterns subCheck)
          annotatedPattern
            | null predicateGivens && null skolems = rebuiltPattern
            | otherwise =
                PAnn
                  (mkAnnotation (pendingAnnotation conTy typeArgs (map ctEvVar predicateGivens) []))
                  rebuiltPattern
      pure
        subCheck
          { pcWantedCts = fst scrutCt <> pcWantedCts subCheck,
            pcGivenCts = predicateGivens <> snd scrutCt <> pcGivenCts subCheck,
            pcSkolems = skolems <> pcSkolems subCheck,
            pcPatterns = [annotatedPattern]
          }
    Just other ->
      abortTc ("resolved constructor is not an identifier binder: " <> show conName <> " resolved as " <> show target <> " with binder " <> show other)
    Nothing ->
      abortTc ("resolved constructor missing from type environment: " <> show conName <> " resolved as " <> show target)

constructorGiven :: SourceSpan -> Text -> Pred -> TcM Ct
constructorGiven sp constructorName predicate = do
  evidence <- freshEvVar
  bindEvidence evidence (EvGiven predicate)
  let origin = OccurrenceOf constructorName
  pure
    Ct
      { ctPred = predicate,
        ctFlavor = Given,
        ctEvVar = evidence,
        ctOrigin = origin,
        ctProvenance = FromCtOrigin origin,
        ctLoc = sp
      }

instantiateConstructorPattern :: TypeScheme -> TcM (TcType, [TcType], [Pred], [TyVarId])
instantiateConstructorPattern (ForAll tyVars predicates body) = do
  let resultTyVars = constructorResultTyVars body
      isUniversal tyVar = tvUnique tyVar `Set.member` resultTyVars
  substitutions <- mapM (instantiateTyVar isUniversal) tyVars
  let substitution = Map.fromList [(tvUnique tyVar, ty) | (tyVar, ty, _) <- substitutions]
      instantiateType = applySubst substitution
      typeArgs = map (instantiateType . TcTyVar) tyVars
      skolems = [skolem | (_, _, Just skolem) <- substitutions]
  pure
    ( instantiateType body,
      typeArgs,
      map (instantiatePred substitution) predicates,
      skolems
    )
  where
    instantiateTyVar isUniversal tyVar
      | isUniversal tyVar = do
          meta <- freshMetaTv
          pure (tyVar, meta, Nothing)
      | otherwise = do
          skolem <- setTyVarKind (tvKind tyVar) <$> freshSkolemTv (tvName tyVar)
          pure (tyVar, TcTyVar skolem, Just skolem)

constructorResultTyVars :: TcType -> Set.Set Unique
constructorResultTyVars = typeTyVars . dropConstructorArguments
  where
    dropConstructorArguments (TcFunTy _ result) = dropConstructorArguments result
    dropConstructorArguments result = result

typeTyVars :: TcType -> Set.Set Unique
typeTyVars ty =
  case ty of
    TcTyVar tyVar -> Set.singleton (tvUnique tyVar)
    TcMetaTv {} -> Set.empty
    TcTyCon _ arguments -> Set.unions (map typeTyVars arguments)
    TcFunTy argument result -> typeTyVars argument <> typeTyVars result
    TcForAllTy tyVar body -> Set.delete (tvUnique tyVar) (typeTyVars body)
    TcQualTy predicates body -> Set.unions (typeTyVars body : map predTyVars predicates)
    TcAppTy function argument -> typeTyVars function <> typeTyVars argument
    TcBuiltinTyCon _ _ arguments -> Set.unions (map typeTyVars arguments)

predTyVars :: Pred -> Set.Set Unique
predTyVars predicate =
  case predicate of
    ClassPred _ arguments -> Set.unions (map typeTyVars arguments)
    EqPred left right -> typeTyVars left <> typeTyVars right

instantiatePred :: Map.Map Unique TcType -> Pred -> Pred
instantiatePred substitution predicate =
  case predicate of
    ClassPred className arguments -> ClassPred className (map (applySubst substitution) arguments)
    EqPred left right -> EqPred (applySubst substitution left) (applySubst substitution right)

replaceConstructorSubpatterns :: Pattern -> [Pattern] -> Pattern
replaceConstructorSubpatterns pat subPats =
  case pat of
    PCon name typeArgs _ -> PCon name typeArgs subPats
    PInfix _ op _ ->
      case subPats of
        [lhs, rhs] -> PInfix lhs op rhs
        _ -> pat
    _ -> pat

constructorScrutineeCt :: GadtHandling -> SourceSpan -> Text -> TcType -> TcType -> TcM ([Ct], [Ct])
constructorScrutineeCt gadtHandling sp conName scrutTy conResTy = do
  ev <- freshEvVar
  gadtCon <- isGadtCon conName
  if gadtHandling == GadtAsGiven && gadtCon
    then
      pure
        ( [],
          [ Ct
              { ctPred = EqPred scrutTy conResTy,
                ctFlavor = Given,
                ctEvVar = ev,
                ctOrigin = AppOrigin sp,
                ctProvenance = FromCtOrigin (AppOrigin sp),
                ctLoc = sp
              }
          ]
        )
    else do
      let wantedCt = mkWantedCt (EqPred scrutTy conResTy) ev (AppOrigin sp) sp
      pure ([wantedCt], [])

splitConTy :: Int -> TcType -> TcM ([TcType], TcType)
splitConTy 0 ty = pure ([], ty)
splitConTy n (TcFunTy arg rest) = do
  (args, result) <- splitConTy (n - 1) rest
  pure (arg : args, result)
splitConTy n result = do
  missingArgs <- mapM (const freshMetaTv) [1 .. n]
  pure (missingArgs, result)

wantedEq :: SourceSpan -> TcType -> TcType -> TcM Ct
wantedEq sp left right = do
  ev <- freshEvVar
  pure (mkWantedCt (EqPred left right) ev (AppOrigin sp) sp)

withPatternBindings :: [(UnqualifiedName, TcType)] -> TcM a -> TcM a
withPatternBindings [] action = action
withPatternBindings ((name, ty) : rest) action =
  extendResolvedTermEnv name (TcMonoIdBinder ty) (withPatternBindings rest action)

tupleTyConText :: TupleFlavor -> Int -> Text
tupleTyConText flavor arity =
  case flavor of
    Boxed -> boxedTupleTyConName arity
    Unboxed -> unboxedTupleTyConName arity

tupleTyConModule :: TupleFlavor -> Text
tupleTyConModule flavor =
  case flavor of
    Boxed -> "GHC.Tuple"
    Unboxed -> "GHC.Types"

patternNameText :: Name -> Text
patternNameText name =
  case nameQualifier name of
    Nothing -> nameText name
    Just qualifier -> qualifier <> "." <> nameText name
