From 68330ed53b988eea1b0fa3f626629c5a42f66734 Mon Sep 17 00:00:00 2001 From: Michal Kozakiewicz Date: Sun, 12 Apr 2026 11:30:05 +0000 Subject: [PATCH 1/5] Optimize replaceAllTypeSynonyms with per-node TypeFlags MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add a TypeFlags field to every Type constructor that caches structural properties of the subtree. Pattern synonyms auto-compute flags on construction and ignore them on matching, so existing code is unchanged. Three flags are tracked: - tfHasWildcards: subtree contains TypeWildcard nodes - tfHasUnscopedForAlls: subtree contains ForAll without SkolemScope - tfSynonymsFree: subtree has been fully synonym-expanded This enables short-circuiting in three hot traversals: - replaceAllTypeSynonyms skips types already marked synonym-free - replaceTypeWildcards skips types with no wildcards - introduceSkolemScope skips types with no unscoped ForAlls The synonym expansion also uses a custom single-pass traversal that both expands synonyms and marks all output nodes as synonym-free, so subsequent calls on the same type or any subtree return in O(1). Profile results (pr-admin, 1758 modules): - replaceAllTypeSynonyms'.go: 16.9% → 0.1% - introduceSkolemScope: 2.4% → 0.0% - replaceTypeWildcards: 2.2% → 0.0% - Full build wall time: ~72s → ~65s (~10% faster) Co-Authored-By: Claude Opus 4.6 (1M context) --- .../PureScript/TypeChecker/Skolems.hs | 11 +- .../PureScript/TypeChecker/Synonyms.hs | 102 +++++- src/Language/PureScript/TypeChecker/Unify.hs | 9 +- src/Language/PureScript/Types.hs | 312 ++++++++++++++---- tests/TestAst.hs | 6 +- 5 files changed, 363 insertions(+), 77 deletions(-) diff --git a/src/Language/PureScript/TypeChecker/Skolems.hs b/src/Language/PureScript/TypeChecker/Skolems.hs index aa49997fd6..2a8700149f 100644 --- a/src/Language/PureScript/TypeChecker/Skolems.hs +++ b/src/Language/PureScript/TypeChecker/Skolems.hs @@ -21,7 +21,7 @@ import Language.PureScript.Crash (internalError) import Language.PureScript.Errors (ErrorMessage(..), MultipleErrors, SimpleErrorMessage(..), positionedError, singleError) import Language.PureScript.Traversals (defS) import Language.PureScript.TypeChecker.Monad (CheckState(..)) -import Language.PureScript.Types (SkolemScope(..), SourceType, Type(..), everythingOnTypes, everywhereOnTypesM, replaceTypeVars) +import Language.PureScript.Types (SkolemScope(..), SourceType, Type(..), everythingOnTypes, everywhereOnTypesM, hasFlag, replaceTypeVars, tfHasUnscopedForAlls, typeFlags) -- | Generate a new skolem constant newSkolemConstant :: MonadState CheckState m => m Int @@ -30,11 +30,14 @@ newSkolemConstant = do modify $ \st -> st { checkNextSkolem = s + 1 } return s --- | Introduce skolem scope at every occurrence of a ForAll +-- | Introduce skolem scope at every occurrence of a ForAll. +-- Short-circuits if the type has no unscoped ForAlls. introduceSkolemScope :: MonadState CheckState m => Type a -> m (Type a) -introduceSkolemScope = everywhereOnTypesM go +introduceSkolemScope ty + | not (hasFlag tfHasUnscopedForAlls (typeFlags ty)) = return ty + | otherwise = everywhereOnTypesM go ty where - go (ForAll ann vis ident mbK ty Nothing) = ForAll ann vis ident mbK ty <$> (Just <$> newSkolemScope) + go (ForAll ann vis ident mbK t Nothing) = ForAll ann vis ident mbK t <$> (Just <$> newSkolemScope) go other = return other -- | Generate a new skolem scope diff --git a/src/Language/PureScript/TypeChecker/Synonyms.hs b/src/Language/PureScript/TypeChecker/Synonyms.hs index 9672836d6a..ed8f89dfca 100644 --- a/src/Language/PureScript/TypeChecker/Synonyms.hs +++ b/src/Language/PureScript/TypeChecker/Synonyms.hs @@ -19,22 +19,71 @@ import Language.PureScript.Environment (Environment(..), TypeKind) import Language.PureScript.Errors (MultipleErrors, SimpleErrorMessage(..), SourceSpan, errorMessage') import Language.PureScript.Names (ProperName, ProperNameType(..), Qualified) import Language.PureScript.TypeChecker.Monad (getEnv, TypeCheckM) -import Language.PureScript.Types (SourceType, Type(..), completeBinderList, everywhereOnTypesTopDownM, getAnnForType, replaceAllTypeVars) +import Language.PureScript.Types + ( SourceType, Type(..), TypeFlags + , combineFlags, completeBinderList, constraintNodeFlags, forAllNodeFlags + , getAnnForType, hasFlag, overConstraintArgsAll, replaceAllTypeVars + , setFlag, skolemNodeFlags, tfSynonymsFree, typeFlags + ) -- | Type synonym information (arguments with kinds, aliased type), indexed by name type SynonymMap = M.Map (Qualified (ProperName 'TypeName)) ([(Text, Maybe SourceType)], SourceType) type KindMap = M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind) +-- | Replace fully applied type synonyms and mark every output node +-- with 'tfSynonymsFree'. Uses a custom traversal that: +-- +-- 1. Short-circuits on subtrees already marked synonym-free +-- 2. Only tries synonym expansion on potential application heads +-- 3. Sets 'tfSynonymsFree' on every output node in a single pass replaceAllTypeSynonyms' :: SynonymMap -> KindMap -> SourceType -> Either MultipleErrors SourceType -replaceAllTypeSynonyms' syns kinds = everywhereOnTypesTopDownM try +replaceAllTypeSynonyms' syns kinds + | M.null syns = Right . markSF + | otherwise = walk where - try :: SourceType -> Either MultipleErrors SourceType - try t = fromMaybe t <$> go (fst $ getAnnForType t) 0 [] [] t + sf :: TypeFlags -> TypeFlags + sf = setFlag tfSynonymsFree + + -- Mark a single node as synonym-free (no recursion) + markSF :: SourceType -> SourceType + markSF (TUnknown_ f a b) = TUnknown_ (sf f) a b + markSF (TypeVar_ f a b) = TypeVar_ (sf f) a b + markSF (TypeLevelString_ f a b) = TypeLevelString_ (sf f) a b + markSF (TypeLevelInt_ f a b) = TypeLevelInt_ (sf f) a b + markSF (TypeWildcard_ f a b) = TypeWildcard_ (sf f) a b + markSF (TypeConstructor_ f a b) = TypeConstructor_ (sf f) a b + markSF (TypeOp_ f a b) = TypeOp_ (sf f) a b + markSF (TypeApp_ f a t1 t2) = TypeApp_ (sf f) a t1 t2 + markSF (KindApp_ f a t1 t2) = KindApp_ (sf f) a t1 t2 + markSF (ForAll_ f a v i k t s) = ForAll_ (sf f) a v i k t s + markSF (ConstrainedType_ f a c t) = ConstrainedType_ (sf f) a c t + markSF (Skolem_ f a n k i s) = Skolem_ (sf f) a n k i s + markSF (REmpty_ f a) = REmpty_ (sf f) a + markSF (RCons_ f a l t r) = RCons_ (sf f) a l t r + markSF (KindedType_ f a t k) = KindedType_ (sf f) a t k + markSF (BinaryNoParensType_ f a t1 t2 t3) = BinaryNoParensType_ (sf f) a t1 t2 t3 + markSF (ParensInType_ f a t) = ParensInType_ (sf f) a t + + -- Main walk: try synonym expansion at potential application sites, + -- then recurse into children. Sets tfSynonymsFree on all output nodes. + walk :: SourceType -> Either MultipleErrors SourceType + walk t | hasFlag tfSynonymsFree (typeFlags t) = Right t + walk t@(TypeApp_ _ _ _ _) = trySyn t >>= walkChildren + walk t@(KindApp_ _ _ _ _) = trySyn t >>= walkChildren + walk t@(TypeConstructor_ _ _ _) = trySyn t >>= \t' -> case t' of + TypeConstructor_ _ _ _ -> Right (markSF t') -- leaf + _ -> walkChildren t' -- synonym expanded to non-leaf + walk t = walkChildren t + + -- Try to expand a synonym application at the root. + -- Uses the original 'go' logic to peel TypeApp/KindApp and find the constructor. + trySyn :: SourceType -> Either MultipleErrors SourceType + trySyn t = fromMaybe t <$> go (fst $ getAnnForType t) 0 [] [] t go :: SourceSpan -> Int -> [SourceType] -> [SourceType] -> SourceType -> Either MultipleErrors (Maybe SourceType) go ss c kargs args (TypeConstructor _ ctor) @@ -43,7 +92,7 @@ replaceAllTypeSynonyms' syns kinds = everywhereOnTypesTopDownM try , kindArgs <- lookupKindArgs ctor , length kargs == length kindArgs = let repl = replaceAllTypeVars (zip (map fst synArgs) args <> zip kindArgs kargs) body - in Just <$> try repl + in Just <$> trySyn repl | Just (synArgs, _) <- M.lookup ctor syns , length synArgs > c = throwError . errorMessage' ss $ PartiallyAppliedSynonym ctor @@ -51,11 +100,46 @@ replaceAllTypeSynonyms' syns kinds = everywhereOnTypesTopDownM try go ss c kargs args (KindApp _ f arg) = go ss c (arg : kargs) args f go _ _ _ _ _ = return Nothing + -- Walk children and reconstruct with recomputed structural flags + tfSynonymsFree. + -- Uses raw constructors to set flags in a single allocation. + walkChildren :: SourceType -> Either MultipleErrors SourceType + walkChildren (TypeApp_ _ ann t1 t2) = do + t1' <- walk t1; t2' <- walk t2 + return $! TypeApp_ (sf (typeFlags t1' `combineFlags` typeFlags t2')) ann t1' t2' + walkChildren (KindApp_ _ ann t1 t2) = do + t1' <- walk t1; t2' <- walk t2 + return $! KindApp_ (sf (typeFlags t1' `combineFlags` typeFlags t2')) ann t1' t2' + walkChildren (ForAll_ _ ann vis ident mbK ty sco) = do + mbK' <- traverse walk mbK; ty' <- walk ty + return $! ForAll_ (sf (forAllNodeFlags mbK' ty' sco)) ann vis ident mbK' ty' sco + walkChildren (ConstrainedType_ _ ann c ty) = do + c' <- overConstraintArgsAll (mapM walk) c; ty' <- walk ty + return $! ConstrainedType_ (sf (constraintNodeFlags c' ty')) ann c' ty' + walkChildren (Skolem_ _ ann name mbK i sc) = do + mbK' <- traverse walk mbK + return $! Skolem_ (sf (skolemNodeFlags mbK')) ann name mbK' i sc + walkChildren (RCons_ _ ann name ty rest) = do + ty' <- walk ty; rest' <- walk rest + return $! RCons_ (sf (typeFlags ty' `combineFlags` typeFlags rest')) ann name ty' rest' + walkChildren (KindedType_ _ ann ty k) = do + ty' <- walk ty; k' <- walk k + return $! KindedType_ (sf (typeFlags ty' `combineFlags` typeFlags k')) ann ty' k' + walkChildren (BinaryNoParensType_ _ ann t1 t2 t3) = do + t1' <- walk t1; t2' <- walk t2; t3' <- walk t3 + return $! BinaryNoParensType_ (sf (typeFlags t1' `combineFlags` typeFlags t2' `combineFlags` typeFlags t3')) ann t1' t2' t3' + walkChildren (ParensInType_ _ ann t) = do + t' <- walk t + return $! ParensInType_ (sf (typeFlags t')) ann t' + walkChildren other = return $! markSF other + lookupKindArgs :: Qualified (ProperName 'TypeName) -> [Text] lookupKindArgs ctor = fromMaybe [] $ fmap (fmap (fst . snd) . fst) . completeBinderList . fst =<< M.lookup ctor kinds --- | Replace fully applied type synonyms +-- | Replace fully applied type synonyms. +-- Short-circuits if the type is already marked as synonym-free. replaceAllTypeSynonyms :: SourceType -> TypeCheckM SourceType -replaceAllTypeSynonyms d = do - env <- getEnv - either throwError return $ replaceAllTypeSynonyms' (typeSynonyms env) (types env) d +replaceAllTypeSynonyms d + | hasFlag tfSynonymsFree (typeFlags d) = return d + | otherwise = do + env <- getEnv + either throwError return $ replaceAllTypeSynonyms' (typeSynonyms env) (types env) d diff --git a/src/Language/PureScript/TypeChecker/Unify.hs b/src/Language/PureScript/TypeChecker/Unify.hs index 72b8086599..511c82574d 100644 --- a/src/Language/PureScript/TypeChecker/Unify.hs +++ b/src/Language/PureScript/TypeChecker/Unify.hs @@ -32,7 +32,7 @@ import Language.PureScript.Errors (ErrorMessageHint(..), SimpleErrorMessage(..), import Language.PureScript.TypeChecker.Kinds (elaborateKind, instantiateKind, unifyKinds') import Language.PureScript.TypeChecker.Monad (CheckState(..), Substitution(..), UnkLevel(..), Unknown, getLocalContext, guardWith, lookupUnkName, withErrorMessageHint, TypeCheckM) import Language.PureScript.TypeChecker.Skolems (newSkolemConstant, skolemize) -import Language.PureScript.Types (Constraint(..), pattern REmptyKinded, RowListItem(..), SourceType, Type(..), WildcardData(..), alignRowsWith, everythingOnTypes, everywhereOnTypes, everywhereOnTypesM, getAnnForType, mkForAll, rowFromList, srcTUnknown) +import Language.PureScript.Types (Constraint(..), pattern REmptyKinded, RowListItem(..), SourceType, Type(..), WildcardData(..), alignRowsWith, everythingOnTypes, everywhereOnTypes, everywhereOnTypesM, getAnnForType, hasFlag, mkForAll, rowFromList, srcTUnknown, tfHasWildcards, typeFlags) import Data.Set qualified as S -- | Generate a fresh type variable with an unknown kind. Avoid this if at all possible. @@ -192,10 +192,13 @@ unifyRows r1 r2 = sequence_ matches *> uncurry unifyTails rest where throwError . errorMessage $ TypesDoNotUnify r1 r2 -- | --- Replace type wildcards with unknowns +-- Replace type wildcards with unknowns. +-- Short-circuits if the type has no wildcards. -- replaceTypeWildcards :: SourceType -> TypeCheckM SourceType -replaceTypeWildcards = everywhereOnTypesM replace +replaceTypeWildcards ty + | not (hasFlag tfHasWildcards (typeFlags ty)) = return ty + | otherwise = everywhereOnTypesM replace ty where replace (TypeWildcard ann wdata) = do t <- freshType diff --git a/src/Language/PureScript/Types.hs b/src/Language/PureScript/Types.hs index 063c1ebc32..53450b9b77 100644 --- a/src/Language/PureScript/Types.hs +++ b/src/Language/PureScript/Types.hs @@ -1,7 +1,10 @@ -- | -- Data types for types -- -module Language.PureScript.Types where +module Language.PureScript.Types + ( module Language.PureScript.Types + , Type(TUnknown, TypeVar, TypeLevelString, TypeLevelInt, TypeWildcard, TypeConstructor, TypeOp, TypeApp, KindApp, ForAll, ConstrainedType, Skolem, REmpty, RCons, KindedType, BinaryNoParensType, ParensInType) + ) where import Prelude import Protolude (ordNub, fromMaybe) @@ -15,12 +18,14 @@ import Control.Monad ((<=<), (>=>)) import Data.Aeson ((.:), (.:?), (.!=), (.=)) import Data.Aeson qualified as A import Data.Aeson.Types qualified as A +import Data.Bits ((.&.), (.|.)) import Data.Foldable (fold, foldl') import Data.IntSet qualified as IS import Data.List (sortOn) import Data.Maybe (isJust) import Data.Text (Text) import Data.Text qualified as T +import Data.Word (Word8) import GHC.Generics (Generic) import Language.PureScript.AST.SourcePos (pattern NullSourceAnn, SourceAnn, SourceSpan) @@ -66,55 +71,241 @@ typeVarVisibilityPrefix = \case TypeVarVisible -> "@" TypeVarInvisible -> mempty --- | +-- --------------------------------------------------------------------------- +-- Type flags: cached structural properties of a type subtree +-- --------------------------------------------------------------------------- + +-- | Cached information about what a type subtree contains. Stored per-node +-- so that traversals can short-circuit when a subtree is known to not +-- contain the nodes they are looking for. +newtype TypeFlags = TypeFlags Word8 + deriving (Show, Eq, Ord, Generic) + +instance NFData TypeFlags +instance Serialise TypeFlags + +-- | No flags set. +noFlags :: TypeFlags +noFlags = TypeFlags 0 + +-- | Subtree contains a 'TypeWildcard'. +tfHasWildcards :: TypeFlags +tfHasWildcards = TypeFlags 0x01 + +-- | Subtree contains a 'ForAll' without a 'SkolemScope'. +tfHasUnscopedForAlls :: TypeFlags +tfHasUnscopedForAlls = TypeFlags 0x02 + +-- | Subtree has been fully synonym-expanded by 'replaceAllTypeSynonyms'. +tfSynonymsFree :: TypeFlags +tfSynonymsFree = TypeFlags 0x04 + +-- | Combine flags from child subtrees. Only structural flags (HasWildcards, +-- HasUnscopedForAlls) propagate. Processing flags (SynonymsFree) are cleared +-- because constructing a new type from synonym-free children may create a +-- new synonym application. +combineFlags :: TypeFlags -> TypeFlags -> TypeFlags +combineFlags (TypeFlags a) (TypeFlags b) = TypeFlags ((a .|. b) .&. structuralMask) + where structuralMask = 0x03 -- bits 0 and 1 only + +-- | Test whether a specific flag is set. +hasFlag :: TypeFlags -> TypeFlags -> Bool +hasFlag (TypeFlags mask) (TypeFlags w) = w .&. mask /= 0 + +-- | Set a flag. +setFlag :: TypeFlags -> TypeFlags -> TypeFlags +setFlag (TypeFlags f) (TypeFlags w) = TypeFlags (w .|. f) + +-- | Clear a flag. +clearFlag :: TypeFlags -> TypeFlags -> TypeFlags +clearFlag (TypeFlags f) (TypeFlags w) = TypeFlags (w .&. (0xFF - f)) + +-- | Extract the flags from a Type node. +typeFlags :: Type a -> TypeFlags +typeFlags (TUnknown_ f _ _) = f +typeFlags (TypeVar_ f _ _) = f +typeFlags (TypeLevelString_ f _ _) = f +typeFlags (TypeLevelInt_ f _ _) = f +typeFlags (TypeWildcard_ f _ _) = f +typeFlags (TypeConstructor_ f _ _) = f +typeFlags (TypeOp_ f _ _) = f +typeFlags (TypeApp_ f _ _ _) = f +typeFlags (KindApp_ f _ _ _) = f +typeFlags (ForAll_ f _ _ _ _ _ _) = f +typeFlags (ConstrainedType_ f _ _ _) = f +typeFlags (Skolem_ f _ _ _ _ _) = f +typeFlags (REmpty_ f _) = f +typeFlags (RCons_ f _ _ _ _) = f +typeFlags (KindedType_ f _ _ _) = f +typeFlags (BinaryNoParensType_ f _ _ _ _) = f +typeFlags (ParensInType_ f _ _) = f + +-- | Mask to extract only structural flags (clearing processing flags). +maskStructural :: TypeFlags -> TypeFlags +maskStructural (TypeFlags w) = TypeFlags (w .&. 0x03) + +-- | Compute ForAll flags from its components. +forAllNodeFlags :: Maybe (Type a) -> Type a -> Maybe SkolemScope -> TypeFlags +forAllNodeFlags mbK ty Nothing = maybe noFlags (maskStructural . typeFlags) mbK `combineFlags` maskStructural (typeFlags ty) `combineFlags` tfHasUnscopedForAlls +forAllNodeFlags mbK ty (Just _) = maybe noFlags (maskStructural . typeFlags) mbK `combineFlags` maskStructural (typeFlags ty) + +-- | Compute ConstrainedType flags from its components. +constraintNodeFlags :: Constraint a -> Type a -> TypeFlags +constraintNodeFlags c ty = foldl' combineFlags (maskStructural (typeFlags ty)) (map (maskStructural . typeFlags) (constraintKindArgs c) ++ map (maskStructural . typeFlags) (constraintArgs c)) + +-- | Compute Skolem flags from its components. +skolemNodeFlags :: Maybe (Type a) -> TypeFlags +skolemNodeFlags = maybe noFlags (maskStructural . typeFlags) + +-- | Recursively set a flag on every node in a type tree, short-circuiting +-- on subtrees that already have the flag set. Uses raw constructors to +-- avoid recomputing structural flags. +markAllTypeFlags :: TypeFlags -> Type a -> Type a +markAllTypeFlags tf = go where + s = setFlag tf + go t | hasFlag tf (typeFlags t) = t + go (TUnknown_ f a b) = TUnknown_ (s f) a b + go (TypeVar_ f a b) = TypeVar_ (s f) a b + go (TypeLevelString_ f a b) = TypeLevelString_ (s f) a b + go (TypeLevelInt_ f a b) = TypeLevelInt_ (s f) a b + go (TypeWildcard_ f a b) = TypeWildcard_ (s f) a b + go (TypeConstructor_ f a b) = TypeConstructor_ (s f) a b + go (TypeOp_ f a b) = TypeOp_ (s f) a b + go (TypeApp_ f a t1 t2) = TypeApp_ (s f) a (go t1) (go t2) + go (KindApp_ f a t1 t2) = KindApp_ (s f) a (go t1) (go t2) + go (ForAll_ f a vis ident mbK ty sco) = ForAll_ (s f) a vis ident (go <$> mbK) (go ty) sco + go (ConstrainedType_ f a c ty) = ConstrainedType_ (s f) a (mapConstraintArgsAll (map go) c) (go ty) + go (Skolem_ f a name mbK i sc) = Skolem_ (s f) a name (go <$> mbK) i sc + go (REmpty_ f a) = REmpty_ (s f) a + go (RCons_ f a l ty rest) = RCons_ (s f) a l (go ty) (go rest) + go (KindedType_ f a ty k) = KindedType_ (s f) a (go ty) (go k) + go (BinaryNoParensType_ f a t1 t2 t3) = BinaryNoParensType_ (s f) a (go t1) (go t2) (go t3) + go (ParensInType_ f a t) = ParensInType_ (s f) a (go t) + +-- | Set a flag on the root node of a type (using raw constructors to preserve existing flags). +setTypeFlags :: TypeFlags -> Type a -> Type a +setTypeFlags tf (TUnknown_ f a b) = TUnknown_ (setFlag tf f) a b +setTypeFlags tf (TypeVar_ f a b) = TypeVar_ (setFlag tf f) a b +setTypeFlags tf (TypeLevelString_ f a b) = TypeLevelString_ (setFlag tf f) a b +setTypeFlags tf (TypeLevelInt_ f a b) = TypeLevelInt_ (setFlag tf f) a b +setTypeFlags tf (TypeWildcard_ f a b) = TypeWildcard_ (setFlag tf f) a b +setTypeFlags tf (TypeConstructor_ f a b) = TypeConstructor_ (setFlag tf f) a b +setTypeFlags tf (TypeOp_ f a b) = TypeOp_ (setFlag tf f) a b +setTypeFlags tf (TypeApp_ f a b c) = TypeApp_ (setFlag tf f) a b c +setTypeFlags tf (KindApp_ f a b c) = KindApp_ (setFlag tf f) a b c +setTypeFlags tf (ForAll_ f a b c d e g) = ForAll_ (setFlag tf f) a b c d e g +setTypeFlags tf (ConstrainedType_ f a b c) = ConstrainedType_ (setFlag tf f) a b c +setTypeFlags tf (Skolem_ f a b c d e) = Skolem_ (setFlag tf f) a b c d e +setTypeFlags tf (REmpty_ f a) = REmpty_ (setFlag tf f) a +setTypeFlags tf (RCons_ f a b c d) = RCons_ (setFlag tf f) a b c d +setTypeFlags tf (KindedType_ f a b c) = KindedType_ (setFlag tf f) a b c +setTypeFlags tf (BinaryNoParensType_ f a b c d) = BinaryNoParensType_ (setFlag tf f) a b c d +setTypeFlags tf (ParensInType_ f a b) = ParensInType_ (setFlag tf f) a b + +-- --------------------------------------------------------------------------- -- The type of types --- +-- --------------------------------------------------------------------------- + +-- | The type of types. The actual constructors have a @_@ suffix and carry +-- a 'TypeFlags' field. Use the pattern synonyms (without suffix) which +-- auto-compute flags on construction and ignore them on matching. data Type a - -- | A unification variable of type Type - = TUnknown a Int - -- | A named type variable - | TypeVar a Text - -- | A type-level string - | TypeLevelString a PSString - -- | A type-level natural - | TypeLevelInt a Integer - -- | A type wildcard, as would appear in a partial type synonym - | TypeWildcard a WildcardData - -- | A type constructor - | TypeConstructor a (Qualified (ProperName 'TypeName)) - -- | A type operator. This will be desugared into a type constructor during the - -- "operators" phase of desugaring. - | TypeOp a (Qualified (OpName 'TypeOpName)) - -- | A type application - | TypeApp a (Type a) (Type a) - -- | Explicit kind application - | KindApp a (Type a) (Type a) - -- | Forall quantifier - | ForAll a TypeVarVisibility Text (Maybe (Type a)) (Type a) (Maybe SkolemScope) - -- | A type with a set of type class constraints - | ConstrainedType a (Constraint a) (Type a) - -- | A skolem constant - | Skolem a Text (Maybe (Type a)) Int SkolemScope - -- | An empty row - | REmpty a - -- | A non-empty row - | RCons a Label (Type a) (Type a) - -- | A type with a kind annotation - | KindedType a (Type a) (Type a) - -- | Binary operator application. During the rebracketing phase of desugaring, - -- this data constructor will be removed. - | BinaryNoParensType a (Type a) (Type a) (Type a) - -- | Explicit parentheses. During the rebracketing phase of desugaring, this - -- data constructor will be removed. - -- - -- Note: although it seems this constructor is not used, it _is_ useful, - -- since it prevents certain traversals from matching. - | ParensInType a (Type a) + = TUnknown_ !TypeFlags a Int + | TypeVar_ !TypeFlags a Text + | TypeLevelString_ !TypeFlags a PSString + | TypeLevelInt_ !TypeFlags a Integer + | TypeWildcard_ !TypeFlags a WildcardData + | TypeConstructor_ !TypeFlags a (Qualified (ProperName 'TypeName)) + | TypeOp_ !TypeFlags a (Qualified (OpName 'TypeOpName)) + | TypeApp_ !TypeFlags a (Type a) (Type a) + | KindApp_ !TypeFlags a (Type a) (Type a) + | ForAll_ !TypeFlags a TypeVarVisibility Text (Maybe (Type a)) (Type a) (Maybe SkolemScope) + | ConstrainedType_ !TypeFlags a (Constraint a) (Type a) + | Skolem_ !TypeFlags a Text (Maybe (Type a)) Int SkolemScope + | REmpty_ !TypeFlags a + | RCons_ !TypeFlags a Label (Type a) (Type a) + | KindedType_ !TypeFlags a (Type a) (Type a) + | BinaryNoParensType_ !TypeFlags a (Type a) (Type a) (Type a) + | ParensInType_ !TypeFlags a (Type a) deriving (Show, Generic, Functor, Foldable, Traversable) instance NFData a => NFData (Type a) instance Serialise a => Serialise (Type a) +-- --------------------------------------------------------------------------- +-- Pattern synonyms: auto-compute flags on construction, ignore on match +-- --------------------------------------------------------------------------- + +pattern TUnknown :: a -> Int -> Type a +pattern TUnknown a i <- TUnknown_ _ a i + where TUnknown a i = TUnknown_ noFlags a i + +pattern TypeVar :: a -> Text -> Type a +pattern TypeVar a t <- TypeVar_ _ a t + where TypeVar a t = TypeVar_ noFlags a t + +pattern TypeLevelString :: a -> PSString -> Type a +pattern TypeLevelString a s <- TypeLevelString_ _ a s + where TypeLevelString a s = TypeLevelString_ noFlags a s + +pattern TypeLevelInt :: a -> Integer -> Type a +pattern TypeLevelInt a n <- TypeLevelInt_ _ a n + where TypeLevelInt a n = TypeLevelInt_ noFlags a n + +pattern TypeWildcard :: a -> WildcardData -> Type a +pattern TypeWildcard a w <- TypeWildcard_ _ a w + where TypeWildcard a w = TypeWildcard_ tfHasWildcards a w + +pattern TypeConstructor :: a -> Qualified (ProperName 'TypeName) -> Type a +pattern TypeConstructor a q <- TypeConstructor_ _ a q + where TypeConstructor a q = TypeConstructor_ noFlags a q + +pattern TypeOp :: a -> Qualified (OpName 'TypeOpName) -> Type a +pattern TypeOp a q <- TypeOp_ _ a q + where TypeOp a q = TypeOp_ noFlags a q + +pattern TypeApp :: a -> Type a -> Type a -> Type a +pattern TypeApp a t1 t2 <- TypeApp_ _ a t1 t2 + where TypeApp a t1 t2 = TypeApp_ (typeFlags t1 `combineFlags` typeFlags t2) a t1 t2 + +pattern KindApp :: a -> Type a -> Type a -> Type a +pattern KindApp a t1 t2 <- KindApp_ _ a t1 t2 + where KindApp a t1 t2 = KindApp_ (typeFlags t1 `combineFlags` typeFlags t2) a t1 t2 + +pattern ForAll :: a -> TypeVarVisibility -> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a +pattern ForAll a vis ident mbK ty sco <- ForAll_ _ a vis ident mbK ty sco + where ForAll a vis ident mbK ty sco = ForAll_ (forAllNodeFlags mbK ty sco) a vis ident mbK ty sco + +pattern ConstrainedType :: a -> Constraint a -> Type a -> Type a +pattern ConstrainedType a c ty <- ConstrainedType_ _ a c ty + where ConstrainedType a c ty = ConstrainedType_ (constraintNodeFlags c ty) a c ty + +pattern Skolem :: a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a +pattern Skolem a t mbK i s <- Skolem_ _ a t mbK i s + where Skolem a t mbK i s = Skolem_ (skolemNodeFlags mbK) a t mbK i s + +pattern REmpty :: a -> Type a +pattern REmpty a <- REmpty_ _ a + where REmpty a = REmpty_ noFlags a + +pattern RCons :: a -> Label -> Type a -> Type a -> Type a +pattern RCons a l ty rest <- RCons_ _ a l ty rest + where RCons a l ty rest = RCons_ (typeFlags ty `combineFlags` typeFlags rest) a l ty rest + +pattern KindedType :: a -> Type a -> Type a -> Type a +pattern KindedType a ty k <- KindedType_ _ a ty k + where KindedType a ty k = KindedType_ (typeFlags ty `combineFlags` typeFlags k) a ty k + +pattern BinaryNoParensType :: a -> Type a -> Type a -> Type a -> Type a +pattern BinaryNoParensType a t1 t2 t3 <- BinaryNoParensType_ _ a t1 t2 t3 + where BinaryNoParensType a t1 t2 t3 = BinaryNoParensType_ (typeFlags t1 `combineFlags` typeFlags t2 `combineFlags` typeFlags t3) a t1 t2 t3 + +pattern ParensInType :: a -> Type a -> Type a +pattern ParensInType a t <- ParensInType_ _ a t + where ParensInType a t = ParensInType_ (maskStructural (typeFlags t)) a t + +{-# COMPLETE TUnknown, TypeVar, TypeLevelString, TypeLevelInt, TypeWildcard, TypeConstructor, TypeOp, TypeApp, KindApp, ForAll, ConstrainedType, Skolem, REmpty, RCons, KindedType, BinaryNoParensType, ParensInType #-} + srcTUnknown :: Int -> SourceType srcTUnknown = TUnknown NullSourceAnn @@ -763,24 +954,25 @@ everythingWithContextOnTypes s0 r0 (<+>) f = go' s0 where go _ _ = r0 {-# INLINE everythingWithContextOnTypes #-} +-- | Lens to access the annotation. Uses raw constructors to preserve flags. annForType :: Lens' (Type a) a -annForType k (TUnknown a b) = (\z -> TUnknown z b) <$> k a -annForType k (TypeVar a b) = (\z -> TypeVar z b) <$> k a -annForType k (TypeLevelString a b) = (\z -> TypeLevelString z b) <$> k a -annForType k (TypeLevelInt a b) = (\z -> TypeLevelInt z b) <$> k a -annForType k (TypeWildcard a b) = (\z -> TypeWildcard z b) <$> k a -annForType k (TypeConstructor a b) = (\z -> TypeConstructor z b) <$> k a -annForType k (TypeOp a b) = (\z -> TypeOp z b) <$> k a -annForType k (TypeApp a b c) = (\z -> TypeApp z b c) <$> k a -annForType k (KindApp a b c) = (\z -> KindApp z b c) <$> k a -annForType k (ForAll a b c d e f) = (\z -> ForAll z b c d e f) <$> k a -annForType k (ConstrainedType a b c) = (\z -> ConstrainedType z b c) <$> k a -annForType k (Skolem a b c d e) = (\z -> Skolem z b c d e) <$> k a -annForType k (REmpty a) = REmpty <$> k a -annForType k (RCons a b c d) = (\z -> RCons z b c d) <$> k a -annForType k (KindedType a b c) = (\z -> KindedType z b c) <$> k a -annForType k (BinaryNoParensType a b c d) = (\z -> BinaryNoParensType z b c d) <$> k a -annForType k (ParensInType a b) = (\z -> ParensInType z b) <$> k a +annForType k (TUnknown_ f a b) = (\z -> TUnknown_ f z b) <$> k a +annForType k (TypeVar_ f a b) = (\z -> TypeVar_ f z b) <$> k a +annForType k (TypeLevelString_ f a b) = (\z -> TypeLevelString_ f z b) <$> k a +annForType k (TypeLevelInt_ f a b) = (\z -> TypeLevelInt_ f z b) <$> k a +annForType k (TypeWildcard_ f a b) = (\z -> TypeWildcard_ f z b) <$> k a +annForType k (TypeConstructor_ f a b) = (\z -> TypeConstructor_ f z b) <$> k a +annForType k (TypeOp_ f a b) = (\z -> TypeOp_ f z b) <$> k a +annForType k (TypeApp_ f a b c) = (\z -> TypeApp_ f z b c) <$> k a +annForType k (KindApp_ f a b c) = (\z -> KindApp_ f z b c) <$> k a +annForType k (ForAll_ f a b c d e g) = (\z -> ForAll_ f z b c d e g) <$> k a +annForType k (ConstrainedType_ f a b c) = (\z -> ConstrainedType_ f z b c) <$> k a +annForType k (Skolem_ f a b c d e) = (\z -> Skolem_ f z b c d e) <$> k a +annForType k (REmpty_ f a) = (\z -> REmpty_ f z) <$> k a +annForType k (RCons_ f a b c d) = (\z -> RCons_ f z b c d) <$> k a +annForType k (KindedType_ f a b c) = (\z -> KindedType_ f z b c) <$> k a +annForType k (BinaryNoParensType_ f a b c d) = (\z -> BinaryNoParensType_ f z b c d) <$> k a +annForType k (ParensInType_ f a b) = (\z -> ParensInType_ f z b) <$> k a getAnnForType :: Type a -> a getAnnForType = (^. annForType) diff --git a/tests/TestAst.hs b/tests/TestAst.hs index bb2e880443..c37d63cb0d 100644 --- a/tests/TestAst.hs +++ b/tests/TestAst.hs @@ -12,7 +12,7 @@ import Test.QuickCheck (Arbitrary(..), Gen, Property, Testable, counterexample, import Language.PureScript.Label (Label(..)) import Language.PureScript.Names (pattern ByNullSourcePos, OpName(..), OpNameType(..), ProperName(..), ProperNameType(..), Qualified(..)) import Language.PureScript.PSString (PSString) -import Language.PureScript.Types (Constraint, ConstraintData, SkolemScope(..), Type(..), TypeVarVisibility(..), WildcardData, annForType, everythingOnTypes, everythingWithContextOnTypes, everywhereOnTypes, everywhereOnTypesM, everywhereOnTypesTopDownM, getAnnForType) +import Language.PureScript.Types (Constraint, ConstraintData, SkolemScope(..), Type(..), TypeFlags(..), TypeVarVisibility(..), WildcardData, annForType, everythingOnTypes, everythingWithContextOnTypes, everywhereOnTypes, everywhereOnTypesM, everywhereOnTypesTopDownM, getAnnForType) spec :: Spec spec = do @@ -66,6 +66,7 @@ genTypeAnnotatedWith genTypeAnn genConstraintAnn = genType where :+ maybeOf genType :+ genWildcardData :+ genVisibility + :+ genTypeFlags genConstraint :: Gen (Constraint a) genConstraint = genericArbitraryUG (genConstraintAnn :+ generatorEnvironment) @@ -76,6 +77,9 @@ genTypeAnnotatedWith genTypeAnn genConstraintAnn = genType where genQualified :: forall b. (Text -> b) -> Gen (Qualified b) genQualified ctor = Qualified ByNullSourcePos . ctor <$> genText + genTypeFlags :: Gen TypeFlags + genTypeFlags = TypeFlags <$> arbitrary + genSkolemScope :: Gen SkolemScope genSkolemScope = SkolemScope <$> arbitrary From d2d682b4d308feb3aee6733a97a4bd647e5b377e Mon Sep 17 00:00:00 2001 From: Michal Kozakiewicz Date: Sun, 12 Apr 2026 14:27:44 +0000 Subject: [PATCH 2/5] Remove unused clearFlag, markAllTypeFlags, and setTypeFlags MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit These utility functions were defined during development but ended up unused — the custom traversal in Synonyms.hs uses raw constructors directly instead. Weeder flagged them as dead code. Co-Authored-By: Claude Opus 4.6 (1M context) --- src/Language/PureScript/Types.hs | 49 -------------------------------- 1 file changed, 49 deletions(-) diff --git a/src/Language/PureScript/Types.hs b/src/Language/PureScript/Types.hs index 53450b9b77..c64151b1d8 100644 --- a/src/Language/PureScript/Types.hs +++ b/src/Language/PureScript/Types.hs @@ -116,10 +116,6 @@ hasFlag (TypeFlags mask) (TypeFlags w) = w .&. mask /= 0 setFlag :: TypeFlags -> TypeFlags -> TypeFlags setFlag (TypeFlags f) (TypeFlags w) = TypeFlags (w .|. f) --- | Clear a flag. -clearFlag :: TypeFlags -> TypeFlags -> TypeFlags -clearFlag (TypeFlags f) (TypeFlags w) = TypeFlags (w .&. (0xFF - f)) - -- | Extract the flags from a Type node. typeFlags :: Type a -> TypeFlags typeFlags (TUnknown_ f _ _) = f @@ -157,51 +153,6 @@ constraintNodeFlags c ty = foldl' combineFlags (maskStructural (typeFlags ty)) ( skolemNodeFlags :: Maybe (Type a) -> TypeFlags skolemNodeFlags = maybe noFlags (maskStructural . typeFlags) --- | Recursively set a flag on every node in a type tree, short-circuiting --- on subtrees that already have the flag set. Uses raw constructors to --- avoid recomputing structural flags. -markAllTypeFlags :: TypeFlags -> Type a -> Type a -markAllTypeFlags tf = go where - s = setFlag tf - go t | hasFlag tf (typeFlags t) = t - go (TUnknown_ f a b) = TUnknown_ (s f) a b - go (TypeVar_ f a b) = TypeVar_ (s f) a b - go (TypeLevelString_ f a b) = TypeLevelString_ (s f) a b - go (TypeLevelInt_ f a b) = TypeLevelInt_ (s f) a b - go (TypeWildcard_ f a b) = TypeWildcard_ (s f) a b - go (TypeConstructor_ f a b) = TypeConstructor_ (s f) a b - go (TypeOp_ f a b) = TypeOp_ (s f) a b - go (TypeApp_ f a t1 t2) = TypeApp_ (s f) a (go t1) (go t2) - go (KindApp_ f a t1 t2) = KindApp_ (s f) a (go t1) (go t2) - go (ForAll_ f a vis ident mbK ty sco) = ForAll_ (s f) a vis ident (go <$> mbK) (go ty) sco - go (ConstrainedType_ f a c ty) = ConstrainedType_ (s f) a (mapConstraintArgsAll (map go) c) (go ty) - go (Skolem_ f a name mbK i sc) = Skolem_ (s f) a name (go <$> mbK) i sc - go (REmpty_ f a) = REmpty_ (s f) a - go (RCons_ f a l ty rest) = RCons_ (s f) a l (go ty) (go rest) - go (KindedType_ f a ty k) = KindedType_ (s f) a (go ty) (go k) - go (BinaryNoParensType_ f a t1 t2 t3) = BinaryNoParensType_ (s f) a (go t1) (go t2) (go t3) - go (ParensInType_ f a t) = ParensInType_ (s f) a (go t) - --- | Set a flag on the root node of a type (using raw constructors to preserve existing flags). -setTypeFlags :: TypeFlags -> Type a -> Type a -setTypeFlags tf (TUnknown_ f a b) = TUnknown_ (setFlag tf f) a b -setTypeFlags tf (TypeVar_ f a b) = TypeVar_ (setFlag tf f) a b -setTypeFlags tf (TypeLevelString_ f a b) = TypeLevelString_ (setFlag tf f) a b -setTypeFlags tf (TypeLevelInt_ f a b) = TypeLevelInt_ (setFlag tf f) a b -setTypeFlags tf (TypeWildcard_ f a b) = TypeWildcard_ (setFlag tf f) a b -setTypeFlags tf (TypeConstructor_ f a b) = TypeConstructor_ (setFlag tf f) a b -setTypeFlags tf (TypeOp_ f a b) = TypeOp_ (setFlag tf f) a b -setTypeFlags tf (TypeApp_ f a b c) = TypeApp_ (setFlag tf f) a b c -setTypeFlags tf (KindApp_ f a b c) = KindApp_ (setFlag tf f) a b c -setTypeFlags tf (ForAll_ f a b c d e g) = ForAll_ (setFlag tf f) a b c d e g -setTypeFlags tf (ConstrainedType_ f a b c) = ConstrainedType_ (setFlag tf f) a b c -setTypeFlags tf (Skolem_ f a b c d e) = Skolem_ (setFlag tf f) a b c d e -setTypeFlags tf (REmpty_ f a) = REmpty_ (setFlag tf f) a -setTypeFlags tf (RCons_ f a b c d) = RCons_ (setFlag tf f) a b c d -setTypeFlags tf (KindedType_ f a b c) = KindedType_ (setFlag tf f) a b c -setTypeFlags tf (BinaryNoParensType_ f a b c d) = BinaryNoParensType_ (setFlag tf f) a b c d -setTypeFlags tf (ParensInType_ f a b) = ParensInType_ (setFlag tf f) a b - -- --------------------------------------------------------------------------- -- The type of types -- --------------------------------------------------------------------------- From 16abb5a9ce25c84a76a7f38d89ebc78f458c32cd Mon Sep 17 00:00:00 2001 From: Michal Kozakiewicz Date: Wed, 15 Apr 2026 12:57:43 +0000 Subject: [PATCH 3/5] Add debug assertions to verify TypeFlags invariants When short-circuiting based on tfSynonymsFree, tfHasWildcards, or tfHasUnscopedForAlls, assert that a fresh scan of the type confirms the flag's claim. Catches any bug where a flag is set on a type that actually contains the nodes it claims to exclude. Uses Control.Exception.assert, which is active in --fast builds (no -O) but compiled away in optimized builds, so there is no production cost. All 1340 tests pass with assertions active, confirming the invariants hold across the full test corpus. The key invariant: any construction via pattern synonyms calls combineFlags, which masks to structural flags only (0x03), so tfSynonymsFree is always cleared on reconstructed internal nodes. This means substituteType (which uses everywhereOnTypes and thus pattern synonyms) cannot sneak an unexpanded synonym past the flag. Co-Authored-By: Claude Opus 4.6 (1M context) --- src/Language/PureScript/TypeChecker/Skolems.hs | 14 +++++++++++++- .../PureScript/TypeChecker/Synonyms.hs | 18 ++++++++++++++++-- src/Language/PureScript/TypeChecker/Unify.hs | 14 +++++++++++++- 3 files changed, 42 insertions(+), 4 deletions(-) diff --git a/src/Language/PureScript/TypeChecker/Skolems.hs b/src/Language/PureScript/TypeChecker/Skolems.hs index 2a8700149f..cbc73e856d 100644 --- a/src/Language/PureScript/TypeChecker/Skolems.hs +++ b/src/Language/PureScript/TypeChecker/Skolems.hs @@ -10,6 +10,7 @@ module Language.PureScript.TypeChecker.Skolems import Prelude +import Control.Exception (assert) import Control.Monad.Error.Class (MonadError(..)) import Control.Monad.State.Class (MonadState(..), gets, modify) import Data.Foldable (traverse_) @@ -34,12 +35,23 @@ newSkolemConstant = do -- Short-circuits if the type has no unscoped ForAlls. introduceSkolemScope :: MonadState CheckState m => Type a -> m (Type a) introduceSkolemScope ty - | not (hasFlag tfHasUnscopedForAlls (typeFlags ty)) = return ty + -- Sanity check in debug builds: the flag says no unscoped ForAlls exist, + -- so a scan should agree. 'assert' is compiled away with -O. + | not (hasFlag tfHasUnscopedForAlls (typeFlags ty)) = + return $! assert (not (containsUnscopedForAlls ty)) ty | otherwise = everywhereOnTypesM go ty where go (ForAll ann vis ident mbK t Nothing) = ForAll ann vis ident mbK t <$> (Just <$> newSkolemScope) go other = return other +-- | Scan a type for ForAll nodes missing a SkolemScope. +-- Used as a correctness check for the 'tfHasUnscopedForAlls' flag. +containsUnscopedForAlls :: Type a -> Bool +containsUnscopedForAlls = everythingOnTypes (||) isUnscoped + where + isUnscoped (ForAll _ _ _ _ _ Nothing) = True + isUnscoped _ = False + -- | Generate a new skolem scope newSkolemScope :: MonadState CheckState m => m SkolemScope newSkolemScope = do diff --git a/src/Language/PureScript/TypeChecker/Synonyms.hs b/src/Language/PureScript/TypeChecker/Synonyms.hs index ed8f89dfca..f1996c6525 100644 --- a/src/Language/PureScript/TypeChecker/Synonyms.hs +++ b/src/Language/PureScript/TypeChecker/Synonyms.hs @@ -11,6 +11,7 @@ module Language.PureScript.TypeChecker.Synonyms import Prelude +import Control.Exception (assert) import Control.Monad.Error.Class (MonadError(..)) import Data.Maybe (fromMaybe) import Data.Map qualified as M @@ -21,7 +22,7 @@ import Language.PureScript.Names (ProperName, ProperNameType(..), Qualified) import Language.PureScript.TypeChecker.Monad (getEnv, TypeCheckM) import Language.PureScript.Types ( SourceType, Type(..), TypeFlags - , combineFlags, completeBinderList, constraintNodeFlags, forAllNodeFlags + , combineFlags, completeBinderList, constraintNodeFlags, everythingOnTypes, forAllNodeFlags , getAnnForType, hasFlag, overConstraintArgsAll, replaceAllTypeVars , setFlag, skolemNodeFlags, tfSynonymsFree, typeFlags ) @@ -139,7 +140,20 @@ replaceAllTypeSynonyms' syns kinds -- Short-circuits if the type is already marked as synonym-free. replaceAllTypeSynonyms :: SourceType -> TypeCheckM SourceType replaceAllTypeSynonyms d - | hasFlag tfSynonymsFree (typeFlags d) = return d + | hasFlag tfSynonymsFree (typeFlags d) = do + env <- getEnv + -- Sanity check in debug builds: the flag says this type is synonym-free, + -- so scanning should confirm no TypeConstructor in it refers to a synonym. + -- 'assert' is compiled away with -O, so this is a no-op in production. + return $! assert (not (containsTypeSynonyms (typeSynonyms env) d)) d | otherwise = do env <- getEnv either throwError return $ replaceAllTypeSynonyms' (typeSynonyms env) (types env) d + +-- | Scan a type for TypeConstructors that are type synonyms. +-- Used as a correctness check for the 'tfSynonymsFree' flag. +containsTypeSynonyms :: SynonymMap -> Type a -> Bool +containsTypeSynonyms syns = everythingOnTypes (||) isSyn + where + isSyn (TypeConstructor _ ctor) = M.member ctor syns + isSyn _ = False diff --git a/src/Language/PureScript/TypeChecker/Unify.hs b/src/Language/PureScript/TypeChecker/Unify.hs index 511c82574d..68e5bb8992 100644 --- a/src/Language/PureScript/TypeChecker/Unify.hs +++ b/src/Language/PureScript/TypeChecker/Unify.hs @@ -16,6 +16,7 @@ module Language.PureScript.TypeChecker.Unify import Prelude +import Control.Exception (assert) import Control.Monad (forM_, void, when) import Control.Monad.Error.Class (MonadError(..)) import Control.Monad.State.Class (MonadState(..), gets, modify, state) @@ -197,7 +198,10 @@ unifyRows r1 r2 = sequence_ matches *> uncurry unifyTails rest where -- replaceTypeWildcards :: SourceType -> TypeCheckM SourceType replaceTypeWildcards ty - | not (hasFlag tfHasWildcards (typeFlags ty)) = return ty + -- Sanity check in debug builds: the flag says no wildcards, so a scan + -- should agree. 'assert' is compiled away with -O. + | not (hasFlag tfHasWildcards (typeFlags ty)) = + return $! assert (not (containsTypeWildcards ty)) ty | otherwise = everywhereOnTypesM replace ty where replace (TypeWildcard ann wdata) = do @@ -211,6 +215,14 @@ replaceTypeWildcards ty return t replace other = return other +-- | Scan a type for TypeWildcard nodes. +-- Used as a correctness check for the 'tfHasWildcards' flag. +containsTypeWildcards :: Type a -> Bool +containsTypeWildcards = everythingOnTypes (||) isWild + where + isWild (TypeWildcard _ _) = True + isWild _ = False + -- | -- Replace outermost unsolved unification variables with named type variables -- From 92bd49e517ebb9014c3db9760c660e6e498d6495 Mon Sep 17 00:00:00 2001 From: Michal Kozakiewicz Date: Wed, 15 Apr 2026 18:39:51 +0000 Subject: [PATCH 4/5] Document why combineFlags must clear tfSynonymsFree Add a concrete example showing how substitution can introduce a new synonym application at a parent node even when both children are synonym-free in isolation. This explains why we conservatively clear the flag on every reconstruction instead of propagating it. Co-Authored-By: Claude Opus 4.6 (1M context) --- src/Language/PureScript/Types.hs | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/src/Language/PureScript/Types.hs b/src/Language/PureScript/Types.hs index c64151b1d8..b30a6541fe 100644 --- a/src/Language/PureScript/Types.hs +++ b/src/Language/PureScript/Types.hs @@ -100,10 +100,28 @@ tfHasUnscopedForAlls = TypeFlags 0x02 tfSynonymsFree :: TypeFlags tfSynonymsFree = TypeFlags 0x04 --- | Combine flags from child subtrees. Only structural flags (HasWildcards, --- HasUnscopedForAlls) propagate. Processing flags (SynonymsFree) are cleared --- because constructing a new type from synonym-free children may create a --- new synonym application. +-- | Combine flags from child subtrees. Only structural flags +-- ('tfHasWildcards', 'tfHasUnscopedForAlls') propagate; the processing flag +-- 'tfSynonymsFree' is always cleared. +-- +-- Why clear 'tfSynonymsFree'? Constructing a new type from synonym-free +-- children can still create a new synonym application at the parent, even +-- when both children are themselves synonym-free. Example: +-- +-- @ +-- Before substitution: TypeApp (TUnknown u) someArg -- no synonyms +-- Substitution: u -> TypeConstructor SomeAlias -- standalone, fine +-- After substitution: TypeApp (TypeConstructor SomeAlias) someArg +-- -- now a fully-applied synonym that needs expansion! +-- @ +-- +-- In PureScript the convention is to expand synonyms before unification, so +-- the substitution /values/ are synonym-free in isolation. But when a +-- 'TUnknown' in function position is substituted with a synonym constructor, +-- the /resulting/ parent @TypeApp@ is a synonym application that must be +-- expanded. We can't detect this from the children's flags alone without +-- inspecting the spine, so we conservatively clear the flag and let +-- 'replaceAllTypeSynonyms' re-scan when asked. combineFlags :: TypeFlags -> TypeFlags -> TypeFlags combineFlags (TypeFlags a) (TypeFlags b) = TypeFlags ((a .|. b) .&. structuralMask) where structuralMask = 0x03 -- bits 0 and 1 only From bc2386729b4c1a5f38b7431e7b7214ce0ac1b9a3 Mon Sep 17 00:00:00 2001 From: Michal Kozakiewicz Date: Thu, 16 Apr 2026 19:56:52 +0000 Subject: [PATCH 5/5] Define structuralMask from flag constants, not a magic number Derive the mask from tfHasWildcards and tfHasUnscopedForAlls so that adding a new structural flag automatically includes it in propagation. Co-Authored-By: Claude Opus 4.6 (1M context) --- src/Language/PureScript/Types.hs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/Language/PureScript/Types.hs b/src/Language/PureScript/Types.hs index b30a6541fe..aef3ab0de9 100644 --- a/src/Language/PureScript/Types.hs +++ b/src/Language/PureScript/Types.hs @@ -124,7 +124,13 @@ tfSynonymsFree = TypeFlags 0x04 -- 'replaceAllTypeSynonyms' re-scan when asked. combineFlags :: TypeFlags -> TypeFlags -> TypeFlags combineFlags (TypeFlags a) (TypeFlags b) = TypeFlags ((a .|. b) .&. structuralMask) - where structuralMask = 0x03 -- bits 0 and 1 only + +-- | Mask of flags that propagate structurally from children to parents. +-- Processing flags (like 'tfSynonymsFree') are excluded — see 'combineFlags'. +structuralMask :: Word8 +structuralMask = w .|. w' where + TypeFlags w = tfHasWildcards + TypeFlags w' = tfHasUnscopedForAlls -- | Test whether a specific flag is set. hasFlag :: TypeFlags -> TypeFlags -> Bool @@ -156,7 +162,7 @@ typeFlags (ParensInType_ f _ _) = f -- | Mask to extract only structural flags (clearing processing flags). maskStructural :: TypeFlags -> TypeFlags -maskStructural (TypeFlags w) = TypeFlags (w .&. 0x03) +maskStructural (TypeFlags w) = TypeFlags (w .&. structuralMask) -- | Compute ForAll flags from its components. forAllNodeFlags :: Maybe (Type a) -> Type a -> Maybe SkolemScope -> TypeFlags