diff --git a/idris-jvm-assembler/src/main/java/io/github/mmhelloworld/idrisjvm/assembler/Assembler.java b/idris-jvm-assembler/src/main/java/io/github/mmhelloworld/idrisjvm/assembler/Assembler.java
index 462f15aa8..f57725039 100644
--- a/idris-jvm-assembler/src/main/java/io/github/mmhelloworld/idrisjvm/assembler/Assembler.java
+++ b/idris-jvm-assembler/src/main/java/io/github/mmhelloworld/idrisjvm/assembler/Assembler.java
@@ -9,7 +9,6 @@
 import org.objectweb.asm.Opcodes;
 import org.objectweb.asm.Type;
 
-import java.io.BufferedInputStream;
 import java.io.File;
 import java.io.IOException;
 import java.nio.file.Files;
@@ -21,10 +20,6 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Map.Entry;
-import java.util.jar.Attributes;
-import java.util.jar.JarEntry;
-import java.util.jar.JarOutputStream;
-import java.util.jar.Manifest;
 import java.util.stream.IntStream;
 import java.util.stream.Stream;
 
@@ -33,12 +28,8 @@
 import static java.lang.String.format;
 import static java.lang.System.lineSeparator;
 import static java.nio.charset.StandardCharsets.UTF_8;
-import static java.nio.file.Files.newInputStream;
-import static java.nio.file.Files.newOutputStream;
 import static java.nio.file.Files.setPosixFilePermissions;
 import static java.util.Objects.requireNonNull;
-import static java.util.jar.Attributes.Name.MAIN_CLASS;
-import static java.util.jar.Attributes.Name.MANIFEST_VERSION;
 import static java.util.stream.Collectors.joining;
 import static java.util.stream.Collectors.toList;
 import static org.objectweb.asm.ClassWriter.COMPUTE_FRAMES;
@@ -206,17 +197,6 @@ public Assembler() {
         this.env = new HashMap<>();
     }
 
