GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 13:01:31 +03:00
Code Issues Projects Releases Wiki Activity

expect* functions use correct argument order for mismatch

Browse Source 
The `Type` argument is always the "expected" type (not the
"inferred" type) and so it should be the first argument to
`TypeMismatch` or `unify`.

Fixes #382.
This commit is contained in:
Brian Huffman 2016-09-20 11:24:24 -07:00
parent 6c2f0fc399
commit d895c97c8b
1 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/Cryptol/TypeCheck/Infer.hs
View File

@ -266,7 +266,7 @@ checkE expr tGoal =
P.EComp e mss ->
do (mss', dss, ts) <- unzip3 `fmap` zipWithM inferCArm [ 1 .. ] mss
(len,a)<- expectSeq tGoal
(len,a) <- expectSeq tGoal
newGoals CtComprehension =<< unify len =<< smallest ts
@ -337,12 +337,12 @@ expectSeq ty =
TVar _ ->
do tys@(a,b) <- genTys
newGoals CtExactType =<< unify (tSeq a b) ty
newGoals CtExactType =<< unify ty (tSeq a b)
return tys
_ ->
do tys@(a,b) <- genTys
recordError (TypeMismatch (tSeq a b) ty)
recordError (TypeMismatch ty (tSeq a b))
return tys
where
genTys =
@ -363,12 +363,12 @@ expectTuple n ty =
TVar _ ->
do tys <- genTys
newGoals CtExactType =<< unify (tTuple tys) ty
newGoals CtExactType =<< unify ty (tTuple tys)
return tys
_ ->
do tys <- genTys
recordError (TypeMismatch (tTuple tys) ty)
recordError (TypeMismatch ty (tTuple tys))
return tys
where
@ -391,9 +391,9 @@ expectRec fs ty =
_ ->
do (tys,res) <- genTys
case ty of
TVar TVFree{} -> do ps <- unify (TRec tys) ty
TVar TVFree{} -> do ps <- unify ty (TRec tys)
newGoals CtExactType ps
_ -> recordError (TypeMismatch (TRec tys) ty)
_ -> recordError (TypeMismatch ty (TRec tys))
return res
where
@ -422,7 +422,7 @@ expectFin n ty =
return ()
_ ->
do newGoals CtExactType =<< unify (tNum n) ty
do newGoals CtExactType =<< unify ty (tNum n)
expectFun :: Int -> Type -> InferM ([Type],Type)
expectFun = go []
@ -442,9 +442,9 @@ expectFun = go []
do args <- genArgs arity
res <- newType (text "result of function") KType
case ty of
TVar TVFree{} -> do ps <- unify (foldr tFun res args) ty
TVar TVFree{} -> do ps <- unify ty (foldr tFun res args)
newGoals CtExactType ps
_ -> recordError (TypeMismatch (foldr tFun res args) ty)
_ -> recordError (TypeMismatch ty (foldr tFun res args))
return (reverse tys ++ args, res)
| otherwise =