diff --git a/src/main.rs b/src/main.rs
index 8f7ffdf..80517e1 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1376,5 +1376,48 @@ c")"#;
             let result = eval(source);
             assert!(result.is_ok(), "Expected success but got: {:?}", result);
         }
+
+        #[test]
+        fn test_effect_inference_function() {
+            // Test that effects are inferred when not explicitly declared
+            // This function uses Console effect without declaring it
+            let source = r#"
+                effect Console {
+                    fn print(msg: String): Unit
+                }
+                fn greet(name: String): Unit = Console.print("Hello")
+                let result = 42
+            "#;
+            let result = eval(source);
+            assert!(result.is_ok(), "Expected success with inferred effects but got: {:?}", result);
+        }
+
+        #[test]
+        fn test_effect_inference_lambda() {
+            // Test that lambda effects are inferred
+            let source = r#"
+                effect Logger {
+                    fn log(msg: String): Unit
+                }
+                let logFn = fn(msg: String) => Logger.log(msg)
+                let result = 42
+            "#;
+            let result = eval(source);
+            assert!(result.is_ok(), "Expected success with inferred lambda effects but got: {:?}", result);
+        }
+
+        #[test]
+        fn test_explicit_effects_validation() {
+            // Test that explicitly declared effects are validated against usage
+            let source = r#"
+                effect Console {
+                    fn print(msg: String): Unit
+                }
+                fn greet(name: String): Unit with {Console} = Console.print("Hello")
+                let result = 42
+            "#;
+            let result = eval(source);
+            assert!(result.is_ok(), "Expected success with explicit effects but got: {:?}", result);
+        }
     }
 }