-    public static void createJar(String directory, String fileName, String mainClass) throws IOException {
-        String jarFileName = fileName + ".jar";
-        File jarFile = new File(directory, jarFileName);
-        jarFile.delete();
-        try (JarOutputStream target =
-                 new JarOutputStream(newOutputStream(jarFile.toPath()), createManifest(mainClass))) {
-            File sourceDirectory = new File(directory);
-            add(sourceDirectory, target, jarFile, sourceDirectory);
-        }
-    }
-
     public static void createExecutable(String directoryName, String fileName, String mainClass) throws IOException {
         String javaOptsProp = System.getProperty("JAVA_OPTS", System.getenv("JAVA_OPTS"));
         String javaOpts = javaOptsProp == null ? "-Xss8m -Xms2g -Xmx3g" : javaOptsProp;
@@ -257,74 +237,6 @@ private static byte[] createExecutableFileContent(String... lines) {
         return String.join(lineSeparator(), lines).getBytes(UTF_8);
     }
 
-    private static Manifest createManifest(String mainClass) {
-        Manifest manifest = new Manifest();
-        Attributes manifestAttributes = manifest.getMainAttributes();
-        manifestAttributes.put(MANIFEST_VERSION, "1.0");
-        manifestAttributes.put(MAIN_CLASS, mainClass);
-        return manifest;
-    }
-
-    private static void add(File source, JarOutputStream target, File jarFile, File rootDirectory) throws IOException {
-        if (source.isDirectory()) {
-            addDirectory(source, target, jarFile, rootDirectory);
-        } else {
-            addFile(source, target, jarFile, rootDirectory);
-        }
-        if (source.isDirectory() || !source.getName().endsWith(".jar")) {
-            source.delete();
-        }
-    }
-
-    private static void addFile(File source, JarOutputStream jarOutputStream, File jarFile, File rootDirectory)
-        throws IOException {
-        if (source.equals(jarFile)) {
-            return;
-        }
-        JarEntry entry = new JarEntry(getJarEntryName(source, rootDirectory));
-        entry.setTime(source.lastModified());
-        jarOutputStream.putNextEntry(entry);
-        try (BufferedInputStream in = new BufferedInputStream(newInputStream(source.toPath()))) {
-            byte[] buffer = new byte[BUFFER_SIZE];
-            while (true) {
-                int count = in.read(buffer);
-                if (count == -1) {
-                    break;
-                }
-                jarOutputStream.write(buffer, 0, count);
-            }
-            jarOutputStream.closeEntry();
-        }
-    }
-
-    private static void addDirectory(File source, JarOutputStream jarOutputStream, File jarFile, File rootDirectory)
-        throws IOException {
-        String name = getJarEntryName(source, rootDirectory);
-        if (!name.isEmpty()) {
-            createDirectory(name, source.lastModified(), jarOutputStream);
-        }
-        File[] files = requireNonNull(source.listFiles(), "Unable to get files from directory " + source);
-        for (File file : files) {
-            add(file, jarOutputStream, jarFile, rootDirectory);
-        }
-    }
-
-    private static String getJarEntryName(File source, File rootDirectory) {
-        String name = source.getPath().replace(rootDirectory.getPath(), "").replace("\\", "/");
-        return !name.startsWith("/") ? name : name.substring(1);
-    }
-
-    private static void createDirectory(String name, long lastModified, JarOutputStream jarOutputStream)
-        throws IOException {
-        if (!name.endsWith("/")) {
-            name += "/";
-        }
-        JarEntry entry = new JarEntry(name);
-        entry.setTime(lastModified);
-        jarOutputStream.putNextEntry(entry);
-        jarOutputStream.closeEntry();
-    }
-
     private static Type getType(String typeDescriptor) {
         switch (typeDescriptor) {
             case "boolean":
diff --git a/idris-jvm-runtime/src/main/java/io/github/mmhelloworld/idrisjvm/runtime/Conversion.java b/idris-jvm-runtime/src/main/java/io/github/mmhelloworld/idrisjvm/runtime/Conversion.java
index 939ccf839..5af59cd16 100644
--- a/idris-jvm-runtime/src/main/java/io/github/mmhelloworld/idrisjvm/runtime/Conversion.java
+++ b/idris-jvm-runtime/src/main/java/io/github/mmhelloworld/idrisjvm/runtime/Conversion.java
@@ -23,8 +23,6 @@ public static int toInt(Object that) {
             return 0;
         } else if (that instanceof Integer) {
             return (int) that;
-        } else if (that instanceof Thunk) {
-            return ((Thunk) that).getInt();
         } else if (that instanceof BigInteger) {
             return ((BigInteger) that).intValue();
         } else if (that instanceof Long) {
diff --git a/idris-jvm-runtime/src/main/java/io/github/mmhelloworld/idrisjvm/runtime/Runtime.java b/idris-jvm-runtime/src/main/java/io/github/mmhelloworld/idrisjvm/runtime/Runtime.java
index 93610d35b..90be0a855 100644
--- a/idris-jvm-runtime/src/main/java/io/github/mmhelloworld/idrisjvm/runtime/Runtime.java
+++ b/idris-jvm-runtime/src/main/java/io/github/mmhelloworld/idrisjvm/runtime/Runtime.java
@@ -1,7 +1,10 @@
 package io.github.mmhelloworld.idrisjvm.runtime;
 
+import java.io.PrintWriter;
+import java.io.StringWriter;
 import java.lang.management.ManagementFactory;
 import java.nio.channels.Channels;
+import java.util.Arrays;
 import java.util.List;
 import java.util.concurrent.ExecutionException;
 import java.util.concurrent.ForkJoinPool;
@@ -118,6 +121,18 @@ public static String getErrorMessage(int errorNumber) {
         return "Error code: " + errorNumber;
     }
 
+    public static String getStackTraceString() {
+        StackTraceElement[] trace = new Throwable().getStackTrace();
+        StringWriter stringWriter = new StringWriter();
+        PrintWriter printWriter = new PrintWriter(stringWriter, true);
+        for (int index = 1; index < trace.length; index++) {
+            StackTraceElement traceElement = trace[index];
+            printWriter.println("\tat " + traceElement);
+        }
+        printWriter.flush();
+        return stringWriter.toString();
+    }
+
     public static void free(Object object) {
     }
 
diff --git a/libs/base/System.idr b/libs/base/System.idr
index afd44c858..53416bee5 100644
--- a/libs/base/System.idr
+++ b/libs/base/System.idr
@@ -271,7 +271,7 @@ namespace Escaped
 
 %foreign supportC "idris2_time"
          "javascript:lambda:() => Math.floor(new Date().getTime() / 1000)"
-         "jvm:time(java/lang/Object int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
+         "jvm:time(int),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
 prim__time : PrimIO Int
 
 ||| Return the number of seconds since epoch.
diff --git a/pom.xml b/pom.xml
index 5e0773364..268da8c3a 100644
--- a/pom.xml
+++ b/pom.xml
@@ -25,7 +25,7 @@
     </developers>
 
     <properties>
-        <asm.version>9.4</asm.version>
+        <asm.version>9.7.1</asm.version>
         <assertj.version>3.16.1</assertj.version>
         <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
         <project.scm.id>github</project.scm.id>
diff --git a/src/Compiler/Jvm/Asm.idr b/src/Compiler/Jvm/Asm.idr
index fb4d728d9..f16ec54ae 100644
--- a/src/Compiler/Jvm/Asm.idr
+++ b/src/Compiler/Jvm/Asm.idr
@@ -451,31 +451,6 @@ namespace AsmGlobalState
     addFunction : HasIO io => AsmGlobalState -> Jname -> Function -> io ()
     addFunction globalState name function = jaddFunction globalState (getSimpleName name) function
 
-    export
-    %foreign jvm' "io/github/mmhelloworld/idrisjvm/assembler/AsmGlobalState" ".isUntypedFunction"
-                "io/github/mmhelloworld/idrisjvm/assembler/AsmGlobalState String" "boolean"
-    prim_jisUntypedFunction : AsmGlobalState -> String -> PrimIO Bool
-
-    jisUntypedFunction : HasIO io => AsmGlobalState -> String -> io Bool
-    jisUntypedFunction state name = primIO $ prim_jisUntypedFunction state name
-
-    public export
-    isUntypedFunction : HasIO io => AsmGlobalState -> Jname -> io Bool
-    isUntypedFunction globalState name = jisUntypedFunction globalState (getSimpleName name)
-
-    public export
-    %foreign jvm' "io/github/mmhelloworld/idrisjvm/assembler/AsmGlobalState" ".addUntypedFunction"
-                "io/github/mmhelloworld/idrisjvm/assembler/AsmGlobalState String" "void"
-    prim_jaddUntypedFunction : AsmGlobalState -> String -> PrimIO ()
-
-    public export
-    jaddUntypedFunction : HasIO io => AsmGlobalState -> String -> io ()
-    jaddUntypedFunction state name = primIO $ prim_jaddUntypedFunction state name
-
-    public export
-    addUntypedFunction : HasIO io => AsmGlobalState -> Jname -> io ()
-    addUntypedFunction globalState name = jaddUntypedFunction globalState (getSimpleName name)
-
     public export
     %foreign jvm' "io/github/mmhelloworld/idrisjvm/assembler/AsmGlobalState" ".classCodeEnd"
                 "io/github/mmhelloworld/idrisjvm/assembler/AsmGlobalState String String String" "void"
@@ -638,6 +613,7 @@ Show Scope where
         ("index", show $ index scope),
         ("parentIndex", show $ parentIndex scope),
         ("nextVariableIndex", show $ nextVariableIndex scope),
+        ("variableTypes", show $ unsafePerformIO $ Map.toList $ variableTypes scope),
         ("lineNumbers", show $ lineNumbers scope),
         ("variableIndices", toString $ variableIndices scope),
         ("returnType", show $ returnType scope),
@@ -680,10 +656,17 @@ public export
 %foreign "jvm:crash(String java/lang/Object),io/github/mmhelloworld/idrisjvm/runtime/Runtime"
 crash : String -> Object
 
+public export
+%foreign "jvm:getStackTraceString(String),io/github/mmhelloworld/idrisjvm/runtime/Runtime"
+getStackTraceString : PrimIO String
+
 export
 asmCrash : String -> Core a
-asmCrash message = throw (InternalError message)
+asmCrash message = do
+  stackTrace <- coreLift $ primIO getStackTraceString
+  throw (InternalError $ message ++ "\n" ++ stackTrace)
 
+export
 isBoolTySpec : Name -> Bool
 isBoolTySpec name = name == basics "Bool" || name == (NS preludeNS (UN $ Basic "Bool"))
 
@@ -730,14 +713,6 @@ export
 arrayName : Name
 arrayName = NS (mkNamespace "Java.Lang") (UN $ Basic "Array")
 
-getIdrisConstructorType : ConInfo -> (tag: Maybe Int) -> Nat -> Name -> InferredType
-getIdrisConstructorType conInfo tag arity name =
-  if isBoolTySpec name then IBool
-  else if name == basics "List" then idrisListType
-  else if name == preludetypes "Maybe" then idrisMaybeType
-  else if name == preludetypes "Nat" then inferredBigIntegerType
-  else inferredObjectType
-
 parseName : String -> Maybe InferredType
 parseName name =
   case words name of
@@ -2320,14 +2295,6 @@ export
 getFcAndDefinition : {auto stateRef: Ref AsmState AsmState} -> String -> Core (FC, NamedDef)
 getFcAndDefinition name = coreLift $ AsmGlobalState.getFcAndDefinition !getGlobalState name
 
-export
-isUntypedFunction : {auto stateRef: Ref AsmState AsmState} -> Jname -> Core Bool
-isUntypedFunction name = coreLift $ AsmGlobalState.isUntypedFunction !getGlobalState name
-
-export
-addUntypedFunction : {auto stateRef: Ref AsmState AsmState} -> Jname -> Core ()
-addUntypedFunction name = coreLift $ AsmGlobalState.addUntypedFunction !getGlobalState name
-
 export
 setCurrentFunction : {auto stateRef: Ref AsmState AsmState} -> Function -> Core ()
 setCurrentFunction function = updateState $ { currentIdrisFunction := function }
@@ -2546,7 +2513,19 @@ retrieveVariableIndicesByName scopeIndex = do
         go1 scopeIndex = do
             scope <- getScope scopeIndex
             coreLift $ updateVariableIndices acc (variableIndices scope)
-            maybe (pure ()) go1 (parentIndex scope)
+            let Just nextScopeIndex = parentIndex scope
+                  | Nothing => pure ()
+            go1 nextScopeIndex
+
+isParameter : {auto stateRef: Ref AsmState AsmState} -> String -> Core Bool
+isParameter name = do
+  scope <- getScope 0
+  optIndex <- coreLift $ Map.get {value=Int} (variableIndices scope) name
+  case nullableToMaybe optIndex of
+    Nothing => pure False
+    Just index => do
+      function <- getCurrentFunction
+      pure (index < cast (length (parameterTypes (inferredFunctionType function))))
 
 export
 retrieveVariables : {auto stateRef: Ref AsmState AsmState} -> Int -> Core (List String)
@@ -2649,21 +2628,14 @@ export
 getVariableType : {auto stateRef: Ref AsmState AsmState} -> String -> Core InferredType
 getVariableType name = getVariableTypeAtScope !getCurrentScopeIndex name
 
-updateArgumentsForUntyped : Map Int InferredType -> Nat -> IO ()
-updateArgumentsForUntyped _ Z = pure ()
-updateArgumentsForUntyped types (S n) = do
-  ignore $ Map.put types (cast {to=Int} n) inferredObjectType
-  updateArgumentsForUntyped types n
-
 export
-updateScopeVariableTypes : {auto stateRef: Ref AsmState AsmState} -> Nat -> Core ()
-updateScopeVariableTypes arity = go (scopeCounter !getState - 1) where
+updateScopeVariableTypes : {auto stateRef: Ref AsmState AsmState} -> Core ()
+updateScopeVariableTypes = go (scopeCounter !getState - 1) where
     go : Int -> Core ()
     go scopeIndex =
         if scopeIndex < 0 then pure ()
         else do
             variableTypes <- retrieveVariableTypesAtScope scopeIndex
-            when (scopeIndex == 0) $ coreLift $ updateArgumentsForUntyped variableTypes arity
             variableIndices <- retrieveVariableIndicesByName scopeIndex
             scope <- getScope scopeIndex
             saveScope $ {allVariableTypes := variableTypes, allVariableIndices := variableIndices} scope
@@ -2679,18 +2651,23 @@ getVariableScope name = go !getCurrentScopeIndex where
             Just _ => pure scope
             Nothing => case parentIndex scope of
                 Just parentScopeIndex => go parentScopeIndex
-                Nothing => asmCrash ("Unknown variable " ++ name)
+                Nothing => do
+                  let functionName = idrisName !getCurrentFunction
+                  asmCrash ("Unknown variable \{name} in function \{show functionName}")
 
 export
-addVariableType : {auto stateRef: Ref AsmState AsmState} -> String -> InferredType -> Core InferredType
-addVariableType var IUnknown = pure IUnknown
-addVariableType var ty = do
+addVariableType : {auto stateRef: Ref AsmState AsmState} -> String -> InferredType -> Core ()
+addVariableType _ IUnknown = pure ()
+addVariableType var ty = when (not !(isParameter var)) $ do
     scope <- getVariableScope var
-    let scopeIndex = index scope
-    existingTy <- retrieveVariableTypeAtScope scopeIndex var
-    let newTy = existingTy <+> ty
-    _ <- coreLift $ Map.put (variableTypes scope) var newTy
-    pure newTy
+    ignore $ coreLift $ Map.put (variableTypes scope) var ty
+
+export
+retrieveVariableType : {auto stateRef: Ref AsmState AsmState} -> String -> Core InferredType
+retrieveVariableType var = do
+  scope <- getVariableScope var
+  let scopeIndex = index scope
+  retrieveVariableTypeAtScope scopeIndex var
 
 %inline
 export
@@ -2733,9 +2710,18 @@ mutual
       then pure $ parseName namePartsStr
       else pure Nothing
   parseJvmReferenceType (NmCon _ name conInfo tag args) =
-    if name == primio "IORes" then
-      maybe (asmCrash "Expected an argument for IORes") (\res => pure $ Just !(tySpec res)) (head' args)
-    else pure $ Just $ getIdrisConstructorType conInfo tag (length args) name
+      if name == primio "IORes" then
+        maybe (asmCrash "Expected an argument for IORes") (\res => pure $ Just !(tySpec res)) (head' args)
+      else pure $ Just $ getIdrisConstructorType name
+    where
+      getIdrisConstructorType : Name -> InferredType
+      getIdrisConstructorType name =
+        if isBoolTySpec name then IBool
+        else if name == basics "List" then idrisListType
+        else if name == preludetypes "Maybe" then idrisMaybeType
+        else if name == preludetypes "Nat" then inferredBigIntegerType
+        else inferredObjectType
+
   parseJvmReferenceType (NmApp fc (NmRef _ name) _) = do
     (_, MkNmFun _ def) <- getFcAndDefinition (jvmSimpleName name)
       | _ => asmCrash ("Expected a function returning a tuple containing interface type and method type at " ++
@@ -2768,7 +2754,6 @@ mutual
     ty <- tryParse expr
     pure $ fromMaybe inferredObjectType ty
 
-
 export
 asmReturn : {auto stateRef: Ref AsmState AsmState} -> InferredType -> Core ()
 asmReturn IVoid    = return
diff --git a/src/Compiler/Jvm/Codegen.idr b/src/Compiler/Jvm/Codegen.idr
index 6b4b3b767..4d03c3647 100644
--- a/src/Compiler/Jvm/Codegen.idr
+++ b/src/Compiler/Jvm/Codegen.idr
@@ -21,13 +21,6 @@ import Data.Vect
 
 import Debug.Trace
 
-import Core.Env
-
-import Idris.Pretty.Annotations
-import Idris.Syntax
-import Idris.Resugar
-import Idris.Doc.String
-
 import Libraries.Data.NameMap
 import Libraries.Data.SortedMap
 import Libraries.Utils.Path
@@ -57,14 +50,6 @@ import Idris.Syntax
 %hide Core.Name.Scoped.Scope
 %hide System.FFI.runtimeClass
 
-getType : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> Name -> Core (Maybe (Term []))
-getType name = do
-  defs <- get Ctxt
-  Just gdef <- lookupCtxtExact name (gamma defs)
-    | Nothing => pure Nothing
-  ty <- normaliseHoles defs [] gdef.type
-  Just <$> toFullNames ty
-
 addScopeLocalVariables : {auto stateRef: Ref AsmState AsmState} -> Scope -> Core ()
 addScopeLocalVariables scope = do
     let scopeIndex = index scope
@@ -227,7 +212,8 @@ getSwitchCasesWithEndLabel switchCases labelStarts = go $ zip switchCases (drop
 labelHashCodeAlt : {auto stateRef: Ref AsmState AsmState} -> (Int, a) -> Core (String, Int, a)
 labelHashCodeAlt (hash, expressions) = pure (!newLabel, hash, expressions)
 
-getHashCodeCasesWithLabels : {auto stateRef: Ref AsmState AsmState} -> SortedMap Int (List (Int, a)) -> Core (List (String, Int, List (Int, a)))
+getHashCodeCasesWithLabels : {auto stateRef: Ref AsmState AsmState} -> SortedMap Int (List (Int, a))
+                           -> Core (List (String, Int, List (Int, a)))
 getHashCodeCasesWithLabels positionAndAltsByHash = traverse labelHashCodeAlt $ SortedMap.toList positionAndAltsByHash
 
 toUnsignedInt : {auto stateRef: Ref AsmState AsmState} -> Int -> Core ()
@@ -325,7 +311,8 @@ intToBigInteger = do
   invokeMethod InvokeStatic "java/math/BigInteger" "valueOf" "(J)Ljava/math/BigInteger;" False
 
 mutual
-    assembleExpr : {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool) -> InferredType -> NamedCExp -> Core ()
+    assembleExpr : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool)
+                 -> InferredType -> NamedCExp -> Core ()
     assembleExpr isTailCall returnType (NmDelay _ _ expr) =
         assembleSubMethodWithScope isTailCall returnType Nothing Nothing expr
     assembleExpr isTailCall returnType (NmLocal _ loc) = do
@@ -432,8 +419,7 @@ mutual
       assembleCons isTailCall returnType head tail
     assembleExpr isTailCall returnType expr@(NmCon fc _ CONS _ _) = throw $ GenericMsg fc "Invalid CONS constructor"
 
-    assembleExpr isTailCall returnType expr@(NmCon fc name conInfo tag args) =
-        assembleCon isTailCall returnType fc name tag args
+    assembleExpr isTailCall returnType expr@(NmCon fc name conInfo tag args) = assembleCon isTailCall returnType fc name tag args
 
     assembleExpr isTailCall returnType (NmOp fc fn args) = do
         assembleExprOp returnType fc fn args
@@ -506,17 +492,21 @@ mutual
         when isTailCall $ asmReturn returnType
     assembleExpr _ _ expr = throw $ GenericMsg (getFC expr) $ "Cannot compile " ++ show expr ++ " yet"
 
-    castInt : {auto stateRef: Ref AsmState AsmState} -> InferredType -> Core () -> NamedCExp -> Core ()
+    castInt : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType -> Core ()
+            -> NamedCExp -> Core ()
     castInt returnType conversionOp expr = jassembleCast returnType IInt IInt conversionOp expr
 
-    jassembleCast : {auto stateRef: Ref AsmState AsmState} -> InferredType -> InferredType -> InferredType -> Core ()
+    jassembleCast : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType
+                  -> InferredType -> InferredType -> Core ()
                   -> NamedCExp -> Core ()
     jassembleCast returnType from to conversionOp expr = do
         assembleExpr False from expr
         conversionOp
         asmCast to returnType
 
-    assembleNmAppNilArity : {auto stateRef: Ref AsmState AsmState} -> (isTailCall : Bool) -> InferredType -> Name -> Core ()
+    assembleNmAppNilArity : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo}
+                          -> {auto stateRef: Ref AsmState AsmState} -> (isTailCall : Bool)
+                          -> InferredType -> Name -> Core ()
     assembleNmAppNilArity isTailCall returnType idrisName = do
         let jname = jvmName idrisName
         let functionName = getIdrisFunctionName !getProgramName (className jname) (methodName jname)
@@ -540,7 +530,8 @@ mutual
       invokeMethod InvokeVirtual "java/math/BigInteger" "intValue" "()I" False
       op
 
-    assembleCon : {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool) -> InferredType -> FC -> Name -> (tag : Maybe Int) -> List NamedCExp -> Core ()
+    assembleCon : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool)
+                -> InferredType -> FC -> Name -> (tag : Maybe Int) -> List NamedCExp -> Core ()
     assembleCon isTailCall returnType fc name tag args = do
         let fileName = fst $ getSourceLocationFromFc fc
         let constructorClassName = getIdrisConstructorClassName (jvmSimpleName name)
@@ -563,7 +554,8 @@ mutual
         asmCast idrisObjectType returnType
         when isTailCall $ asmReturn returnType
 
-    assembleCons : {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool) -> InferredType -> NamedCExp -> NamedCExp -> Core ()
+    assembleCons : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool)
+                 -> InferredType -> NamedCExp -> NamedCExp -> Core ()
     assembleCons isTailCall returnType head tail = do
         new idrisConsClass
         dup
@@ -573,7 +565,8 @@ mutual
         asmCast idrisObjectType returnType
         when isTailCall $ asmReturn returnType
 
-    assembleJust : {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool) -> InferredType -> NamedCExp -> Core ()
+    assembleJust : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool)
+                 -> InferredType -> NamedCExp -> Core ()
     assembleJust isTailCall returnType value = do
         new idrisJustClass
         dup
@@ -582,7 +575,8 @@ mutual
         asmCast idrisObjectType returnType
         when isTailCall $ asmReturn returnType
 
-    assembleConstructorSwitchExpr : {auto stateRef: Ref AsmState AsmState} -> NamedCExp -> Core Int
+    assembleConstructorSwitchExpr : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                                  -> NamedCExp -> Core Int
     assembleConstructorSwitchExpr (NmLocal _ loc) = getVariableIndex $ jvmSimpleName loc
     assembleConstructorSwitchExpr sc = do
         idrisObjectVariableIndex <- getVariableIndex $ "constructorSwitchValue" ++ show !newDynamicVariableIndex
@@ -590,7 +584,9 @@ mutual
         storeVar idrisObjectType idrisObjectType idrisObjectVariableIndex
         pure idrisObjectVariableIndex
 
-    assembleExprBinaryOp : {auto stateRef: Ref AsmState AsmState} -> InferredType -> InferredType -> Core ()
+    assembleExprBinaryOp : {auto c : Ref Ctxt Defs}
+                         -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType
+                         -> InferredType -> Core ()
                          -> NamedCExp -> NamedCExp -> Core ()
     assembleExprBinaryOp returnType exprType operator expr1 expr2 = do
         assembleExpr False exprType expr1
@@ -598,8 +594,8 @@ mutual
         operator
         asmCast exprType returnType
 
-    assembleExprBinaryBoolOp : {auto stateRef: Ref AsmState AsmState} -> InferredType -> InferredType
-                             -> (String -> Core ()) -> NamedCExp -> NamedCExp -> Core ()
+    assembleExprBinaryBoolOp : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType
+                             -> InferredType -> (String -> Core ()) -> NamedCExp -> NamedCExp -> Core ()
     assembleExprBinaryBoolOp returnType exprType operator expr1 expr2 = do
         assembleExpr False exprType expr1
         assembleExpr False exprType expr2
@@ -618,8 +614,9 @@ mutual
         labelStart endLabel
         asmCast IInt returnType
 
-    assembleExprComparableBinaryBoolOp : {auto stateRef: Ref AsmState AsmState} -> InferredType -> String -> (String -> Core ()) ->
-        NamedCExp -> NamedCExp -> Core ()
+    assembleExprComparableBinaryBoolOp : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                                       -> InferredType -> String -> (String -> Core ())
+                                       -> NamedCExp -> NamedCExp -> Core ()
     assembleExprComparableBinaryBoolOp returnType className operator expr1 expr2 = do
         let exprType = IRef className Class []
         assembleExpr False exprType expr1
@@ -640,13 +637,15 @@ mutual
         labelStart endLabel
         asmCast IInt returnType
 
-    assembleExprUnaryOp : {auto stateRef: Ref AsmState AsmState} -> InferredType -> InferredType -> Core () -> NamedCExp -> Core ()
+    assembleExprUnaryOp : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType
+                        -> InferredType -> Core () -> NamedCExp -> Core ()
     assembleExprUnaryOp returnType exprType operator expr = do
         assembleExpr False exprType expr
         operator
         asmCast exprType returnType
 
-    assembleStrCons : {auto stateRef: Ref AsmState AsmState} -> InferredType -> (char: NamedCExp) -> (str: NamedCExp) -> Core ()
+    assembleStrCons : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType
+                    -> (char: NamedCExp) -> (str: NamedCExp) -> Core ()
     assembleStrCons returnType char str = do
         new "java/lang/StringBuilder"
         dup
@@ -659,7 +658,8 @@ mutual
         invokeMethod InvokeVirtual "java/lang/StringBuilder" "toString" "()Ljava/lang/String;" False
         asmCast inferredStringType returnType
 
-    assembleStrReverse : {auto stateRef: Ref AsmState AsmState} -> InferredType -> NamedCExp -> Core ()
+    assembleStrReverse : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType
+                       -> NamedCExp -> Core ()
     assembleStrReverse returnType str = do
         new "java/lang/StringBuilder"
         dup
@@ -678,7 +678,8 @@ mutual
     compareSignedLong : {auto stateRef: Ref AsmState AsmState} -> (String -> Core ()) -> String -> Core ()
     compareSignedLong op label = do lcmp; op label
 
-    assembleCast : {auto stateRef: Ref AsmState AsmState} -> InferredType -> FC -> PrimType -> PrimType -> NamedCExp -> Core ()
+    assembleCast : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType -> FC
+                 -> PrimType -> PrimType -> NamedCExp -> Core ()
     assembleCast returnType fc from to x =
       jassembleCast returnType (getInferredType from) (getInferredType to) (getCastAsmOp from to) x
 
@@ -922,7 +923,8 @@ mutual
         invokeMethod InvokeStatic "java/lang/Integer" "toString" "(I)Ljava/lang/String;" False
     getCastAsmOp _ _ = pure ()
 
-    assembleExprOp : {auto stateRef: Ref AsmState AsmState} -> InferredType -> FC -> PrimFn arity -> Vect arity NamedCExp -> Core ()
+    assembleExprOp : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType -> FC
+                   -> PrimFn arity -> Vect arity NamedCExp -> Core ()
     assembleExprOp returnType fc (Neg Bits64Type) [x] = assembleExprUnaryOp returnType ILong lneg x
     assembleExprOp returnType fc (ShiftR Bits64Type) [x, y] = assembleExprBinaryOp returnType ILong (do l2i; lushr) x y
     assembleExprOp returnType fc (BAnd Bits64Type) [x, y] = assembleExprBinaryOp returnType ILong land x y
@@ -1144,10 +1146,11 @@ mutual
 
     assembleExprOp returnType fc op _ = throw $ GenericMsg fc ("Unsupported operator " ++ show op)
 
-    assembleParameter : {auto stateRef: Ref AsmState AsmState} -> (NamedCExp, InferredType) -> Core ()
+    assembleParameter : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                      -> (NamedCExp, InferredType) -> Core ()
     assembleParameter (param, ty) = assembleExpr False ty param
 
-    storeParameter : {auto stateRef: Ref AsmState AsmState} -> Map Int InferredType
+    storeParameter : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> Map Int InferredType
                    -> (Int, NamedCExp, InferredType) -> Core Int
     storeParameter variableTypes (var, (NmLocal _ loc), ty) = do
         let valueVariableName = jvmSimpleName loc
@@ -1166,7 +1169,8 @@ mutual
         storeVar ty ty targetVariableIndex
         pure targetVariableIndex
 
-    createMethodReference : {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool) -> (arity: Nat) -> Name -> Core ()
+    createMethodReference : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                          -> (isTailCall: Bool) -> (arity: Nat) -> Name -> Core ()
     createMethodReference isTailCall arity name = do
         let jname = jvmName name
         functionType <- case !(findFunctionType jname) of
@@ -1185,13 +1189,15 @@ mutual
           invokeMethod InvokeStatic functionsClass "curry" methodDescriptor False
         when isTailCall $ asmReturn inferredLambdaType
 
-    assembleSubMethodWithScope1 : {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool) -> InferredType
+    assembleSubMethodWithScope1 : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                                -> (isTailCall: Bool) -> InferredType
                                 -> (parameterName : Maybe Name) -> NamedCExp -> Core ()
     assembleSubMethodWithScope1 isTailCall returnType parameterName body = do
         parentScope <- getScope !getCurrentScopeIndex
         withScope $ assembleSubMethod isTailCall returnType Nothing parameterName parentScope body
 
-    assembleMethodReference : {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool) -> InferredType
+    assembleMethodReference : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                            -> (isTailCall: Bool) -> InferredType
                             -> (isMethodReference : Bool) -> (arity: Nat) -> (functionName: Name)
                             -> (parameterName : Maybe Name) -> NamedCExp -> Core ()
     assembleMethodReference isTailCall returnType isMethodReference arity functionName parameterName body =
@@ -1199,7 +1205,9 @@ mutual
         then createMethodReference isTailCall arity functionName
         else assembleSubMethodWithScope1 isTailCall returnType parameterName body
 
-    assembleSubMethodWithScope : {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool) -> InferredType
+    assembleSubMethodWithScope : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo}
+                               -> {auto stateRef: Ref AsmState AsmState}
+                               -> (isTailCall: Bool) -> InferredType
                                -> (parameterValue: Maybe NamedCExp) -> (parameterName : Maybe Name)
                                -> NamedCExp -> Core ()
     assembleSubMethodWithScope isTailCall returnType (Just value) (Just name) body = do
@@ -1218,52 +1226,36 @@ mutual
           assembleValue enclosingScope variableName = do
             lambdaScopeIndex <- getCurrentScopeIndex
             updateCurrentScopeIndex (index enclosingScope)
-            assembleExpr False !(getVariableType variableName) value
+            assembleExpr False !(getVariableTypeAtScope lambdaScopeIndex variableName) value
             updateCurrentScopeIndex lambdaScopeIndex
 
     assembleSubMethodWithScope isTailCall returnType _ p0
       body@(NmLam _ p1 (NmLam _ p2 (NmLam _ p3 (NmLam _ p4 (NmApp _ (NmRef _ name) [NmLocal _ arg0, NmLocal _ arg1,
-        NmLocal _ arg2, NmLocal _ arg3, NmLocal _ arg4]))))) = assembleMethodReference
-            isTailCall returnType
-            (maybe False ((==) arg0) p0 && p1 == arg1 && p2 == arg2 && p3 == arg3 && p4 == arg4)
-            5 name p0 body
+        NmLocal _ arg2, NmLocal _ arg3, NmLocal _ arg4]))))) = do
+          isMethodReference <- canUseMethodReference name [arg0, arg1, arg2, arg3, arg4] p0 [p1, p2, p3, p4]
+          assembleMethodReference isTailCall returnType isMethodReference 5 name p0 body
     assembleSubMethodWithScope isTailCall returnType _ p0
       body@(NmLam _ p1 (NmLam _ p2 (NmLam _ p3 (NmApp _ (NmRef _ name) [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2,
-        NmLocal _ arg3])))) = assembleMethodReference isTailCall returnType
-          (maybe False ((==) arg0) p0 && p1 == arg1 && p2 == arg2 && p3 == arg3) 4 name p0 body
+        NmLocal _ arg3])))) = do
+          isMethodReference <- canUseMethodReference name [arg0, arg1, arg2, arg3] p0 [p1, p2, p3]
+          assembleMethodReference isTailCall returnType isMethodReference 4 name p0 body
     assembleSubMethodWithScope isTailCall returnType _ p0
