Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 17 additions & 17 deletions src/Solcore/Frontend/TypeInference/TcMonad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ addUniqueType :: Name -> DataTy -> TcM ()
addUniqueType n dt
= do
modify (\ ctx -> ctx{ uniqueTypes = Map.insert n dt (uniqueTypes ctx)})
checkDataType dt
checkDataType dt

lookupUniqueTy :: Name -> TcM (Maybe DataTy)
lookupUniqueTy n
Expand Down Expand Up @@ -163,10 +163,10 @@ isDirectCall n
checkDataType :: DataTy -> TcM ()
checkDataType d@(DataTy n vs constrs)
= do
-- check if the type is already defined.
r <- maybeAskTypeInfo n
unless (isNothing r) $
typeAlreadyDefinedError d n
-- check if the type is already defined.
r <- maybeAskTypeInfo n
unless (isNothing r) $
typeAlreadyDefinedError d n
let vals' = map (\ (n, ty) -> (n, Forall (bv ty) ([] :=> ty))) vals
mapM_ (uncurry extEnv) vals'
modifyTypeInfo n ti
Expand Down Expand Up @@ -643,28 +643,28 @@ undefinedClass :: Name -> TcM a
undefinedClass n
= throwError $ unlines ["Undefined class:", pretty n]

typeAlreadyDefinedError :: DataTy -> Name -> TcM a
typeAlreadyDefinedError d n
= do
-- get type info
typeAlreadyDefinedError :: DataTy -> Name -> TcM a
typeAlreadyDefinedError d n
= do
-- get type info
di <- askTypeInfo n
d' <- dataTyFromInfo n di `wrapError` d
d' <- dataTyFromInfo n di `wrapError` d
throwError $ unlines ["Duplicated type definition for " ++ pretty n ++ ":"
, pretty d
, "and"
, pretty d']

dataTyFromInfo :: Name -> TypeInfo -> TcM DataTy
dataTyFromInfo n (TypeInfo ar cs _)
= do
-- getting data constructor types
dataTyFromInfo :: Name -> TypeInfo -> TcM DataTy
dataTyFromInfo n (TypeInfo ar cs _)
= do
-- getting data constructor types
(constrs, vs) <- unzip <$> mapM constrsFromEnv cs
pure (DataTy n (concat vs) constrs)

constrsFromEnv :: Name -> TcM (Constr, [Tyvar])
constrsFromEnv n
= do
(Forall vs (_ :=> ty)) <- askEnv n
constrsFromEnv n
= do
(Forall vs (_ :=> ty)) <- askEnv n
let (ts, _) = splitTy ty
pure (Constr n ts, vs)

Expand Down
31 changes: 19 additions & 12 deletions src/Solcore/Frontend/TypeInference/TcStmt.hs
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,13 @@ tcStmt e@(Let n mt me)
return (Just e', ps, t1)
(Nothing, Nothing) ->
(Nothing, [],) <$> freshTyVar
-- here, we could remove the unique type when
-- the variable has the same name as a function
-- that has been type checked before.
r <- lookupUniqueTy n
when (isJust r) $ do
modify (\ sig -> sig {uniqueTypes = Map.delete n (uniqueTypes sig) })
----
extEnv n (monotype tf)
let e' = Let (Id n tf) (Just tf) me'
withCurrentSubst (e', psf, unit)
Expand Down Expand Up @@ -338,7 +345,7 @@ createClosureType ids vs ty
i <- incCounter
s <- getSubst
let
ts = map idType ids
ts = map idType ids
dn = Name $ "t_closure" ++ show i
ts' = everywhere (mkT gen) ts
ns = map Var $ (apply s ids)
Expand Down Expand Up @@ -460,7 +467,7 @@ tiFunDef d@(FunDef sig@(Signature _ _ n args _) bd)
-- typing function body
(bd1, ps1, t1) <- withLocalCtx lctx' (tcBody bd) `wrapError` d
-- unifying context introduced type with infered function type
s <- unify nt (funtype ts' t1) `wrapError` d
s <- unify nt (funtype ts' t1) `wrapError` d
-- building the function type scheme
rs <- reduce [] ps1 `wrapError` d
ty <- withCurrentSubst nt
Expand Down Expand Up @@ -494,7 +501,7 @@ annotatedScheme vs' sig@(Signature vs ps n args rt)
tcFunDef :: Bool -> [Tyvar] -> [Pred] -> FunDef Name -> TcM (FunDef Id, Scheme)
tcFunDef incl vs' qs d@(FunDef sig@(Signature vs ps n args rt) bd)
| hasAnn sig = do
info ["\n# tcFunDef ", pretty d]
info ["\n# tcFunDef ", pretty sig]
let vars = vs `union` vs'
-- check if all variables are bound in signature.
when (any (\ v -> v `notElem` vars) (bv sig)) $ do
Expand All @@ -515,15 +522,15 @@ tcFunDef incl vs' qs d@(FunDef sig@(Signature vs ps n args rt) bd)
let lctx' = if incl then (n, monotype nt) : lctx else lctx
-- typing function body
(bd1', ps1', t1') <- withLocalCtx lctx' (tcBody bd1) `wrapError` d
-- checking if the type checking have changed the type
-- checking if the type checking have changed the type
-- due to unique type creation.
let tynames = tyconNames t1'
changeTy <- or <$> mapM isUniqueTyName tynames
changeTy <- or <$> mapM isUniqueTyName tynames
let rt2 = if changeTy then t1' else rt1'
info ["Trying to unify: ", pretty rt2, " with ", pretty t1']
unify rt2 t1' `wrapError` d
info ["Trying to unify: ", pretty nt, " with ", pretty (funtype ts' rt2)]
unify nt (funtype ts' rt2) `wrapError` d
unify nt (funtype ts' rt2) `wrapError` d
-- building the function type scheme
free <- getEnvMetaVars
rs <- reduce (qs1 `union` ps1) ps1' `wrapError` d
Expand All @@ -536,11 +543,11 @@ tcFunDef incl vs' qs d@(FunDef sig@(Signature vs ps n args rt) bd)
when (ambiguous inf) $
ambiguousTypeError inf sig
-- checking subsumption
unless changeTy $ do
unless changeTy $ do
subsCheck sig inf ann `wrapError` d
-- elaborating function body
let ann' = if changeTy then inf else ann
fdt <- elabFunDef vs' sig1 bd1' inf ann' `wrapError` d
fdt <- elabFunDef vs' sig1 bd1' inf ann' `wrapError` d
withCurrentSubst (fdt, ann')
| otherwise = tiFunDef d

Expand Down Expand Up @@ -691,7 +698,7 @@ verifySignatures instd@(Instance _ _ ps n ts t funs) =
do
-- get class info
mcinfo <- Map.lookup n <$> gets classTable
when (isNothing mcinfo) (undefinedClass n) `wrapError` instd
when (isNothing mcinfo) (undefinedClass n) `wrapError` instd
-- building instance constraint
let
-- this use of fromJust is safe, because is
Expand Down Expand Up @@ -813,10 +820,10 @@ checkInstance idef@(Instance d vs ctx n ts t funs)
-- checking the coverage condition
insts' <- askInstEnv n `wrapError` ipred
-- check overlapping only for non-default instances
let vs1 = bv ipred
ts1 <- mapM (const freshTyVar) vs1
let vs1 = bv ipred
ts1 <- mapM (const freshTyVar) vs1
let env = zip vs1 ts1
ipred' = insts env ipred
ipred' = insts env ipred
unless d (checkOverlap ipred' insts' `wrapError` idef)
-- check if default instance has a type variable as main argument.
when d (checkDefaultInst (ctx :=> ipred) `wrapError` idef)
Expand Down
1 change: 1 addition & 0 deletions test/Cases.hs
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,7 @@ cases =
, runTestExpectingFailure "overlapping-heads.solc" caseFolder
, runTestExpectingFailure "instance-wrong-sig.solc" caseFolder
, runTestForFile "match-yul.solc" caseFolder
, runTestForFile "local-variable-mess.solc" caseFolder
]
where
caseFolder = "./test/examples/cases"
Expand Down
20 changes: 20 additions & 0 deletions test/examples/cases/local-variable-mess.solc
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
forall t . class t:Sub {
function sub(l: t, r: t) -> t;
}

instance word:Sub {
function sub(l: word, r: word) -> word {
let rw : word;
assembly {
rw := sub(l,r);
}
return rw;
}
}

function start() -> () {}

function g() -> word {
let start : word = 0;
return Sub.sub(9, start);
}