diff --git a/src/typechecker.rs b/src/typechecker.rs
index 0bd9023..74dea11 100644
--- a/src/typechecker.rs
+++ b/src/typechecker.rs
@@ -102,6 +102,10 @@ fn categorize_type_error(message: &str) -> (String, Vec<String>) {
 pub struct TypeChecker {
     env: TypeEnv,
     current_effects: EffectSet,
+    /// Effects inferred from the current function body (for effect inference)
+    inferred_effects: EffectSet,
+    /// Whether we're inferring effects (no explicit declaration)
+    inferring_effects: bool,
     errors: Vec<TypeError>,
 }
 
@@ -110,6 +114,8 @@ impl TypeChecker {
         Self {
             env: TypeEnv::with_builtins(),
             current_effects: EffectSet::empty(),
+            inferred_effects: EffectSet::empty(),
+            inferring_effects: false,
             errors: Vec::new(),
         }
     }
@@ -296,17 +302,26 @@ impl TypeChecker {
             local_env.bind(&param.name.name, TypeScheme::mono(param_type));
         }
 
-        // Set current effects
-        let old_effects = std::mem::replace(
-            &mut self.current_effects,
-            EffectSet::from_iter(func.effects.iter().map(|e| e.name.clone())),
-        );
+        // Determine if we need to infer effects
+        let explicit_effects = !func.effects.is_empty();
+        let declared_effects = EffectSet::from_iter(func.effects.iter().map(|e| e.name.clone()));
+
+        // Save old state
+        let old_effects = std::mem::replace(&mut self.current_effects, declared_effects.clone());
+        let old_inferring = std::mem::replace(&mut self.inferring_effects, !explicit_effects);
+        let old_inferred = std::mem::replace(&mut self.inferred_effects, EffectSet::empty());
 
         // Type check the body
         let old_env = std::mem::replace(&mut self.env, local_env);
         let body_type = self.infer_expr(&func.body);
         self.env = old_env;
+
+        // Get the inferred effects before restoring state
+        let inferred = std::mem::replace(&mut self.inferred_effects, old_inferred);
+
+        // Restore state
         self.current_effects = old_effects;
+        self.inferring_effects = old_inferring;
 
         // Check that body type matches return type
         let return_type = self.resolve_type(&func.return_type);
@@ -324,16 +339,45 @@ impl TypeChecker {
         let properties = PropertySet::from_ast(&func.properties);
 
         // Pure functions cannot have effects
-        if properties.is_pure() && !func.effects.is_empty() {
+        let effective_effects = if explicit_effects {
+            &declared_effects
+        } else {
+            &inferred
+        };
+
+        if properties.is_pure() && !effective_effects.is_empty() {
+            let effects_str = if explicit_effects {
+                func.effects
+                    .iter()
+                    .map(|e| e.name.as_str())
+                    .collect::<Vec<_>>()
+                    .join(", ")
+            } else {
+                format!("{} (inferred)", inferred)
+            };
             self.errors.push(TypeError {
                 message: format!(
                     "Function '{}' is declared as pure but has effects: {{{}}}",
+                    func.name.name, effects_str
+                ),
+                span: func.span,
+            });
+        }
+
+        // If effects were declared, verify that inferred effects are a subset
+        if explicit_effects && !inferred.is_subset(&declared_effects) {
+            let missing: Vec<_> = inferred
+                .effects
+                .iter()
+                .filter(|e| !declared_effects.contains(e))
+                .cloned()
+                .collect();
+            self.errors.push(TypeError {
+                message: format!(
+                    "Function '{}' uses effects {{{}}} but only declares {{{}}}",
                     func.name.name,
-                    func.effects
-                        .iter()
-                        .map(|e| e.name.as_str())
-                        .collect::<Vec<_>>()
-                        .join(", ")
+                    missing.join(", "),
+                    declared_effects
                 ),
                 span: func.span,
             });
@@ -758,8 +802,14 @@ impl TypeChecker {
         let builtin_effects = ["Console", "Fail", "State"];
         let is_builtin = builtin_effects.contains(&effect.name.as_str());
 
+        // Track this effect for inference
+        if self.inferring_effects {
+            self.inferred_effects.insert(effect.name.clone());
+        }
+
         // Check that we're in a context that allows this effect
-        if !is_builtin && !self.current_effects.contains(&effect.name) {
+        // Skip this check if we're inferring effects (no explicit declaration)
+        if !self.inferring_effects && !is_builtin && !self.current_effects.contains(&effect.name) {
             self.errors.push(TypeError {
                 message: format!(
                     "Effect '{}' not available in current context. Available: {{{}}}",
@@ -877,15 +927,26 @@ impl TypeChecker {
             })
             .collect();
 
-        // Set current effects
-        let effect_set = EffectSet::from_iter(effects.iter().map(|e| e.name.clone()));
-        let old_effects = std::mem::replace(&mut self.current_effects, effect_set.clone());
+        // Determine if we need to infer effects for this lambda
+        let explicit_effects = !effects.is_empty();
+        let declared_effects = EffectSet::from_iter(effects.iter().map(|e| e.name.clone()));
+
+        // Save old state
+        let old_effects = std::mem::replace(&mut self.current_effects, declared_effects.clone());
+        let old_inferring = std::mem::replace(&mut self.inferring_effects, !explicit_effects);
+        let old_inferred = std::mem::replace(&mut self.inferred_effects, EffectSet::empty());
 
         // Type check body
         let old_env = std::mem::replace(&mut self.env, local_env);
         let body_type = self.infer_expr(body);
         self.env = old_env;
+
+        // Get the inferred effects before restoring state
+        let inferred = std::mem::replace(&mut self.inferred_effects, old_inferred);
+
+        // Restore state
         self.current_effects = old_effects;
+        self.inferring_effects = old_inferring;
 
         // Check return type if specified
         let ret_type = if let Some(rt) = return_type {
@@ -904,7 +965,14 @@ impl TypeChecker {
             body_type
         };
 
-        Type::function_with_effects(param_types, ret_type, effect_set)
+        // Use inferred effects if not explicitly declared
+        let final_effects = if explicit_effects {
+            declared_effects
+        } else {
+            inferred
+        };
+
+        Type::function_with_effects(param_types, ret_type, final_effects)
     }
 
     fn infer_let(