-      body@(NmLam _ p1 (NmLam _ p2 (NmApp _ (NmRef _ name) [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2]))) =
-        assembleMethodReference isTailCall returnType (maybe False ((==) arg0) p0 && p1 == arg1 && p2 == arg2)
-          3 name p0 body
+      body@(NmLam _ p1 (NmLam _ p2 (NmApp _ (NmRef _ name) [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2]))) = do
+        isMethodReference <- canUseMethodReference name [arg0, arg1, arg2] p0 [p1, p2]
+        assembleMethodReference isTailCall returnType isMethodReference 3 name p0 body
     assembleSubMethodWithScope isTailCall returnType _ p0
-      body@(NmLam _ p1 (NmApp _ (NmRef _ name) [NmLocal _ arg0, NmLocal _ arg1])) =
-        assembleMethodReference isTailCall returnType (maybe False ((==) arg0) p0 && p1 == arg1)
-          2 name p0 body
-    assembleSubMethodWithScope isTailCall returnType _ p0 body@(NmApp _ (NmRef _ name) [NmLocal _ arg0]) =
-      assembleMethodReference isTailCall returnType (maybe False ((==) arg0) p0) 1 name p0 body
-
-    assembleSubMethodWithScope isTailCall returnType _ parameterName body@(NmLam _ c (NmLam _ a (NmLocal _ b))) =
-      let hasParameter = isJust parameterName
-      in if hasParameter && c == b
-          then assembleConstant1Lambda isTailCall
-          else if hasParameter && a == b
-            then assembleIdentity2Lambda isTailCall
-            else assembleSubMethodWithScope1 isTailCall returnType parameterName body
-    assembleSubMethodWithScope isTailCall returnType _ parameterName body@(NmLam _ a (NmLocal _ b)) =
-      if maybe False ((==) b) parameterName
-        then assembleConstantLambda isTailCall
-        else if isJust parameterName && a == b
-          then assembleIdentity1Lambda isTailCall
-          else assembleSubMethodWithScope1 isTailCall returnType parameterName body
-    assembleSubMethodWithScope isTailCall returnType _ parameterName body@(NmLocal _ b) =
-      if maybe False ((==) b) parameterName
-        then assembleIdentityLambda isTailCall
-        else assembleSubMethodWithScope1 isTailCall returnType parameterName body
+      body@(NmLam _ p1 (NmApp _ (NmRef _ name) [NmLocal _ arg0, NmLocal _ arg1])) = do
+        isMethodReference <- canUseMethodReference name [arg0, arg1] p0 [p1]
+        assembleMethodReference isTailCall returnType isMethodReference 2 name p0 body
+    assembleSubMethodWithScope isTailCall returnType _ p0 body@(NmApp _ (NmRef _ name) [NmLocal _ arg0]) = do
+      isMethodReference <- canUseMethodReference name [arg0] p0 []
+      assembleMethodReference isTailCall returnType isMethodReference 1 name p0 body
+
     assembleSubMethodWithScope isTailCall returnType _ parameterName body =
       assembleSubMethodWithScope1 isTailCall returnType parameterName body
 
-    assembleSubMethod : {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool) -> InferredType
-                      -> (parameterValueExpr: (Maybe (Core ()))) -> (parameterName: Maybe Name) -> Scope
+    assembleSubMethod : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> (isTailCall: Bool)
+                      -> InferredType -> (parameterValueExpr: (Maybe (Core ()))) -> (parameterName: Maybe Name) -> Scope
                       -> NamedCExp -> Core ()
     assembleSubMethod isTailCall lambdaReturnType parameterValueExpr parameterName declaringScope expr = do
             scope <- getScope !getCurrentScopeIndex
@@ -1392,9 +1384,9 @@ mutual
         defaultValue returnType
         asmReturn returnType
 
-    assembleConstantSwitch : {auto stateRef: Ref AsmState AsmState} -> (returnType: InferredType)
-                           -> (switchExprType: InferredType) -> FC -> NamedCExp -> List NamedConstAlt
-                           -> Maybe NamedCExp -> Core ()
+    assembleConstantSwitch : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                           -> (returnType: InferredType) -> (switchExprType: InferredType) -> FC -> NamedCExp
+                           -> List NamedConstAlt -> Maybe NamedCExp -> Core ()
     assembleConstantSwitch _ _ fc _ [] _ = throw $ GenericMsg fc "Empty cases"
 
     assembleConstantSwitch returnType IInt fc sc alts def = do
@@ -1529,7 +1521,9 @@ mutual
                         switchBody label nextLabel position alt
                         go nextLabel positionAndAlts
 
-    assembleConCase : {auto stateRef: Ref AsmState AsmState} -> InferredType -> FC -> (sc : NamedCExp) -> List NamedConAlt -> Maybe NamedCExp -> Core ()
+    assembleConCase : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo}
+                    -> {auto stateRef: Ref AsmState AsmState}
+                    -> InferredType -> FC -> (sc : NamedCExp) -> List NamedConAlt -> Maybe NamedCExp -> Core ()
     assembleConCase returnType fc sc alts def = do
         idrisObjectVariableIndex <- assembleConstructorSwitchExpr sc
         let hasTypeCase = any isTypeCase alts
@@ -1537,8 +1531,10 @@ mutual
         variableTypes <- getVariableTypes
         optTy <- coreLift $ Map.get variableTypes idrisObjectVariableIndex
         let idrisObjectVariableType = fromMaybe IUnknown $ nullableToMaybe optTy
-        loadVar variableTypes idrisObjectVariableType idrisObjectType idrisObjectVariableIndex
-        when (idrisObjectVariableType /= idrisObjectType) $ do
+        let isIdrisObject = idrisObjectVariableType /= IUnknown && idrisObjectVariableType /= inferredObjectType
+        let targetType = if (not isIdrisObject) then idrisObjectType else idrisObjectVariableType
+        loadVar variableTypes idrisObjectVariableType targetType idrisObjectVariableIndex
+        when (not isIdrisObject) $ do
             storeVar idrisObjectType idrisObjectType idrisObjectVariableIndex
             loadVar !getVariableTypes idrisObjectType idrisObjectType idrisObjectVariableIndex
         let constructorGetter = if hasTypeCase then "getStringConstructorId" else "getConstructorId"
@@ -1547,7 +1543,8 @@ mutual
             then assembleStringConstructorSwitch returnType fc idrisObjectVariableIndex alts def
             else assembleConstructorSwitch returnType fc idrisObjectVariableIndex alts def
 
-    assembleConCaseExpr : {auto stateRef: Ref AsmState AsmState} -> InferredType -> Int -> List Name -> NamedCExp -> Core ()
+    assembleConCaseExpr : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType -> Int
+                        -> List Name -> NamedCExp -> Core ()
     assembleConCaseExpr returnType idrisObjectVariableIndex args expr = do
             variableTypes <- getVariableTypes
             optTy <- coreLift $ Map.get variableTypes idrisObjectVariableIndex
@@ -1567,7 +1564,8 @@ mutual
                     storeVar inferredObjectType !(getVariableType variableName) variableIndex
                 bindArg idrisObjectVariableType variableTypes (index + 1) vars
 
-    assembleConstructorSwitch : {auto stateRef: Ref AsmState AsmState} -> InferredType -> FC -> Int -> List NamedConAlt -> Maybe NamedCExp -> Core ()
+    assembleConstructorSwitch : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState} -> InferredType
+                              -> FC -> Int -> List NamedConAlt -> Maybe NamedCExp -> Core ()
     assembleConstructorSwitch returnType fc idrisObjectVariableIndex alts def = do
             switchCases <- getCasesWithLabels alts
             let labels = fst <$> switchCases
@@ -1613,7 +1611,8 @@ mutual
             assembleExprConAlt (labelStart, _, (MkNConAlt _ _ _ args expr), labelEnd) =
                 assembleCaseWithScope labelStart labelEnd args expr
 
-    assembleStringConstructorSwitch : {auto stateRef: Ref AsmState AsmState} -> InferredType -> FC -> Int -> List NamedConAlt -> Maybe NamedCExp -> Core ()
+    assembleStringConstructorSwitch : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                                    -> InferredType -> FC -> Int -> List NamedConAlt -> Maybe NamedCExp -> Core ()
     assembleStringConstructorSwitch returnType fc idrisObjectVariableIndex alts def = do
         constantExprVariableSuffixIndex <- newDynamicVariableIndex
         let constantExprVariableName = "constructorCaseExpr" ++ show constantExprVariableSuffixIndex
@@ -1691,14 +1690,14 @@ mutual
                     switchBody label nextLabel position alt
                     go nextLabel positionAndAlts
 
-    asmJavaLambda : {auto stateRef: Ref AsmState AsmState} -> FC -> InferredType -> NamedCExp -> NamedCExp -> NamedCExp -> Core ()
+    asmJavaLambda : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                  -> FC -> InferredType -> NamedCExp -> NamedCExp -> NamedCExp -> Core ()
     asmJavaLambda fc returnType functionType javaInterfaceType lambda = do
         assembleExpr False inferredLambdaType lambda
         lambdaType <- getJavaLambdaType fc [functionType, javaInterfaceType, lambda]
         let samType =
           if isIoAction then {parameterTypes $= dropWorldType} lambdaType.methodType else lambdaType.methodType
-        let lambdaImplementationType = lambdaType.implementationType
-        let lambdaImplementationType = updateImplementationType samType.returnType lambdaImplementationType
+        let lambdaImplementationType = updateImplementationType samType.returnType lambdaType.implementationType
         let invokeDynamicType = MkInferredFunctionType lambdaType.javaInterface [inferredLambdaType]
         let invokeDynamicDescriptor = getMethodDescriptor invokeDynamicType
         let implementationParameterTypes = lambdaImplementationType.parameterTypes
@@ -1764,7 +1763,8 @@ mutual
           when (rest /= [] || isIoAction) $ asmCast inferredObjectType inferredLambdaType
           applyParameters typesByIndex (index + 1) returnType rest
 
-    jvmExtPrim : {auto stateRef: Ref AsmState AsmState} -> FC -> InferredType -> ExtPrim -> List NamedCExp -> Core ()
+    jvmExtPrim : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+               -> FC -> InferredType -> ExtPrim -> List NamedCExp -> Core ()
     jvmExtPrim fc returnType JvmInstanceMethodCall [ret, NmApp _ _ [functionNamePrimVal], fargs, world] =
       jvmExtPrim fc returnType JvmInstanceMethodCall [ret, functionNamePrimVal, fargs, world]
     jvmExtPrim _ returnType JvmInstanceMethodCall [ret, NmPrimVal fc (Str fn), fargs, world] = do
@@ -1793,7 +1793,7 @@ mutual
         else aconstnull
     jvmExtPrim fc returnType JvmStaticMethodCall [ret, NmApp _ _ [functionNamePrimVal], fargs, world] =
       jvmExtPrim fc returnType JvmStaticMethodCall [ret, functionNamePrimVal, fargs, world]
-    jvmExtPrim _ returnType JvmStaticMethodCall [ret, NmPrimVal fc (Str fn), fargs, world] = do
+    jvmExtPrim _ returnType JvmStaticMethodCall [ret, NmPrimVal fc (Str fn), fargs, _] = do
         args <- getFArgs fargs
         argTypes <- traverse tySpec (map fst args)
         let (cname, mnameWithDot) = break (== '.') fn
@@ -1812,7 +1812,7 @@ mutual
         let mname = if isSuper then "<init>" else mname
         invokeMethod invocationType cname mname methodDescriptor False
         asmCast methodReturnType returnType
-    jvmExtPrim _ returnType SetInstanceField [ret, NmPrimVal fc (Str fn), fargs, world] = do
+    jvmExtPrim _ returnType SetInstanceField [ret, NmPrimVal fc (Str fn), fargs, _] = do
         (obj :: value :: []) <- getFArgs fargs
             | _ => asmCrash ("Setting an instance field should have two arguments for " ++ fn)
         fieldType <- tySpec (fst value)
@@ -1823,7 +1823,7 @@ mutual
         field PutField cname fieldName (getJvmTypeDescriptor fieldType)
         aconstnull
         asmCast inferredObjectType returnType
-    jvmExtPrim _ returnType SetStaticField [ret, NmPrimVal fc (Str fn), fargs, world] = do
+    jvmExtPrim _ returnType SetStaticField [ret, NmPrimVal fc (Str fn), fargs, _] = do
         (value :: []) <- getFArgs fargs
             | _ => asmCrash ("Setting a static field should have one argument for " ++ fn)
         fieldType <- tySpec (fst value)
@@ -1833,7 +1833,7 @@ mutual
         field PutStatic cname fieldName (getJvmTypeDescriptor fieldType)
         aconstnull
         asmCast inferredObjectType returnType
-    jvmExtPrim _ returnType GetInstanceField [ret, NmPrimVal fc (Str fn), fargs, world] = do
+    jvmExtPrim _ returnType GetInstanceField [ret, NmPrimVal fc (Str fn), fargs, _] = do
         (obj :: []) <- getFArgs fargs
             | _ => asmCrash ("Getting an instance field should have one argument for " ++ fn)
         fieldType <- tySpec ret
@@ -1842,34 +1842,34 @@ mutual
         let (_, fieldName) = break (\c => c /= '.' && c /= '#') fnameWithDot
         field GetField cname fieldName (getJvmTypeDescriptor fieldType)
         asmCast fieldType returnType
