diff --git a/intTests/test_type_errors/err002.log.good b/intTests/test_type_errors/err002.log.good new file mode 100644 index 000000000..6bd5db604 --- /dev/null +++ b/intTests/test_type_errors/err002.log.good @@ -0,0 +1,12 @@ + Loading file "err002.saw" + err002.saw:5:44-5:57: Type mismatch. + Mismatch of type constructors. Expected: String but got ([]) + internal:1:1-1:7: The type String arises from this type annotation + err002.saw:5:44-5:57: The type [LLVMType] arises from the type of this term + + Expected: String + Found: [LLVMType] + + within "spec" (err002.saw:4:5-4:9) + +FAILED diff --git a/intTests/test_type_errors/err002.saw b/intTests/test_type_errors/err002.saw new file mode 100644 index 000000000..888af8e1a --- /dev/null +++ b/intTests/test_type_errors/err002.saw @@ -0,0 +1,8 @@ +// llvm_alias takes a string, pass it a list of types instead +// (user meant to use llvm_struct_type and used llvm_struct, +// which is a deprecated name for llvm_alias) +let spec = do { + input <- llvm_fresh_var "x" (llvm_alias [llvm_int 32]); + llvm_execute_func [llvm_term input]; +}; + diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs index f31089be3..1cba82a32 100644 --- a/src/SAWScript/MGU.hs +++ b/src/SAWScript/MGU.hs @@ -849,12 +849,13 @@ inferExpr (ln, expr) = case expr of (body', t) <- withPattern pat' $ inferExpr (ln, body) return (Function pos pat' body', tFun (PosInferred InfContext (getPos body)) pt t) - Application pos f v -> - do (v',fv) <- inferExpr (ln,v) - t <- getFreshTyVar pos - let ft = tFun (PosInferred InfContext $ getPos f) fv t - f' <- checkExpr ln f ft - return (Application pos f' v', t) + Application pos f arg -> + do argtype <- getFreshTyVar pos + rettype <- getFreshTyVar pos + let ftype = tFun (PosInferred InfContext $ getPos f) argtype rettype + f' <- checkExpr ln f ftype + arg' <- checkExpr ln arg argtype + return (Application pos f' arg', rettype) Let pos dg body -> do dg' <- inferDeclGroup dg