forbid kind loops #251
forbid kind loops #251
Conversation
WalkthroughThe changes made in the Changes
Assessment against linked issues
Thank you for using CodeRabbit. We offer it for free to the OSS community and would appreciate your support in helping us grow. If you find it useful, would you consider giving us a shout-out on your favorite social media? 🪧 TipsChatThere are 3 ways to chat with CodeRabbit:
Note: Be mindful of the bot's finite context window. It's strongly recommended to break down tasks such as reading entire modules into smaller chunks. For a focused discussion, use review comments to chat about specific files and their changes, instead of using the PR comments. CodeRabbit Commands (Invoked using PR comments)
Other keywords and placeholders
CodeRabbit Configuration File (
|
|
|
CI failed (happy could not build) and it seems easier to drop support for this old version of ghc than to debug CI.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
🧹 Outside diff range and nitpick comments (2)
examples/non-examples/kind-occurs-check.golden (1)
1-2: Approve the new error message with a suggestion for improvement.The new error message effectively addresses the issue of infinite kinds, which is directly related to the PR objective of forbidding kind loops. This change will help prevent the infinite loop problem during type-checking as described in issue #250.
The message is clear and provides specific details about the detected infinite kind. However, to enhance user understanding, consider adding a brief explanation of what this means and its implications.
Consider expanding the error message slightly to improve clarity for users who might not be familiar with kind theory. For example:
Infinite kind detected: (KindVar 55708) = (META(KindVar 55708) → META(KindVar 55701)) + +This error occurs when a type's kind is defined in terms of itself, creating an +infinite loop. Such definitions are not allowed as they cannot be resolved +during type-checking.This additional explanation helps users understand the nature of the error and why it's problematic.
src/Expander/TC.hs (1)
369-369: Include additional context inKindMismatcherrors.When throwing a
KindMismatcherror at line 369, the current implementation providesloc,k1', andk2'. To aid in debugging, consider including more contextual information, such as the types or expressions involved in the kind mismatch.This can be done by enhancing the
KindMismatchdata constructor or by appending a descriptive message to the error.
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
📒 Files selected for processing (6)
- examples/non-examples/kind-occurs-check.golden (1 hunks)
- examples/non-examples/kind-occurs-check.kl (1 hunks)
- examples/non-examples/type-occurs-check.golden (1 hunks)
- examples/non-examples/type-occurs-check.kl (1 hunks)
- src/Expander/Error.hs (5 hunks)
- src/Expander/TC.hs (2 hunks)
🔇 Additional comments (14)
examples/non-examples/type-occurs-check.golden (1)
1-1: LGTM! This golden file correctly captures the infinite type detection.This new golden file accurately represents the expected output for detecting an infinite type, which aligns with the PR objective of addressing the infinite loop during type-checking (issue #250). The message clearly indicates the problematic type equation that leads to the infinite loop.
Some observations:
- The error message is clear and informative, helping developers identify the source of the infinite type.
- The use of
MetaPtr 57868suggests that the type checker is using unique identifiers for type variables, which is a good practice for disambiguation.- The file's name
type-occurs-check.goldenappropriately describes its purpose, as the "occurs check" is a common term for detecting these kinds of recursive type definitions.This addition will serve as a valuable test case to ensure that the type checker correctly identifies and reports infinite types, preventing the compiler from entering an infinite loop during type-checking.
examples/non-examples/type-occurs-check.kl (3)
1-8: LGTM: Valid example demonstrating polymorphic type inferenceThis example effectively illustrates let-generalization, a key feature in polymorphic type systems. It shows how
xs, initialized as an empty list (nil), can be interpreted as bothList AandList (List A). This demonstrates the flexibility of the type system in generalizing types within let bindings.
1-13: Summary: Excellent examples for type system behaviorThis file effectively serves its purpose in the
examples/non-examplesdirectory by providing both a valid case of polymorphic type inference and an invalid case of infinite type definition. These examples are crucial for testing and demonstrating the behavior of the type system, particularly in relation to let-generalization and occurs-check mechanisms.The examples align well with the PR objectives of addressing infinite loops during type-checking. They provide concrete test cases that can be used to verify that the type system correctly handles both valid polymorphic types and rejects invalid infinite types.
Consider adding more complex examples or edge cases in the future to further strengthen the test suite for the type system.
10-13: LGTM: Correctly demonstrates infinite type detectionThis function definition effectively illustrates a case that should trigger the occurs-check in the type system. By asserting that
xsis of the same type asList xs, it creates an infinite type definition. This aligns well with the PR objective of addressing infinite loops during type-checking.The comment accurately describes the expected behavior: the type equality
?1 ~ List ?1should be rejected by the occurs-check mechanism. This example serves as a valuable test case for ensuring that the type system correctly handles potentially infinite types.To ensure this example is properly utilized in the test suite, let's verify its inclusion:
examples/non-examples/kind-occurs-check.kl (3)
3-4: Definition ofPhantomdatatype is correctThe
Phantomdatatype is correctly defined with type parameterAand constructormk-phantom. This establishes a simple structure for testing kind equality without carrying additional type information.
9-12: Example usage ofPhantomeffectively tests kind equalityThe example demonstrates the creation of a
Phantominstance with an unknown typeAusing(with-unknown-type [A] ...). This is appropriate for testing the compiler's handling of kind unification and ensures that the previous infinite loop issue is resolved.
16-17: Definition ofInfiniteKinddatatype is valid and tests occurs-check properlyThe
InfiniteKinddatatype is defined with a constructormk-infinite-kindthat takes(Phantom (A A)). This introduces a self-referential type parameter(A A), which is a valid construct for testing the kind occurs-check mechanism. It effectively ensures that the compiler handles such cases without entering infinite recursion.src/Expander/Error.hs (6)
9-9: Properly exportingKindCheckErrorand its constructorsBy exporting
KindCheckError(..), the module makes all constructors ofKindCheckErroravailable to other modules, which is essential for comprehensive pattern matching on kind checking errors.
67-67: Correctly extendingExpansionErrwithKindCheckErrorAdding the
KindCheckError KindCheckErrorconstructor to theExpansionErrdata type appropriately integrates kind checking errors into the existing error handling framework.
101-104: Well-definedKindCheckErrordata type for encapsulating kind errorsThe
KindCheckErrordata type is properly defined with constructorsKindMismatchandKindOccursCheckFailed, effectively capturing the possible errors that can occur during kind checking.
224-224: Proper delegation toKindCheckErrorpretty-printer inExpansionErrThe
ppfunction inExpansionErrnow correctly delegates to theKindCheckErrorpretty-printer, ensuring that kind checking errors are formatted consistently with other error types.
269-270: Consistency in error messages for occurs check failuresThe error messages for
OccursCheckFailedinTypeCheckErrorandKindOccursCheckFailedinKindCheckErrorare consistent, which enhances readability and user understanding.Also applies to: 280-283
273-283: Effective implementation ofPrettyinstance forKindCheckErrorThe
Prettyinstance forKindCheckErroris correctly implemented, providing clear and informative error messages for kind mismatches and infinite kind detections.src/Expander/TC.hs (1)
324-331:⚠️ Potential issueVerify proper error propagation from
kindOccursCheck.The
kindOccursCheckfunction throws aKindCheckErrorwhen a kind variable occurs within a kind, preventing kind loops. Ensure that all callers of this function correctly handle this exception to maintain the stability of the kind-checking mechanism.
src/Expander/Error.hs
Outdated
| pp env (KindOccursCheckFailed ptr ty) = | ||
| hang 2 $ group $ vsep [ text "Infinite kind detected:" | ||
| , group (vsep [viaShow ptr, "=", pp env ty]) | ||
| ] |
There was a problem hiding this comment.
🛠️ Refactor suggestion
Consider renaming variable ty to k for clarity
In the pp function for KindOccursCheckFailed, consider renaming the variable ty to k or kind to better reflect that it represents a kind, not a type.
Apply this diff to improve clarity:
pp env (KindOccursCheckFailed ptr ty) =
hang 2 $ group $ vsep [ text "Infinite kind detected:"
- , group (vsep [viaShow ptr, "=", pp env ty])
+ , group (vsep [viaShow ptr, "=", pp env k])
]Committable suggestion was skipped due to low confidence.
|
I added tests to |
I thought type variables were represented by random numbers under the hood, but that is not the case, so the type variables are not a good source of inspiration after all. |
the type-level unification variables are called "MetaPtr", but the kind-level unification variables are called "KindVar", so "v" is a more appropriate name for a KindVar than "ptr".
There was a problem hiding this comment.
Actionable comments posted: 9
🧹 Outside diff range and nitpick comments (8)
src/Util/Store.hs (2)
78-82: Consider enhancing the error message for better debuggingWhile the implementation is correct, the error message could be more informative by including the actual key value that wasn't found. This would be particularly helpful for debugging type-checking issues.
-(!) :: HasKey p => Store p v -> p -> v +(!) :: (HasKey p, Show p) => Store p v -> p -> v graph ! ptr = case lookup ptr graph of Just v -> v - Nothing -> error "Store.!!: key not found" + Nothing -> error $ "Store.!!: key " ++ show ptr ++ " not found"
114-115: LGTM: size implementation is correctThe implementation properly wraps IntMap's size function. Consider adding Haddock documentation to describe the complexity guarantees, as this information would be valuable for users of the Store type.
src/Type.hs (1)
Line range hint
39-125: Strong type-safety approach to prevent kind loops.The introduction of
SchemeVarand its systematic integration throughout the type system is a robust approach to preventing kind loops. The type-level distinction between scheme variables and other natural numbers will help catch potential issues at compile time rather than runtime.Some benefits of this approach:
- Type safety through newtype wrapper
- Clear separation of concerns
- Compile-time guarantees
src/Expander/Error.hs (1)
101-104: LGTM: Well-structured error type with appropriate constructors.The
KindCheckErrortype follows the established pattern of error handling in the codebase. The constructors are well-chosen for reporting kind-level errors.Consider adding Haddock documentation to describe when each constructor is used:
-- | Errors that can occur during kind checking data KindCheckError = KindMismatch (Maybe SrcLoc) Kind Kind -- ^ Occurs when two kinds don't match during unification | KindOccursCheckFailed KindVar Kind -- ^ Occurs when a kind variable occurs within the kind it's being unified withsrc/Expander/TC.hs (1)
340-365: Consider enhancing documentation for path compressionThe implementation is solid with the path compression optimization and cycle prevention. However, the complex path compression logic in the
KMetaVarcase could benefit from more detailed documentation explaining the algorithm and its invariants.Add detailed comments explaining:
- Why path compression is necessary
- How it prevents indirect cycles
- The invariants maintained by the algorithm
src/Pretty.hs (1)
320-321: Consider adding documentation for the scheme variable naming functions.The implementation of
schemeVarNamesandschemeVarNameis correct, but adding documentation would help explain:
- The naming pattern (Greek letters followed by numbered sequences)
- The relationship between
SchemeVarand the generated namesAdd Haddock documentation:
+-- | List of names for scheme variables, starting with Greek letters (α, β, ...) +-- followed by numbered sequences (α0, β0, ...) when we run out of letters schemeVarNames :: [Text] schemeVarNames = ... +-- | Convert a SchemeVar to its corresponding display name +-- using the schemeVarNames list schemeVarName :: SchemeVar -> Text schemeVarName (SchemeVar n) = ...Also applies to: 335-336
src/Pretty/Renumber.hs (2)
18-19: Derive standard typeclasses for 'Renumbered'You may benefit from deriving standard typeclasses such as
Eq,Ord, orShowfor theRenumberednewtype. This can enhance usability and integration with other parts of the codebase.
21-32: Enhance documentation with usage examplesThe comment explaining the purpose of the
renumberfunction is helpful. Consider adding an example of how to userenumberin practice to assist future developers in understanding its application.
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
📒 Files selected for processing (12)
klister.cabal(1 hunks)src/Expander.hs(4 hunks)src/Expander/Error.hs(5 hunks)src/Expander/Monad.hs(1 hunks)src/Expander/Primitives.hs(2 hunks)src/Expander/Syntax.hs(1 hunks)src/Expander/TC.hs(6 hunks)src/Pretty.hs(4 hunks)src/Pretty/Renumber.hs(1 hunks)src/Type.hs(3 hunks)src/Util/Key.hs(1 hunks)src/Util/Store.hs(4 hunks)
✅ Files skipped from review due to trivial changes (1)
- src/Expander/Syntax.hs
🔇 Additional comments (26)
src/Util/Key.hs (2)
7-7: LGTM: Clean import addition
The import is correctly placed and properly scoped for the new Natural instance.
17-19:
Add bounds checking for safe type conversion
The current implementation using fromIntegral could lead to unsafe conversions:
- Converting negative Int values to Natural will silently wrap to large numbers
- Converting large Natural values to Int might cause overflow and key collisions
Consider adding bounds checking:
instance HasKey Natural where
- getKey = fromIntegral
- fromKey = fromIntegral
+ getKey n | n > fromIntegral (maxBound :: Int) = error "Natural value too large for Int key"
+ | otherwise = fromIntegral n
+ fromKey i | i < 0 = error "Negative Int cannot be converted to Natural key"
+ | otherwise = fromIntegral iLet's check if there are any existing uses of negative keys in the codebase:
klister.cabal (1)
84-84: LGTM! The new module is properly integrated.
The addition of Pretty.Renumber to exposed-modules is well-placed and aligns with the PR's goal of improving error message consistency.
Let's verify the module exists:
✅ Verification successful
Module exists and is properly placed in the codebase
The Pretty.Renumber module is correctly located at src/Pretty/Renumber.hs, confirming its proper integration into the codebase.
🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash
# Description: Verify the Pretty.Renumber module exists
# Expected: Find the module file in the src directory
fd --type f "Renumber.hs" src/Pretty/
Length of output: 60
src/Util/Store.hs (5)
13-13: LGTM: TypeOperators extension is required for the new (!) operator
The extension is appropriately placed with other language pragmas and is necessary for the new functionality.
19-30: LGTM: Export list properly includes all new functions
The new exports are consistently placed within the existing export list structure.
92-94: LGTM: toAscList provides deterministic ordering
The implementation correctly preserves ordering and is consistent with the existing toList function.
111-113: LGTM: empty implementation is correct
The implementation properly wraps IntMap's empty constructor.
78-82: Verify the usage of new Store functions in type-checking code
These new Store utilities appear to support changes in the type-checking implementation. Let's verify their usage:
Also applies to: 92-94, 111-113, 114-115
src/Type.hs (3)
39-44: Well-designed type wrapper for scheme variables!
Good choice using a newtype wrapper around Natural. This provides type safety by preventing accidental mixing of scheme variable indices with other Natural numbers in the system.
125-125: Type class signature properly updated for SchemeVar.
The method signature change maintains consistency with the concrete implementations in both TyF and Ty instances.
56-56: Verify all TSchemaVar constructor usage has been updated.
The change to use SchemeVar is consistent with the new type-safe approach.
✅ Verification successful
Let me analyze the usage of TSchemaVar to ensure it's consistently using SchemeVar.
All TSchemaVar usages have been properly updated to use SchemeVar
The verification confirms that:
- All TSchemaVar constructor usages are consistent with the SchemeVar type
- The SchemeVar type is properly defined as
newtype SchemeVar = SchemeVar Natural - No direct Natural usage with TSchemaVar exists in the codebase
- All related functions (schemeVarName, etc.) correctly handle the SchemeVar type
🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash
# Search for any remaining direct Natural usage with TSchemaVar to ensure complete migration
rg "TSchemaVar.*Natural"
# Find all usages of TSchemaVar to verify they use SchemeVar
ast-grep --pattern 'TSchemaVar $_'
Length of output: 555
Script:
#!/bin/bash
# Check the definition and usage of schemeVarName to verify SchemeVar type
rg "schemeVarName" -A 2
# Look for any Natural imports or type definitions related to TSchemaVar
rg "import.*Natural|type.*Natural" src/Type.hs
Length of output: 964
src/Expander/Error.hs (4)
9-9: LGTM: Export declaration is appropriate.
The export of KindCheckError(..) correctly exposes the type and all its constructors, which is standard practice for error types.
273-283: LGTM: Clear and consistent error message formatting.
The Pretty instance follows the established patterns in the codebase and provides clear, well-formatted error messages. The use of unicode '≠' enhances readability.
67-67: LGTM: Clean integration with ExpansionErr.
The KindCheckError is properly integrated into the ExpansionErr type and its pretty printing instance, following the same pattern as TypeCheckError.
Also applies to: 224-224
269-270: LGTM: Improved error message clarity.
The change from "Occurs check failed" to "Infinite type detected" makes the error message more descriptive and user-friendly, while maintaining consistency with the new KindOccursCheckFailed error.
src/Expander/TC.hs (4)
111-118: LGTM: Type-safe instantiation using Store
The change from [Ty] to Store SchemeVar Ty improves type safety by ensuring proper association between scheme variables and types. The use of toAscList ensures deterministic ordering.
316-327: LGTM: Comprehensive kind variable collection
The implementation correctly traverses the kind structure to collect all kind variables, which is essential for the occurs check mechanism.
329-338: LGTM: Robust kind cycle detection
The implementation effectively prevents infinite loops in kind definitions by detecting cycles. This directly addresses the issue #250 where the compiler entered an infinite loop during type-checking.
Line range hint 366-376: LGTM: Improved kind error reporting
The change to use KindCheckError instead of TypeCheckError improves error reporting by using the appropriate error type. The inclusion of source location information will help users better understand where kind mismatches occur.
src/Pretty.hs (3)
314-314: LGTM: Variable name change is consistent with the new naming convention.
The change from typeVarNames to schemeVarNames better reflects its purpose in the context of type schemes.
348-349: LGTM: Consistent use of the new naming function.
The change to use schemeVarName for TSchemaVar pretty-printing is correct and aligns with the new naming scheme.
395-395: LGTM: Consistent variable naming in data constructor pretty-printing.
The change to use schemeVarNames in the data constructor pretty-printing is consistent with the new naming scheme.
src/Expander/Monad.hs (1)
243-244: LGTM: Type variable representation change improves type-checking safety.
The change from Natural to SchemeVar for type variable representation in ETypeVar is a good improvement. This change aligns with the PR's objective of preventing infinite loops during type-checking by providing a more structured and type-safe representation for type variables.
Let's verify that this change is consistently applied across the codebase:
✅ Verification successful
Change from Natural to SchemeVar is consistent and well-integrated
The change from Natural to SchemeVar in ETypeVar is part of a broader, consistent type system implementation where:
SchemeVaris a newtype wrapper aroundNaturaldefined insrc/Type.hs- The change is properly integrated with type instantiation, generalization, and unification logic
- All type variable handling code uses
SchemeVarconsistently, including:- Type instantiation (
instfunction) - Type generalization (
generalizeTypefunction) - Constructor expansion (
prepareTypeVarfunction) - Standard type schemes (e.g., in
Maybe,Listdefinitions)
- Type instantiation (
🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash
# Description: Check for any remaining uses of Natural with type variables
# Expect: No direct use of Natural for type variables
# Search for Natural type usage in type-related contexts
rg --type haskell "Natural.*[Tt]ype[Vv]ar"
# Search for SchemeVar usage to confirm the new pattern
rg --type haskell "SchemeVar.*[Tt]ype[Vv]ar"
Length of output: 91
Script:
#!/bin/bash
# Let's try a more comprehensive search strategy
# 1. Find all files that might contain type variable definitions
fd -e hs
# 2. Look for Natural type usage in a broader context
rg --type haskell "Natural" -B 2 -A 2
# 3. Look for SchemeVar definitions and usage
rg --type haskell "SchemeVar" -B 2 -A 2
# 4. Look specifically at the type variable constructors
rg --type haskell "ETypeVar" -B 2 -A 2
Length of output: 13095
src/Expander/Primitives.hs (2)
132-133: Code change aligns with enhanced type variable indexing
The use of firstSchemeVar in place of a hardcoded value improves flexibility and consistency in type variable management within the datatype function.
Line range hint 714-718: Updated prepareTypeVar signature ensures consistency
Changing the parameter of prepareTypeVar from Natural to SchemeVar aligns with the updated handling of type variables, enhancing type safety and consistency across the module.
src/Expander.hs (1)
552-557: LGTM!
The bind-IO function correctly introduces two type variables and matches the kinds appropriately.
| renumberTypeVar :: MetaPtr -> State (Store MetaPtr Renumbered) Renumbered | ||
| renumberTypeVar metaPtr = do | ||
| store <- get | ||
| case Store.lookup metaPtr store of | ||
| Just renumbered -> do | ||
| pure renumbered | ||
| Nothing -> do | ||
| let i = Store.size store | ||
| let r = Renumbered i | ||
| put $ Store.insert metaPtr r store | ||
| pure r | ||
|
|
There was a problem hiding this comment.
🛠️ Refactor suggestion
Abstract common logic in 'renumberTypeVar' and 'renumberKindVar'
The functions renumberTypeVar and renumberKindVar share similar logic for renumbering variables. Consider abstracting the common logic into a generic function to enhance code reusability and maintainability.
Also applies to: 60-70
| renumber | ||
| :: forall s t u | ||
| . Traversal s t MetaPtr Renumbered | ||
| -> Traversal t u KindVar Renumbered | ||
| -> s -> u | ||
| renumber typeVars kindVars s = u | ||
| where | ||
| (t, n) = flip evalState Store.empty $ do | ||
| t_ <- traverseOf typeVars renumberTypeVar s | ||
| store <- get | ||
| let n_ = Store.size store | ||
| pure (t_, n_) | ||
| u = flip evalState Store.empty $ do | ||
| traverseOf kindVars renumberKindVar t | ||
|
|
There was a problem hiding this comment.
🛠️ Refactor suggestion
Combine traversals to simplify the 'renumber' function
In the renumber function, you perform two separate traversals with their own state monads for type variables and kind variables. Consider combining these traversals into a single pass with a unified state. This may simplify the code and improve efficiency.
| {-# LANGUAGE MultiParamTypeClasses #-} | ||
| {-# LANGUAGE FlexibleInstances #-} | ||
| {-# LANGUAGE FunctionalDependencies #-} | ||
| {-# LANGUAGE ImportQualifiedPost #-} | ||
| {-# LANGUAGE RankNTypes #-} | ||
| {-# LANGUAGE ScopedTypeVariables #-} |
There was a problem hiding this comment.
🛠️ Refactor suggestion
Review language extensions for necessity
Verify that all enabled language extensions are required for this module. Extensions like FunctionalDependencies and MultiParamTypeClasses may not be necessary and can be removed to simplify the code.
| let tyStore = S.fromList $ zip [firstSchemeVar..] argTys | ||
| unify dest t $ tDatatype dt argTys | ||
| args' <- for args \a -> inst dest (Scheme argKinds a) argTys | ||
| args' <- for args \a -> inst dest (Scheme argKinds a) tyStore |
There was a problem hiding this comment.
Ensure uniqueness of type variable indices in tyStore
In constructing tyStore by zipping [firstSchemeVar..] with argTys, there is a risk of reusing type variable indices, which can lead to conflicts. Ensure that the range of indices starting from firstSchemeVar does not overlap with other uses.
Consider maintaining a separate type variable index or using a function to generate fresh type variables to guarantee uniqueness.
| , let a = tSchemaVar firstSchemeVar [] | ||
| in Scheme [KStar, KStar] $ tFun [a] (tIO a) |
There was a problem hiding this comment.
Incorrect number of kind annotations in pure-IO function definition
In the definition of pure-IO, the Scheme is given a kind list [KStar, KStar], but only one type variable a is introduced. The number of kinds in the kind list should match the number of type variables.
Apply this diff to fix the issue:
- in Scheme [KStar, KStar] $ tFun [a] (tIO a)
+ in Scheme [KStar] $ tFun [a] (tIO a)📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| , let a = tSchemaVar firstSchemeVar [] | |
| in Scheme [KStar, KStar] $ tFun [a] (tIO a) | |
| , let a = tSchemaVar firstSchemeVar [] | |
| in Scheme [KStar] $ tFun [a] (tIO a) |
| in ("Maybe", [KStar], [("nothing", []), ("just", [a])]) | ||
| , let a = tSchemaVar firstSchemeVar [] |
There was a problem hiding this comment.
Potential type variable conflict due to reuse of firstSchemeVar
The type variable a is defined using tSchemaVar firstSchemeVar [] without ensuring uniqueness. Reusing firstSchemeVar may lead to conflicts if it's used elsewhere. Please ensure that each type variable is unique.
Consider using a mechanism to generate fresh type variable indices for each new type variable. For example:
- , let a = tSchemaVar firstSchemeVar []
+ , let a = tSchemaVar nextSchemeVar []Ensure that nextSchemeVar is incremented appropriately to prevent collisions.
Committable suggestion was skipped due to low confidence.
| in ("List" | ||
| , [KStar] | ||
| , [ ("nil", []) | ||
| , ("::", [a, Prims.primitiveDatatype "List" [a]]) | ||
| ] | ||
| ) |
There was a problem hiding this comment.
Potential type variable conflict due to reuse of firstSchemeVar
Similar to the issue above, in the definition of List, the type variable a is defined using tSchemaVar firstSchemeVar []. This may cause conflicts if firstSchemeVar is not unique. Ensure that a is uniquely identified.
Consider generating fresh type variables for each new type. For example:
- , let a = tSchemaVar firstSchemeVar []
+ , let a = tSchemaVar nextSchemeVar []Where nextSchemeVar is ensured to be unique.
Committable suggestion was skipped due to low confidence.
| let tyStore = S.fromList $ zip [firstSchemeVar..] tyArgs | ||
| argTypes <- for args \ a -> | ||
| inst loc (Scheme argKinds a) tyArgs | ||
| inst loc (Scheme argKinds a) tyStore |
There was a problem hiding this comment.
Ensure uniqueness of type variable indices when instantiating types
When instantiating argument types with inst, ensure that the tyStore mapping uses unique type variable indices. Reusing firstSchemeVar without managing uniqueness can cause type variable clashes.
Adjust the tyStore to use unique indices:
- let tyStore = S.fromList $ zip [firstSchemeVar..] tyArgs
+ let tyStore = S.fromList $ zip [nextSchemeVar..] tyArgsWhere nextSchemeVar is managed to ensure it provides fresh indices.
Committable suggestion was skipped due to low confidence.
| , let a = tSchemaVar firstSchemeVar [] | ||
| in [ ("list-contents", [Prims.primitiveDatatype "List" [a]]) | ||
| , ("integer-contents", [tInteger]) | ||
| , ("string-contents", [tString]) | ||
| , ("identifier-contents", [tString]) | ||
| -- if you add a constructor here, remember to also add a | ||
| -- corresponding pattern in close-syntax! | ||
| ] |
There was a problem hiding this comment.
Potential type variable conflict due to reuse of firstSchemeVar
In the definition of Syntax-Contents, the type variable a is introduced using tSchemaVar firstSchemeVar []. Reusing firstSchemeVar can lead to conflicts. Ensure that a is unique within this context.
Modify the code to use a fresh type variable:
- , let a = tSchemaVar firstSchemeVar []
+ , let a = tSchemaVar nextSchemeVar []Again, nextSchemeVar should be uniquely generated.
Committable suggestion was skipped due to low confidence.
fixes #250
Summary by CodeRabbit
New Features
Bug Fixes
Chores