-    jvmExtPrim _ returnType GetStaticField [ret, NmPrimVal fc (Str fn), fargs, world] = do
+    jvmExtPrim _ returnType GetStaticField [ret, NmPrimVal fc (Str fn), fargs, _] = do
         fieldType <- tySpec ret
         let (cname, fnameWithDot) = break (== '.') fn
         let (_, fieldName) = break (\c => c /= '.' && c /= '#') fnameWithDot
         field GetStatic cname fieldName (getJvmTypeDescriptor fieldType)
         asmCast fieldType returnType
-    jvmExtPrim _ returnType NewArray [_, size, val, world] = do
+    jvmExtPrim _ returnType NewArray [_, size, val, _] = do
         assembleExpr False IInt size
         assembleExpr False IUnknown val
         invokeMethod InvokeStatic arraysClass "create" "(ILjava/lang/Object;)Ljava/util/ArrayList;" False
         asmCast arrayListType returnType
-    jvmExtPrim _ returnType ArrayGet [_, arr, pos, world] = do
+    jvmExtPrim _ returnType ArrayGet [_, arr, pos, _] = do
         assembleExpr False arrayListType arr
         assembleExpr False IInt pos
         invokeMethod InvokeVirtual arrayListClass "get" "(I)Ljava/lang/Object;" False
         asmCast inferredObjectType returnType
-    jvmExtPrim _ returnType ArraySet [_, arr, pos, val, world] = do
+    jvmExtPrim _ returnType ArraySet [_, arr, pos, val, _] = do
         assembleExpr False arrayListType arr
         assembleExpr False IInt pos
         assembleExpr False IUnknown val
         invokeMethod InvokeVirtual arrayListClass "set" "(ILjava/lang/Object;)Ljava/lang/Object;" False
         asmCast inferredObjectType returnType
-    jvmExtPrim _ returnType JvmNewArray [tyExpr, size, world] = do
+    jvmExtPrim _ returnType JvmNewArray [tyExpr, size, _] = do
         assembleExpr False IInt size
         elemTy <- tySpec tyExpr
         assembleArray elemTy
         asmCast (IArray elemTy) returnType
-    jvmExtPrim _ returnType JvmSetArray [tyExpr, index, val, arr, world] = do
+    jvmExtPrim _ returnType JvmSetArray [tyExpr, index, val, arr, _] = do
         elemTy <- tySpec tyExpr
         assembleExpr False (IArray elemTy) arr
         assembleExpr False IInt index
@@ -1877,7 +1877,7 @@ mutual
         storeArray elemTy
         aconstnull
         asmCast inferredObjectType returnType
-    jvmExtPrim _ returnType JvmGetArray [tyExpr, index, arr, world] = do
+    jvmExtPrim _ returnType JvmGetArray [tyExpr, index, arr, _] = do
         elemTy <- tySpec tyExpr
         assembleExpr False (IArray elemTy) arr
         assembleExpr False IInt index
@@ -1888,17 +1888,17 @@ mutual
         assembleExpr False (IArray elemTy) arr
         arraylength
         asmCast IInt returnType
-    jvmExtPrim _ returnType NewIORef [_, val, world] = do
+    jvmExtPrim _ returnType NewIORef [_, val, _] = do
         new refClass
         dup
         assembleExpr False IUnknown val
         invokeMethod InvokeSpecial refClass "<init>" "(Ljava/lang/Object;)V" False
         asmCast refType returnType
-    jvmExtPrim _ returnType ReadIORef [_, ref, world] = do
+    jvmExtPrim _ returnType ReadIORef [_, ref, _] = do
         assembleExpr False refType ref
         invokeMethod InvokeVirtual refClass "getValue" "()Ljava/lang/Object;" False
         asmCast inferredObjectType returnType
-    jvmExtPrim _ returnType WriteIORef [_, ref, val, world] = do
+    jvmExtPrim _ returnType WriteIORef [_, ref, val, _] = do
         assembleExpr False refType ref
         assembleExpr False IUnknown val
         invokeMethod InvokeVirtual refClass "setValue" "(Ljava/lang/Object;)V" False
@@ -1945,7 +1945,8 @@ initializeFunctionState = do
       lineNumberLabels := lineNumberLabels }
   updateCurrentFunction $ { dynamicVariableCounter := 0 }
 
-assembleDefinition : {auto stateRef: Ref AsmState AsmState} -> Name -> FC -> Core ()
+assembleDefinition : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                   -> Name -> FC -> Core ()
 assembleDefinition idrisName fc = do
     let jname = jvmName idrisName
     resetScope
@@ -1959,8 +1960,10 @@ assembleDefinition idrisName fc = do
     let methodReturnType = returnType functionType
     initializeFunctionState
     let optimizedExpr = optimizedBody function
-    when (shouldDebugFunction jname) $ logAsm $ "Assembling " ++ declaringClassName ++ "." ++ methodName ++ "\n" ++
-      showNamedCExp 0 optimizedExpr
+    when (shouldDebugFunction jname) $
+      logAsm $ "Assembling " ++ declaringClassName ++ "." ++ methodName ++
+        ": " ++ show functionType ++ "\n" ++
+        showNamedCExp 0 optimizedExpr
     let fileName = fst $ getSourceLocationFromFc fc
     let descriptor = getMethodDescriptor functionType
     -- Cache only top level nil arity functions. Don't cache extracted function results.
@@ -2010,31 +2013,23 @@ createMainMethod programName mainFunctionName = do
     maxStackAndLocal (-1) (-1)
     methodCodeEnd
 
-assemble : AsmGlobalState -> Map String (FC, NamedDef) -> Name -> IO ()
-assemble globalState fcAndDefinitionsByName name = do
-    fcDef <- Map.get {value=(FC, NamedDef)} fcAndDefinitionsByName (jvmSimpleName name)
-    case nullableToMaybe fcDef of
-        Just (fc, def) => do
-            programName <- AsmGlobalState.getProgramName globalState
-            asmState <- createAsmState globalState name
-            ignore $ runAsm asmState $ \stateRef => do
-                inferDef programName name fc def
-                assembleDefinition name fc
-                scopes <- coreLift $ ArrayList.new {elemTy=Scope}
-                updateCurrentFunction $ { scopes := (subtyping scopes), optimizedBody := emptyFunction }
-        Nothing => pure ()
+assemble : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo}
+         -> {auto stateRef: Ref AsmState AsmState} -> Name -> FC -> Core ()
+assemble name fc = do
+  inferDef name fc
+  assembleDefinition name fc
+  scopes <- coreLift $ ArrayList.new {elemTy=Scope}
+  updateCurrentFunction $ { scopes := (subtyping scopes), optimizedBody := emptyFunction }
 
 getNameStrFcDef : (Name, FC, NamedDef) -> (String, FC, NamedDef)
 getNameStrFcDef (name, fc, def) = (jvmSimpleName name, fc, def)
 
-getNameStrDef : (String, FC, NamedDef) -> (String, NamedDef)
-getNameStrDef (name, fc, def) = (name, def)
-
 isForeignDef : (Name, FC, NamedDef) -> Bool
 isForeignDef (_, _, MkNmForeign _ _ _) = True
 isForeignDef _ = False
 
-exportConstructor : {auto stateRef: Ref AsmState AsmState} -> SortedMap Namespace (List String) -> Map Int InferredType
+exportConstructor : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                  -> SortedMap Namespace (List String) -> Map Int InferredType
                   -> InferredType -> Int -> Jname -> Name -> InferredFunctionType -> Core ()
 exportConstructor typeExports jvmArgumentTypesByIndex jvmReturnType arity jvmIdrisName idrisName idrisFunctionType = do
   function <- getCurrentFunction
@@ -2067,7 +2062,8 @@ exportConstructor typeExports jvmArgumentTypesByIndex jvmReturnType arity jvmIdr
   maxStackAndLocal (-1) (-1)
   methodCodeEnd
 
-exportFunction : {auto stateRef: Ref AsmState AsmState} -> SortedMap Namespace (List String) -> MethodExport -> Core ()
+exportFunction : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+               -> SortedMap Namespace (List String) -> MethodExport -> Core ()
 exportFunction typeExports (MkMethodExport jvmFunctionName idrisName type shouldPerformIO encloser
   modifiers annotations parameterAnnotations) = do
     let jvmClassName = encloser.name
@@ -2376,8 +2372,9 @@ generateDataClass descriptorsByEncloser classExport = do
   generateEquals descriptorsByEncloser classExport
   generateToString descriptorsByEncloser classExport
 
-exportMemberIo : AsmGlobalState -> SortedMap Namespace (List String) ->
-                   SortedMap ClassExport (List ExportDescriptor) -> ExportDescriptor -> IO ()
+exportMemberIo : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo}
+               -> AsmGlobalState -> SortedMap Namespace (List String)
+               -> SortedMap ClassExport (List ExportDescriptor) -> ExportDescriptor -> IO ()
 exportMemberIo globalState typeExports descriptorsByEncloser (MkMethodExportDescriptor desc) =
   if desc.name == "<init>"
     then do
@@ -2388,12 +2385,12 @@ exportMemberIo globalState typeExports descriptorsByEncloser (MkMethodExportDesc
             let jname = jvmName desc.idrisName
             let dottedClassName = replace (className jname) '/' '.'
             let constructorIdrisName = NS (mkNamespace desc.encloser.name) (UN $ Basic (methodName jname ++ "<init>"))
-            programName <- AsmGlobalState.getProgramName globalState
             asmState <- createAsmStateJavaName globalState desc.encloser.name
             ignore $ runAsm asmState $ \stateRef => do
               Just superCallExpr <- getSuperCallExpr expr
                 | Nothing => asmCrash ("Constructor export for " ++ show idrisName ++ " should call 'super'")
-              inferDef programName constructorIdrisName fc (MkNmFun args superCallExpr)
+              inferFunctionType (constructorIdrisName, fc, (MkNmFun args superCallExpr))
+              inferDef constructorIdrisName fc
               resetScope
               loadFunction $ jvmName constructorIdrisName
               exportFunction typeExports desc
@@ -2469,7 +2466,8 @@ exportTypeIo globalState name = do
 exportTypes : AsmGlobalState -> SortedMap Namespace (List String) -> IO ()
 exportTypes globalState typeExports = traverse_ (exportTypeIo globalState) $ concat $ values typeExports
 
-exportDefs : AsmGlobalState -> List (Name, String) -> IO ()
+exportDefs : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo}
+           -> AsmGlobalState -> List (Name, String) -> IO ()
 exportDefs globalState nameAndDescriptors = do
   (typeExports, descriptors) <- parseExportDescriptors globalState nameAndDescriptors
   let descriptorsByEncloser = groupByEncloser descriptors
@@ -2493,21 +2491,32 @@ compileToJvmBytecode outputDirectory outputFile term = do
     let programName = if outputFile == "" then "repl" else outputFile
     let mainFunctionName = idrisMainFunctionName programName
     let allDefs = (mainFunctionName, emptyFC, MkNmFun [] idrisMainBody) :: ndefs
-    let nameFcDefs = optimize programName allDefs ++ filter isForeignDef allDefs
+    let nameFcDefs = filter isForeignDef allDefs ++ optimize programName allDefs
     let nameStrFcDefs = getNameStrFcDef <$> nameFcDefs
     fcAndDefinitionsByName <- coreLift $ Map.fromList nameStrFcDefs
-    let nameStrDefs = getNameStrDef <$> nameStrFcDefs
-    definitionsByName <- coreLift $ Map.fromList nameStrDefs
     globalState <- coreLift $ newAsmGlobalState programName fcAndDefinitionsByName
-    let names = fst <$> nameFcDefs
+    nameFcStateRefs <- inferFunctionTypes globalState nameFcDefs
+    ignore $ traverse (\(name, fc, stateRef) => assemble {stateRef=stateRef} name fc) nameFcStateRefs
     coreLift $ do
-        traverse_ (assemble globalState fcAndDefinitionsByName) names
-        exportDefs globalState $ mapMaybe (getExport noMangleMap) (fst <$> allDefs)
+        exportDefs globalState $ mapMaybe (getExport noMangleMap . fst) allDefs
         mainAsmState <- createAsmState globalState mainFunctionName
         let mainFunctionJname = jvmName mainFunctionName
-        _ <- runAsm mainAsmState $ \stateRef => createMainMethod programName mainFunctionJname
+        ignore $ runAsm mainAsmState $ \stateRef => createMainMethod programName mainFunctionJname
         classCodeEnd globalState outputDirectory outputFile (className mainFunctionJname)
 
+  where
+    inferFunctionTypes : AsmGlobalState -> List (Name, FC, NamedDef)
+                       -> Core (List (Name, FC, Ref AsmState AsmState))
+    inferFunctionTypes globalState nameFcDefs = go [] nameFcDefs where
+      go : List (Name, FC, (Ref AsmState AsmState)) -> List (Name, FC, NamedDef)
+         -> Core (List (Name, FC, (Ref AsmState AsmState)))
+      go acc [] = pure acc
+      go acc (nameFcDef@(name, fc, def) :: rest) = do
+        asmState <- coreLift $ createAsmState globalState name
+        asmStateRef <- newRef AsmState asmState
+        ignore $ inferFunctionType nameFcDef
+        go ((name, fc, asmStateRef) :: acc) rest
+
 ||| JVM bytecode implementation of the `compileExpr` interface.
 compileExprJvm : Ref Ctxt Defs
                -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (outDir: String) -> ClosedTerm
diff --git a/src/Compiler/Jvm/Foreign.idr b/src/Compiler/Jvm/Foreign.idr
index 775d5dc69..a9952f9d3 100644
--- a/src/Compiler/Jvm/Foreign.idr
+++ b/src/Compiler/Jvm/Foreign.idr
@@ -166,39 +166,48 @@ getJvmType (_, _, jvmType) = jvmType
 shouldPassToForeign : (CFType, Nat, Bool, InferredType) -> Bool
 shouldPassToForeign (_, _, shouldPass, _) = shouldPass
 
-getArgumentNameAndTypes : {auto stateRef: Ref AsmState AsmState} -> FC -> List InferredType -> List (Nat, Bool, InferredType) -> Core (List (String, InferredType))
+getArgumentNameAndTypes : {auto stateRef: Ref AsmState AsmState} -> FC -> List InferredType
+                        -> List (Nat, Bool, InferredType) -> Core (List (String, InferredType))
 getArgumentNameAndTypes fc descriptorTypes params = reverse <$> go [] descriptorTypes params where
-  go : List (String, InferredType) -> List InferredType -> List (Nat, Bool, InferredType) -> Core (List (String, InferredType))
+  go : List (String, InferredType) -> List InferredType -> List (Nat, Bool, InferredType)
+     -> Core (List (String, InferredType))
   go acc [] _ = pure acc -- Ignore any additional arguments from Idris
   go acc _ [] = throw $ GenericMsg fc "Foreign descriptor and Idris types do not match"
   go acc (descriptorType :: descriptorTypes) ((index, _, _) :: rest) =
     go (("arg" ++ show index, descriptorType) :: acc) descriptorTypes rest
 
 export
-inferForeign : {auto stateRef: Ref AsmState AsmState} -> String -> Name -> FC -> List String -> List CFType -> CFType -> Core ()
-inferForeign programName idrisName fc foreignDescriptors argumentTypes returnType = do
+isForeign : NamedCExp -> Bool
+isForeign (NmDelay _ LLazy expr) = isForeign expr
+isForeign (NmExtPrim _ (NS ns (UN (Basic name))) _) =
+  ns == mkNamespace "" &&
+    (name `elem` the (List String) ["prim__jvmInstance", "prim__setInstanceField", "prim__setStaticField",
+      "prim__getInstanceField", "prim__getStaticField", "prim__jvmStatic"])
+isForeign _ = False
+
+export
+inferForeign : {auto stateRef: Ref AsmState AsmState} -> Name -> FC -> List String -> List CFType -> CFType -> Core ()
+inferForeign idrisName fc foreignDescriptors argumentTypes returnType = do
     resetScope
     let jname = jvmName idrisName
-    let jvmClassAndMethodName = getIdrisFunctionName programName (className jname) (methodName jname)
+    let jvmClassAndMethodName = getIdrisFunctionName !getProgramName (className jname) (methodName jname)
     idrisJvmParameters <- getIdrisJvmParameters fc argumentTypes
     let validIdrisTypes = map fst $ filter shouldPassToForeign $ zip argumentTypes idrisJvmParameters
     let idrisArgumentTypes = getJvmType <$> idrisJvmParameters
     let jvmArguments = filter (fst . snd) idrisJvmParameters
     let jvmArgumentTypes = getJvmType <$> jvmArguments
