content: {- HLINT ignore "Unused LANGUAGE pragma" -} -- HLint doesn't recognize that TypeApplications is used in a pattern
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeAbstractions #-}
  module Language.PureScript.TypeChecker.Deriving (deriveInstance) where
  
  import Protolude hiding (Type)
  
  import Control.Lens (both, over)
  import Control.Monad.Error.Class (liftEither)
  import Control.Monad.Trans.Writer (Writer, WriterT, runWriter, runWriterT)
  import Control.Monad.Writer.Class (MonadWriter(..))
  import Data.Align (align, unalign)
  import Data.Foldable (foldl1, foldr1)
  import Data.List (init, last, zipWith3, (!!))
  import Data.Map qualified as M
  import Data.These (These(..), mergeTheseWith, these)
  
  import Control.Monad.Supply.Class (MonadSupply)
  import Language.PureScript.AST (Binder(..), CaseAlternative(..), ErrorMessageHint(..), Expr(..), InstanceDerivationStrategy(..), Literal(..), SourceSpan, nullSourceSpan)
  import Language.PureScript.AST.Utils (UnwrappedTypeConstructor(..), lam, lamCase, lamCase2, mkBinder, mkCtor, mkCtorBinder, mkLit, mkRef, mkVar, unguarded, unwrapTypeConstructor, utcQTyCon)
  import Language.PureScript.Constants.Libs qualified as Libs
  import Language.PureScript.Constants.Prim qualified as Prim
  import Language.PureScript.Crash (internalError)
  import Language.PureScript.Environment (DataDeclType(..), Environment(..), FunctionalDependency(..), TypeClassData(..), TypeKind(..), kindType, (-:>))
  import Language.PureScript.Errors (MultipleErrors, SimpleErrorMessage(..), addHint, errorMessage, internalCompilerError)
  import Language.PureScript.Label (Label(..))
  import Language.PureScript.Names (pattern ByNullSourcePos, Ident(..), ModuleName(..), Name(..), ProperName(..), ProperNameType(..), Qualified(..), QualifiedBy(..), coerceProperName, freshIdent, qualify)
  import Language.PureScript.PSString (PSString, mkString)
  import Language.PureScript.Sugar.TypeClasses (superClassDictionaryNames)
  import Language.PureScript.TypeChecker.Entailment (InstanceContext, findDicts)
  import Language.PureScript.TypeChecker.Monad (CheckState, getEnv, getTypeClassDictionaries, unsafeCheckCurrentModule)
  import Language.PureScript.TypeChecker.Synonyms (replaceAllTypeSynonyms)
  import Language.PureScript.TypeClassDictionaries (TypeClassDictionaryInScope(..))
  import Language.PureScript.Types (Constraint(..), pattern REmptyKinded, SourceType, Type(..), completeBinderList, eqType, everythingOnTypes, replaceAllTypeVars, srcTypeVar, usedTypeVariables)
  
  -- | Extract the name of the newtype appearing in the last type argument of
  -- a derived newtype instance.
  --
  -- Note: since newtypes in newtype instances can only be applied to type arguments
  -- (no flexible instances allowed), we don't need to bother with unification when
  -- looking for matching superclass instances, which saves us a lot of work. Instead,
  -- we just match the newtype name.
  extractNewtypeName :: ModuleName -> [SourceType] -> Maybe (ModuleName, ProperName 'TypeName)
  extractNewtypeName mn
    = fmap (qualify mn . utcQTyCon)
    . (unwrapTypeConstructor <=< lastMay)
  
  deriveInstance
    :: forall m
     . MonadError MultipleErrors m
    => MonadState CheckState m
    => MonadSupply m
    => MonadWriter MultipleErrors m
    => SourceType
    -> Qualified (ProperName 'ClassName)
    -> InstanceDerivationStrategy
    -> m Expr
  deriveInstance instType className strategy = do
    mn <- unsafeCheckCurrentModule
    env <- getEnv
    instUtc@UnwrappedTypeConstructor{ utcArgs = tys } <- maybe (internalCompilerError "invalid instance type") pure $ unwrapTypeConstructor instType
    let ctorName = coerceProperName <$> utcQTyCon instUtc
  
    TypeClassData{..} <-
      note (errorMessage . UnknownName $ fmap TyClassName className) $
        className `M.lookup` typeClasses env
  
    case strategy of
      KnownClassStrategy -> let
        unaryClass :: (UnwrappedTypeConstructor -> m [(PSString, Expr)]) -> m Expr
        unaryClass f = case tys of
          [ty] -> case unwrapTypeConstructor ty of
            Just utc | mn == utcModuleName utc -> do
              let superclassesDicts = flip map typeClassSuperclasses $ \(Constraint _ superclass _ suTyArgs _) ->
                    let tyArgs = map (replaceAllTypeVars (zip (map fst typeClassArguments) tys)) suTyArgs
                    in lam UnusedIdent (DeferredDictionary superclass tyArgs)
              let superclasses = map mkString (superClassDictionaryNames typeClassSuperclasses) `zip` superclassesDicts
              App (Constructor nullSourceSpan ctorName) . mkLit . ObjectLiteral . (++ superclasses) <$> f utc
            _ -> throwError . errorMessage $ ExpectedTypeConstructor className tys ty
          _ -> throwError . errorMessage $ InvalidDerivedInstance className tys 1
  
        unaryClass' f = unaryClass (f className)
  
        in case className of
          Libs.Bifoldable -> unaryClass' $ deriveFoldable True
          Libs.Bifunctor -> unaryClass' $ deriveFunctor (Just False) False Libs.S_bimap
          Libs.Bitraversable -> unaryClass' $ deriveTraversable True
          Libs.Contravariant -> unaryClass' $ deriveFunctor Nothing True Libs.S_cmap
          Libs.Eq -> unaryClass deriveEq
          Libs.Eq1 -> unaryClass $ const deriveEq1
          Libs.Foldable -> unaryClass' $ deriveFoldable False
          Libs.Functor -> unaryClass' $ deriveFunctor Nothing False Libs.S_map
          Libs.Ord -> unaryClass deriveOrd
          Libs.Ord1 -> unaryClass $ const deriveOrd1
          Libs.Profunctor -> unaryClass' $ deriveFunctor (Just True) False Libs.S_dimap
          Libs.Traversable -> unaryClass' $ deriveTraversable False
          -- See L.P.Sugar.TypeClasses.Deriving for the classes that can be
          -- derived prior to type checking.
          _ -> throwError . errorMessage $ CannotDerive className tys
  
      NewtypeStrategy ->
        case tys of
          _ : _ | Just utc <- unwrapTypeConstructor (last tys)
                , mn == utcModuleName utc
                -> deriveNewtypeInstance className tys utc
                | otherwise -> throwError . errorMessage $ ExpectedTypeConstructor className tys (last tys)
          _ -> throwError . errorMessage $ InvalidNewtypeInstance className tys
  
  deriveNewtypeInstance
    :: forall m
     . MonadError MultipleErrors m
    => MonadState CheckState m
    => MonadWriter MultipleErrors m
    => Qualified (ProperName 'ClassName)
    -> [SourceType]
    -> UnwrappedTypeConstructor
    -> m Expr
  deriveNewtypeInstance className tys (UnwrappedTypeConstructor mn tyConNm dkargs dargs) = do
      verifySuperclasses
      (dtype, tyKindNames, tyArgNames, ctors) <- lookupTypeDecl mn tyConNm
      go dtype tyKindNames tyArgNames ctors
    where
      go (Just Newtype) tyKindNames tyArgNames [(_, [wrapped])] = do
        -- The newtype might not be applied to all type arguments.
        -- This is okay as long as the newtype wraps something which ends with
        -- sufficiently many type applications to variables.
        -- For example, we can derive Functor for
        --
        -- newtype MyArray a = MyArray (Array a)
        --
        -- since Array a is a type application which uses the last
        -- type argument
        wrapped' <- replaceAllTypeSynonyms wrapped
        case stripRight (takeReverse (length tyArgNames - length dargs) tyArgNames) wrapped' of
          Just wrapped'' -> do
            let subst = zipWith (\(name, _) t -> (name, t)) tyArgNames dargs <> zip tyKindNames dkargs
            wrapped''' <- replaceAllTypeSynonyms $ replaceAllTypeVars subst wrapped''
            tys' <- mapM replaceAllTypeSynonyms tys
            return (DeferredDictionary className (init tys' ++ [wrapped''']))
          Nothing -> throwError . errorMessage $ InvalidNewtypeInstance className tys
      go _ _ _ _ = throwError . errorMessage $ InvalidNewtypeInstance className tys
  
      takeReverse :: Int -> [a] -> [a]
      takeReverse n = take n . reverse
  
      stripRight :: [(Text, Maybe kind)] -> SourceType -> Maybe SourceType
      stripRight [] ty = Just ty
      stripRight ((arg, _) : args) (TypeApp _ t (TypeVar _ arg'))
        | arg == arg' = stripRight args t
      stripRight _ _ = Nothing
  
      verifySuperclasses :: m ()
      verifySuperclasses = do
        env <- getEnv
        for_ (M.lookup className (typeClasses env)) $ \TypeClassData{ typeClassArguments = args, typeClassSuperclasses = superclasses } ->
          for_ superclasses $ \Constraint{..} -> do
            let constraintClass' = qualify (internalError "verifySuperclasses: unknown class module") constraintClass
            for_ (M.lookup constraintClass (typeClasses env)) $ \TypeClassData{ typeClassDependencies = deps } ->
              -- We need to check whether the newtype is mentioned, because of classes like MonadWriter
              -- with its Monoid superclass constraint.
              when (not (null args) && any ((fst (last args) `elem`) . usedTypeVariables) constraintArgs) $ do
                -- For now, we only verify superclasses where the newtype is the only argument,
                -- or for which all other arguments are determined by functional dependencies.
                -- Everything else raises a UnverifiableSuperclassInstance warning.
                -- This covers pretty much all cases we're interested in, but later we might want to do
                -- more work to extend this to other superclass relationships.
                let determined = map (srcTypeVar . fst . (args !!)) . ordNub . concatMap fdDetermined . filter ((== [length args - 1]) . fdDeterminers) $ deps
                if eqType (last constraintArgs) (srcTypeVar . fst $ last args) && all (`elem` determined) (init constraintArgs)
                  then do
                    -- Now make sure that a superclass instance was derived. Again, this is not a complete
                    -- check, since the superclass might have multiple type arguments, so overlaps might still
                    -- be possible, so we warn again.
                    for_ (extractNewtypeName mn tys) $ \nm -> do
                      unless (hasNewtypeSuperclassInstance constraintClass' nm (typeClassDictionaries env)) $
                        tell . errorMessage $ MissingNewtypeSuperclassInstance constraintClass className tys
                  else tell . errorMessage $ UnverifiableSuperclassInstance constraintClass className tys
  
      -- Note that this check doesn't actually verify that the superclass is
      -- newtype-derived; see #3168. The whole verifySuperclasses feature
      -- is pretty sketchy, and could use a thorough review and probably rewrite.
      hasNewtypeSuperclassInstance (suModule, suClass) nt@(newtypeModule, _) dicts =
        let su = Qualified (ByModuleName suModule) suClass
            lookIn mn'
              = elem nt
              . (toList . extractNewtypeName mn' . tcdInstanceTypes
                  <=< foldMap toList . M.elems
                  <=< toList . (M.lookup su <=< M.lookup (ByModuleName mn')))
              $ dicts
        in lookIn suModule || lookIn newtypeModule
  
  data TypeInfo = TypeInfo
    { tiTypeParams :: [Text]
    , tiCtors :: [(ProperName 'ConstructorName, [SourceType])]
    , tiArgSubst :: [(Text, SourceType)]
    }
  
  lookupTypeInfo
    :: forall m
     . MonadError MultipleErrors m
    => MonadState CheckState m
    => UnwrappedTypeConstructor
    -> m TypeInfo
  lookupTypeInfo UnwrappedTypeConstructor{..} = do
    (_, kindParams, map fst -> tiTypeParams, tiCtors) <- lookupTypeDecl utcModuleName utcTyCon
    let tiArgSubst = zip tiTypeParams utcArgs <> zip kindParams utcKindArgs
    pure TypeInfo{..}
  
  deriveEq
    :: forall m
     . MonadError MultipleErrors m
    => MonadState CheckState m
    => MonadSupply m
    => UnwrappedTypeConstructor
    -> m [(PSString, Expr)]
  deriveEq utc = do
    TypeInfo{..} <- lookupTypeInfo utc
    eqFun <- mkEqFunction tiCtors
    pure [(Libs.S_eq, eqFun)]
    where
      mkEqFunction :: [(ProperName 'ConstructorName, [SourceType])] -> m Expr
      mkEqFunction ctors = do
        x <- freshIdent "x"
        y <- freshIdent "y"
        lamCase2 x y . addCatch <$> mapM mkCtorClause ctors
  
      preludeConj :: Expr -> Expr -> Expr
      preludeConj = App . App (mkRef Libs.I_conj)
  
      preludeEq :: Expr -> Expr -> Expr
      preludeEq = App . App (mkRef Libs.I_eq)
  
      preludeEq1 :: Expr -> Expr -> Expr
      preludeEq1 = App . App (mkRef Libs.I_eq1)
  
      addCatch :: [CaseAlternative] -> [CaseAlternative]
      addCatch xs
        | length xs /= 1 = xs ++ [catchAll]
        | otherwise = xs -- Avoid redundant case
        where
        catchAll = CaseAlternative [NullBinder, NullBinder] (unguarded (mkLit (BooleanLiteral False)))
  
      mkCtorClause :: (ProperName 'ConstructorName, [SourceType]) -> m CaseAlternative
      mkCtorClause (ctorName, tys) = do
        identsL <- replicateM (length tys) (freshIdent "l")
        identsR <- replicateM (length tys) (freshIdent "r")
        tys' <- mapM replaceAllTypeSynonyms tys
        let tests = zipWith3 toEqTest (map mkVar identsL) (map mkVar identsR) tys'
        return $ CaseAlternative [caseBinder identsL, caseBinder identsR] (unguarded (conjAll tests))
        where
        caseBinder idents = mkCtorBinder (utcModuleName utc) ctorName $ map mkBinder idents
  
      conjAll :: [Expr] -> Expr
      conjAll = \case
        [] -> mkLit (BooleanLiteral True)
        xs -> foldl1 preludeConj xs
  
      toEqTest :: Expr -> Expr -> SourceType -> Expr
      toEqTest l r ty
        | Just fields <- decomposeRec <=< objectType $ ty
          = conjAll
          . map (\(Label str, typ) -> toEqTest (Accessor str l) (Accessor str r) typ)
          $ fields
        | isAppliedVar ty = preludeEq1 l r
        | otherwise = preludeEq l r
  
  deriveEq1 :: forall m. Applicative m => m [(PSString, Expr)]
  deriveEq1 = pure [(Libs.S_eq1, mkRef Libs.I_eq)]
  
  deriveOrd
    :: forall m
     . MonadError MultipleErrors m
    => MonadState CheckState m
    => MonadSupply m
    => UnwrappedTypeConstructor
    -> m [(PSString, Expr)]
  deriveOrd utc = do
    TypeInfo{..} <- lookupTypeInfo utc
    compareFun <- mkCompareFunction tiCtors
    pure [(Libs.S_compare, compareFun)]
    where
      mkCompareFunction :: [(ProperName 'ConstructorName, [SourceType])] -> m Expr
      mkCompareFunction ctors = do
        x <- freshIdent "x"
        y <- freshIdent "y"
        lamCase2 x y <$> (addCatch . concat <$> mapM mkCtorClauses (splitLast ctors))
  
      splitLast :: [a] -> [(a, Bool)]
      splitLast [] = []
      splitLast [x] = [(x, True)]
      splitLast (x : xs) = (x, False) : splitLast xs
  
      addCatch :: [CaseAlternative] -> [CaseAlternative]
      addCatch xs
        | null xs = [catchAll] -- No type constructors
        | otherwise = xs
        where
        catchAll = CaseAlternative [NullBinder, NullBinder] (unguarded (orderingCtor "EQ"))
  
      orderingMod :: ModuleName
      orderingMod = ModuleName "Data.Ordering"
  
      orderingCtor :: Text -> Expr
      orderingCtor = mkCtor orderingMod . ProperName
  
      orderingBinder :: Text -> Binder
      orderingBinder name = mkCtorBinder orderingMod (ProperName name) []
  
      ordCompare :: Expr -> Expr -> Expr
      ordCompare = App . App (mkRef Libs.I_compare)
  
      ordCompare1 :: Expr -> Expr -> Expr
      ordCompare1 = App . App (mkRef Libs.I_compare1)
  
      mkCtorClauses :: ((ProperName 'ConstructorName, [SourceType]), Bool) -> m [CaseAlternative]
      mkCtorClauses ((ctorName, tys), isLast) = do
        identsL <- replicateM (length tys) (freshIdent "l")
        identsR <- replicateM (length tys) (freshIdent "r")
        tys' <- mapM replaceAllTypeSynonyms tys
        let tests = zipWith3 toOrdering (map mkVar identsL) (map mkVar identsR) tys'
            extras | not isLast = [ CaseAlternative [nullCaseBinder, NullBinder] (unguarded (orderingCtor "LT"))
                                  , CaseAlternative [NullBinder, nullCaseBinder] (unguarded (orderingCtor "GT"))
                                  ]
                   | otherwise = []
        return $ CaseAlternative [ caseBinder identsL
                                 , caseBinder identsR
                                 ]
                                 (unguarded (appendAll tests))
               : extras
  
        where
        mn = utcModuleName utc
        caseBinder idents = mkCtorBinder mn ctorName $ map mkBinder idents
        nullCaseBinder = mkCtorBinder mn ctorName $ replicate (length tys) NullBinder
  
      appendAll :: [Expr] -> Expr
      appendAll = \case
        [] -> orderingCtor "EQ"
        [x] -> x
        (x : xs) -> Case [x] [ CaseAlternative [orderingBinder "LT"] (unguarded (orderingCtor "LT"))
                             , CaseAlternative [orderingBinder "GT"] (unguarded (orderingCtor "GT"))
                             , CaseAlternative [NullBinder] (unguarded (appendAll xs))
                             ]
  
      toOrdering :: Expr -> Expr -> SourceType -> Expr
      toOrdering l r ty
        | Just fields <- decomposeRec <=< objectType $ ty
          = appendAll
          . map (\(Label str, typ) -> toOrdering (Accessor str l) (Accessor str r) typ)
          $ fields
        | isAppliedVar ty = ordCompare1 l r
        | otherwise = ordCompare l r
  
  deriveOrd1 :: forall m. Applicative m => m [(PSString, Expr)]
  deriveOrd1 = pure [(Libs.S_compare1, mkRef Libs.I_compare)]
  
  lookupTypeDecl
    :: forall m
     . MonadError MultipleErrors m
    => MonadState CheckState m
    => ModuleName
    -> ProperName 'TypeName
    -> m (Maybe DataDeclType, [Text], [(Text, Maybe SourceType)], [(ProperName 'ConstructorName, [SourceType])])
  lookupTypeDecl mn typeName = do
    env <- getEnv
    note (errorMessage $ CannotFindDerivingType typeName) $ do
      (kind, DataType _ args dctors) <- Qualified (ByModuleName mn) typeName `M.lookup` types env
      (kargs, _) <- completeBinderList kind
      let dtype = do
            (ctorName, _) <- headMay dctors
            (a, _, _, _) <- Qualified (ByModuleName mn) ctorName `M.lookup` dataConstructors env
            pure a
      pure (dtype, fst . snd <$> kargs, map (\(v, k, _) -> (v, k)) args, dctors)
  
  isAppliedVar :: Type a -> Bool
  isAppliedVar (TypeApp _ (TypeVar _ _) _) = True
  isAppliedVar _ = False
  
  objectType :: Type a -> Maybe (Type a)
  objectType (TypeApp _ (TypeConstructor _ Prim.Record) rec) = Just rec
  objectType _ = Nothing
  
  decomposeRec :: SourceType -> Maybe [(Label, SourceType)]
  decomposeRec = fmap (sortOn fst) . go
    where go (RCons _ str typ typs) = fmap ((str, typ) :) (go typs)
          go (REmptyKinded _ _) = Just []
          go _ = Nothing
  
  decomposeRec' :: SourceType -> [(Label, SourceType)]
  decomposeRec' = sortOn fst . go
    where go (RCons _ str typ typs) = (str, typ) : go typs
          go _ = []
  
  -- | The parameter `c` is used to allow or forbid contravariance for different
  -- type classes. When deriving a type class that is a variation on Functor, a
  -- witness for `c` will be provided; when deriving a type class that is a
  -- variation on Foldable or Traversable, `c` will be Void and the contravariant
  -- ParamUsage constructor can be skipped in pattern matching.
  data ParamUsage c
    = IsParam
    | IsLParam
      -- ^ enables biparametric classes (of any variance) to be derived
    | MentionsParam (ParamUsage c)
      -- ^ enables monoparametric classes to be used in a derivation
    | MentionsParamBi (These (ParamUsage c) (ParamUsage c))
      -- ^ enables biparametric classes to be used in a derivation
    | MentionsParamContravariantly !c (ContravariantParamUsage c)
      -- ^ enables contravariant classes (of either parametricity) to be used in a derivation
    | IsRecord (NonEmpty (PSString, ParamUsage c))
  
  data ContravariantParamUsage c
    = MentionsParamContra (ParamUsage c)
      -- ^ enables Contravariant to be used in a derivation
    | MentionsParamPro (These (ParamUsage c) (ParamUsage c))
      -- ^ enables Profunctor to be used in a derivation
  
  data CovariantClasses = CovariantClasses
    { monoClass :: Qualified (ProperName 'ClassName)
    , biClass :: Qualified (ProperName 'ClassName)
    }
  
  data ContravariantClasses = ContravariantClasses
    { contraClass :: Qualified (ProperName 'ClassName)
    , proClass :: Qualified (ProperName 'ClassName)
    }
  
  data ContravarianceSupport c = ContravarianceSupport
    { contravarianceWitness :: c
    , paramIsContravariant :: Bool
    , lparamIsContravariant :: Bool
    , contravariantClasses :: ContravariantClasses
    }
  
  -- | Return, if possible, a These the contents of which each satisfy the
  -- predicate.
  filterThese :: forall a. (a -> Bool) -> These a a -> Maybe (These a a)
  filterThese p = uncurry align . over both (mfilter p) . unalign . Just
  
  validateParamsInTypeConstructors
    :: forall c m
     . MonadError MultipleErrors m
    => MonadState CheckState m
    => Qualified (ProperName 'ClassName)
    -> UnwrappedTypeConstructor
    -> Bool
    -> CovariantClasses
    -> Maybe (ContravarianceSupport c)
    -> m [(ProperName 'ConstructorName, [Maybe (ParamUsage c)])]
  validateParamsInTypeConstructors derivingClass utc isBi CovariantClasses{..} contravarianceSupport = do
    TypeInfo{..} <- lookupTypeInfo utc
    (mbLParam, param) <- liftEither . first (errorMessage . flip KindsDoNotUnify kindType . (kindType -:>)) $
      case (isBi, reverse tiTypeParams) of
        (False, x : _)    -> Right (Nothing, x)
        (False, _)        -> Left kindType
        (True, y : x : _) -> Right (Just x, y)
        (True, _ : _)     -> Left kindType
        (True, _)         -> Left $ kindType -:> kindType
    ctors <- traverse (traverse $ traverse replaceAllTypeSynonyms) tiCtors
    tcds <- getTypeClassDictionaries
    let (ctorUsages, problemSpans) = runWriter $ traverse (traverse . traverse $ typeToUsageOf tcds tiArgSubst (maybe That These mbLParam param) False) ctors
    let relatedClasses = [monoClass, biClass] ++ ([contraClass, proClass] <*> (contravariantClasses <$> toList contravarianceSupport))
    for_ (nonEmpty $ ordNub problemSpans) $ \sss ->
      throwError . addHint (RelatedPositions sss) . errorMessage $ CannotDeriveInvalidConstructorArg derivingClass relatedClasses (isJust contravarianceSupport)
    pure ctorUsages
  
    where
    typeToUsageOf :: InstanceContext -> [(Text, SourceType)] -> These Text Text -> Bool -> SourceType -> Writer [SourceSpan] (Maybe (ParamUsage c))
    typeToUsageOf tcds subst = fix $ \go params isNegative -> let
      goCo = go params isNegative
      goContra = go params $ not isNegative
  
      assertNoParamUsedIn :: SourceType -> Writer [SourceSpan] ()
      assertNoParamUsedIn ty = void $ both (flip assertParamNotUsedIn ty) params
  
      assertParamNotUsedIn :: Text -> SourceType -> Writer [SourceSpan] ()
      assertParamNotUsedIn param = everythingOnTypes (*>) $ \case
        TypeVar (ss, _) name | name == param -> tell [ss]
        _ -> pure ()
  
      tryBiClasses ht tyLArg tyArg
        | hasInstance tcds ht biClass
          = goCo tyLArg >>= preferMonoClass MentionsParamBi
        | Just (ContravarianceSupport c _ _ ContravariantClasses{..}) <- contravarianceSupport, hasInstance tcds ht proClass
          = goContra tyLArg >>= preferMonoClass (MentionsParamContravariantly c . MentionsParamPro)
        | otherwise
          = assertNoParamUsedIn tyLArg *> tryMonoClasses ht tyArg
        where
        preferMonoClass f lUsage =
          (if isNothing lUsage && hasInstance tcds ht monoClass then fmap MentionsParam else fmap f . align lUsage) <$> goCo tyArg
  
      tryMonoClasses ht tyArg
        | hasInstance tcds ht monoClass
          = fmap MentionsParam <$> goCo tyArg
        | Just (ContravarianceSupport c _ _ ContravariantClasses{..}) <- contravarianceSupport, hasInstance tcds ht contraClass
          = fmap (MentionsParamContravariantly c . MentionsParamContra) <$> goContra tyArg
        | otherwise
          = assertNoParamUsedIn tyArg $> Nothing
  
      headOfTypeWithSubst :: SourceType -> Qualified (Either Text (ProperName 'TypeName))
      headOfTypeWithSubst = headOfType . replaceAllTypeVars subst
  
      in \case
        ForAll _ _ name _ ty _ ->
          fmap join . traverse (\params' -> go params' isNegative ty) $ filterThese (/= name) params
  
        ConstrainedType _ _ ty ->
          goCo ty
  
        TypeApp _ (TypeConstructor _ Prim.Record) row ->
          fmap (fmap IsRecord . nonEmpty . catMaybes) . for (decomposeRec' row) $ \(Label lbl, ty) ->
            fmap (lbl, ) <$> goCo ty
  
        TypeApp _ (TypeApp _ tyFn tyLArg) tyArg ->
          assertNoParamUsedIn tyFn *> tryBiClasses (headOfTypeWithSubst tyFn) tyLArg tyArg
  
        TypeApp _ tyFn tyArg ->
          assertNoParamUsedIn tyFn *> tryMonoClasses (headOfTypeWithSubst tyFn) tyArg
  
        TypeVar (ss, _) name -> mergeTheseWith (checkName lparamIsContra IsLParam) (checkName paramIsContra IsParam) (liftA2 (<|>)) params
          where
          checkName thisParamIsContra usage param
            | name == param = when (thisParamIsContra /= isNegative) (tell [ss]) $> Just usage
            | otherwise = pure Nothing
  
        ty ->
          assertNoParamUsedIn ty $> Nothing
  
    paramIsContra = any paramIsContravariant contravarianceSupport
    lparamIsContra = any lparamIsContravariant contravarianceSupport
  
    hasInstance :: InstanceContext -> Qualified (Either Text (ProperName 'TypeName)) -> Qualified (ProperName 'ClassName) -> Bool
    hasInstance tcds ht@(Qualified qb _) cn@(Qualified cqb _) =
      any (any tcdAppliesToType . findDicts tcds cn) (ordNub [ByNullSourcePos, cqb, qb])
      where
      tcdAppliesToType tcd = case tcdInstanceTypes tcd of
        [headOfType -> ht'] -> ht == ht'
          -- It's possible that, if ht and ht' are Lefts, this might require
          -- verifying that the name isn't shadowed by something in tcdForAll. I
          -- can't devise a legal program that causes this issue, but if in the
          -- future it seems like a good idea, it probably is.
        _ -> False
  
    headOfType :: SourceType -> Qualified (Either Text (ProperName 'TypeName))
    headOfType = fix $ \go -> \case
      TypeApp _ ty _ -> go ty
      KindApp _ ty _ -> go ty
      TypeVar _ nm -> Qualified ByNullSourcePos (Left nm)
      Skolem _ nm _ _ _ -> Qualified ByNullSourcePos (Left nm)
      TypeConstructor _ (Qualified qb nm) -> Qualified qb (Right nm)
      ty -> internalError $ "headOfType missing a case: " <> show (void ty)
  
  usingLamIdent :: forall m. MonadSupply m => (Expr -> m Expr) -> m Expr
  usingLamIdent cb = do
    ident <- freshIdent "v"
    lam ident <$> cb (mkVar ident)
  
  traverseFields :: forall c f. Applicative f => (ParamUsage c -> Expr -> f Expr) -> NonEmpty (PSString, ParamUsage c) -> Expr -> f Expr
  traverseFields f fields r = fmap (ObjectUpdate r) . for (toList fields) $ \(lbl, usage) -> (lbl, ) <$> f usage (Accessor lbl r)
  
  unnestRecords :: forall c f. Applicative f => (ParamUsage c -> Expr -> f Expr) -> ParamUsage c -> Expr -> f Expr
  unnestRecords f = fix $ \go -> \case
    IsRecord fields -> traverseFields go fields
    usage -> f usage
  
  mkCasesForTraversal
    :: forall c f m
     . Applicative f -- this effect distinguishes the semantics of maps, folds, and traversals
    => MonadSupply m
    => ModuleName
    -> (ParamUsage c -> Expr -> f Expr) -- how to handle constructor arguments
    -> (f Expr -> m Expr) -- resolve the applicative effect into an expression
    -> [(ProperName 'ConstructorName, [Maybe (ParamUsage c)])]
    -> m Expr
  mkCasesForTraversal mn handleArg extractExpr ctors = do
    m <- freshIdent "m"
    fmap (lamCase m) . for ctors $ \(ctorName, ctorUsages) -> do
      ctorArgs <- for ctorUsages $ \usage -> freshIdent "v" <&> (, usage)
      let ctor = mkCtor mn ctorName
      let caseBinder = mkCtorBinder mn ctorName $ map (mkBinder . fst) ctorArgs
      fmap (CaseAlternative [caseBinder] . unguarded) . extractExpr $
        fmap (foldl' App ctor) . for ctorArgs $ \(ident, mbUsage) -> maybe pure handleArg mbUsage $ mkVar ident
  
  data TraversalExprs = TraversalExprs
    { recurseVar :: Expr -- a var representing map, foldMap, or traverse, for handling structured values
    , birecurseVar :: Expr -- same, but bimap, bifoldMap, or bitraverse
    , lrecurseExpr :: Expr -- same, but lmap or ltraverse (there is no lfoldMap, but we can use `flip bifoldMap mempty`)
    , rrecurseExpr :: Expr -- same, but rmap or rtraverse etc., which conceptually should be the same as recurseVar but the bi classes aren't subclasses of the mono classes
    }
  
  data ContraversalExprs = ContraversalExprs
    { crecurseVar :: Expr
    , direcurseVar :: Expr
    , lcrecurseVar :: Expr
    , rprorecurseVar :: Expr
    }
  
  appBirecurseExprs :: TraversalExprs -> These Expr Expr -> Expr
  appBirecurseExprs TraversalExprs{..} = these (App lrecurseExpr) (App rrecurseExpr) (App . App birecurseVar)
  
  appDirecurseExprs :: ContraversalExprs -> These Expr Expr -> Expr
  appDirecurseExprs ContraversalExprs{..} = these (App lcrecurseVar) (App rprorecurseVar) (App . App direcurseVar)
  
  data TraversalOps m = forall f. Applicative f => TraversalOps
    { visitExpr :: m Expr -> f Expr -- lift an expression into the applicative effect defining the traversal
    , extractExpr :: f Expr -> m Expr -- resolve the applicative effect into an expression
    }
  
  mkTraversal
    :: forall c m
     . MonadSupply m
    => ModuleName
    -> Bool
    -> TraversalExprs
    -> (c -> ContraversalExprs)
    -> TraversalOps m
    -> [(ProperName 'ConstructorName, [Maybe (ParamUsage c)])]
    -> m Expr
  mkTraversal mn isBi te@TraversalExprs{..} getContraversalExprs (TraversalOps @_ @f visitExpr extractExpr) ctors = do
    f <- freshIdent "f"
    g <- if isBi then freshIdent "g" else pure f
    let
      handleValue :: ParamUsage c -> Expr -> f Expr
      handleValue = unnestRecords $ \usage inputExpr -> visitExpr $ flip App inputExpr <$> mkFnExprForValue usage
  
      mkFnExprForValue :: ParamUsage c -> m Expr
      mkFnExprForValue = \case
        IsParam ->
          pure $ mkVar g
        IsLParam ->
          pure $ mkVar f
        MentionsParam innerUsage ->
          App recurseVar <$> mkFnExprForValue innerUsage
        MentionsParamBi theseInnerUsages ->
          appBirecurseExprs te <$> both mkFnExprForValue theseInnerUsages
        MentionsParamContravariantly c contraUsage -> do
          let ce@ContraversalExprs{..} = getContraversalExprs c
          case contraUsage of
            MentionsParamContra innerUsage ->
              App crecurseVar <$> mkFnExprForValue innerUsage
            MentionsParamPro theseInnerUsages ->
              appDirecurseExprs ce <$> both mkFnExprForValue theseInnerUsages
        IsRecord fields ->
          usingLamIdent $ extractExpr . traverseFields handleValue fields
  
    lam f . applyWhen isBi (lam g) <$> mkCasesForTraversal mn handleValue extractExpr ctors
  
  deriveFunctor
    :: forall m
     . MonadError MultipleErrors m
    => MonadState CheckState m
    => MonadSupply m
    => Maybe Bool -- does left parameter exist, and is it contravariant?
    -> Bool -- is the (right) parameter contravariant?
    -> PSString -- name of the map function for this functor type
    -> Qualified (ProperName 'ClassName)
    -> UnwrappedTypeConstructor
    -> m [(PSString, Expr)]
  deriveFunctor mbLParamIsContravariant paramIsContravariant mapName nm utc = do
    ctors <- validateParamsInTypeConstructors nm utc isBi functorClasses $ Just $ ContravarianceSupport
      { contravarianceWitness = ()
      , paramIsContravariant
      , lparamIsContravariant = or mbLParamIsContravariant
      , contravariantClasses
      }
    mapFun <- mkTraversal (utcModuleName utc) isBi mapExprs (const cmapExprs) (TraversalOps identity identity) ctors
    pure [(mapName, mapFun)]
    where
    isBi = isJust mbLParamIsContravariant
    mapExprs = TraversalExprs
      { recurseVar = mkRef Libs.I_map
      , birecurseVar = mkRef Libs.I_bimap
      , lrecurseExpr = mkRef Libs.I_lmap
      , rrecurseExpr = mkRef Libs.I_rmap
      }
    cmapExprs = ContraversalExprs
      { crecurseVar = mkRef Libs.I_cmap
      , direcurseVar = mkRef Libs.I_dimap
      , lcrecurseVar = mkRef Libs.I_lcmap
      , rprorecurseVar = mkRef Libs.I_profunctorRmap
      }
    functorClasses = CovariantClasses Libs.Functor Libs.Bifunctor
    contravariantClasses = ContravariantClasses Libs.Contravariant Libs.Profunctor
  
  toConst :: forall f a b. f a -> Const [f a] b
  toConst = Const . pure
  
  consumeConst :: forall f a b c. Applicative f => ([a] -> b) -> Const [f a] c -> f b
  consumeConst f = fmap f . sequenceA . getConst
  
  applyWhen :: forall a. Bool -> (a -> a) -> a -> a
  applyWhen cond f = if cond then f else identity
  
  deriveFoldable
    :: forall m
     . MonadError MultipleErrors m
    => MonadState CheckState m
    => MonadSupply m
    => Bool -- is there a left parameter (are we deriving Bifoldable)?
    -> Qualified (ProperName 'ClassName)
    -> UnwrappedTypeConstructor
    -> m [(PSString, Expr)]
  deriveFoldable isBi nm utc = do
    ctors <- validateParamsInTypeConstructors nm utc isBi foldableClasses Nothing
    foldlFun <- mkAsymmetricFoldFunction False foldlExprs ctors
    foldrFun <- mkAsymmetricFoldFunction True foldrExprs ctors
    foldMapFun <- mkTraversal mn isBi foldMapExprs absurd foldMapOps ctors
    pure
      [ (if isBi then Libs.S_bifoldl else Libs.S_foldl, foldlFun)
      , (if isBi then Libs.S_bifoldr else Libs.S_foldr, foldrFun)
      , (if isBi then Libs.S_bifoldMap else Libs.S_foldMap, foldMapFun)
      ]
    where
    mn = utcModuleName utc
    foldableClasses = CovariantClasses Libs.Foldable Libs.Bifoldable
    foldlExprs = TraversalExprs
      { recurseVar = mkRef Libs.I_foldl
      , birecurseVar = bifoldlVar
      , lrecurseExpr = App (App flipVar bifoldlVar) constVar
      , rrecurseExpr = App bifoldlVar constVar
      }
    foldrExprs = TraversalExprs
      { recurseVar = mkRef Libs.I_foldr
      , birecurseVar = bifoldrVar
      , lrecurseExpr = App (App flipVar bifoldrVar) (App constVar identityVar)
      , rrecurseExpr = App bifoldrVar (App constVar identityVar)
      }
    foldMapExprs = TraversalExprs
      { recurseVar = mkRef Libs.I_foldMap
      , birecurseVar = bifoldMapVar
      , lrecurseExpr = App (App flipVar bifoldMapVar) memptyVar
      , rrecurseExpr = App bifoldMapVar memptyVar
      }
    bifoldlVar = mkRef Libs.I_bifoldl
    bifoldrVar = mkRef Libs.I_bifoldr
    bifoldMapVar = mkRef Libs.I_bifoldMap
    constVar = mkRef Libs.I_const
    flipVar = mkRef Libs.I_flip
    identityVar = mkRef Libs.I_identity
    memptyVar = mkRef Libs.I_mempty
  
    mkAsymmetricFoldFunction :: Bool -> TraversalExprs -> [(ProperName 'ConstructorName, [Maybe (ParamUsage Void)])] -> m Expr
    mkAsymmetricFoldFunction isRightFold te@TraversalExprs{..} ctors = do
      f <- freshIdent "f"
      g <- if isBi then freshIdent "g" else pure f
      z <- freshIdent "z"
      let
        appCombiner :: (Bool, Expr) -> Expr -> Expr -> Expr
        appCombiner (isFlipped, fn) = applyWhen (isFlipped == isRightFold) flip $ App . App fn
  
        mkCombinerExpr :: ParamUsage Void -> m Expr
        mkCombinerExpr = fmap (uncurry $ \isFlipped -> applyWhen isFlipped $ App flipVar) . getCombiner
  
        handleValue :: ParamUsage Void -> Expr -> Const [m (Expr -> Expr)] Expr
        handleValue = unnestRecords $ \usage inputExpr -> toConst $ flip appCombiner inputExpr <$> getCombiner usage
  
        getCombiner :: ParamUsage Void -> m (Bool, Expr)
        getCombiner = \case
          IsParam ->
            pure (False, mkVar g)
          IsLParam ->
            pure (False, mkVar f)
          MentionsParam innerUsage ->
            (isRightFold, ) . App recurseVar <$> mkCombinerExpr innerUsage
          MentionsParamBi theseInnerUsages ->
            (isRightFold, ) . appBirecurseExprs te <$> both mkCombinerExpr theseInnerUsages
          IsRecord fields -> do
            let foldFieldsOf = traverseFields handleValue fields
            fmap (False, ) . usingLamIdent $ \lVar ->
              usingLamIdent $
                if isRightFold
                then flip extractExprStartingWith $ foldFieldsOf lVar
                else extractExprStartingWith lVar . foldFieldsOf
  
        extractExprStartingWith :: Expr -> Const [m (Expr -> Expr)] Expr -> m Expr
        extractExprStartingWith = consumeConst . if isRightFold then foldr ($) else foldl' (&)
  
      lam f . applyWhen isBi (lam g) . lam z <$> mkCasesForTraversal mn handleValue (extractExprStartingWith $ mkVar z) ctors
  
  foldMapOps :: forall m. Applicative m => TraversalOps m
  foldMapOps = TraversalOps { visitExpr = toConst, .. }
    where
    appendVar = mkRef Libs.I_append
    memptyVar = mkRef Libs.I_mempty
  
    extractExpr :: Const [m Expr] Expr -> m Expr
    extractExpr = consumeConst $ \case
      [] -> memptyVar
      exprs -> foldr1 (App . App appendVar) exprs
  
  deriveTraversable
    :: forall m
     . MonadError MultipleErrors m
    => MonadState CheckState m
    => MonadSupply m
    => Bool -- is there a left parameter (are we deriving Bitraversable)?
    -> Qualified (ProperName 'ClassName)
    -> UnwrappedTypeConstructor
    -> m [(PSString, Expr)]
  deriveTraversable isBi nm utc = do
    ctors <- validateParamsInTypeConstructors nm utc isBi traversableClasses Nothing
    traverseFun <- mkTraversal (utcModuleName utc) isBi traverseExprs absurd traverseOps ctors
    sequenceFun <- usingLamIdent $ pure . App (App (if isBi then App bitraverseVar identityVar else traverseVar) identityVar)
    pure
      [ (if isBi then Libs.S_bitraverse else Libs.S_traverse, traverseFun)
      , (if isBi then Libs.S_bisequence else Libs.S_sequence, sequenceFun)
      ]
    where
    traversableClasses = CovariantClasses Libs.Traversable Libs.Bitraversable
    traverseExprs = TraversalExprs
      { recurseVar = traverseVar
      , birecurseVar = bitraverseVar
      , lrecurseExpr = mkRef Libs.I_ltraverse
      , rrecurseExpr = mkRef Libs.I_rtraverse
      }
    traverseVar = mkRef Libs.I_traverse
    bitraverseVar = mkRef Libs.I_bitraverse
    identityVar = mkRef Libs.I_identity
  
  traverseOps :: forall m. MonadSupply m => TraversalOps m
  traverseOps = TraversalOps { .. }
    where
    pureVar = mkRef Libs.I_pure
    mapVar = mkRef Libs.I_map
    applyVar = mkRef Libs.I_apply
  
    visitExpr :: m Expr -> WriterT [(Ident, m Expr)] m Expr
    visitExpr traversedExpr = do
      ident <- freshIdent "v"
      tell [(ident, traversedExpr)] $> mkVar ident
  
    extractExpr :: WriterT [(Ident, m Expr)] m Expr -> m Expr
    extractExpr = runWriterT >=> \(result, unzip -> (ctx, args)) -> flip mkApps (foldr lam result ctx) <$> sequenceA args
  
    mkApps :: [Expr] -> Expr -> Expr
    mkApps = \case
      [] -> App pureVar
      h : t -> \l -> foldl' (App . App applyVar) (App (App mapVar l) h) t
  