-- | This module contains functions to generate instances for supported
--   typeclasses for user-defined Haskell data types.
--
--   Suppose we have a type
--   > data T α₁ … αₙ = C₁ τ₍₁,₁₎ … τ₍₁,ₘ₁₎ | … | Cₖ τ₍ₖ,₁₎ … τ₍ₖ,ₘₖ₎.
--   We wish to generate an instance of class @C@ providing the function
--   @f : T α₁ … αₙ -> τ@, where @τ@ is a type.
--   For example, for the @Normalform@ class, @f@ would be
--   > nf' : T α₁ … αₙ -> Free Shape Pos (T α₁ … αₙ).
--
--   The generated function has the following basic structure:
--
--   > f'T < class-specific binders > (x : T α₁ … αₙ) : B
--   >      := match x with
--   >         | C₁ fx₍₁,₁₎ … fx₍₁,ₘ₁₎ => < buildValue x [fx₍₁,₁₎, …, fx₍₁,ₘ₁₎ >
--   >         | …
--   >         | Cₖ fx₍ₖ,₁₎ … fx₍ₖ,ₘₖ₎ => < buildValue x [fx₍ₖ,₁₎, …, fxk₍ₖ,ₘₖ₎] >
--   >         end.
--
--   @buildValue x [fx₍ᵢ,₁₎, …, fx₍ᵢ,ₘᵢ₎]@ represents class-specific code that
--   actually constructs a value of type @τ@ when given @x@ and the
--   constructor's parameters as arguments.
--
--   For example, for a @Normalform@ instance of a type
--   @data List a = Nil | Cons a (List a)@,
--   the function would look as follows.
--
--   > nf'List_ {Shape : Type} {Pos : Shape -> Type}
--   >          {a b : Type} `{Normalform Shape Pos a b}
--   >          (x : List Shape Pos a)
--   >   : Free Shape Pos (List Identity.Shape Identity.Pos b)
--   >      := match x with
--   >         | nil => pure nil
--   >         | cons fx_0 fx_1 => nf fx_0 >>= fun nx_0 =>
--   >                             fx_1 >>= fun x_1 =>
--   >                             nf'List x_1 >>= fun nx_1 =>
--   >                             pure (cons (pure nx_0) (pure nx_1))
--   >         end.
--
--   Typically, @buildValue@ will use the class function @f@ on all components,
--   then reconstruct the value using the results of those function calls.
--   In the example above, we use @nf@ on @fx_0@ of type @a@. @nf fx_0@ means
--   the same as @fx_0 >>= fun x_0 => nf' x_0@.
--
--   Since we translate types in topological order and @C@ instances exist for
--   all previously translated types (and types from the Prelude), we can use
--   @f@ on most arguments.
--   For all type variables, we introduce class constraints into the type
--   signature of the function.
--   However, this is not possible for (indirectly) recursive arguments.
--
--   A directly recursive argument has the type @T τ₁ … τₙ@, where @τᵢ@ is a
--   type expressions (not necessarily type variables). We assume that @τᵢ'@
--   does not contain @T@ for any @i@, as this would constitute a non-positive
--   occurrence of @T@ and make @T@ invalid in Coq.
--   For these arguments, instead of the function @f@ we call @fT@ recursively.
--
--   An indirectly recursive argument is an argument of a type that is not @T@,
--   but contains @T@.
--   These arguments are problematic because we can neither use @f@ on them
--   (as that would generally require a @C@ instance of @T@) nor can we use
--   @fT@.
--
--   The problem is solved by introducing a local function @fT'@ for every type
--   @T'@ that contains @T@ that inlines the definition of a @T'@ instance of
--   @C@, and call this function for arguments of type @T'@.
--   These local functions are as polymorphic as possible to reduce the number
--   of local functions we need.
--
--   For example, if we want to generate an instance for the Haskell type
--
--   > data Forest a = AForest [Forest a]
--   >               | IntForest [Forest Int]
--   >               | BoolForest [Forest Bool]
--
--   only one local function is needed. In the case of @Normalform@, the local
--   function would look as follows.
--
--   > nf'ListForest_ {a b : Type} `{Normalform Shape Pos a b}
--   >   : List Shape Pos (Forest Shape Pos a)
--   >   -> Free Shape Pos (List Identity.Shape Identity.Pos
--   >                     (Forest Identity.Shape Identity.Pos b))
--
--   To generate these local functions, for every type expression @τ₍ᵢ,ⱼ₎@ in the
--   constructors of @T@, we collect all types that contain the original type
--   @T@.
--   More specifically, a type expression @T' τ₁ … τₙ@ is collected if
--   @τᵢ = T τ₁' … τₙ'@ for some type expressions @τ₁, …, τₙ@, or if @τᵢ@
--   is collected for some @i@.
--   During this process, any type expression that does not contain @T@ is
--   replaced by a placeholder variable @_@.
--
--   We keep track of which types correspond to which function with a map.
--
--   The generated functions @fT₁, …, fTₙ@ for @n@ mutually recursive types
--   @T₁, … Tₙ@ are a set of @n@ @Fixpoint@ definitions linked with @with@.
--   Indirectly recursive types and local functions based on them are computed
--   for each type.
--   In this case, a type @T'@ is considered indirectly recursive if it
--   contains any of the types @T₁, …, Tₙ@.
--   Arguments of type @Tᵢ@ can be treated like directly recursive arguments.
module FreeC.Backend.Coq.Converter.TypeDecl.TypeclassInstances where

import           Control.Monad
  ( foldM, mapAndUnzipM, replicateM )
import           Control.Monad.Extra              ( concatMapM )
import           Data.List                        ( nub )
import qualified Data.List.NonEmpty               as NonEmpty
import qualified Data.Map.Strict                  as Map
import           Data.Maybe                       ( fromJust )
import           Language.Coq.Subst

import qualified FreeC.Backend.Coq.Base           as Coq.Base
import           FreeC.Backend.Coq.Converter.Free
import qualified FreeC.Backend.Coq.Syntax         as Coq
import           FreeC.Environment
import           FreeC.Environment.Entry
import           FreeC.Environment.Fresh
import           FreeC.Environment.LookupOrFail
import           FreeC.IR.SrcSpan                 ( SrcSpan(NoSrcSpan) )
import           FreeC.IR.Subst
import qualified FreeC.IR.Syntax                  as IR
import           FreeC.IR.TypeSynExpansion
import           FreeC.IR.Unification
import           FreeC.Monad.Converter
import           FreeC.Pretty

-------------------------------------------------------------------------------
-- Instance Generation                                                       --
-------------------------------------------------------------------------------
-- | Data type for a type with certain components replaced by underscores.
data StrippedType
  = StrippedType
  | StrippedTypeCon IR.TypeConName [StrippedType]
 deriving ( Eq, Ord, Show )

isStripped :: StrippedType -> Bool
isStripped StrippedType = True
isStripped _            = False

-- | Type synonym for a map mapping types to function names.
type TypeMap' = Map.Map IR.Type Coq.Qualid

type TypeMap = Map.Map StrippedType Coq.Qualid

-- | Builds instances for all supported typeclasses.
--   Currently, @Normalform@ and @ShareableArgs@ instances are generated.
generateTypeclassInstances :: [IR.TypeDecl] -> Converter [Coq.Sentence]
generateTypeclassInstances dataDecls = do
  -- The types of the data declaration's constructors' arguments.
  let argTypes = map (concatMap IR.conDeclFields . IR.dataDeclCons) dataDecls
  -- The same types where all type synonyms are expanded.
  argTypesExpanded <- mapM (mapM expandAllTypeSynonyms) argTypes
  -- A list where all fully-applied type constructors that do not contain one of the types
  -- for which we are defining instances and all type variables are replaced with
  -- the same type variable (an underscore). The list is reversed so its entries are
  -- in topological order.
  let reducedTypes = map (nub . reverse . concatMap collectSubTypes)
        argTypesExpanded
  -- Like 'reducedTypes', but with all occurrences of the types for which we are defining
  -- instances and all type variables removed from the list.
  -- This leaves exactly the types with indirect recursion, with all non-recursive
  -- components replaced by underscores.
  let recTypeList = map
        (filter (\t -> not (t `elem` declTypes || isStripped t))) reducedTypes
  -- Construct @Normalform@ instances.
  nfInstances <- buildInstances recTypeList
    (fromJust $ Coq.unpackQualid Coq.Base.nf')
    (fromJust $ Coq.unpackQualid Coq.Base.normalform) nfBindersAndReturnType
    buildNormalformValue
  -- Construct @ShareableArgs@ instances.
  shareableArgsInstances <- buildInstances recTypeList
    (fromJust $ Coq.unpackQualid Coq.Base.shareArgs)
    (fromJust $ Coq.unpackQualid Coq.Base.shareableArgs)
    shareArgsBindersAndReturnType buildShareArgsValue
  return (nfInstances ++ shareableArgsInstances)
 where
  -- | The (mutually recursive) data types for which we are defining
  --   instances, converted to types. All type variable are converted
  --   to underscores.
  declTypes :: [StrippedType]
  declTypes = [StrippedTypeCon (IR.typeDeclQName dataDecl)
                (replicate (length (IR.typeDeclArgs dataDecl)) StrippedType)
              | dataDecl <- dataDecls
              ]

  -- The names of the type constructors of the data types for which
  -- we are defining instances.
  typeConNames :: [IR.TypeConName]
  typeConNames = map IR.typeDeclQName dataDecls

  -- | Constructs instances of a typeclass for a set of mutually recursive
  --   types. The typeclass is specified by the arguments.
  buildInstances
    :: [[StrippedType]]
    -- ^ For each data declaration, this list contains the occurrences of
    -- indirect recursion in the constructors of that data declaration.
    -> String -- ^ The name of the class function.
    -> String -- ^ The name of the typeclass.
    -> (StrippedType
        -> Coq.Qualid
        -> Converter ([Coq.Binder], [Coq.Binder], Coq.Term, Coq.Term))
    -- ^ A function to get class-specific binders and return types.
    -> (TypeMap
        -> Coq.Qualid
        -> [(StrippedType, Coq.Qualid)]
        -> Converter Coq.Term)
    -- ^ A function to compute a class-specific value given a data constructor
    --   with arguments.
    -> Converter [Coq.Sentence]
  buildInstances recTypeList functionPrefix className getBindersAndReturnTypes
    buildValue = do
      -- This map defines the name of the top-level class function for each
      -- of the mutually recursive types.
      -- It must be defined outside of a local environment to prevent any
      -- clashes of the function names with other names.
      topLevelMap <- nameFunctionsAndInsert functionPrefix Map.empty declTypes
      (fixBodies, instances) <- mapAndUnzipM
        (uncurry (buildFixBodyAndInstance topLevelMap))
        (zip declTypes recTypeList)
      return
        $ Coq.comment (className
                       ++ " instance"
                       ++ ['s' | length dataDecls > 1]
                       ++ " for "
                       ++ showPretty (map IR.typeDeclName dataDecls))
        : Coq.FixpointSentence (Coq.Fixpoint (NonEmpty.fromList fixBodies) [])
        : instances
   where
        -- Constructs the class function and class instance for a single type.
    buildFixBodyAndInstance
      :: TypeMap
      -- ^ A map to map occurrences of the top-level types to recursive
      --   function calls.
      -> StrippedType -- ^ The type for which we are defining an instance.
      -> [StrippedType] -- ^ The list of indirectly recursive types.
      -> Converter (Coq.FixBody, Coq.Sentence)
    buildFixBodyAndInstance topLevelMap t recTypes = do
      -- Locally visible definitions are defined in a local environment.
      (fixBody, typeLevelMap, instanceBinders, instanceRetType) <- localEnv $ do
        -- This map names necessary local functions and maps indirectly
        -- recursive types to the appropriate function names.
        typeLevelMap
          <- nameFunctionsAndInsert functionPrefix topLevelMap recTypes
        -- Name the argument of type @t@ given to the class
        -- function.
        topLevelVar <- freshCoqQualid freshArgPrefix
        -- Compute class-specific binders and return types.
        (implicitBinders, explicitBinders, retType, instanceRetType)
          <- getBindersAndReturnTypes t topLevelVar
        -- Build the implementation of the class function.
        let functionBinders = implicitBinders ++ explicitBinders
        fixBody <- makeFixBody typeLevelMap topLevelVar t functionBinders
          retType recTypes
        return (fixBody, typeLevelMap, implicitBinders, instanceRetType)
      -- Build the class instance for the given type.
      -- The instance must be defined outside of a local environment so
      -- that the instance name does not clash with any other names.
      instanceDefinition
        <- buildInstance typeLevelMap t instanceBinders instanceRetType
      return (fixBody, instanceDefinition)

    -- | Builds an instance for a specific type and typeclass.
    buildInstance
      :: TypeMap
      -- ^ A mapping from (in)directly recursive types to function names.
      -> StrippedType -- ^ The type for which we are defining an instance.
      -> [Coq.Binder] -- ^ The binders for the type class instance.
      -> Coq.Term -- ^ The type of the instance.
      -> Converter Coq.Sentence
    buildInstance m t binders retType = do
      -- Define the class function as the function to which the current type
      -- is mapped.
      let instanceBody
            = (Coq.bare functionPrefix, Coq.Qualid (fromJust (Map.lookup t m)))
      instanceName <- nameFunction className t
      return
        $ Coq.InstanceSentence
        (Coq.InstanceDefinition instanceName (freeArgsBinders ++ binders)
         retType [instanceBody] Nothing)

    -- | Generates the implementation of the body of a class function for the
    --   given type.
    makeFixBody
      :: TypeMap
      -- ^ A mapping from (in)directly recursive types to function names.
      -> Coq.Qualid -- ^ The name of the argument of type @t@.
      -> StrippedType -- ^ The type for which we are defining an instance.
      -> [Coq.Binder] -- ^ The binders for the class function.
      -> Coq.Term -- ^ The return type of the class function.
      -> [StrippedType] -- ^ The list of indirectly recursive types.
      -> Converter Coq.FixBody
    makeFixBody m varName t binders retType recTypes = do
      rhs <- generateBody m varName t recTypes
      return
        $ Coq.FixBody (fromJust (Map.lookup t m))
        (NonEmpty.fromList (freeArgsBinders ++ binders))
        (Just (Coq.StructOrder varName)) (Just retType) rhs

    -- | Creates the function body for a class function by creating local
    --   functions for all indirectly recursive types.
    generateBody
      :: TypeMap
      -- ^ A mapping from (in)directly recursive types to function names.
      -> Coq.Qualid -- ^ The name of the argument of type @t@.
      -> StrippedType -- ^ The type for which we are defining an instance.
      -> [StrippedType] -- ^ The list of indirectly recursive types.
      -> Converter Coq.Term

    -- If there are no indirectly recursive types, match on the constructors of
    -- the original type.
    generateBody m varName t []
      = matchConstructors m varName t
    -- For each indirectly recursive type, create a local function as a
    -- @let fix@ declaration and generate the definition of the class function
    -- for that type.
    -- This local declaration is wrapped around all remaining declarations and
    -- is therefore visible when defining them.
    generateBody m varName t (recType : recTypes) = do
      inBody <- generateBody m varName t recTypes
      var <- freshCoqQualid freshArgPrefix
      -- Create the body of the local function by matching on the type's
      -- constructors.
      letBody <- matchConstructors m var recType
      (implicitBinders, explicitBinders, retType, _)
        <- getBindersAndReturnTypes recType var
      let binders            = implicitBinders ++ explicitBinders
          Just localFuncName = Map.lookup recType m
      return
        $ Coq.Let localFuncName [] Nothing
        (Coq.Fix
         (Coq.FixOne (Coq.FixBody localFuncName (NonEmpty.fromList binders)
                      (Just (Coq.StructOrder var)) (Just retType) letBody)))
        inBody

    -- | Matches on the constructors of a type.
    matchConstructors
      :: TypeMap -> Coq.Qualid -> StrippedType -> Converter Coq.Term
    matchConstructors m varName t@(StrippedTypeCon conName _) = do
      entry <- lookupEntryOrFail NoSrcSpan IR.TypeScope conName
      equations <- mapM (buildEquation m t) (entryConsNames entry)
      return $ Coq.match (Coq.Qualid varName) equations
    matchConstructors _ _ StrippedType
      = error "generateTypeclassInstances: unexpected type placeholder."

    -- | Creates a match equation on a given data constructor with a
    --   class-specific right-hand side.
    buildEquation
      :: TypeMap -> StrippedType -> IR.ConName -> Converter Coq.Equation
    buildEquation m t conName = do
      conEntry <- lookupEntryOrFail NoSrcSpan IR.ValueScope conName
      retType <- expandAllTypeSynonyms (entryReturnType conEntry)
      -- Get the Coq name of the constructor.
      let conIdent = entryIdent conEntry
      -- Generate fresh variables for the constructor's parameters.
      conArgIdents <- freshQualids (entryArity conEntry) freshArgPrefix
      -- Replace all underscores with fresh variables before unification.
      tFreshVars <- insertFreshVariables t
      sub <- unifyOrFail NoSrcSpan tFreshVars retType
      -- Find out the type of each constructor argument by unifying its return
      -- type with the given type expression and applying the resulting
      -- substitution to each constructor argument's type.
      -- Then convert all irrelevant components to underscores again so the
      -- type can be looked up in the type map.
      expandedArgTypes <- mapM expandAllTypeSynonyms (entryArgTypes conEntry)
      let modArgTypes = map (stripType . applySubst sub) expandedArgTypes
      let lhs = Coq.ArgsPat conIdent (map Coq.QualidPat conArgIdents)
      -- Build the right-hand side of the equation by applying the
      -- class-specific function @buildValue@.
      rhs <- buildValue m conIdent (zip modArgTypes conArgIdents)
      return $ Coq.equation lhs rhs

  -------------------------------------------------------------------------------
  -- Functions to Produce @Normalform@ Instances                                 --
  -------------------------------------------------------------------------------
  -- | The binders and return types for the @Normalform@ class function and instance.
  nfBindersAndReturnType
    :: StrippedType
    -- ^ The type @t@ for which we are defining an instance.
    -> Coq.Qualid -- ^ The name of the argument of type @t@.
    -> Converter
    ( [Coq.Binder] -- Type variable binders and @Normalform@ constraints.
    , [Coq.Binder] -- Binder for the argument of type @t@.
    , Coq.Term -- Return type of @nf'@.
    , Coq.Term -- Return type of the @Normalform@ instance.
    )
  nfBindersAndReturnType t varName = do
    (sourceType, sourceVars) <- toCoqType t
    -- The return types of the type variables' @Normalform@ instances.
    let nTypes            = map (\v -> genericApply Coq.Base.nType []
                                 [Coq.Qualid v, Coq.Underscore] []) sourceVars
        -- Build a substitution to create the normalized type from the source
        -- type.
        targetTypeMap     = buildNFSubst (zip sourceVars nTypes)
        targetType        = subst targetTypeMap sourceType
        -- For each type variable @aᵢ@, build a constraint
        -- @`{Normalform Shape Pos aᵢ}@.
        constraints       = map Coq.Base.normalformBinder sourceVars
        varBinder         = [typeVarBinder sourceVars | not (null sourceVars)]
        binders           = varBinder ++ constraints
        -- Create an explicit argument binder for the value to be normalized.
        topLevelVarBinder
          = Coq.typedBinder' Coq.Ungeneralizable Coq.Explicit varName sourceType
        instanceRetType   = genericApply Coq.Base.normalform [] [] [sourceType]
        funcRetType       = applyFree targetType
    return (binders, [topLevelVarBinder], funcRetType, instanceRetType)
   where
    buildNFSubst :: [(Coq.Qualid, Coq.Term)] -> Map.Map Coq.Qualid Coq.Term
    buildNFSubst kvs = Map.insert Coq.Base.shape (Coq.Qualid Coq.Base.idShape)
      (Map.insert Coq.Base.pos (Coq.Qualid Coq.Base.idPos)
       (foldr (uncurry Map.insert) Map.empty kvs))

  -- | Builds a normalized @Free@ value for the given constructor
  --   and constructor arguments.
  buildNormalformValue
    :: TypeMap
    -- ^ A map to associate types with the appropriate functions to call.
    -> Coq.Qualid -- ^ The data constructor used to build a value.
    -> [(StrippedType, Coq.Qualid)]
    -- ^ The types and names of the constructor's arguments.
    -> Converter Coq.Term
  buildNormalformValue nameMap consName = buildNormalformValue' []
   where
    -- | Like 'buildNormalformValue', but with an additional parameter to accumulate
    --   bound variables.
    buildNormalformValue'
      :: [Coq.Term] -> [(StrippedType, Coq.Qualid)] -> Converter Coq.Term

    -- If all components have been normalized, apply the constructor to
    -- the normalized components.
    buildNormalformValue' boundVars [] = do
      args <- mapM generatePure (reverse boundVars)
      generatePure (Coq.app (Coq.Qualid consName) args)
    -- For each component, apply the appropriate function, bind the
    -- result and do the remaining computation.
    buildNormalformValue' boundVars ((t, varName) : consVars)
      = let f = (\nx -> buildNormalformValue' (nx : boundVars) consVars)
        in case Map.lookup t nameMap of
             -- For recursive or indirectly recursive calls, the type map
             -- returns the name of the appropriate function to call.
             Just funcName -> do
               -- Because the functions work on bare values, the component
               -- must be bound before applying the normalization.
               generateBind (Coq.Qualid varName) freshArgPrefix Nothing
                 (\x -> generateBind (Coq.app (Coq.Qualid funcName) [x])
                  freshNormalformArgPrefix Nothing f)
             -- If there is no entry in the type map, we can assume that an instance
             -- already exists. Therefore, we apply @nf@ to the component to receive
             -- a normalized value.
             Nothing       -> generateBind
               (Coq.app (Coq.Qualid Coq.Base.nf) [Coq.Qualid varName])
               freshNormalformArgPrefix Nothing f

  -------------------------------------------------------------------------------
  -- Functions to Produce @ShareableArgs@ Instances                              --
  -------------------------------------------------------------------------------
  -- | The binders and return types for the @ShareableArgs@ class function and instance.
  shareArgsBindersAndReturnType
    :: StrippedType
    -- ^ The type @t@ for which we are defining an instance.
    -> Coq.Qualid -- ^ The name of the argument of type @t@.
    -> Converter
    ( [Coq.Binder] -- Binders to add to the type class and functions.
    , [Coq.Binder] -- Binders to add to the function only.
    , Coq.Term -- Return type of @shareArgs@.
    , Coq.Term -- Return type of the @ShareableArgs@ instance.
    )
  shareArgsBindersAndReturnType t varName = do
    (coqType, vars) <- toCoqType t
    let constraints     = map Coq.Base.shareableArgsBinder vars
        typeVarBinders  = [typeVarBinder vars | not (null vars)]
        implicitBinders = typeVarBinders ++ constraints
        varBinder
          = Coq.typedBinder' Coq.Ungeneralizable Coq.Explicit varName coqType
        explicitBinders = [Coq.Base.strategyBinder, varBinder]
        instanceRetType = genericApply Coq.Base.shareableArgs [] [] [coqType]
        funcRetType     = applyFree coqType
    return (implicitBinders, explicitBinders, funcRetType, instanceRetType)

  -- | Shares all arguments of the given constructor and reconstructs the
  --   value with the shared components.
  buildShareArgsValue
    :: TypeMap
    -- ^ A map to associate types with the appropriate functions to call.
    -> Coq.Qualid -- ^ The data constructor used to build a value.
    -> [(StrippedType, Coq.Qualid)]
    -- ^ The types and names of the constructor's arguments.
    -> Converter Coq.Term
  buildShareArgsValue nameMap consName = buildShareArgsValue' []
   where
    buildShareArgsValue'
      :: [Coq.Term] -> [(StrippedType, Coq.Qualid)] -> Converter Coq.Term
    buildShareArgsValue' vals [] = generatePure
      (Coq.app (Coq.Qualid consName) (reverse vals))
    buildShareArgsValue' vals ((t, varName) : consVars) = do
      let funcName = Map.findWithDefault Coq.Base.shareArgs t nameMap
          lhs
            = genericApply Coq.Base.shareWith [Coq.Qualid Coq.Base.strategyArg]
            [] [Coq.Qualid funcName, Coq.Qualid varName]
      generateBind lhs freshSharingArgPrefix Nothing
        (\val -> buildShareArgsValue' (val : vals) consVars)

  -------------------------------------------------------------------------------
  -- Helper Functions                                                          --
  -------------------------------------------------------------------------------
  -- | Creates an entry with a unique name for each of the given types and
  --   inserts them into the given map.
  nameFunctionsAndInsert
    :: String -> TypeMap -> [StrippedType] -> Converter TypeMap
  nameFunctionsAndInsert prefix = foldM (nameFunctionAndInsert prefix)

  -- | Like 'nameFunctionsAndInsert', but for a single type.
  nameFunctionAndInsert
    :: String -> TypeMap -> StrippedType -> Converter TypeMap
  nameFunctionAndInsert prefix m t = do
    name <- nameFunction prefix t
    return (Map.insert t name m)

  -- | Names a function based on a type expression while avoiding name clashes
  --   with other identifiers.
  nameFunction :: String -> StrippedType -> Converter Coq.Qualid
  nameFunction prefix t = do
    prettyType <- showPrettyType t
    freshCoqQualid (prefix ++ prettyType)

  -- | Collects all fully-applied type constructors of arity at least 1
  --   (including their arguments) that occur in the given type. All arguments
  --   that do not contain occurrences of the types for which we are defining
  --   an instance are replaced by the type variable @_@.
  --   The resulting list contains (in reverse topological order) exactly all
  --   types for which we must define a separate function in the instance
  --   definition, where all occurrences of @_@ represent the polymorphic
  --   components of the function.
  collectSubTypes :: IR.Type -> [StrippedType]
  collectSubTypes = collectFullyAppliedTypes True
   where
    -- | Like 'collectSubTypes', but with an additional flag to denote whether
    --   @t@ is a full application of a type constructor, e.g. @Pair Int Bool@,
    --   or a partial application, e.g. @Pair Int@.
    --   Only full applications are collected.
    collectFullyAppliedTypes :: Bool -> IR.Type -> [StrippedType]
    collectFullyAppliedTypes fullApplication t@(IR.TypeApp _ l r)
      -- The left-hand side of a type application is the partial
      -- application of a type constructor.
      -- The right-hand side is a fully-applied type constructor,
      -- a variable or a function type.
       = let remainingTypes = collectFullyAppliedTypes False l
               ++ collectFullyAppliedTypes True r
         in if fullApplication
              then stripType t : remainingTypes
              else remainingTypes
    -- Type variables, function types and type constructors with arity 0 are not
    -- collected.
    collectFullyAppliedTypes _ _ = []

  -- | Returns the same type with all type expressions that do not contain one
  --   of the type constructors for which we are defining instances replaced
  --   with the type variable @_@.
  stripType :: IR.Type -> StrippedType
  stripType = stripType' False
   where
    -- | Like 'stripType', but with an additional flag to denote whether an
    --   occurrence of a relevant type was found in an argument of a type
    --   application.
    --   This is necessary so that, for example, @Pair Bool t@ is not
    --   transformed to @_ t@, but to @Pair _ t@.
    stripType' :: Bool -> IR.Type -> StrippedType
    stripType' flag (IR.TypeCon _ conName)
      | flag || conName `elem` typeConNames = StrippedTypeCon conName []
      | otherwise = StrippedType
    -- For a type application, check if a relevant type occurs in its
    -- right-hand side.
    stripType' flag (IR.TypeApp _ l r) = case stripType' False r of
      -- If not, check if a relevant type occurs in its left-hand side,
      -- otherwise replace the whole expression with an underscore.
      StrippedType -> case stripType' flag l of
        StrippedType             -> StrippedType
        StrippedTypeCon con args -> StrippedTypeCon con (args ++ [StrippedType])
      -- If a relevant type does occur in the right-hand side,
      -- the type application must be preserved, so only its arguments are
      -- stripped.
      r'           -> let StrippedTypeCon con args = stripType' True l
                      in StrippedTypeCon con (args ++ [r'])
    -- Type variables and function types are not relevant and are replaced by @_@.
    stripType' _ _ = StrippedType

  showPrettyType :: StrippedType -> Converter String

  -- For a placeholder, show "_".
  showPrettyType StrippedType               = return "_"
  -- For a type constructor and its arguments, return the constructor's
  -- Coq identifier as a string with the conversions of the arguments appended.
  showPrettyType (StrippedTypeCon con args) = do
    prettyCon <- fromJust . (>>= Coq.unpackQualid)
      <$> inEnv (lookupIdent IR.TypeScope con)
    prettyArgs <- concatMapM showPrettyType args
    return (prettyCon ++ prettyArgs)

  -- | Converts a @StrippedType@ to an @IR.Type@, replacing all
  --   placeholders with fresh variables.
  insertFreshVariables :: StrippedType -> Converter IR.Type
  insertFreshVariables StrippedType               = do
    freshVar <- freshHaskellIdent freshArgPrefix
    return (IR.TypeVar NoSrcSpan freshVar)
  insertFreshVariables (StrippedTypeCon con args) = do
    args' <- mapM insertFreshVariables args
    return (foldl (IR.TypeApp NoSrcSpan) (IR.TypeCon NoSrcSpan con) args')

  -- | Binders for (implicit) Shape and Pos arguments.
  --
  --   > freeArgsBinders = [ {Shape : Type}, {Pos : Shape -> Type} ]
  freeArgsBinders :: [Coq.Binder]
  freeArgsBinders = genericArgDecls Coq.Implicit

  -- | Shortcut for the construction of an implicit binder for type variables.
  --
  --   > typeVarBinder [α₁, …, an] = {α₁ …αₙ : Type}
  typeVarBinder :: [Coq.Qualid] -> Coq.Binder
  typeVarBinder typeVars
    = Coq.typedBinder Coq.Ungeneralizable Coq.Implicit typeVars Coq.sortType

  -- | Given an @A@, returns @Free Shape Pos A@.
  applyFree :: Coq.Term -> Coq.Term
  applyFree a = genericApply Coq.Base.free [] [] [a]

  -- | Converts a type into a Coq type (a term) with fresh Coq
  --   identifiers for all underscores.
  --   Returns a pair of the result term and a list of the fresh variables.
  toCoqType :: StrippedType -- ^ The type to convert.
            -> Converter (Coq.Term, [Coq.Qualid])

  -- A type variable is translated into a fresh type variable.
  toCoqType StrippedType               = do
    x <- freshCoqQualid freshTypeVarPrefix
    return (Coq.Qualid x, [x])
  toCoqType (StrippedTypeCon con args) = do
    entry <- lookupEntryOrFail NoSrcSpan IR.TypeScope con
    (coqArgs, freshVars) <- mapAndUnzipM toCoqType args
    return (genericApply (entryIdent entry) [] [] coqArgs, concat freshVars)

  -- | Produces @n@ new Coq identifiers (Qualids) with the same prefix.
  freshQualids :: Int -> String -> Converter [Coq.Qualid]
  freshQualids n prefix = replicateM n (freshCoqQualid prefix)