-    let arityNat = length argumentTypes
-    let isNilArity = arityNat == 0
     jvmDescriptor <- findJvmDescriptor fc idrisName foreignDescriptors
     jvmReturnType <- parse fc returnType
     (foreignFunctionClassName, foreignFunctionName, jvmReturnType, jvmArgumentTypesFromDescriptor) <-
         parseForeignFunctionDescriptor fc jvmDescriptor jvmArgumentTypes jvmReturnType
 
     scopeIndex <- newScopeIndex
-    let arity = the Int $ cast arityNat
-    let argumentNames =
-       if isNilArity then [] else (\argumentIndex => "arg" ++ show argumentIndex) <$> [0 .. arity - 1]
     argumentNameAndTypes <- getArgumentNameAndTypes fc jvmArgumentTypesFromDescriptor jvmArguments
-    let methodReturnType = if isNilArity then delayedType else inferredObjectType
-    let inferredFunctionType = MkInferredFunctionType methodReturnType (replicate arityNat inferredObjectType)
+    let arityNat = length idrisArgumentTypes
+    let isNilArity = arityNat == 0
+    let methodReturnType = if isNilArity then delayedType else jvmReturnType
+    let argumentTypes = snd <$> argumentNameAndTypes
+
     scopes <- coreLift $ ArrayList.new {elemTy=Scope}
     let extPrimName = NS (mkNamespace "") $ UN $ Basic $
       getPrimMethodName (length argumentNameAndTypes) foreignFunctionName
@@ -209,18 +218,22 @@ inferForeign programName idrisName fc foreignDescriptors argumentTypes returnTyp
            getJvmExtPrimArguments $ zip validIdrisTypes argumentNameAndTypes,
            NmPrimVal fc WorldVal]
     let functionBody = if isNilArity then NmDelay fc LLazy externalFunctionBody else externalFunctionBody
+    let idrisReturnType = if methodReturnType == IVoid then IInt else methodReturnType
+    let inferredFunctionType = MkInferredFunctionType idrisReturnType idrisArgumentTypes
     let function = MkFunction jname inferredFunctionType (subtyping scopes) 0 jvmClassAndMethodName functionBody
     setCurrentFunction function
-    coreLift $ AsmGlobalState.addFunction !getGlobalState jname function
-    let parameterTypes = parameterTypes inferredFunctionType
+    coreLift $ addFunction !getGlobalState jname function
+    let arity = the Int $ cast arityNat
+    let argumentNames =
+      if isNilArity then [] else (\argumentIndex => "arg" ++ show argumentIndex) <$> [0 .. arity - 1]
     argumentTypesByIndex <- coreLift $
         if isNilArity
             then Map.newTreeMap {key=Int} {value=InferredType}
-            else Map.fromList $ zip [0 .. arity - 1] parameterTypes
-    argumentTypesByName <- coreLift $ Map.fromList $ zip argumentNames parameterTypes
+            else Map.fromList $ zip [0 .. arity - 1] idrisArgumentTypes
+    argumentTypesByName <- coreLift $ Map.fromList $ zip argumentNames idrisArgumentTypes
     argIndices <- coreLift $ getArgumentIndices arity argumentNames
     let functionScope = MkScope scopeIndex Nothing argumentTypesByName argumentTypesByIndex argIndices argIndices
-                            methodReturnType arity (0, 0) ("", "") []
+                            idrisReturnType arity (0, 0) ("", "") []
     saveScope functionScope
     when isNilArity $ do
         let parentScopeIndex = scopeIndex
@@ -233,7 +246,7 @@ inferForeign programName idrisName fc foreignDescriptors argumentTypes returnTyp
             MkScope scopeIndex (Just parentScopeIndex) variableTypes allVariableTypes
                 variableIndices allVariableIndices IUnknown 0 (0, 0) ("", "") []
         saveScope delayLambdaScope
-    updateScopeVariableTypes arityNat
+    updateScopeVariableTypes
   where
     getJvmExtPrimArguments : List (CFType, String, InferredType) -> NamedCExp
     getJvmExtPrimArguments [] = NmCon fc (UN $ Basic "emptyForeignArg") DATACON (Just 0) []
diff --git a/src/Compiler/Jvm/InferredType.idr b/src/Compiler/Jvm/InferredType.idr
index f3ef2115b..d4989fd86 100644
--- a/src/Compiler/Jvm/InferredType.idr
+++ b/src/Compiler/Jvm/InferredType.idr
@@ -71,7 +71,7 @@ mutual
   export
   Show InferredFunctionType where
     show (MkInferredFunctionType returnType argumentTypes) =
-      assert_total $ showSep "⟶" (show <$> (argumentTypes ++ [returnType]))
+      assert_total $ showSep " -> " (show <$> (argumentTypes ++ [returnType]))
 
   export
   Show JavaLambdaType where
diff --git a/src/Compiler/Jvm/Jname.idr b/src/Compiler/Jvm/Jname.idr
index db76dfe7c..8dbd54c8c 100644
--- a/src/Compiler/Jvm/Jname.idr
+++ b/src/Compiler/Jvm/Jname.idr
@@ -39,15 +39,15 @@ getSimpleName : Jname -> String
 getSimpleName = getSimpleNameWithSep "/"
 
 export
-implementation Eq Jname where
+Eq Jname where
     name1 == name2 = getSimpleName name1 == getSimpleName name2
 
 export
-implementation Ord Jname where
+Ord Jname where
   compare name1 name2 = compare (getSimpleName name1) (getSimpleName name2)
 
 export
-implementation Show Jname where
+Show Jname where
     show = getSimpleName
 
 export
diff --git a/src/Compiler/Jvm/Optimizer.idr b/src/Compiler/Jvm/Optimizer.idr
index 9f7f5a0c4..e56b19053 100644
--- a/src/Compiler/Jvm/Optimizer.idr
+++ b/src/Compiler/Jvm/Optimizer.idr
@@ -1,5 +1,6 @@
 module Compiler.Jvm.Optimizer
 
+import Algebra
 import Compiler.Common
 import Compiler.CompileExpr
 import Compiler.Inline
@@ -11,10 +12,17 @@ import Control.Monad.State
 import Compiler.Common
 import Core.CompileExpr
 import Core.Context
+import Core.Core
 import Core.Name
 import Core.Reflect
 import Core.TT
 import Core.TT.Primitive
+import Core.Env
+
+import Idris.Pretty.Annotations
+import Idris.Syntax
+import Idris.Resugar
+import Idris.Doc.String
 
 import Libraries.Data.SortedMap
 import Libraries.Data.SortedSet
@@ -35,6 +43,7 @@ import Compiler.Jvm.ShowUtil
 %hide Core.Context.Context.Constructor.arity
 %hide Compiler.TailRec.Function.fc
 %hide Compiler.TailRec.TcFunction.fc
+%hide Libraries.Text.PrettyPrint.Prettyprinter.Util.words
 
 namespace InferredPrimType
   export
@@ -449,6 +458,15 @@ Eq LambdaType where
     Function5Lambda == Function5Lambda = True
     _ == _ = False
 
+export
+Show LambdaType where
+  show DelayedLambda = "DelayedLambda"
+  show FunctionLambda = "FunctionLambda"
+  show Function2Lambda = "Function2Lambda"
+  show Function3Lambda = "Function3Lambda"
+  show Function4Lambda = "Function4Lambda"
+  show Function5Lambda = "Function5Lambda"
+
 export
 getLambdaTypeByParameter : (parameterName: Maybe Name) -> LambdaType
 getLambdaTypeByParameter Nothing = DelayedLambda
