Type System

-- | Types with annotation parameter
data Type a
  = TUnknown a Int                                      -- Unknown type variable
  | TypeVar a Text                                      -- Type variable
  | TypeLevelString a PSString                          -- Type-level string
  | TypeLevelInt a Integer                             -- Type-level integer
  | TypeWildcard a (Maybe Text)                        -- Type wildcard _
  | TypeConstructor a (Qualified (ProperName 'TypeName)) -- Type constructor
  | TypeOp a (Qualified (OpName 'TypeOpName))         -- Type operator
  | TypeApp a (Type a) (Type a)                       -- Type application
  | KindApp a (Type a) (Type a)                       -- Kind application
  | ForAll a TypeVarVisibility (ProperName 'TypeName) (Maybe (Type a)) (Type a) (Maybe SkolemScope) -- Universal quantification
  | ConstrainedType a (Constraint a) (Type a)         -- Constrained type
  | Skolem a Text (Maybe (Type a)) Int SkolemScope    -- Skolem variable
  | REmpty a                                           -- Empty row
  | RCons a Label (Type a) (Type a)                   -- Row cons
  | KindedType a (Type a) (Type a)                    -- Kind annotation
  | BinaryNoParensType a (Type a) (Type a) (Type a)   -- Binary operator (no parens)
  | ParensInType a (Type a)                           -- Parentheses in type

-- | Source types (types with source annotations)
type SourceType = Type SourceAnn

-- | Type constraints
data Constraint a = Constraint a (Qualified (ProperName 'ClassName)) [Type a] (Maybe ConstraintData)

-- | Source constraints
type SourceConstraint = Constraint SourceAnn

-- | Kinds (types of types)
type SourceKind = Type SourceAnn

-- | Kind inference
inferKind :: SourceType -> InferM SourceKind

-- | Check kind
checkKind :: SourceType -> SourceKind -> InferM ()

-- | Kind of a type constructor
kindOf :: Environment -> Qualified (ProperName 'TypeName) -> Maybe SourceKind

-- | Built-in kinds
kindType :: SourceKind      -- Type (kind of ordinary types)
kindConstraint :: SourceKind -- Constraint (kind of type class constraints)
kindSymbol :: SourceKind     -- Symbol (kind of type-level strings)
kindRowWildcard :: SourceKind -- RowList (kind of row lists)

-- | Type variable visibility
data TypeVarVisibility = TypeVarVisible | TypeVarInvisible

-- | Skolem scope for rank-N types
data SkolemScope = SkolemScope Int

-- | Unknown type variable
data Unknown = Unknown Int

-- | Generate fresh type variables
freshType :: MonadSupply m => m SourceType

-- | Generate fresh kind variables  
freshKind :: MonadSupply m => m SourceKind

-- | Create skolem type
skolemize :: Text -> Int -> SkolemScope -> Maybe SourceKind -> SourceType

-- | Check if type contains skolems
containsSkolems :: Type a -> Bool

-- | Type substitution
type Substitution = M.Map Int SourceType

-- | Empty substitution
emptySubstitution :: Substitution

-- | Compose substitutions
composeSubstitutions :: Substitution -> Substitution -> Substitution

-- | Apply substitution to type
applySubstitution :: Substitution -> SourceType -> SourceType

-- | Apply substitution to constraint
applySubstitutionToConstraint :: Substitution -> SourceConstraint -> SourceConstraint

-- | Get free type variables
freeTypeVariables :: Type a -> S.Set Int

-- | Get unknown type variables
unknowns :: Type a -> S.Set Int

-- | Unify two types
unifyTypes :: SourceType -> SourceType -> UnifyT SourceType

-- | Unify type lists
unifyMany :: [SourceType] -> [SourceType] -> UnifyT [SourceType]

-- | Most general unifier
mgu :: SourceType -> SourceType -> Either ErrorMessage Substitution

-- | Occurs check
occursCheck :: Int -> SourceType -> Bool

-- | Unification error
data UnificationError
  = UnificationFailed SourceType SourceType
  | InfiniteType Int SourceType
  | MultipleUnificationErrors [UnificationError]

-- | Row operations
data RowListItem = RowListItem
  { rowListType :: SourceType
  , rowListIndex :: Int
  }

-- | Convert row to list
rowToList :: Type a -> ([RowListItem], Type a)

-- | Convert list to row
rowFromList :: ([RowListItem], Type a) -> Type a

-- | Row difference
rowDifference :: Type a -> Type a -> Type a

-- | Check if row contains label
rowContainsLabel :: Label -> Type a -> Bool

-- | Free variables in row
freeVariablesInRow :: Type a -> S.Set Int

-- | Constraint data for functional dependencies
data ConstraintData = ConstraintData [Int] [FunctionalDependency] Bool

-- | Functional dependency
data FunctionalDependency = FunctionalDependency [Int] [Int]

-- | Type class dictionary
data TypeClassDictionaryInScope = TypeClassDictionaryInScope
  { tcdName :: Qualified Ident
  , tcdClassName :: Qualified (ProperName 'ClassName)
  , tcdInstanceTypes :: [SourceType]
  , tcdDependencies :: Maybe [Qualified Ident]
  }

-- | Entailment relation
entails :: [SourceConstraint] -> SourceConstraint -> Bool

-- | Constraint solving
solveConstraints :: [SourceConstraint] -> Either ErrorMessage [TypeClassDictionaryInScope]

-- | Infer expression type
inferType :: Environment -> Expr -> InferM (Expr, SourceType)

-- | Check expression against type
checkType :: Environment -> Expr -> SourceType -> InferM Expr

-- | Infer declaration types
inferDeclaration :: Environment -> Declaration -> InferM (Environment, Declaration)

-- | Type generalization
generalize :: Environment -> SourceType -> InferM SourceType

-- | Type instantiation
instantiate :: SourceType -> InferM SourceType

-- | Pretty print options
data TypeRenderOptions = TypeRenderOptions
  { troSugarRows :: Bool      -- Sugar record/variant syntax
  , troUnicodeArrows :: Bool  -- Use unicode arrows
  , troPreferTypeConstructors :: Bool -- Prefer type constructors over operators
  }

-- | Default pretty print options
defaultTypeRenderOptions :: TypeRenderOptions

-- | Pretty print type
prettyPrintType :: Int -> Type a -> String

-- | Pretty print type with options
prettyPrintTypeWithOptions :: TypeRenderOptions -> Int -> Type a -> String

-- | Pretty print constraint
prettyPrintConstraint :: Constraint a -> String

-- | Render type as text
renderType :: Type a -> Text

-- | Check if type is monomorphic
isMonoType :: Type a -> Bool

-- | Get type constructor
getTypeConstructor :: Type a -> Maybe (Qualified (ProperName 'TypeName))

-- | Check if types are equal (ignoring annotations)
eqType :: Type a -> Type b -> Bool

-- | Get type head (outermost constructor)
typeHead :: Type a -> Maybe (Qualified (ProperName 'TypeName))

-- | Collect type variables
collectTypeVars :: Type a -> [Text]

-- | Replace type variables
replaceTypeVars :: M.Map Text (Type a) -> Type a -> Type a

-- | Check if type is function type
isFunctionType :: Type a -> Bool

-- | Decompose function type
uncurryType :: Type a -> ([Type a], Type a)

-- | Built-in type constructors
tyFunction :: SourceType -> SourceType -> SourceType    -- Function type (->)
tyString :: SourceType                                  -- String
tyChar :: SourceType                                    -- Char  
tyInt :: SourceType                                     -- Int
tyNumber :: SourceType                                  -- Number
tyBoolean :: SourceType                                 -- Boolean
tyArray :: SourceType -> SourceType                     -- Array
tyRecord :: SourceType -> SourceType                    -- Record (row type)
tyVariant :: SourceType -> SourceType                   -- Variant (row type)

-- | Prim module types
primSubstitution :: M.Map (Qualified (ProperName 'TypeName)) SourceType

-- | Check if type is built-in
isBuiltinType :: Qualified (ProperName 'TypeName) -> Bool

-- | Record/variant labels
newtype Label = Label PSString

-- | Label utilities
runLabel :: Label -> PSString
mkLabel :: PSString -> Label

-- | Record type operations
recordType :: [(Label, SourceType)] -> SourceType
recordLookup :: Label -> SourceType -> Maybe SourceType
recordUpdate :: Label -> SourceType -> SourceType -> SourceType
recordDelete :: Label -> SourceType -> SourceType

-- | Type environment for inference
data Environment = Environment
  { names :: M.Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
  , types :: M.Map (Qualified (ProperName 'TypeName)) (SourceKind, TypeKind)
  , dataConstructors :: M.Map (Qualified (ProperName 'ConstructorName)) (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
  , typeSynonyms :: M.Map (Qualified (ProperName 'TypeName)) ([(Text, Maybe SourceKind)], SourceType)
  , typeClassDictionaries :: [TypeClassDictionaryInScope]
  , typeClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
  , roles :: M.Map (Qualified (ProperName 'TypeName)) [Role]
  }

-- | Empty environment
emptyEnvironment :: Environment

-- | Combine environments
combineEnvironments :: Environment -> Environment -> Environment

-- | Lookup name in environment
lookupValue :: Environment -> Qualified Ident -> Maybe (SourceType, NameKind, NameVisibility)

-- | Lookup type in environment
lookupType :: Environment -> Qualified (ProperName 'TypeName) -> Maybe (SourceKind, TypeKind)