diff --git a/pnpm-lock.yaml b/pnpm-lock.yaml
index 089da2d..726ebde 100644
--- a/pnpm-lock.yaml
+++ b/pnpm-lock.yaml
@@ -16,7 +16,7 @@ importers:
         version: 5.2.5
       dope2:
         specifier: git+https://deemz.org/git/joeri/dope2.git
-        version: git+https://deemz.org/git/joeri/dope2.git#d3515d39a51d0baf9fcc775b8d2fb74c74e24868
+        version: git+https://deemz.org/git/joeri/dope2.git#1fe40858444cc4d0f9e4ba4223b280aef0ea4fb2
       react:
         specifier: ^19.1.0
         version: 19.1.0
@@ -597,8 +597,8 @@ packages:
   deep-is@0.1.4:
     resolution: {integrity: sha512-oIPzksmTg4/MriiaYGO+okXDT7ztn/w3Eptv/+gSIdMdKsJo0u4CfYNFJPy+4SKMuCqGw2wxnA+URMg3t8a/bQ==}
 
-  dope2@git+https://deemz.org/git/joeri/dope2.git#d3515d39a51d0baf9fcc775b8d2fb74c74e24868:
-    resolution: {commit: d3515d39a51d0baf9fcc775b8d2fb74c74e24868, repo: https://deemz.org/git/joeri/dope2.git, type: git}
+  dope2@git+https://deemz.org/git/joeri/dope2.git#1fe40858444cc4d0f9e4ba4223b280aef0ea4fb2:
+    resolution: {commit: 1fe40858444cc4d0f9e4ba4223b280aef0ea4fb2, repo: https://deemz.org/git/joeri/dope2.git, type: git}
     version: 0.0.1
 
   esbuild@0.25.4:
@@ -1431,7 +1431,7 @@ snapshots:
 
   deep-is@0.1.4: {}
 
-  dope2@git+https://deemz.org/git/joeri/dope2.git#d3515d39a51d0baf9fcc775b8d2fb74c74e24868:
+  dope2@git+https://deemz.org/git/joeri/dope2.git#1fe40858444cc4d0f9e4ba4223b280aef0ea4fb2:
     dependencies:
       functional-red-black-tree: 1.0.1
 
diff --git a/src/EnvContext.ts b/src/EnvContext.ts
index f2d100e..9717ae4 100644
--- a/src/EnvContext.ts
+++ b/src/EnvContext.ts
@@ -1,13 +1,20 @@
 import { createContext } from "react";
 import { getDefaultTypeParser, module2Env, ModuleStd } from "dope2";
+import type { Dynamic, Environment } from "./eval";
 
 export const functionWith3Params = i => j => k => i+j+k;
 export const functionWith4Params = i => j => k => l => i+j+k+l;
 
 const mkType = getDefaultTypeParser();
-export const extendedEnv = module2Env(ModuleStd.concat([
-  ["functionWith3Params", { i: functionWith3Params, t: mkType("Int->Int->Int->Int") }],
-  ["functionWith4Params", { i: functionWith4Params, t: mkType("Int->Int->Int->Int->Int")}]
-]));
+
+export const extendedEnv: Environment = {
+  names: module2Env(ModuleStd.concat([
+      ["functionWith3Params", { i: functionWith3Params, t: mkType("Int->Int->Int->Int") }],
+      ["functionWith4Params", { i: functionWith4Params, t: mkType("Int->Int->Int->Int->Int")}]
+    ]).map(([name, {i,t}]) => [name, { kind: "value", i, t, unification: new Map() }] as [string, Dynamic])
+  ).name2dyn,
+  nextFreeTypeVar: 0,
+  typeVars: new Set(),
+};
 
 export const EnvContext = createContext(extendedEnv);
\ No newline at end of file
diff --git a/src/InputBlock.tsx b/src/InputBlock.tsx
index 3ea0345..8151a9f 100644
--- a/src/InputBlock.tsx
+++ b/src/InputBlock.tsx
@@ -44,7 +44,7 @@ const computeSuggestions = (text, env, suggestionPriority: (s: ResolvedType) =>
     ... literals.map((lit) => ["literal", text, lit]),
 
     // names
-    ... trie.suggest(env.name2dyn)(text)(Infinity)
+    ... trie.suggest(env.names)(text)(Infinity)
         .map(([name,type]) => [
           "name",
           name, {
@@ -53,8 +53,7 @@ const computeSuggestions = (text, env, suggestionPriority: (s: ResolvedType) =>
             kind: type.kind || "value",
           }]),
   ]
-  // return ls;
-  return [];
+  return []; // <-- uncomment to disable suggestions (useful for debugging)
   return ls
     .map(suggestion => [suggestionPriority(suggestion[2]), ...suggestion] as PrioritizedSuggestionType)
     .sort(([priorityA], [priorityB]) => priorityB - priorityA)
@@ -67,7 +66,7 @@ export function InputBlock({ state, setState, suggestionPriority, onCancel }: In
   const [i, setI] = useState(0); // selected suggestion idx
   const [haveFocus, setHaveFocus] = useState(false); // whether to render suggestions or not
 
-  const singleSuggestion = trie.growPrefix(env.name2dyn)(text);
+  const singleSuggestion = trie.growPrefix(env.names)(text);
   const suggestions = useMemo(() => computeSuggestions(text, env, suggestionPriority), [text, suggestionPriority, env]);
 
   useEffect(() => autoInputWidth(inputRef, text+singleSuggestion), [inputRef, text, singleSuggestion]);
diff --git a/src/LambdaBlock.tsx b/src/LambdaBlock.tsx
index 1db6261..eb9592a 100644
--- a/src/LambdaBlock.tsx
+++ b/src/LambdaBlock.tsx
@@ -1,13 +1,14 @@
 import { useContext, useEffect, useRef } from "react";
 
-import { growEnv } from "dope2";
+import { eqType, getSymbol, reduceUnification, trie } from "dope2";
 
 import { ExprBlock, type ExprBlockState, type State2Props } from "./ExprBlock";
 import { EnvContext } from "./EnvContext";
-import { getUnusedTypeVar } from "./eval";
+import { evalEditorBlock, makeInnerEnv, makeTypeVar } from "./eval";
 import { autoInputWidth } from "./util/dom_trickery";
 
 import "./LambdaBlock.css";
+import { Type } from "./Type";
 
 export interface LambdaBlockState {
   kind: "lambda";
@@ -47,11 +48,20 @@ export function LambdaBlock({state, setState, suggestionPriority}: LambdaBlockPr
 
   useEffect(() => autoInputWidth(nameRef, state.paramName, 60), [nameRef, state.paramName]);
 
-  const innerEnv = growEnv(env)(state.paramName)({
-    kind: "unknown",
-    i: undefined,
-    t: getUnusedTypeVar(env),
-  });
+  const [paramType, staticInnerEnv] = makeTypeVar(env, state.paramName);
+
+  const exprResolved = evalEditorBlock(state.expr, staticInnerEnv);
+
+  const inferredParamType = reduceUnification(exprResolved.unification).get(getSymbol(paramType)) || paramType;
+
+  const betterInnerEnv = eqType(paramType)(inferredParamType)
+    ? staticInnerEnv
+    : makeInnerEnv(env, state.paramName, {
+      kind: "unknown",
+      t: inferredParamType,
+      unification: new Map(), // <- is this correct?
+    })
+
   
   return <span className="lambdaBlock">
     <span className="keyword">&#955;</span>
@@ -66,11 +76,14 @@ export function LambdaBlock({state, setState, suggestionPriority}: LambdaBlockPr
           onChange={e => setParamName(e.target.value)}
           />
     </span>
+    <div className="typeSignature">
+        &nbsp;::&nbsp;<Type type={inferredParamType} />
+        </div>
     &nbsp;
     <span className="keyword">:</span>
     &nbsp;
     <div className="lambdaInner">
-      <EnvContext value={innerEnv}>
+      <EnvContext value={betterInnerEnv}>
         <ExprBlock
           state={state.expr}
           setState={setExpr}
diff --git a/src/eval.ts b/src/eval.ts
index d756806..0bef1fe 100644
--- a/src/eval.ts
+++ b/src/eval.ts
@@ -1,19 +1,27 @@
-import { assignFnSubstitutions, dict, Double, fnType, getSymbol, growEnv, Int, NotAFunctionError, prettyT, substitute, symbolFunction, trie, TYPE_VARS, UnifyError } from "dope2";
+import { dict, Double, fnType, getHumanReadableName, getSymbol, Int, mergeUnifications, NotAFunctionError, occurring, prettyT, prettyU, recomputeTypeVars, reduceUnification, substitute, symbolFunction, trie, TYPE_VARS, UNBOUND_SYMBOLS, UnifyError, unifyLL } from "dope2";
 
 import type { ExprBlockState } from "./ExprBlock";
-import type { InputValueType, SuggestionType } from "./InputBlock";
+import type { InputValueType } from "./InputBlock";
+
+export interface Environment {
+  names: any;
+  nextFreeTypeVar: number;
+  typeVars: Set<string>;
+}
 
 interface Type {
   symbol: string;
   params: any[];
 };
 
+type Unification = Map<string, any>;
+
 export interface DeepError {
   kind: "error";
   e: Error;
   depth: number;
   t: Type;
-  substitutions: Map<Type,Type>;
+  unification: Unification;
 }
 
 // a dynamically typed value = tuple (instance, type)
@@ -21,21 +29,15 @@ export interface Dynamic {
   kind: "value",
   i: any;
   t: Type;
-  substitutions: Map<Type,Type>;
+  unification: Unification;
 };
 
 export interface Unknown {
   kind: "unknown";
   t: Type;
-  substitutions: Map<Type,Type>;
+  unification: Unification;
 }
 
-export const entirelyUnknown = env => ({
-  kind: "unknown",
-  t: getUnusedTypeVar(env),
-  substitutions: new Map(),
-} as Unknown);
-
 // the value of every block is either known (Dynamic), an error, or unknown
 export type ResolvedType = Dynamic | DeepError | Unknown;
 
@@ -43,17 +45,15 @@ export const evalEditorBlock = (s: ExprBlockState, env): ResolvedType => {
   if (s.kind === "input") {
     return evalInputBlock(s.text, s.value, env);
   }
-  if (s.kind === "call") {
+  else if (s.kind === "call") {
     return evalCallBlock(s.fn, s.input, env);
   }
-  if (s.kind === "let") {
+  else if (s.kind === "let") {
     return evalLetInBlock(s.value, s.name, s.inner, env);
   }
-  if (s.kind === "lambda") {
+  else { // (s.kind === "lambda")
     return evalLambdaBlock(s.paramName, s.expr, env);
-
   }
-  return entirelyUnknown(env); // todo
 };
 
 export function evalInputBlock(text: string, value: InputValueType, env): ResolvedType {
@@ -61,56 +61,57 @@ export function evalInputBlock(text: string, value: InputValueType, env): Resolv
     return parseLiteral(text, value.type, env);
   }
   else if (value.kind === "name") {
-    const found = trie.get(env.name2dyn)(text);
+    const found = trie.get(env.names)(text);
     if (found) {
-      return {
-        kind: found.kind || "value",
-        ...found,
-        substitutions: found.substitutions || new Map(),
-      };
+      return found;
     }
   }
   // kind === "text" -> unresolved
   return {
     kind: "error",
-    t: getUnusedTypeVar(env),
+    t: makeTypeVar(env, 'err')[0],
     e: new Error(`'${text}' not found`),
     depth: 0,
-    substitutions: new Map(),
+    unification: new Map(),
   };
 }
 
-const mergeMaps = (...maps: Map<Type,Type>[]) => {
-  return new Map(maps.flatMap(m => [...m]));
-}
 
 export function evalCallBlock2(fnResolved: ResolvedType, inputResolved: ResolvedType, env): ResolvedType {
   if (getSymbol(fnResolved.t) !== symbolFunction) {
     // worst outcome: we know nothing about the result!
-    return {
-      kind: "error",
-      e: new NotAFunctionError(`${prettyT(fnResolved.t)} is not a function type!`),
-      t: getUnusedTypeVar(env),
-      substitutions: mergeMaps(fnResolved.substitutions, inputResolved.substitutions),
-      depth: 0,
-    };
+    return makeError(env,
+      new NotAFunctionError(`${prettyT(fnResolved.t)} is not a function type!`),
+      mergeUnifications(fnResolved.unification, inputResolved.unification),
+    )
   }
   try {
     // fn is a function...
-    const [_inType, inSubst, outType, _outSubst] = assignFnSubstitutions(fnResolved.t, inputResolved.t, getUnusedTypeVarIdx(env)); // may throw
+    const [rewrittenFnType] = recomputeTypeVars([fnResolved.t], env.nextFreeTypeVar);
+    const unification = unifyLL(rewrittenFnType.params[0](rewrittenFnType), inputResolved.t);
 
-    console.log('==================================')
-    console.log('fnResolvedT:', prettyT(fnResolved.t));
-    console.log('inputResolvedT:', prettyT(inputResolved.t));
-    console.log('_inType:',prettyT(_inType));
-    console.log('inSubst:', [...inSubst].map(([key,val]) => [key,prettyT(val)]));
-    console.log('outType:',prettyT(outType));
-    console.log('_outSubst:', [..._outSubst].map(([key,val]) => [key,prettyT(val)]));
+    const inputTypeVars = occurring(inputResolved.t);
+    const subsetOfUnification = new Map([...unification].filter(([typeVar]) => inputTypeVars.has(typeVar)));
+
+    const outType = substitute(
+      rewrittenFnType.params[1](rewrittenFnType),
+      reduceUnification(subsetOfUnification),
+      []); // <- not important
+
+    console.log('========= evalCallBlock2 =========')
+    console.log('fnType             :', prettyT(fnResolved.t));
+    console.log('rewrittenFnType    :', prettyT(rewrittenFnType));
+    console.log('inputType          :', prettyT(inputResolved.t));
+    console.log('outType            :', prettyT(outType));
+    console.log('unification        :', prettyU(unification));
+    console.log('inputTypeVars      :', [...inputTypeVars].map(getHumanReadableName));
+    console.log('fn.unification     :', prettyU(fnResolved.unification));
+    console.log('input.unification  :', prettyU(inputResolved.unification));
+    console.log('subsetOfUnification:', prettyU(subsetOfUnification));
     console.log('==================================')
 
-    // console.log('assignFn...', 'fn.t:', prettyT(fnResolved.t), 'input:', inputResolved, 'input.t:', prettyT(inputResolved.t), '\nout =', prettyT(outType), 'subst:', substitutions, substitutions.size);
-  
-    const mergedSubstitutions = mergeMaps(inSubst, fnResolved.substitutions, inputResolved.substitutions);
+    const grandUnification = [fnResolved.unification, inputResolved.unification]
+      .reduce(mergeUnifications, subsetOfUnification);
 
     if (inputResolved.kind === "error") {
       return {
@@ -118,7 +119,7 @@ export function evalCallBlock2(fnResolved: ResolvedType, inputResolved: Resolved
         e: inputResolved.e, // bubble up the error
         depth: 0,
         t: outType,
-        substitutions: mergedSubstitutions,
+        unification: grandUnification,
       };
     }
     if (fnResolved.kind === "error") {
@@ -128,7 +129,7 @@ export function evalCallBlock2(fnResolved: ResolvedType, inputResolved: Resolved
         e: fnResolved.e,
         depth: fnResolved.depth+1,
         t: outType,
-        substitutions: mergedSubstitutions,
+        unification: grandUnification,
       };
     }
     // if the above statement did not throw => types are compatible...
@@ -138,7 +139,7 @@ export function evalCallBlock2(fnResolved: ResolvedType, inputResolved: Resolved
         kind: "value",
         i: outValue,
         t: outType,
-        substitutions: mergedSubstitutions,
+        unification: grandUnification,
       };
     }
     else {
@@ -146,7 +147,7 @@ export function evalCallBlock2(fnResolved: ResolvedType, inputResolved: Resolved
       return {
         kind: "unknown",
         t: outType,
-        substitutions: mergedSubstitutions,
+        unification: grandUnification,
       };
     }
   }
@@ -159,7 +160,7 @@ export function evalCallBlock2(fnResolved: ResolvedType, inputResolved: Resolved
         e,
         depth: 0,
         t: outType,
-        substitutions: mergeMaps(fnResolved.substitutions, inputResolved.substitutions),
+        unification: mergeUnifications(fnResolved.unification, inputResolved.unification),
       };
     }
     throw e;
@@ -174,35 +175,28 @@ export function evalCallBlock(fn: ExprBlockState, input: ExprBlockState, env): R
 
 export function evalLetInBlock(value: ExprBlockState, name: string, inner: ExprBlockState, env): ResolvedType {
   const valueResolved = evalEditorBlock(value, env);
-  // console.log('eval', name, '...', valueResolved.kind, valueResolved.e);
-  // const innerEnv = growEnv(env)(name)(valueResolved);
   const innerEnv = makeInnerEnv(env, name, valueResolved);
   return evalEditorBlock(inner, innerEnv);
 }
 
-function getUnusedTypeVarIdx(env) {
-  for (let i=0; ; i++) {
-    if (!dict.has(env.typeDict)(TYPE_VARS[i])) {
-      return i;
-    }
-  }
-}
-
-export function getUnusedTypeVar(env) {
-  return TYPE_VARS[getUnusedTypeVarIdx(env)];
-}
 
 export function evalLambdaBlock(paramName: string, expr: ExprBlockState, env): ResolvedType {
-  const paramType = getUnusedTypeVar(env);
-  // static env: we only know the name and the type
-  const staticInnerEnv = growEnv(env)(paramName)({
-    kind: "unknown", // parameter value is not statically known
-    t: paramType,
-    substitutions: new Map(),
-  })
+  const [paramType, staticInnerEnv] = makeTypeVar(env, paramName);
   const exprResolved = evalEditorBlock(expr, staticInnerEnv);
   const lambdaT = fnType(_ => paramType)(_ => exprResolved.t);
-  const lambdaTSubstituted = substitute(lambdaT, exprResolved.substitutions, []);
+  // This is the only place in the code where we actually do something with the 'substitutions'. We compute the type of our lambda function:
+  const lambdaTSubstituted = substitute(
+    lambdaT,
+    reduceUnification(exprResolved.unification),
+    []); // <- not important
+
+  console.log('========= evalLambdaBlock =========')
+  console.log('paramType           :', prettyT(paramType));
+  console.log('exprType            :', prettyT(exprResolved.t));
+  console.log('lambdaType          :', prettyT(lambdaT));
+  console.log('lambdaTypeSubsituted:', prettyT(lambdaTSubstituted));
+  console.log('===================================')
+
   // console.log('inner kind', exprResolved.kind, paramName);
   if (exprResolved.kind === "error") {    
     return {
@@ -210,8 +204,7 @@ export function evalLambdaBlock(paramName: string, expr: ExprBlockState, env): R
       t: lambdaTSubstituted,
       depth: 0,
       e: exprResolved.e,
-      // substitutions: new Map(),
-      substitutions: exprResolved.substitutions,
+      unification: exprResolved.unification,
     }
   }
   const paramTypeSubstituted = lambdaTSubstituted.params[0](lambdaTSubstituted);
@@ -220,7 +213,7 @@ export function evalLambdaBlock(paramName: string, expr: ExprBlockState, env): R
       kind: "value",
       i: x,
       t: paramTypeSubstituted,
-      substitutions: new Map(),
+      unification: new Map(),
     });
     const result = evalEditorBlock(expr, innerEnv);
     if (result.kind === "value") {
@@ -231,7 +224,7 @@ export function evalLambdaBlock(paramName: string, expr: ExprBlockState, env): R
     kind: "value",
     t: lambdaTSubstituted,
     i: fn,
-    substitutions: exprResolved.substitutions,
+    unification: exprResolved.unification,
   };
 }
 
@@ -248,7 +241,7 @@ function parseLiteral(text: string, type: string, env): ResolvedType {
   if (type === "Double") {
     return parseAsDouble(text, env);
   }
-  return entirelyUnknown(env);
+  return makeError(env, new Error("Failed to parse"));
 }
 
 function parseAsDouble(text: string, env): ResolvedType {
@@ -259,11 +252,11 @@ function parseAsDouble(text: string, env): ResolvedType {
         kind: "value",
         i: num,
         t: Double,
-        substitutions: new Map(),
+        unification: new Map(),
       };
     }
   }
-  return entirelyUnknown(env);
+  return makeError(env, new Error("Failed to parse as Double"));
 }
 function parseAsInt(text: string, env): ResolvedType {
   if (text !== '') {
@@ -272,12 +265,12 @@ function parseAsInt(text: string, env): ResolvedType {
         kind: "value",
         i: BigInt(text),
         t: Int,
-        substitutions: new Map(),
+        unification: new Map(),
       }; // may throw
     }
     catch {}
   }
-  return entirelyUnknown(env);
+  return makeError(env, new Error("Failed to parse as Int"));
 }
 
 const literalParsers = [parseAsDouble, parseAsInt];
@@ -304,10 +297,45 @@ export function scoreResolved(resolved: ResolvedType, outPriority: (s:ResolvedTy
   }
 }
 
-export function makeInnerEnv(env, name: string, value: ResolvedType) {
-  if (name !== "" && value.kind === "value") {
-    return growEnv(env)(name)(value);
+export function makeInnerEnv(env: Environment, name: string, value: ResolvedType): Environment {
+  if (name !== "") {
+    return {
+      names: trie.insert(env.names)(name)(value),
+      nextFreeTypeVar: env.nextFreeTypeVar,
+      typeVars: env.typeVars,
+    }
   }
   return env;
 }
 
+export function makeTypeVar(env: Environment, name: string): [Type, Environment] {
+  const idx = env.nextFreeTypeVar;
+  const typeVar = TYPE_VARS[idx];
+  const unknown: Unknown = {
+    kind: "unknown",
+    t: typeVar,
+    unification: new Map(),
+  };
+  return [ typeVar, {
+    names: trie.insert(env.names)(name)(unknown),
+    nextFreeTypeVar: idx + 1,
+    typeVars: new Set([...env.typeVars, UNBOUND_SYMBOLS[idx]]),
+  }];
+}
+
+function makeError(env: Environment, e: Error, unification: Unification=new Map()): DeepError {
+  const idx = env.nextFreeTypeVar;
+  const typeVar = TYPE_VARS[idx];
+  const deepError: DeepError = {
+    kind: "error",
+    t: typeVar,
+    unification: new Map(),
+    e,
+    depth: 0,
+  };
+  return deepError;
+  // , {
+  //   names: trie.insert(env.names)('err')(deepError),
+  //   nextFreeTypeVar: idx + 1,
+  // }];
+}
\ No newline at end of file