@@ -548,7 +566,16 @@ combineSwitchTypes defaultTy altTypes@(altTy :: rest) = maybe (go altTy rest) (f
 createNewVariable : {auto stateRef: Ref AsmState AsmState} -> (variablePrefix: String) -> InferredType -> Core ()
 createNewVariable variablePrefix ty = do
     variable <- generateVariable variablePrefix
-    ignore $ addVariableType variable ty
+    addVariableType variable ty
+
+export
+canUseMethodReference : {auto stateRef: Ref AsmState AsmState} -> Name -> List Name -> Maybe Name -> List Name
+                      -> Core Bool
+canUseMethodReference _ _ Nothing _ = pure False
+canUseMethodReference functionName args (Just p0) params = do
+  Just (MkInferredFunctionType returnType parameterTypes) <- findFunctionType (jvmName functionName)
+    | Nothing => throw (GenericMsg emptyFC ("Unable to find function \{show functionName}"))
+  pure $ not (any isPrimitive (returnType :: parameterTypes)) && all (uncurry (==)) (zip args (p0 :: params))
 
 export
 isIoAction : NamedCExp -> Bool
@@ -561,6 +588,10 @@ isIoAction expr = False
 voidTypeExpr : NamedCExp
 voidTypeExpr = NmCon emptyFC (UN (Basic "void")) TYCON Nothing []
 
+tailRecLoopFunctionName : Name
+tailRecLoopFunctionName =
+  NS (mkNamespace "io.github.mmhelloworld.idrisjvm.runtime.Runtime") (UN $ Basic "tailRec")
+
 export
 getJavaLambdaType : {auto stateRef: Ref AsmState AsmState} -> FC -> List NamedCExp -> Core JavaLambdaType
 getJavaLambdaType fc [functionType, javaInterfaceType, _] =
@@ -620,55 +651,55 @@ getJavaLambdaType fc [functionType, javaInterfaceType, _] =
 getJavaLambdaType fc exprs = asmCrash ("Invalid Java lambda at " ++ show fc ++ ": " ++ show exprs)
 
 mutual
-    inferExpr : {auto stateRef: Ref AsmState AsmState} -> InferredType -> NamedCExp -> Core InferredType
-    inferExpr exprTy (NmDelay _ _ expr) = inferExprLam AppliedLambdaUnknown Nothing Nothing expr
-    inferExpr exprTy expr@(NmLocal _ var) = addVariableType (jvmSimpleName var) exprTy
-    inferExpr exprTy (NmRef _ name) = pure exprTy
-    inferExpr exprTy app@(NmApp _ (NmRef _ name) args) = inferExprApp exprTy app
-    inferExpr _ (NmApp fc (NmLam _ var body) [expr]) =
+    inferExpr : {auto stateRef: Ref AsmState AsmState} -> NamedCExp -> Core InferredType
+    inferExpr (NmDelay _ _ expr) = inferExprLam AppliedLambdaUnknown Nothing Nothing expr
+    inferExpr expr@(NmLocal _ var) = retrieveVariableType (jvmSimpleName var)
+    inferExpr (NmRef _ name) = pure IUnknown
+    inferExpr app@(NmApp _ (NmRef _ name) args) = inferExprApp app
+    inferExpr (NmApp fc (NmLam _ var body) [expr]) =
         inferExprLam (getAppliedLambdaType fc) (Just expr) (Just var) body
-    inferExpr _ (NmLam _ var body) = inferExprLam AppliedLambdaUnknown Nothing (Just var) body
-    inferExpr exprTy (NmLet fc var value expr) = inferExprLet fc exprTy var value expr
-    inferExpr exprTy app@(NmApp _ _ _) = inferExprApp exprTy app
-    inferExpr exprTy expr@(NmCon fc name _ tag args) =
-        inferExprCon exprTy (fst $ getSourceLocation expr) name args
-    inferExpr exprTy (NmOp _ fn args) = inferExprOp fn args
-    inferExpr exprTy (NmExtPrim fc fn args) = inferExtPrim fc exprTy (toPrim fn) args
-    inferExpr exprTy (NmForce _ _ expr) = do
-        ignore $ inferExpr delayedType expr
+    inferExpr (NmLam _ var body) = inferExprLam AppliedLambdaUnknown Nothing (Just var) body
+    inferExpr (NmLet fc var value expr) = inferExprLet fc var value expr
+    inferExpr app@(NmApp _ _ _) = inferExprApp app
+    inferExpr expr@(NmCon fc name _ tag args) =
+        inferExprCon (fst $ getSourceLocation expr) name args
+    inferExpr (NmOp _ fn args) = inferExprOp fn args
+    inferExpr (NmExtPrim fc fn args) = inferExtPrim fc (toPrim fn) args
+    inferExpr (NmForce _ _ expr) = do
+        ignore $ inferExpr expr
         pure inferredObjectType
 
-    inferExpr exprTy (NmConCase _ sc [] Nothing) = pure IUnknown
-    inferExpr exprTy (NmConCase _ sc [] (Just def)) = do
+    inferExpr (NmConCase _ sc [] Nothing) = pure IUnknown
+    inferExpr (NmConCase _ sc [] (Just def)) = do
         inferConstructorSwitchExpr sc
-        inferExpr exprTy def
-    inferExpr exprTy (NmConCase _ sc [MkNConAlt _ _ _ args expr] Nothing) = do
+        inferExpr def
+    inferExpr (NmConCase _ sc [MkNConAlt _ _ _ args expr] Nothing) = do
         inferConstructorSwitchExpr sc
-        inferConCaseExpr exprTy args expr
-    inferExpr exprTy (NmConCase _ sc alts def) = do
+        inferConCaseExpr args expr
+    inferExpr (NmConCase _ sc alts def) = do
         inferConstructorSwitchExpr sc
         let hasTypeCase = any isTypeCase alts
         when hasTypeCase $ do
             createNewVariable "constructorCaseExpr" inferredStringType
             createNewVariable "hashCodePosition" IInt
         let sortedAlts = if hasTypeCase then alts else sortConCases alts
-        altTypes <- traverse (inferExprConAlt exprTy) sortedAlts
-        defaultTy <- traverseOpt (inferExprWithNewScope exprTy) def
+        altTypes <- traverse inferExprConAlt sortedAlts
+        defaultTy <- traverseOpt inferExprWithNewScope def
         pure $ combineSwitchTypes defaultTy altTypes
 
-    inferExpr exprTy (NmConstCase fc sc [] Nothing) = pure IUnknown
-    inferExpr exprTy (NmConstCase fc sc [] (Just expr)) = inferExpr exprTy expr
-    inferExpr exprTy (NmConstCase fc sc alts def) = do
+    inferExpr (NmConstCase fc sc [] Nothing) = pure IUnknown
+    inferExpr (NmConstCase fc sc [] (Just expr)) = inferExpr expr
+    inferExpr (NmConstCase fc sc alts def) = do
         constantType <- getConstantType alts
-        ignore $ inferExpr constantType sc
+        ignore $ inferExpr sc
         when (constantType /= IInt) $ do
             constantExprVariable <- generateVariable "constantCaseExpr"
-            ignore $ addVariableType constantExprVariable constantType
+            addVariableType constantExprVariable constantType
             hashCodePositionVariable <- generateVariable "hashCodePosition"
-            ignore $ addVariableType hashCodePositionVariable IInt
+            addVariableType hashCodePositionVariable IInt
         sortedAlts <- sortConstCases constantType alts
-        altTypes <- traverse (inferExprConstAlt exprTy) sortedAlts
-        defaultTy <- traverseOpt (inferExprWithNewScope exprTy) def
+        altTypes <- traverse inferExprConstAlt sortedAlts
+        defaultTy <- traverseOpt inferExprWithNewScope def
         pure $ combineSwitchTypes defaultTy altTypes
       where
         getConstant : NamedConstAlt -> Primitive.Constant
@@ -680,201 +711,182 @@ mutual
             pure $ fst <$> (sortBy (comparing snd) $ zip alts constValues)
         sortConstCases _ alts = pure alts
 
-    inferExpr _ (NmPrimVal fc (I _)) = pure IInt
-    inferExpr _ (NmPrimVal fc (I8 _)) = pure IInt
-    inferExpr _ (NmPrimVal fc (I16 _)) = pure IInt
-    inferExpr _ (NmPrimVal fc (I32 _)) = pure IInt
-    inferExpr _ (NmPrimVal fc (I64 _)) = pure ILong
-    inferExpr _ (NmPrimVal fc (B8 _)) = pure IInt
-    inferExpr _ (NmPrimVal fc (B16 _)) = pure IInt
-    inferExpr _ (NmPrimVal fc (B32 _)) = pure IInt
-    inferExpr _ (NmPrimVal fc (B64 _)) = pure ILong
-    inferExpr _ (NmPrimVal fc (BI _)) = pure inferredBigIntegerType
-    inferExpr _ (NmPrimVal fc (Str _)) = pure inferredStringType
-    inferExpr _ (NmPrimVal fc (Ch _)) = pure IChar
-    inferExpr _ (NmPrimVal fc (Db _)) = pure IDouble
-    inferExpr _ (NmPrimVal fc _) = pure IInt
-    inferExpr exprTy (NmErased fc) = pure exprTy
-    inferExpr exprTy (NmCrash fc msg) = pure exprTy
+    inferExpr (NmPrimVal fc (I _)) = pure IInt
+    inferExpr (NmPrimVal fc (I8 _)) = pure IInt
+    inferExpr (NmPrimVal fc (I16 _)) = pure IInt
+    inferExpr (NmPrimVal fc (I32 _)) = pure IInt
+    inferExpr (NmPrimVal fc (I64 _)) = pure ILong
+    inferExpr (NmPrimVal fc (B8 _)) = pure IInt
+    inferExpr (NmPrimVal fc (B16 _)) = pure IInt
+    inferExpr (NmPrimVal fc (B32 _)) = pure IInt
+    inferExpr (NmPrimVal fc (B64 _)) = pure ILong
+    inferExpr (NmPrimVal fc (BI _)) = pure inferredBigIntegerType
+    inferExpr (NmPrimVal fc (Str _)) = pure inferredStringType
+    inferExpr (NmPrimVal fc (Ch _)) = pure IChar
+    inferExpr (NmPrimVal fc (Db _)) = pure IDouble
+    inferExpr (NmPrimVal fc _) = pure IInt
+    inferExpr (NmErased fc) = pure IUnknown
+    inferExpr (NmCrash fc msg) = pure IUnknown
 
     inferConstructorSwitchExpr : {auto stateRef: Ref AsmState AsmState} -> NamedCExp -> Core ()
     inferConstructorSwitchExpr (NmLocal _ var) = do
         let idrisObjectVariable = jvmSimpleName var
-        ignore $ addVariableType idrisObjectVariable idrisObjectType
+        addVariableType idrisObjectVariable idrisObjectType
     inferConstructorSwitchExpr sc = do
         idrisObjectVariable <- generateVariable "constructorSwitchValue"
-        ignore $ inferExpr idrisObjectType sc
-        ignore $ addVariableType idrisObjectVariable idrisObjectType
+        ignore $ inferExpr sc
+        addVariableType idrisObjectVariable idrisObjectType
 
-    inferExprConstAlt : {auto stateRef: Ref AsmState AsmState} -> InferredType -> NamedConstAlt -> Core InferredType
-    inferExprConstAlt returnType (MkNConstAlt _ expr) = inferExprWithNewScope returnType expr
+    inferExprConstAlt : {auto stateRef: Ref AsmState AsmState} -> NamedConstAlt -> Core InferredType
+    inferExprConstAlt (MkNConstAlt _ expr) = inferExprWithNewScope expr
 
-    inferExprWithNewScope : {auto stateRef: Ref AsmState AsmState} -> InferredType -> NamedCExp -> Core InferredType
-    inferExprWithNewScope returnType expr = do
+    inferExprWithNewScope : {auto stateRef: Ref AsmState AsmState} -> NamedCExp -> Core InferredType
+    inferExprWithNewScope expr = do
          let fc = getFC expr
          let (lineStart, lineEnd) = getLineNumbers (startPos (toNonEmptyFC fc)) (endPos (toNonEmptyFC fc))
-         withInferenceScope lineStart lineEnd $ inferExpr returnType expr
+         withInferenceScope lineStart lineEnd $ inferExpr expr
 
-    inferConCaseExpr : {auto stateRef: Ref AsmState AsmState} -> InferredType -> List Name -> NamedCExp -> Core InferredType
-    inferConCaseExpr exprTy args expr = do
+    inferConCaseExpr : {auto stateRef: Ref AsmState AsmState} -> List Name -> NamedCExp -> Core InferredType
+    inferConCaseExpr args expr = do
             traverse_ inferArg args
-            inferExpr exprTy expr
+            inferExpr expr
         where
             inferArg : Name -> Core ()
             inferArg var =
                 let variableName = jvmSimpleName var
                 in when (used variableName expr) $ createVariable variableName
 
-    inferExprConAlt : {auto stateRef: Ref AsmState AsmState} -> InferredType -> NamedConAlt -> Core InferredType
-    inferExprConAlt exprTy (MkNConAlt _ _ _ args expr) = do
+    inferExprConAlt : {auto stateRef: Ref AsmState AsmState} -> NamedConAlt -> Core InferredType
+    inferExprConAlt (MkNConAlt _ _ _ args expr) = do
       let fc = getFC expr
       let (lineStart, lineEnd) = getLineNumbers (startPos (toNonEmptyFC fc)) (endPos (toNonEmptyFC fc))
-      withInferenceScope lineStart lineEnd $ inferConCaseExpr exprTy args expr
-
-    inferParameter : {auto stateRef: Ref AsmState AsmState} -> (NamedCExp, InferredType) -> Core InferredType
-    inferParameter (param, ty) = inferExpr ty param
+      withInferenceScope lineStart lineEnd $ inferConCaseExpr args expr
 
     inferBinaryOp : {auto stateRef: Ref AsmState AsmState} -> InferredType -> NamedCExp -> NamedCExp -> Core InferredType
     inferBinaryOp ty x y = do
-        ignore $ inferExpr ty x
-        ignore $ inferExpr ty y
+        ignore $ inferExpr x
+        ignore $ inferExpr y
         pure ty
 
-    inferBoolOp : {auto stateRef: Ref AsmState AsmState} -> InferredType -> NamedCExp -> NamedCExp -> Core InferredType
-    inferBoolOp ty x y = do
-        ignore $ inferExpr ty x
-        ignore $ inferExpr ty y
+    inferBoolOp : {auto stateRef: Ref AsmState AsmState} -> NamedCExp -> NamedCExp -> Core InferredType
+    inferBoolOp x y = do
+        ignore $ inferExpr x
+        ignore $ inferExpr y
         pure IBool
 
     inferUnaryOp : {auto stateRef: Ref AsmState AsmState} -> InferredType -> NamedCExp -> Core InferredType
     inferUnaryOp ty x = do
-      ignore $ inferExpr ty x
+      ignore $ inferExpr x
       pure ty
 
-    inferExtPrimArg : {auto stateRef: Ref AsmState AsmState} -> (NamedCExp, InferredType) -> Core InferredType
-    inferExtPrimArg (arg, ty) = inferExpr ty arg
-
-    inferExtPrim : {auto stateRef: Ref AsmState AsmState} -> FC -> InferredType -> ExtPrim -> List NamedCExp -> Core InferredType
-    inferExtPrim fc returnType GetStaticField descriptors = inferExtPrim fc returnType JvmStaticMethodCall descriptors
-    inferExtPrim fc returnType SetStaticField descriptors = inferExtPrim fc returnType JvmStaticMethodCall descriptors
-    inferExtPrim fc returnType GetInstanceField descriptors = inferExtPrim fc returnType JvmStaticMethodCall descriptors
-    inferExtPrim fc returnType SetInstanceField descriptors = inferExtPrim fc returnType JvmStaticMethodCall descriptors
-    inferExtPrim fc returnType JvmInstanceMethodCall descriptors =
-      inferExtPrim fc returnType JvmStaticMethodCall descriptors
-    inferExtPrim fc returnType JvmStaticMethodCall [ret, NmApp _ _ [functionNamePrimVal], fargs, world] =
-      inferExtPrim fc returnType JvmStaticMethodCall [ret, functionNamePrimVal, fargs, world]
-    inferExtPrim _ returnType JvmStaticMethodCall [ret, _, fargs, _]
+    inferExtPrim : {auto stateRef: Ref AsmState AsmState} -> FC -> ExtPrim -> List NamedCExp -> Core InferredType
+    inferExtPrim fc GetStaticField descriptors = inferExtPrim fc JvmStaticMethodCall descriptors
+    inferExtPrim fc SetStaticField descriptors = inferExtPrim fc JvmStaticMethodCall descriptors
+    inferExtPrim fc GetInstanceField descriptors = inferExtPrim fc JvmStaticMethodCall descriptors
+    inferExtPrim fc SetInstanceField descriptors = inferExtPrim fc JvmStaticMethodCall descriptors
+    inferExtPrim fc JvmInstanceMethodCall descriptors =
+      inferExtPrim fc JvmStaticMethodCall descriptors
+    inferExtPrim fc JvmStaticMethodCall [ret, NmApp _ _ [functionNamePrimVal], fargs, world] =
+      inferExtPrim fc JvmStaticMethodCall [ret, functionNamePrimVal, fargs, world]
+    inferExtPrim _ JvmStaticMethodCall [ret, _, fargs, _]
       = do args <- getFArgs fargs
-           argTypes <- traverse tySpec (map fst args)
            methodReturnType <- tySpec ret
-           traverse_ inferExtPrimArg $ zip (map snd args) argTypes
+           traverse_ inferExpr $ map snd args
            pure $ if methodReturnType == IVoid then inferredObjectType else methodReturnType
-    inferExtPrim fc returnType JvmSuper [clazz, fargs, world] = do
+    inferExtPrim fc JvmSuper [clazz, fargs, world] = do
       rootMethodName <- getRootMethodName
       if (endsWith (methodName rootMethodName) "$ltinit$gt")
-        then inferExtPrim fc returnType JvmStaticMethodCall [voidTypeExpr, NmErased fc, fargs, world]
+        then inferExtPrim fc JvmStaticMethodCall [voidTypeExpr, NmErased fc, fargs, world]
         else pure IUnknown
-    inferExtPrim _ returnType NewArray [_, size, val, world] = do
-        ignore $ inferExpr IInt size
-        ignore $ inferExpr IUnknown val
+    inferExtPrim _ NewArray [_, size, val, world] = do
+        ignore $ inferExpr size
+        ignore $ inferExpr val
         pure arrayListType
-    inferExtPrim _ returnType ArrayGet [_, arr, pos, world] = do
-        ignore $ inferExpr arrayListType arr
-        ignore $ inferExpr IInt pos
+    inferExtPrim _ ArrayGet [_, arr, pos, world] = do
+        ignore $ inferExpr arr
+        ignore $ inferExpr pos
         pure IUnknown
-    inferExtPrim _ returnType ArraySet [_, arr, pos, val, world] = do
-        ignore $ inferExpr arrayListType arr
-        ignore $ inferExpr IInt pos
-        ignore $ inferExpr IUnknown val
+    inferExtPrim _ ArraySet [_, arr, pos, val, world] = do
+        ignore $ inferExpr arr
+        ignore $ inferExpr pos
+        ignore $ inferExpr val
         pure inferredObjectType
-    inferExtPrim _ returnType JvmNewArray [tyExpr, size, world] = do
-        ignore $ inferExpr IInt size
+    inferExtPrim _ JvmNewArray [tyExpr, size, world] = do
+        ignore $ inferExpr size
         elemTy <- tySpec tyExpr
         pure $ IArray elemTy
-    inferExtPrim _ returnType JvmSetArray [tyExpr, index, val, arr, world] = do
+    inferExtPrim _ JvmSetArray [tyExpr, index, val, arr, world] = do
         elemTy <- tySpec tyExpr
-        ignore $ inferExpr (IArray elemTy) arr
-        ignore $ inferExpr IInt index
-        ignore $ inferExpr elemTy val
+        ignore $ inferExpr arr
+        ignore $ inferExpr index
+        ignore $ inferExpr val
         pure inferredObjectType
-    inferExtPrim _ returnType JvmGetArray [tyExpr, index, arr, world] = do
+    inferExtPrim _ JvmGetArray [tyExpr, index, arr, world] = do
         elemTy <- tySpec tyExpr
-        ignore $ inferExpr (IArray elemTy) arr
-        ignore $ inferExpr IInt index
+        ignore $ inferExpr arr
+        ignore $ inferExpr index
         pure elemTy
-    inferExtPrim _ returnType JvmArrayLength [tyExpr, arr] = do
+    inferExtPrim _ JvmArrayLength [tyExpr, arr] = do
         elemTy <- tySpec tyExpr
-        ignore $ inferExpr (IArray elemTy) arr
+        ignore $ inferExpr arr
         pure IInt
-    inferExtPrim _ returnType NewIORef [_, val, world] = do
-        ignore $ inferExpr IUnknown val
+    inferExtPrim _ NewIORef [_, val, world] = do
+        ignore $ inferExpr val
         pure refType
-    inferExtPrim _ returnType ReadIORef [_, ref, world] = do
-        ignore $ inferExpr refType ref
+    inferExtPrim _ ReadIORef [_, ref, world] = do
+        ignore $ inferExpr ref
         pure IUnknown
-    inferExtPrim _ returnType WriteIORef [_, ref, val, world] = do
-        ignore $ inferExpr refType ref
-        ignore $ inferExpr IUnknown val
+    inferExtPrim _ WriteIORef [_, ref, val, world] = do
+        ignore $ inferExpr ref
+        ignore $ inferExpr val
         pure inferredObjectType
-    inferExtPrim _ returnType SysOS [] = pure inferredStringType
-    inferExtPrim _ returnType SysCodegen [] = pure inferredStringType
-    inferExtPrim _ returnType VoidElim _ = pure inferredObjectType
-    inferExtPrim _ returnType JvmClassLiteral [_] = pure $ IRef "java/lang/Class" Class []
-    inferExtPrim _ returnType JvmInstanceOf [_, obj, _] = do
-      ignore $ inferExpr IUnknown obj
+    inferExtPrim _ SysOS [] = pure inferredStringType
+    inferExtPrim _ SysCodegen [] = pure inferredStringType
+    inferExtPrim _ VoidElim _ = pure inferredObjectType
+    inferExtPrim _ JvmClassLiteral [_] = pure $ IRef "java/lang/Class" Class []
+    inferExtPrim _ JvmInstanceOf [_, obj, _] = do
+      ignore $ inferExpr obj
       pure IBool
-    inferExtPrim _ returnType JvmRefEq [_, _, x, y] = inferBoolOp IUnknown x y
-    inferExtPrim fc returnType JavaLambda [functionType, javaInterfaceType, lambda] = do
-      ignore $ inferExpr IUnknown lambda
+    inferExtPrim _ JvmRefEq [_, _, x, y] = inferBoolOp x y
+    inferExtPrim fc JavaLambda [functionType, javaInterfaceType, lambda] = do
+      ignore $ inferExpr lambda
       IFunction <$> getJavaLambdaType fc [functionType, javaInterfaceType, lambda]
-    inferExtPrim _ returnType MakeFuture [_, action] = do
-        ignore $ inferExpr delayedType action
+    inferExtPrim _ MakeFuture [_, action] = do
+        ignore $ inferExpr action
         pure inferredForkJoinTaskType
-    inferExtPrim _ returnType (Unknown name) _ = asmCrash $ "Can't compile unknown external directive " ++ show name
-    inferExtPrim fc _ prim args = throw $ GenericMsg fc $ "Unsupported external function " ++ show prim ++ "(" ++
+    inferExtPrim _ (Unknown name) _ = asmCrash $ "Can't compile unknown external directive " ++ show name
+    inferExtPrim fc prim args = throw $ GenericMsg fc $ "Unsupported external function " ++ show prim ++ "(" ++
         (show $ showNamedCExp 0 <$> args) ++ ")"
 
-    inferExprLamWithParameterType : {auto stateRef: Ref AsmState AsmState} -> Maybe (Name, InferredType)
-                                  -> (parameterValueExpr: Maybe (Core ())) -> NamedCExp -> Core InferredType
-    inferExprLamWithParameterType parameterNameAndType parameterValueExpr expr = do
+    inferExprLamWithParameterType : {auto stateRef: Ref AsmState AsmState} -> Maybe Name
+                                  -> (parameterValueExpr: Maybe (Core InferredType)) -> NamedCExp -> Core InferredType
+    inferExprLamWithParameterType parameterName parameterValueExpr expr = do
         let hasParameterValue = isJust parameterValueExpr
         let (_, lineStart, lineEnd) = getSourceLocation expr
-        let jvmParameterNameAndType = (\(name, ty) => (jvmSimpleName name, ty)) <$> parameterNameAndType
-        let lambdaType = getLambdaTypeByParameter (fst <$> parameterNameAndType)
-        lambdaBodyReturnType <- withInferenceLambdaScope lineStart lineEnd (fst <$> parameterNameAndType) expr $ do
-            ignore $ traverseOpt createAndAddVariable jvmParameterNameAndType
-            maybe (pure ()) id parameterValueExpr
-            lambdaBodyReturnType <- inferExpr IUnknown expr
+        let jvmParameterName = jvmSimpleName <$> parameterName
+        let lambdaType = getLambdaTypeByParameter parameterName
+        lambdaBodyReturnType <- withInferenceLambdaScope lineStart lineEnd parameterName expr $ do
+            jname <- getRootMethodName
+            scopeIndex <- getCurrentScopeIndex
+            ignore $ traverseOpt createVariable jvmParameterName
+            valueType <- maybe (pure IUnknown) id parameterValueExpr
+            ignore $ traverseOpt (flip addVariableType valueType) jvmParameterName
+            lambdaBodyReturnType <- inferExpr expr
             currentScope <- getScope !getCurrentScopeIndex
             saveScope $ { returnType := lambdaBodyReturnType } currentScope
             pure lambdaBodyReturnType
         pure $ if hasParameterValue
             then lambdaBodyReturnType
             else getLambdaInterfaceType lambdaType
-      where
-        createAndAddVariable : (String, InferredType) -> Core ()
-        createAndAddVariable (name, ty) = do
-            createVariable name
-            ignore $ addVariableType name ty
 
-    inferExprLamWithParameterType1 : {auto stateRef: Ref AsmState AsmState} -> (isCached : Bool) -> Maybe Name
+    inferExprLamWithParameterType1 : {auto stateRef: Ref AsmState AsmState} -> (isMethodReference : Bool) -> Maybe Name
                                    -> NamedCExp -> Core InferredType
     inferExprLamWithParameterType1 True _ _ = pure inferredLambdaType
-    inferExprLamWithParameterType1 False parameterName expr =
-      inferExprLamWithParameterType ((\name => (name, inferredObjectType)) <$> parameterName) Nothing expr
+    inferExprLamWithParameterType1 False parameterName expr = inferExprLamWithParameterType parameterName Nothing expr
 
     inferExprLam : {auto stateRef: Ref AsmState AsmState} -> AppliedLambdaType -> (parameterValue: Maybe NamedCExp)
                  -> (parameterName : Maybe Name) -> NamedCExp -> Core InferredType
     inferExprLam appliedLambdaType parameterValue@(Just value) (Just parameterName) lambdaBody = do
-        valueType <-
-            if appliedLambdaType == AppliedLambdaSwitch
-                then case lambdaBody of
-                    (NmConstCase _ _ alts _) => getConstantType alts
-                    (NmConCase _ _ _ _) => pure idrisObjectType
-                    _ => pure IUnknown
-                else if appliedLambdaType == AppliedLambdaLet
-                        then pure inferredObjectType
-                        else pure IUnknown
         let shouldGenerateVariable = parameterName == extractedMethodArgumentName
         generatedJvmVariableName <-
             if shouldGenerateVariable
@@ -886,65 +898,60 @@ mutual
                 else parameterName
         let valueExpr = NmLocal (getFC lambdaBody) generatedVariableName
         parentScope <- getScope !getCurrentScopeIndex
-        inferExprLamWithParameterType (Just (generatedVariableName, valueType))
-            (Just (inferValue parentScope shouldGenerateVariable generatedJvmVariableName valueType))
+        inferExprLamWithParameterType (Just generatedVariableName)
+            (Just (inferValue parentScope shouldGenerateVariable generatedJvmVariableName))
             (if appliedLambdaType == AppliedLambdaSwitch || appliedLambdaType == AppliedLambdaLet
                 then substituteVariableSubMethodBody valueExpr lambdaBody
                 else lambdaBody)
       where
-        inferValue : Scope -> Bool -> String -> InferredType -> Core ()
-        inferValue enclosingScope shouldGenerateVariable variableName valueType = do
+        inferValue : Scope -> Bool -> String -> Core InferredType
+        inferValue enclosingScope shouldGenerateVariable variableName = do
             lambdaScopeIndex <- getCurrentScopeIndex
             updateCurrentScopeIndex (index enclosingScope)
-            when shouldGenerateVariable $ createVariable variableName
-            ignore $ inferExpr valueType value
-            ignore $ addVariableType variableName valueType
+            valueType <- inferExpr value
             updateCurrentScopeIndex lambdaScopeIndex
+            pure valueType
     inferExprLam _ _ p0 expr@(NmLam _ p1 (NmLam _ p2 (NmLam _ p3 (NmLam _ p4 (NmApp _ (NmRef _ name)
-      [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2, NmLocal _ arg3, NmLocal _ arg4]))))) =
-        inferExprLamWithParameterType1
-          (maybe False ((==) arg0) p0 && p1 == arg1 && p2 == arg2 && p3 == arg3 && p4 == arg4) p0 expr
+      [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2, NmLocal _ arg3, NmLocal _ arg4]))))) = do
+        isMethodReference <- canUseMethodReference name [arg0, arg1, arg2, arg3, arg4] p0 [p1, p2, p3, p4]
+        inferExprLamWithParameterType1 isMethodReference p0 expr
     inferExprLam _ _ p0 expr@(NmLam _ p1 (NmLam _ p2 (NmLam _ p3 (NmApp _ (NmRef _ name)
-      [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2, NmLocal _ arg3])))) =
-        inferExprLamWithParameterType1
-          (maybe False ((==) arg0) p0 && p1 == arg1 && p2 == arg2 && p3 == arg3) p0 expr
+      [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2, NmLocal _ arg3])))) = do
+        isMethodReference <- canUseMethodReference name [arg0, arg1, arg2, arg3] p0 [p1, p2, p3]
+        inferExprLamWithParameterType1 isMethodReference p0 expr
     inferExprLam _ _ p0 expr@(NmLam _ p1 (NmLam _ p2 (NmApp _ (NmRef _ name)
-      [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2]))) =
-        inferExprLamWithParameterType1 (maybe False ((==) arg0) p0 && p1 == arg1 && p2 == arg2) p0 expr
-    inferExprLam _ _ p0 expr@(NmLam _ p1 (NmApp _ (NmRef _ name) [NmLocal _ arg0, NmLocal _ arg1])) =
-        inferExprLamWithParameterType1 (maybe False ((==) arg0) p0 && p1 == arg1) p0 expr
-    inferExprLam _ _ p0 expr@(NmApp _ (NmRef _ _) [NmLocal _ b]) =
-      inferExprLamWithParameterType1 (maybe False ((==) b) p0) p0 expr
-    inferExprLam _ _ p0 expr@(NmLam _ c (NmLam _ a (NmLocal _ b))) =
-      inferExprLamWithParameterType1 (isJust p0 && (c == b || a == b)) p0 expr
-    inferExprLam _ _ p0 expr@(NmLam _ a (NmLocal _ b)) =
-      inferExprLamWithParameterType1 (maybe False ((==) b) p0 || (isJust p0 && a == b)) p0 expr
-    inferExprLam _ _ p0 expr@(NmLocal _ b) =
-      inferExprLamWithParameterType1 (maybe False ((==) b) p0) p0 expr
+      [NmLocal _ arg0, NmLocal _ arg1, NmLocal _ arg2]))) = do
+        isMethodReference <- canUseMethodReference name [arg0, arg1, arg2] p0 [p1, p2]
+        inferExprLamWithParameterType1 isMethodReference p0 expr
+    inferExprLam _ _ p0 expr@(NmLam _ p1 (NmApp _ (NmRef _ name) [NmLocal _ arg0, NmLocal _ arg1])) = do
+      isMethodReference <- canUseMethodReference name [arg0, arg1] p0 [p1]
+      inferExprLamWithParameterType1 isMethodReference p0 expr
+    inferExprLam _ _ p0 expr@(NmApp _ (NmRef _ name) [NmLocal _ arg0]) = do
+      isMethodReference <- canUseMethodReference name [arg0] p0 []
+      inferExprLamWithParameterType1 isMethodReference p0 expr
     inferExprLam _ _ p0 expr = inferExprLamWithParameterType1 False p0 expr
 
