content: module Language.PureScript.Environment where
  
  import Prelude
  
  import GHC.Generics (Generic)
  import Control.DeepSeq (NFData)
  import Control.Monad (unless)
  import Codec.Serialise (Serialise)
  import Data.Aeson ((.=), (.:))
  import Data.Aeson qualified as A
  import Data.Foldable (find, fold)
  import Data.Functor ((<&>))
  import Data.IntMap qualified as IM
  import Data.IntSet qualified as IS
  import Data.Map qualified as M
  import Data.Set qualified as S
  import Data.Maybe (fromMaybe, mapMaybe)
  import Data.Semigroup (First(..))
  import Data.Text (Text)
  import Data.Text qualified as T
  import Data.List.NonEmpty qualified as NEL
  
  import Language.PureScript.AST.SourcePos (nullSourceAnn)
  import Language.PureScript.Crash (internalError)
  import Language.PureScript.Names (Ident, ProperName(..), ProperNameType(..), Qualified, QualifiedBy, coerceProperName)
  import Language.PureScript.Roles (Role(..))
  import Language.PureScript.TypeClassDictionaries (NamedDict)
  import Language.PureScript.Types (SourceConstraint, SourceType, Type(..), TypeVarVisibility(..), eqType, srcTypeConstructor, freeTypeVariables)
  import Language.PureScript.Constants.Prim qualified as C
  
  -- | The @Environment@ defines all values and types which are currently in scope:
  data Environment = Environment
    { names :: M.Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
    -- ^ Values currently in scope
    , types :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
    -- ^ Type names currently in scope
    , dataConstructors :: M.Map (Qualified (ProperName 'ConstructorName)) (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
    -- ^ Data constructors currently in scope, along with their associated type
    -- constructor name, argument types and return type.
    , typeSynonyms :: M.Map (Qualified (ProperName 'TypeName)) ([(Text, Maybe SourceType)], SourceType)
    -- ^ Type synonyms currently in scope
    , typeClassDictionaries :: M.Map QualifiedBy (M.Map (Qualified (ProperName 'ClassName)) (M.Map (Qualified Ident) (NEL.NonEmpty NamedDict)))
    -- ^ Available type class dictionaries. When looking up 'Nothing' in the
    -- outer map, this returns the map of type class dictionaries in local
    -- scope (ie dictionaries brought in by a constrained type).
    , typeClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
    -- ^ Type classes
    } deriving (Show, Generic)
  
  instance NFData Environment
  
  -- | Information about a type class
  data TypeClassData = TypeClassData
    { typeClassArguments :: [(Text, Maybe SourceType)]
    -- ^ A list of type argument names, and their kinds, where kind annotations
    -- were provided.
    , typeClassMembers :: [(Ident, SourceType, Maybe (S.Set (NEL.NonEmpty Int)))]
    -- ^ A list of type class members and their types and whether or not
    -- they have type variables that must be defined using Visible Type Applications.
    -- Type arguments listed above are considered bound in these types.
    , typeClassSuperclasses :: [SourceConstraint]
    -- ^ A list of superclasses of this type class. Type arguments listed above
    -- are considered bound in the types appearing in these constraints.
    , typeClassDependencies :: [FunctionalDependency]
    -- ^ A list of functional dependencies for the type arguments of this class.
    , typeClassDeterminedArguments :: S.Set Int
    -- ^ A set of indexes of type argument that are fully determined by other
    -- arguments via functional dependencies. This can be computed from both
    -- typeClassArguments and typeClassDependencies.
    , typeClassCoveringSets :: S.Set (S.Set Int)
    -- ^ A sets of arguments that can be used to infer all other arguments.
    , typeClassIsEmpty :: Bool
    -- ^ Whether or not dictionaries for this type class are necessarily empty.
    } deriving (Show, Generic)
  
  instance NFData TypeClassData
  
  -- | A functional dependency indicates a relationship between two sets of
  -- type arguments in a class declaration.
  data FunctionalDependency = FunctionalDependency
    { fdDeterminers :: [Int]
    -- ^ the type arguments which determine the determined type arguments
    , fdDetermined  :: [Int]
    -- ^ the determined type arguments
    } deriving (Show, Generic)
  
  instance NFData FunctionalDependency
  instance Serialise FunctionalDependency
  
  instance A.FromJSON FunctionalDependency where
    parseJSON = A.withObject "FunctionalDependency" $ \o ->
      FunctionalDependency
        <$> o .: "determiners"
        <*> o .: "determined"
  
  instance A.ToJSON FunctionalDependency where
    toJSON FunctionalDependency{..} =
      A.object [ "determiners" .= fdDeterminers
               , "determined" .= fdDetermined
               ]
  
  -- | The initial environment with no values and only the default javascript types defined
  initEnvironment :: Environment
  initEnvironment = Environment M.empty allPrimTypes M.empty M.empty M.empty allPrimClasses
  
  -- | A constructor for TypeClassData that computes which type class arguments are fully determined
  -- and argument covering sets.
  -- Fully determined means that this argument cannot be used when selecting a type class instance.
  -- A covering set is a minimal collection of arguments that can be used to find an instance and
  -- therefore determine all other type arguments.
  --
  -- An example of the difference between determined and fully determined would be with the class:
  -- ```class C a b c | a -> b, b -> a, b -> c```
  -- In this case, `a` must differ when `b` differs, and vice versa - each is determined by the other.
  -- Both `a` and `b` can be used in selecting a type class instance. However, `c` cannot - it is
  -- fully determined by `a` and `b`.
  --
  -- Define a graph of type class arguments with edges being fundep determiners to determined. Each
  -- argument also has a self looping edge.
  -- An argument is fully determined if doesn't appear at the start of a path of strongly connected components.
  -- An argument is not fully determined otherwise.
  --
  -- The way we compute this is by saying: an argument X is fully determined if there are arguments that
  -- determine X that X does not determine. This is the same thing: everything X determines includes everything
  -- in its SCC, and everything determining X is either before it in an SCC path, or in the same SCC.
  makeTypeClassData
    :: [(Text, Maybe SourceType)]
    -> [(Ident, SourceType)]
    -> [SourceConstraint]
    -> [FunctionalDependency]
    -> Bool
    -> TypeClassData
  makeTypeClassData args m s deps = TypeClassData args m' s deps determinedArgs coveringSets
    where
      ( determinedArgs, coveringSets ) = computeCoveringSets (length args) deps
  
      coveringSets' = S.toList coveringSets
  
      m' = map (\(a, b) -> (a, b, addVtaInfo b)) m
      
      addVtaInfo :: SourceType -> Maybe (S.Set (NEL.NonEmpty Int))
      addVtaInfo memberTy = do
        let mentionedArgIndexes = S.fromList (mapMaybe argToIndex $ freeTypeVariables memberTy)
        let leftovers = map (`S.difference` mentionedArgIndexes) coveringSets'
        S.fromList <$> traverse (NEL.nonEmpty . S.toList) leftovers
  
      argToIndex :: Text -> Maybe Int
      argToIndex = flip M.lookup $ M.fromList (zipWith ((,) . fst) args [0..])
  
  -- A moving frontier of sets to consider, along with the fundeps that can be
  -- applied in each case. At each stage, all sets in the frontier will be the
  -- same size, decreasing by 1 each time.
  type Frontier = M.Map IS.IntSet (First (IM.IntMap (NEL.NonEmpty IS.IntSet)))
  --                         ^                 ^          ^          ^
  --         when *these* parameters           |          |          |
  --         are still needed,                 |          |          |
  --                              *these* parameters      |          |
  --                              can be determined       |          |
  --                                         from a non-zero         |
  --                                         number of fundeps,      |
  --                                                      which accept *these*
  --                                                      parameters as inputs.
  
  computeCoveringSets :: Int -> [FunctionalDependency] -> (S.Set Int, S.Set (S.Set Int))
  computeCoveringSets nargs deps = ( determinedArgs, coveringSets )
    where
      argumentIndices = S.fromList [0 .. nargs - 1]
  
      -- Compute all sets of arguments that determine the remaining arguments via
      -- functional dependencies. This is done in stages, where each stage
      -- considers sets of the same size to share work.
      allCoveringSets :: S.Set (S.Set Int)
      allCoveringSets = S.map (S.fromDistinctAscList . IS.toAscList) $ fst $ search $
        -- The initial frontier consists of just the set of all parameters and all
        -- fundeps organized into the map structure.
        M.singleton
          (IS.fromList [0 .. nargs - 1]) $
            First $ IM.fromListWith (<>) $ do
              fd <- deps
              let srcs = pure (IS.fromList (fdDeterminers fd))
              tgt <- fdDetermined fd
              pure (tgt, srcs)
  
        where
  
        -- Recursively advance the frontier until all frontiers are exhausted
        -- and coverings sets found. The covering sets found during the process
        -- are locally-minimal, in that none can be reduced by a fundep, but
        -- there may be subsets found from other frontiers.
        search :: Frontier -> (S.Set IS.IntSet, ())
        search frontier = unless (null frontier) $ M.foldMapWithKey step frontier >>= search
  
        -- The input set from the frontier is known to cover all parameters, but
        -- it may be able to be reduced by more fundeps.
        step :: IS.IntSet -> First (IM.IntMap (NEL.NonEmpty IS.IntSet)) -> (S.Set IS.IntSet, Frontier)
        step needed (First inEdges)
          -- If there are no applicable fundeps, record it as a locally minimal
          -- covering set. This has already been reduced to only applicable fundeps
          | IM.null inEdges = (S.singleton needed, M.empty)
          | otherwise       = (S.empty, foldMap removeParameter paramsToTry)
  
            where
  
            determined = IM.keys inEdges
            -- If there is an acyclically determined functional dependency, prefer
            -- it to reduce the number of cases to check. That is a dependency
            -- that does not help determine other parameters.
            acycDetermined = find (`IS.notMember` (IS.unions $ concatMap NEL.toList $ IM.elems inEdges)) determined
            paramsToTry = maybe determined pure acycDetermined
  
            -- For each parameter to be removed to build the next frontier,
            -- delete the fundeps that determine it and filter out the fundeps
            -- that make use of it. Of course, if it an acyclic fundep we already
            -- found that there are none that use it.
            removeParameter :: Int -> Frontier
            removeParameter y =
              M.singleton
                (IS.delete y needed) $
                  case acycDetermined of
                    Just _ -> First $ IM.delete y inEdges
                    Nothing ->
                      First $ IM.mapMaybe (NEL.nonEmpty . NEL.filter (y `IS.notMember`)) $ IM.delete y inEdges
  
      -- Reduce to the inclusion-minimal sets
      coveringSets = S.filter (\v -> not (any (\c -> c `S.isProperSubsetOf` v) allCoveringSets)) allCoveringSets
  
      -- An argument is determined if it is in no covering set
      determinedArgs = argumentIndices `S.difference` fold coveringSets
  
  -- | The visibility of a name in scope
  data NameVisibility
    = Undefined
    -- ^ The name is defined in the current binding group, but is not visible
    | Defined
    -- ^ The name is defined in the another binding group, or has been made visible by a function binder
    deriving (Show, Eq, Generic)
  
  instance NFData NameVisibility
  instance Serialise NameVisibility
  
  -- | A flag for whether a name is for an private or public value - only public values will be
  -- included in a generated externs file.
  data NameKind
    = Private
    -- ^ A private value introduced as an artifact of code generation (class instances, class member
    -- accessors, etc.)
    | Public
    -- ^ A public value for a module member or foreign import declaration
    | External
    -- ^ A name for member introduced by foreign import
    deriving (Show, Eq, Generic)
  
  instance NFData NameKind
  instance Serialise NameKind
  
  -- | The kinds of a type
  data TypeKind
    = DataType DataDeclType [(Text, Maybe SourceType, Role)] [(ProperName 'ConstructorName, [SourceType])]
    -- ^ Data type
    | TypeSynonym
    -- ^ Type synonym
    | ExternData [Role]
    -- ^ Foreign data
    | LocalTypeVariable
    -- ^ A local type variable
    | ScopedTypeVar
    -- ^ A scoped type variable
    deriving (Show, Eq, Generic)
  
  instance NFData TypeKind
  instance Serialise TypeKind
  
  -- | The type ('data' or 'newtype') of a data type declaration
  data DataDeclType
    = Data
    -- ^ A standard data constructor
    | Newtype
    -- ^ A newtype constructor
    deriving (Show, Eq, Ord, Generic)
  
  instance NFData DataDeclType
  instance Serialise DataDeclType
  
  showDataDeclType :: DataDeclType -> Text
  showDataDeclType Data = "data"
  showDataDeclType Newtype = "newtype"
  
  instance A.ToJSON DataDeclType where
    toJSON = A.toJSON . showDataDeclType
  
  instance A.FromJSON DataDeclType where
    parseJSON = A.withText "DataDeclType" $ \case
      "data" -> return Data
      "newtype" -> return Newtype
      other -> fail $ "invalid type: '" ++ T.unpack other ++ "'"
  
  -- | Kind of ground types
  kindType :: SourceType
  kindType = srcTypeConstructor C.Type
  
  kindConstraint :: SourceType
  kindConstraint = srcTypeConstructor C.Constraint
  
  kindSymbol :: SourceType
  kindSymbol = srcTypeConstructor C.Symbol
  
  kindDoc :: SourceType
  kindDoc = srcTypeConstructor C.Doc
  
  kindOrdering :: SourceType
  kindOrdering = srcTypeConstructor C.TypeOrdering
  
  kindRowList :: SourceType -> SourceType
  kindRowList = TypeApp nullSourceAnn (srcTypeConstructor C.RowList)
  
  kindRow :: SourceType -> SourceType
  kindRow = TypeApp nullSourceAnn (srcTypeConstructor C.Row)
  
  kindOfREmpty :: SourceType
  kindOfREmpty = tyForall "k" kindType (kindRow (tyVar "k"))
  
  -- | Type constructor for functions
  tyFunction :: SourceType
  tyFunction = srcTypeConstructor C.Function
  
  -- | Type constructor for strings
  tyString :: SourceType
  tyString = srcTypeConstructor C.String
  
  -- | Type constructor for strings
  tyChar :: SourceType
  tyChar = srcTypeConstructor C.Char
  
  -- | Type constructor for numbers
  tyNumber :: SourceType
  tyNumber = srcTypeConstructor C.Number
  
  -- | Type constructor for integers
  tyInt :: SourceType
  tyInt = srcTypeConstructor C.Int
  
  -- | Type constructor for booleans
  tyBoolean :: SourceType
  tyBoolean = srcTypeConstructor C.Boolean
  
  -- | Type constructor for arrays
  tyArray :: SourceType
  tyArray = srcTypeConstructor C.Array
  
  -- | Type constructor for records
  tyRecord :: SourceType
  tyRecord = srcTypeConstructor C.Record
  
  tyVar :: Text -> SourceType
  tyVar = TypeVar nullSourceAnn
  
  tyForall :: Text -> SourceType -> SourceType -> SourceType
  tyForall var k ty = ForAll nullSourceAnn TypeVarInvisible var (Just k) ty Nothing
  
  -- | Smart constructor for function types
  function :: SourceType -> SourceType -> SourceType
  function = TypeApp nullSourceAnn . TypeApp nullSourceAnn tyFunction
  
  -- To make reading the kind signatures below easier
  (-:>) :: SourceType -> SourceType -> SourceType
  (-:>) = function
  infixr 4 -:>
  
  primClass :: Qualified (ProperName 'ClassName) -> (SourceType -> SourceType) -> [(Qualified (ProperName 'TypeName), (SourceType, TypeKind))]
  primClass name mkKind =
    [ let k = mkKind kindConstraint
      in (coerceProperName <$> name, (k, ExternData (nominalRolesForKind k)))
    , let k = mkKind kindType
      in (dictTypeName . coerceProperName <$> name, (k, TypeSynonym))
    ]
  
  -- | The primitive types in the external environment with their
  -- associated kinds. There are also pseudo `Fail`, `Warn`, and `Partial` types
  -- that correspond to the classes with the same names.
  primTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
  primTypes =
    M.fromList
      [ (C.Type,                         (kindType, ExternData []))
      , (C.Constraint,                   (kindType, ExternData []))
      , (C.Symbol,                       (kindType, ExternData []))
      , (C.Row,                          (kindType -:> kindType, ExternData [Phantom]))
      , (C.Function,                     (kindType -:> kindType -:> kindType, ExternData [Representational, Representational]))
      , (C.Array,                        (kindType -:> kindType, ExternData [Representational]))
      , (C.Record,                       (kindRow kindType -:> kindType, ExternData [Representational]))
      , (C.String,                       (kindType, ExternData []))
      , (C.Char,                         (kindType, ExternData []))
      , (C.Number,                       (kindType, ExternData []))
      , (C.Int,                          (kindType, ExternData []))
      , (C.Boolean,                      (kindType, ExternData []))
      , (C.Partial <&> coerceProperName, (kindConstraint, ExternData []))
      ]
  
  -- | This 'Map' contains all of the prim types from all Prim modules.
  allPrimTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
  allPrimTypes = M.unions
    [ primTypes
    , primBooleanTypes
    , primCoerceTypes
    , primOrderingTypes
    , primRowTypes
    , primRowListTypes
    , primSymbolTypes
    , primIntTypes
    , primTypeErrorTypes
    ]
  
  primBooleanTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
  primBooleanTypes =
    M.fromList
      [ (C.True, (tyBoolean, ExternData []))
      , (C.False, (tyBoolean, ExternData []))
      ]
  
  primCoerceTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
  primCoerceTypes =
    M.fromList $ mconcat
      [ primClass C.Coercible (\kind -> tyForall "k" kindType $ tyVar "k" -:> tyVar "k" -:> kind)
      ]
  
  primOrderingTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
  primOrderingTypes =
    M.fromList
      [ (C.TypeOrdering, (kindType, ExternData []))
      , (C.LT, (kindOrdering, ExternData []))
      , (C.EQ, (kindOrdering, ExternData []))
      , (C.GT, (kindOrdering, ExternData []))
      ]
  
  primRowTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
  primRowTypes =
    M.fromList $ mconcat
      [ primClass C.RowUnion (\kind -> tyForall "k" kindType $ kindRow (tyVar "k") -:> kindRow (tyVar "k") -:> kindRow (tyVar "k") -:> kind)
      , primClass C.RowNub   (\kind -> tyForall "k" kindType $ kindRow (tyVar "k") -:> kindRow (tyVar "k") -:> kind)
      , primClass C.RowLacks (\kind -> tyForall "k" kindType $ kindSymbol -:> kindRow (tyVar "k") -:> kind)
      , primClass C.RowCons  (\kind -> tyForall "k" kindType $ kindSymbol -:> tyVar "k" -:> kindRow (tyVar "k") -:> kindRow (tyVar "k") -:> kind)
      ]
  
  primRowListTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
  primRowListTypes =
    M.fromList $
      [ (C.RowList, (kindType -:> kindType, ExternData [Phantom]))
      , (C.RowListCons, (tyForall "k" kindType $ kindSymbol -:> tyVar "k" -:> kindRowList (tyVar "k") -:> kindRowList (tyVar "k"), ExternData [Phantom, Phantom, Phantom]))
      , (C.RowListNil, (tyForall "k" kindType $ kindRowList (tyVar "k"), ExternData []))
      ] <> mconcat
      [ primClass C.RowToList  (\kind -> tyForall "k" kindType $ kindRow (tyVar "k") -:> kindRowList (tyVar "k") -:> kind)
      ]
  
  primSymbolTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
  primSymbolTypes =
    M.fromList $ mconcat
      [ primClass C.SymbolAppend  (\kind -> kindSymbol -:> kindSymbol -:> kindSymbol -:> kind)
      , primClass C.SymbolCompare (\kind -> kindSymbol -:> kindSymbol -:> kindOrdering -:> kind)
      , primClass C.SymbolCons    (\kind -> kindSymbol -:> kindSymbol -:> kindSymbol -:> kind)
      ]
  
  primIntTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
  primIntTypes =
    M.fromList $ mconcat
      [ primClass C.IntAdd      (\kind -> tyInt -:> tyInt -:> tyInt -:> kind)
      , primClass C.IntCompare  (\kind -> tyInt -:> tyInt -:> kindOrdering -:> kind)
      , primClass C.IntMul      (\kind -> tyInt -:> tyInt -:> tyInt -:> kind)
      , primClass C.IntToString (\kind -> tyInt -:> kindSymbol -:> kind)
      ]
  
  primTypeErrorTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
  primTypeErrorTypes =
    M.fromList $
      [ (C.Doc, (kindType, ExternData []))
      , (C.Fail <&> coerceProperName, (kindDoc -:> kindConstraint, ExternData [Nominal]))
      , (C.Warn <&> coerceProperName, (kindDoc -:> kindConstraint, ExternData [Nominal]))
      , (C.Text, (kindSymbol -:> kindDoc, ExternData [Phantom]))
      , (C.Quote, (tyForall "k" kindType $ tyVar "k" -:> kindDoc, ExternData [Phantom]))
      , (C.QuoteLabel, (kindSymbol -:> kindDoc, ExternData [Phantom]))
      , (C.Beside, (kindDoc -:> kindDoc -:> kindDoc, ExternData [Phantom, Phantom]))
      , (C.Above, (kindDoc -:> kindDoc -:> kindDoc, ExternData [Phantom, Phantom]))
      ] <> mconcat
      [ primClass C.Fail (\kind -> kindDoc -:> kind)
      , primClass C.Warn (\kind -> kindDoc -:> kind)
      ]
  
  -- | The primitive class map. This just contains the `Partial` class.
  -- `Partial` is used as a kind of magic constraint for partial functions.
  primClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
  primClasses =
    M.fromList
      [ (C.Partial, makeTypeClassData [] [] [] [] True)
      ]
  
  -- | This contains all of the type classes from all Prim modules.
  allPrimClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
  allPrimClasses = M.unions
    [ primClasses
    , primCoerceClasses
    , primRowClasses
    , primRowListClasses
    , primSymbolClasses
    , primIntClasses
    , primTypeErrorClasses
    ]
  
  primCoerceClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
  primCoerceClasses =
    M.fromList
      -- class Coercible (a :: k) (b :: k)
      [ (C.Coercible, makeTypeClassData
          [ ("a", Just (tyVar "k"))
          , ("b", Just (tyVar "k"))
          ] [] [] [] True)
      ]
  
  primRowClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
  primRowClasses =
    M.fromList
      -- class Union (left :: Row k) (right :: Row k) (union :: Row k) | left right -> union, right union -> left, union left -> right
      [ (C.RowUnion, makeTypeClassData
          [ ("left", Just (kindRow (tyVar "k")))
          , ("right", Just (kindRow (tyVar "k")))
          , ("union", Just (kindRow (tyVar "k")))
          ] [] []
          [ FunctionalDependency [0, 1] [2]
          , FunctionalDependency [1, 2] [0]
          , FunctionalDependency [2, 0] [1]
          ] True)
  
      -- class Nub (original :: Row k) (nubbed :: Row k) | original -> nubbed
      , (C.RowNub, makeTypeClassData
          [ ("original", Just (kindRow (tyVar "k")))
          , ("nubbed", Just (kindRow (tyVar "k")))
          ] [] []
          [ FunctionalDependency [0] [1]
          ] True)
  
      -- class Lacks (label :: Symbol) (row :: Row k)
      , (C.RowLacks, makeTypeClassData
          [ ("label", Just kindSymbol)
          , ("row", Just (kindRow (tyVar "k")))
          ] [] [] [] True)
  
      -- class RowCons (label :: Symbol) (a :: k) (tail :: Row k) (row :: Row k) | label tail a -> row, label row -> tail a
      , (C.RowCons, makeTypeClassData
          [ ("label", Just kindSymbol)
          , ("a", Just (tyVar "k"))
          , ("tail", Just (kindRow (tyVar "k")))
          , ("row", Just (kindRow (tyVar "k")))
          ] [] []
          [ FunctionalDependency [0, 1, 2] [3]
          , FunctionalDependency [0, 3] [1, 2]
          ] True)
      ]
  
  primRowListClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
  primRowListClasses =
    M.fromList
      -- class RowToList (row :: Row k) (list :: RowList k) | row -> list
      [ (C.RowToList, makeTypeClassData
          [ ("row", Just (kindRow (tyVar "k")))
          , ("list", Just (kindRowList (tyVar "k")))
          ] [] []
          [ FunctionalDependency [0] [1]
          ] True)
      ]
  
  primSymbolClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
  primSymbolClasses =
    M.fromList
      -- class Append (left :: Symbol) (right :: Symbol) (appended :: Symbol) | left right -> appended, right appended -> left, appended left -> right
      [ (C.SymbolAppend, makeTypeClassData
          [ ("left", Just kindSymbol)
          , ("right", Just kindSymbol)
          , ("appended", Just kindSymbol)
          ] [] []
          [ FunctionalDependency [0, 1] [2]
          , FunctionalDependency [1, 2] [0]
          , FunctionalDependency [2, 0] [1]
          ] True)
  
      -- class Compare (left :: Symbol) (right :: Symbol) (ordering :: Ordering) | left right -> ordering
      , (C.SymbolCompare, makeTypeClassData
          [ ("left", Just kindSymbol)
          , ("right", Just kindSymbol)
          , ("ordering", Just kindOrdering)
          ] [] []
          [ FunctionalDependency [0, 1] [2]
          ] True)
  
      -- class Cons (head :: Symbol) (tail :: Symbol) (symbol :: Symbol) | head tail -> symbol, symbol -> head tail
      , (C.SymbolCons, makeTypeClassData
          [ ("head", Just kindSymbol)
          , ("tail", Just kindSymbol)
          , ("symbol", Just kindSymbol)
          ] [] []
          [ FunctionalDependency [0, 1] [2]
          , FunctionalDependency [2] [0, 1]
          ] True)
      ]
  
  primIntClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
  primIntClasses =
    M.fromList
      -- class Add (left :: Int) (right :: Int) (sum :: Int) | left right -> sum, left sum -> right, right sum -> left
      [ (C.IntAdd, makeTypeClassData
          [ ("left", Just tyInt)
          , ("right", Just tyInt)
          , ("sum", Just tyInt)
          ] [] []
          [ FunctionalDependency [0, 1] [2]
          , FunctionalDependency [0, 2] [1]
          , FunctionalDependency [1, 2] [0]
          ] True)
  
      -- class Compare (left :: Int) (right :: Int) (ordering :: Ordering) | left right -> ordering
      , (C.IntCompare, makeTypeClassData
          [ ("left", Just tyInt)
          , ("right", Just tyInt)
          , ("ordering", Just kindOrdering)
          ] [] []
          [ FunctionalDependency [0, 1] [2]
          ] True)
  
      -- class Mul (left :: Int) (right :: Int) (product :: Int) | left right -> product
      , (C.IntMul, makeTypeClassData
          [ ("left", Just tyInt)
          , ("right", Just tyInt)
          , ("product", Just tyInt)
          ] [] []
          [ FunctionalDependency [0, 1] [2]
          ] True)
  
      -- class ToString (int :: Int) (string :: Symbol) | int -> string
      , (C.IntToString, makeTypeClassData
          [ ("int", Just tyInt)
          , ("string", Just kindSymbol)
          ] [] []
          [ FunctionalDependency [0] [1]
          ] True)
      ]
  
  primTypeErrorClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
  primTypeErrorClasses =
    M.fromList
      -- class Fail (message :: Symbol)
      [ (C.Fail, makeTypeClassData
          [("message", Just kindDoc)] [] [] [] True)
  
      -- class Warn (message :: Symbol)
      , (C.Warn, makeTypeClassData
          [("message", Just kindDoc)] [] [] [] True)
      ]
  
  -- | Finds information about data constructors from the current environment.
  lookupConstructor :: Environment -> Qualified (ProperName 'ConstructorName) -> (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
  lookupConstructor env ctor =
    fromMaybe (internalError "Data constructor not found") $ ctor `M.lookup` dataConstructors env
  
  -- | Finds information about values from the current environment.
  lookupValue :: Environment -> Qualified Ident -> Maybe (SourceType, NameKind, NameVisibility)
  lookupValue env ident = ident `M.lookup` names env
  
  dictTypeName' :: Text -> Text
  dictTypeName' = (<> "$Dict")
  
  dictTypeName :: ProperName a -> ProperName a
  dictTypeName = ProperName . dictTypeName' . runProperName
  
  isDictTypeName :: ProperName a -> Bool
  isDictTypeName = T.isSuffixOf "$Dict" . runProperName
  
  -- |
  -- Given the kind of a type, generate a list @Nominal@ roles. This is used for
  -- opaque foreign types as well as type classes.
  nominalRolesForKind :: Type a -> [Role]
  nominalRolesForKind k = replicate (kindArity k) Nominal
  
  kindArity :: Type a -> Int
  kindArity = length . fst . unapplyKinds
  
  unapplyKinds :: Type a -> ([Type a], Type a)
  unapplyKinds = go [] where
    go kinds (TypeApp _ (TypeApp _ fn k1) k2)
      | eqType fn tyFunction = go (k1 : kinds) k2
    go kinds (ForAll _ _ _ _ k _) = go kinds k
    go kinds k = (reverse kinds, k)
  