Skip to content

Commit

Permalink
Typechecker (MGU.hs): fix unergonomic checking of function applications
Browse files Browse the repository at this point in the history
When checking a function call, and it's wrong, we expect the error to
be reported as the arguments having the wrong type, not the function
being the wrong type for the arguments we provided.

Therefore, check an application by matching the argument against the
function, not the function against the arguments. In particular, we
should generate a fresh argument type and unify it with the type of
the function, _then_ unify it with the argument expression, not the
other way around.

Someone stepped on this today internally and it was confusing all
around.

Add a test case in test_type_errors.
  • Loading branch information
sauclovian-g committed Dec 11, 2024
1 parent 01c4ca8 commit eca889f
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 6 deletions.
12 changes: 12 additions & 0 deletions intTests/test_type_errors/err002.log.good
Original file line number Diff line number Diff line change
@@ -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
8 changes: 8 additions & 0 deletions intTests/test_type_errors/err002.saw
Original file line number Diff line number Diff line change
@@ -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];
};

13 changes: 7 additions & 6 deletions src/SAWScript/MGU.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit eca889f

Please sign in to comment.