-    inferExprLet : {auto stateRef: Ref AsmState AsmState} -> FC -> InferredType -> (x : Name) -> NamedCExp -> NamedCExp -> Core InferredType
-    inferExprLet fc exprTy var value expr = do
+    inferExprLet : {auto stateRef: Ref AsmState AsmState} -> FC -> (x : Name) -> NamedCExp -> NamedCExp -> Core InferredType
+    inferExprLet fc var value expr = do
         let (lineStart, lineEnd) = getLineNumbers (startPos (toNonEmptyFC fc)) (endPos (toNonEmptyFC fc))
         let varName = jvmSimpleName var
         createVariable varName
         let (_, lineStart, lineEnd) = getSourceLocation value
-        valueTy <- withInferenceScope lineStart lineEnd $ inferExpr IUnknown value
-        ignore $ addVariableType varName valueTy
+        valueTy <- withInferenceScope lineStart lineEnd $ inferExpr value
+        addVariableType varName valueTy
         let (_, lineStart, lineEnd) = getSourceLocation expr
-        withInferenceScope lineStart lineEnd $ inferExpr exprTy expr
+        withInferenceScope lineStart lineEnd $ inferExpr expr
 
-    inferSelfTailCallParameter : {auto stateRef: Ref AsmState AsmState} -> Map Int InferredType -> Map Int String -> (NamedCExp, Int) -> Core ()
-    inferSelfTailCallParameter types argumentNameByIndices (arg, index) = do
-        optTy <- coreLift $ Map.get types index
-        let variableType = fromMaybe IUnknown $ nullableToMaybe optTy
-        ty <- inferExpr variableType arg
+    inferSelfTailCallParameter : {auto stateRef: Ref AsmState AsmState} -> Map Int String
+                              -> (NamedCExp, Int) -> Core ()
+    inferSelfTailCallParameter argumentNameByIndices (arg, index) = do
+        ty <- inferExpr arg
         optName <- coreLift $ Map.get {value=String} argumentNameByIndices index
         maybe (pure ()) (doAddVariableType ty) $ nullableToMaybe optName
       where
         doAddVariableType : InferredType -> String -> Core ()
         doAddVariableType ty name = do
-            ignore $ addVariableType name ty
+            addVariableType name ty
             case arg of
                 NmLocal _ loc => do
                     let valueVariableName = jvmSimpleName loc
@@ -952,40 +959,38 @@ mutual
                     when (index /= valueVariableIndex) $ createNewVariable "tailRecArg" ty
                 _ => createNewVariable "tailRecArg" ty
 
-    inferExprApp : {auto stateRef: Ref AsmState AsmState} -> InferredType -> NamedCExp -> Core InferredType
-    inferExprApp exprTy app@(NmApp _ (NmRef _ (UN (Basic "$idrisTailRec"))) args) =
+    inferExprApp : {auto stateRef: Ref AsmState AsmState} -> NamedCExp -> Core InferredType
+    inferExprApp app@(NmApp _ (NmRef _ (UN (Basic "$idrisTailRec"))) args) =
         case args of
-            [] => pure exprTy
+            [] => pure IUnknown -- The type will not be used as it is in tail call position
             args@(_ :: argsTail) => do
-                types <- retrieveVariableTypesAtScope !getCurrentScopeIndex
                 argumentNameByIndices <- coreLift $ Map.transpose $ variableIndices !(getScope 0)
-                traverse_ (inferSelfTailCallParameter types argumentNameByIndices) $
-                    zip args [0 .. the Int $ cast $ length argsTail]
-                pure exprTy
-    inferExprApp exprTy (NmApp _ (NmRef _ idrisName) args) = do
+                traverse_ (inferSelfTailCallParameter argumentNameByIndices) $
+                  zip args [0 .. the Int $ cast $ length argsTail]
+                pure IUnknown -- The type will not be used as it is in tail call position
+    inferExprApp (NmApp fc (NmRef _ idrisName) args) = do
         let functionName = jvmName idrisName
-        functionType <- case !(findFunctionType functionName) of
-            Just ty => pure ty
-            Nothing => pure $ MkInferredFunctionType inferredObjectType $ replicate (length args) inferredObjectType
-        let argsWithTypes = zip args (parameterTypes functionType)
-        traverse_ inferParameter argsWithTypes
-        pure $ returnType functionType
-    inferExprApp exprTy (NmApp _ lambdaVariable args) = do
-        ignore $ inferExpr inferredLambdaType lambdaVariable
-        let argsWithTypes = zip args (replicate (length args) IUnknown)
-        traverse_ inferParameter argsWithTypes
+        retType <- case !(findFunctionType functionName) of
+            Just functionType => pure $ returnType functionType
+            Nothing => if idrisName == tailRecLoopFunctionName
+                         then pure inferredObjectType
+                         else throw $ GenericMsg fc "Unknown type for function \{show functionName}"
+        traverse_ inferExpr args
+        pure retType
+    inferExprApp (NmApp _ lambdaVariable args) = do
+        ignore $ inferExpr lambdaVariable
+        traverse_ inferExpr args
         pure IUnknown
-    inferExprApp _ _ = throw $ GenericMsg emptyFC "Not a function application"
+    inferExprApp _ = throw $ GenericMsg emptyFC "Not a function application"
 
-    inferExprCon : {auto stateRef: Ref AsmState AsmState} -> InferredType -> String -> Name -> List NamedCExp -> Core InferredType
-    inferExprCon exprTy fileName name args = do
-        let argsWithTypes = zip args (replicate (length args) inferredObjectType)
-        traverse_ inferParameter argsWithTypes
+    inferExprCon : {auto stateRef: Ref AsmState AsmState} -> String -> Name -> List NamedCExp -> Core InferredType
+    inferExprCon fileName name args = do
+        traverse_ inferExpr args
         pure idrisObjectType
 
-    inferExprCast : {auto stateRef: Ref AsmState AsmState} -> InferredType -> InferredType -> NamedCExp -> Core InferredType
-    inferExprCast sourceType targetType expr = do
-        ignore $ inferExpr sourceType expr
+    inferExprCast : {auto stateRef: Ref AsmState AsmState} -> InferredType -> NamedCExp -> Core InferredType
+    inferExprCast targetType expr = do
+        ignore $ inferExpr expr
         pure targetType
 
     inferExprOp : {auto stateRef: Ref AsmState AsmState} -> PrimFn arity -> Vect arity NamedCExp -> Core InferredType
@@ -1000,37 +1005,37 @@ mutual
     inferExprOp (BAnd ty) [x, y] = inferBinaryOp (getInferredType ty) x y
     inferExprOp (BOr ty) [x, y] = inferBinaryOp (getInferredType ty) x y
     inferExprOp (BXOr ty) [x, y] = inferBinaryOp (getInferredType ty) x y
-    inferExprOp (LT ty) [x, y] = inferBoolOp (getInferredType ty) x y
-    inferExprOp (LTE ty) [x, y] = inferBoolOp (getInferredType ty) x y
-    inferExprOp (EQ ty) [x, y] = inferBoolOp (getInferredType ty) x y
-    inferExprOp (GT ty) [x, y] = inferBoolOp (getInferredType ty) x y
-    inferExprOp (GTE ty) [x, y] = inferBoolOp (getInferredType ty) x y
+    inferExprOp (LT ty) [x, y] = inferBoolOp x y
+    inferExprOp (LTE ty) [x, y] = inferBoolOp x y
+    inferExprOp (EQ ty) [x, y] = inferBoolOp x y
+    inferExprOp (GT ty) [x, y] = inferBoolOp x y
+    inferExprOp (GTE ty) [x, y] = inferBoolOp x y
 
     inferExprOp StrLength [x] = do
-        ignore $ inferExpr inferredStringType x
+        ignore $ inferExpr x
         pure IInt
     inferExprOp StrHead [x] = do
-        ignore $ inferExpr inferredStringType x
+        ignore $ inferExpr x
         pure IChar
     inferExprOp StrTail [x] = do
-        ignore $ inferExpr inferredStringType x
+        ignore $ inferExpr x
         pure inferredStringType
     inferExprOp StrIndex [x, i] = do
-        ignore $ inferExpr inferredStringType x
-        ignore $ inferExpr IInt i
+        ignore $ inferExpr x
+        ignore $ inferExpr i
         pure IChar
     inferExprOp StrCons [x, y] = do
-        ignore $ inferExpr IChar x
-        ignore $ inferExpr inferredStringType y
+        ignore $ inferExpr x
+        ignore $ inferExpr y
         pure inferredStringType
     inferExprOp StrAppend [x, y] = inferBinaryOp inferredStringType x y
     inferExprOp StrReverse [x] = do
-        ignore $ inferExpr inferredStringType x
+        ignore $ inferExpr x
         pure inferredStringType
     inferExprOp StrSubstr [offset, len, str] = do
-        ignore $ inferExpr IInt offset
-        ignore $ inferExpr IInt len
-        ignore $ inferExpr inferredStringType str
+        ignore $ inferExpr offset
+        ignore $ inferExpr len
+        ignore $ inferExpr str
         pure inferredStringType
     inferExprOp DoubleExp [x] = inferUnaryOp IDouble x
     inferExprOp DoubleLog [x] = inferUnaryOp IDouble x
@@ -1045,15 +1050,15 @@ mutual
     inferExprOp DoubleFloor [x] = inferUnaryOp IDouble x
     inferExprOp DoubleCeiling [x] = inferUnaryOp IDouble x
 
-    inferExprOp (Cast ty1 ty2) [x] = inferExprCast (getInferredType ty1) (getInferredType ty2) x
+    inferExprOp (Cast ty1 ty2) [x] = inferExprCast (getInferredType ty2) x
 
     inferExprOp BelieveMe [a, b, x] = do
-      ignore $ inferExpr IUnknown a
-      ignore $ inferExpr IUnknown b
-      ignore $ inferExpr IUnknown x
+      ignore $ inferExpr a
+      ignore $ inferExpr b
+      ignore $ inferExpr x
       pure IUnknown
     inferExprOp Crash [_, msg] = do
-      ignore $ inferExpr inferredStringType msg
+      ignore $ inferExpr msg
       pure IUnknown
     inferExprOp op _ = throw $ GenericMsg emptyFC ("Unsupported primitive function " ++ show op)
 
@@ -1068,10 +1073,6 @@ showScopes n = do
     logAsm $ show scope
     when (n > 0) $ showScopes (n - 1)
 
-tailRecLoopFunctionName : Name
-tailRecLoopFunctionName =
-  NS (mkNamespace "io.github.mmhelloworld.idrisjvm.runtime.Runtime") (UN $ Basic "tailRec")
-
 delayNilArityExpr : FC -> (args: List Name) -> NamedCExp -> NamedCExp
 delayNilArityExpr fc [] expr = NmDelay fc LLazy expr
 delayNilArityExpr _ _ expr = expr
@@ -1085,6 +1086,102 @@ logFunction logPrefix name args expr result =
     then log (logPrefix ++ " " ++ show name ++ ": " ++ show args ++ "\n" ++ showNamedCExp 0 expr) result
     else result
 
+namespace TermType
+  getConstantType : Primitive.Constant -> InferredType
+  getConstantType (I _) = IInt
+  getConstantType WorldVal = IInt
+  getConstantType (I8 _) = IInt
+  getConstantType (I16 _) = IInt
+  getConstantType (I32 _) = IInt
+  getConstantType (I64 _) = ILong
+  getConstantType (B8 _) = IInt
+  getConstantType (B16 _) = IInt
+  getConstantType (B32 _) = IInt
+  getConstantType (B64 _) = ILong
+  getConstantType (Ch _ ) = IInt
+  getConstantType (Str _) = inferredStringType
+  getConstantType (BI _) = inferredBigIntegerType
+  getConstantType (Db _) = IDouble
+  getConstantType (PrT IntType    ) = IInt
+  getConstantType (PrT IntegerType) = inferredBigIntegerType
+  getConstantType (PrT Int8Type   ) = IInt
+  getConstantType (PrT Int16Type  ) = IInt
+  getConstantType (PrT Int32Type  ) = IInt
+  getConstantType (PrT Int64Type  ) = ILong
+  getConstantType (PrT Bits8Type  ) = IInt
+  getConstantType (PrT Bits16Type ) = IInt
+  getConstantType (PrT Bits32Type ) = IInt
+  getConstantType (PrT Bits64Type ) = ILong
+  getConstantType (PrT StringType ) = inferredStringType
+  getConstantType (PrT CharType   ) = IInt
+  getConstantType (PrT DoubleType ) = IDouble
+  getConstantType (PrT WorldType  ) = IInt
+
+  getTypeTerm : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> Name -> Core (Maybe (Term []))
+  getTypeTerm name = do
+    defs <- get Ctxt
+    Just gdef <- lookupCtxtExact name (gamma defs)
+      | Nothing => pure Nothing
+    ty <- normaliseSizeLimit defs 50 [] gdef.type
+    Just <$> toFullNames ty
+
+  showConType : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> ConInfo -> Name -> Core ()
+  showConType conInfo name = do
+    Just ty <- getTypeTerm name
+      | Nothing => coreLift $ printLn $ "Missing type for " ++ show name
+    coreLift $ printLn $ show name ++ "(" ++ show conInfo ++ ")" ++ ": " ++ show ty
+
+  export
+  getTermJvmType : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> Name -> Core (Maybe InferredFunctionType)
+  getTermJvmType name = do
+      Just term <- getTypeTerm name
+        | Nothing => pure Nothing
+      let (ret ::: args) = go [] term
+      pure $ Just $ MkInferredFunctionType ret (reverse args)
+    where
+
+      log : Show a => Lazy a -> b -> b
+      log value b = if show name == "Prelude.Show.protectEsc" then trace (show value) b else b
+
+      getPrimVal : List (Term vars) -> Maybe Primitive.Constant
+      getPrimVal [PrimVal _ c] = Just c
+      getPrimVal args = Nothing
+
+      getConstructorType : Name -> InferredType
+      getConstructorType name =
+        if isBoolTySpec name then IInt
+        else if name == basics "List" then idrisListType
+        else if name == preludetypes "Maybe" then idrisMaybeType
+        else if name == preludetypes "Nat" then inferredBigIntegerType
+        else inferredObjectType
+
+      mutual
+        getFnType : {vars : _} -> List InferredType -> Term vars -> List (Term vars) -> List1 InferredType
+        getFnType types (Ref _ _ tyName) args = getConstructorType tyName ::: types
+        getFnType types (PrimVal _ c) [] = getConstantType c ::: types
+        getFnType types (Bind _ x (Pi _ count _ ty) sc) [] =
+          if count == plusNeutral then go (toList types) sc
+          else case go [] ty of
+            (jvmType ::: []) => go (toList (jvmType ::: types)) sc
+            xs => go (inferredLambdaType :: toList types) sc
+        getFnType types term _ = (inferredObjectType ::: types)
+
+        go : {vars : _} -> List InferredType -> Term vars -> List1 InferredType
+        go types term =
+          let (fn, args) = getFnArgs term
+          in getFnType types fn args
+
+  export
+  showType : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> Name -> Core ()
+  showType name = do
+    let nameString = show name
+    Just ty <- getTypeTerm name
+      | Nothing => coreLift $ printLn $ "Missing type for " ++ nameString
+    coreLift $ printLn $ "\{nameString}: \{show ty}"
+    Just termJvmType <- getTermJvmType name
+      | Nothing => coreLift $ printLn $ "Missing JVM type for " ++ nameString
+    coreLift $ printLn $ "\{nameString}: \{show termJvmType}"
+
 optimizeTailRecursion : String -> (Name, FC, NamedDef) -> List (Name, FC, NamedDef)
 optimizeTailRecursion programName (name, fc, (MkNmFun args body)) =
   let jname = jvmName name
@@ -1105,64 +1202,64 @@ optimize programName allDefs =
       tailCallOptimizedDefs = TailRec.functions tailRecLoopFunctionName tailRecOptimizedDefs
   in toNameFcDef <$> tailCallOptimizedDefs
 
+getArity : InferredFunctionType -> Nat
+getArity (MkInferredFunctionType _ args) = length args
+
 export
-inferDef : {auto stateRef: Ref AsmState AsmState} -> String -> Name -> FC -> NamedDef -> Core ()
-inferDef programName idrisName fc (MkNmFun args expr) = do
+inferFunctionType : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+                  -> (Name, FC, NamedDef) -> Core ()
+inferFunctionType (idrisName, _, MkNmFun args expr) = do
+  let jname = jvmName idrisName
+  let arity = length args
+  let runtimeInitialFunctionType = MkInferredFunctionType inferredObjectType (replicate arity inferredObjectType)
+  maybeFunctionType <- getTermJvmType idrisName
+  let termInitialFunctionType = fromMaybe runtimeInitialFunctionType maybeFunctionType
+  let termTypeArity = getArity termInitialFunctionType
+  let initialFunctionType = if arity == termTypeArity then termInitialFunctionType else runtimeInitialFunctionType
+  let jvmClassAndMethodName = getIdrisFunctionName !getProgramName (className jname) (methodName jname)
+  scopes <- coreLift $ ArrayList.new {elemTy=Scope}
+  let function = MkFunction jname initialFunctionType (subtyping scopes) 0 jvmClassAndMethodName expr
+  setCurrentFunction function
+  coreLift $ addFunction !getGlobalState jname function
+  resetScope
+  scopeIndex <- newScopeIndex
+  let (_, lineStart, lineEnd) = getSourceLocation expr
+  allVariableTypes <- coreLift $ Map.newTreeMap {key=Int} {value=InferredType}
+  allVariableIndices <- coreLift $ Map.newTreeMap {key=String} {value=Int}
+  let arity = length args
+  let arityInt = the Int $ cast arity
+  let argumentNames = jvmSimpleName <$> args
+  argIndices <- coreLift $ getArgumentIndices arityInt argumentNames
+  argumentTypesByName <- coreLift $ Map.fromList $ zip argumentNames (parameterTypes initialFunctionType)
+  let retType = returnType initialFunctionType
+  let functionScope =
+      MkScope scopeIndex Nothing argumentTypesByName allVariableTypes argIndices
+          allVariableIndices retType arityInt (lineStart, lineEnd) ("", "") []
+  saveScope functionScope
+  when (shouldDebugFunction jname) $ showScopes 0
+
+inferFunctionType (idrisName, fc, MkNmForeign foreignDescriptors argumentTypes returnType) =
+  inferForeign idrisName fc foreignDescriptors argumentTypes returnType
+inferFunctionType (idrisName, fc, MkNmError expr) = inferFunctionType (idrisName, fc, MkNmFun [] expr)
+inferFunctionType _ = pure ()
+
+export
+inferDef : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto stateRef: Ref AsmState AsmState}
+         -> Name -> FC -> Core ()
+inferDef idrisName fc = do
     let jname = jvmName idrisName
-    let jvmClassAndMethodName = getIdrisFunctionName programName (className jname) (methodName jname)
-    let argumentNames = jvmSimpleName <$> args
-    let arity = length args
-    let arityInt = the Int $ cast arity
-    argIndices <- coreLift $ getArgumentIndices arityInt argumentNames
-    let initialArgumentTypes = replicate arity inferredObjectType
-    let inferredFunctionType = MkInferredFunctionType inferredObjectType initialArgumentTypes
-    argumentTypesByName <- coreLift $ Map.fromList $ zip argumentNames initialArgumentTypes
-    scopes <- coreLift $ ArrayList.new {elemTy=Scope}
-    let function = MkFunction jname inferredFunctionType (subtyping scopes) 0 jvmClassAndMethodName emptyFunction
-    setCurrentFunction function
-    coreLift $ AsmGlobalState.addFunction !getGlobalState jname function
-    updateCurrentFunction $ { optimizedBody := expr }
-
-    resetScope
-    scopeIndex <- newScopeIndex
-    let (_, lineStart, lineEnd) = getSourceLocation expr
-    allVariableTypes <- coreLift $ Map.newTreeMap {key=Int} {value=InferredType}
-    allVariableIndices <- coreLift $ Map.newTreeMap {key=String} {value=Int}
-    let functionScope =
-        MkScope scopeIndex Nothing argumentTypesByName allVariableTypes argIndices
-            allVariableIndices IUnknown arityInt (lineStart, lineEnd) ("", "") []
-
-    saveScope functionScope
-    retTy <- inferExpr IUnknown expr
-    updateScopeVariableTypes arity
-    updateCurrentFunction $ { inferredFunctionType := inferredFunctionType }
-    when (shouldDebugFunction jname) $ showScopes (scopeCounter !getState - 1)
-  where
-    getArgumentTypes : List String -> Core (List InferredType)
-    getArgumentTypes argumentNames = do
-        argumentIndicesByName <- getVariableIndicesByName 0
-        argumentTypesByIndex <- getVariableTypesAtScope 0
-        coreLift $ go argumentIndicesByName argumentTypesByIndex argumentNames
-      where
-        go : Map String Int -> Map Int InferredType -> List String -> IO (List InferredType)
-        go argumentIndicesByName argumentTypesByIndex argumentNames = do
-            types <- go1 [] argumentNames
-            pure $ reverse types
-          where
-            go1 : List InferredType -> List String -> IO (List InferredType)
-            go1 acc [] = pure acc
-            go1 acc (arg :: args) = do
-                optIndex <- Map.get {value=Int} argumentIndicesByName arg
-                ty <- case nullableToMaybe optIndex of
-                    Just index => do
-                        optTy <- Map.get argumentTypesByIndex index
-                        pure $ fromMaybe IUnknown $ nullableToMaybe optTy
-                    Nothing => pure IUnknown
-                go1 (ty :: acc) args
-
-inferDef programName n fc (MkNmError expr) = inferDef programName n fc (MkNmFun [] expr)
-
-inferDef programName idrisName fc def@(MkNmForeign foreignDescriptors argumentTypes returnType) =
-    inferForeign programName idrisName fc foreignDescriptors argumentTypes returnType
-
-inferDef _ _ _ _ = pure ()
+    globalState <- getGlobalState
+    Just function <- coreLift $ findFunction globalState jname
+      | Nothing => throw (GenericMsg fc ("Unable to find function \{show jname}"))
+    let expr = optimizedBody function
+    if isForeign expr
+      then pure ()
+      else do
+        when (shouldDebugFunction jname) $ coreLift $ printLn "Optimized: \{showNamedCExp 0 expr}"
+        setCurrentFunction function
+        resetScope
+        size <- coreLift $ Collection.size {elemTy=Scope, obj=Collection Scope} $ believe_me (scopes function)
+        setScopeCounter size
+        ignore $ inferExpr expr
+        updateScopeVariableTypes
+        when (shouldDebugFunction jname) $ showScopes (scopeCounter !getState - 1)
diff --git a/src/Compiler/Jvm/Variable.idr b/src/Compiler/Jvm/Variable.idr
index 77d52762e..952cd7576 100644
--- a/src/Compiler/Jvm/Variable.idr
+++ b/src/Compiler/Jvm/Variable.idr
@@ -131,12 +131,14 @@ asmCast IChar IChar     = pure ()
 asmCast IShort IShort   = pure ()
 asmCast IInt IBool      = pure ()
 asmCast IInt IInt       = pure ()
+asmCast IChar IInt      = pure ()
 asmCast ILong ILong     = pure ()
 asmCast IFloat IFloat   = pure ()
 asmCast IDouble IDouble = pure ()
 asmCast (IArray _) (IArray _) = pure ()
 
 asmCast IBool IInt = boolToInt
+asmCast IVoid IInt = iconst 0 -- for primitive functions returning void, Idris return type will be int
 asmCast IInt IChar = i2c
 asmCast IInt IByte = i2b
 asmCast IInt IShort = i2s
@@ -183,7 +185,6 @@ asmCast (IRef _ _ _) arr@(IArray _) = checkcast $ getJvmTypeDescriptor arr
 asmCast (IArray _) (IRef clazz _ _) = checkcast clazz
 
 asmCast _ IVoid = pure ()
-asmCast IVoid IVoid = pure ()
 asmCast IVoid (IRef _ _ _) = aconstnull
 asmCast IVoid IUnknown = aconstnull
 asmCast ty IUnknown = pure ()
@@ -296,6 +297,9 @@ loadVar sourceLocTys ty ILong var =
     let loadInstr = \index => do aload index; objToLong
     in opWithWordSize sourceLocTys loadInstr var
 
+loadVar sourceLocTys (IRef "java/math/BigInteger" _ _) (IRef "java/math/BigInteger" _ _) var =
+  opWithWordSize sourceLocTys aload var
+
 loadVar sourceLocTys _ (IRef "java/math/BigInteger" _ _) var =
     let loadInstr = \index => do
       aload index
diff --git a/tests/jvm/nat2fin/Check.idr b/tests/jvm/nat2fin/Check.idr
index a812ba99b..63b3ed1f9 100644
--- a/tests/jvm/nat2fin/Check.idr
+++ b/tests/jvm/nat2fin/Check.idr
@@ -15,7 +15,7 @@ isOptimized (_ :: _ :: []) = False
 isOptimized (_ :: []) = False
 isOptimized (line1 :: line2 :: line3 :: rest) = (("String 375" `isSuffixOf` line1) &&
   ("Method java/math/BigInteger.\"<init>\":(Ljava/lang/String;)V" `isSuffixOf` line2) &&
-  ("Method M_Data/Fin.show$show_Show_$lparFin$s$n$rpar:(Ljava/lang/Object;)Ljava/lang/Object;" `isSuffixOf` line3)) ||
+  ("Method M_Data/Fin.show$show_Show_$lparFin$s$n$rpar:" `isInfixOf` line3)) ||
   isOptimized (line2 :: line3 :: rest)
 
 main : IO ()