mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-23 16:28:02 +03:00
report free type vars before starting typechecking
This commit is contained in:
parent
a38ebba0e2
commit
ae72fa22c7
@ -119,7 +119,7 @@ typeMap f t = go t where
|
||||
wrapV :: Ord v => AnnotatedTerm v a -> AnnotatedTerm (ABT.V v) a
|
||||
wrapV = vmap ABT.Bound
|
||||
|
||||
freeVars :: Term v -> Set v
|
||||
freeVars :: AnnotatedTerm' vt v a -> Set v
|
||||
freeVars = ABT.freeVars
|
||||
|
||||
freeTypeVars :: Ord vt => AnnotatedTerm' vt v a -> Set vt
|
||||
|
@ -13,7 +13,7 @@ underlying (Universal v) = v
|
||||
underlying (Existential v) = v
|
||||
|
||||
instance Show v => Show (TypeVar v) where
|
||||
show (Universal v) = "@" ++ show v
|
||||
show (Universal v) = show v
|
||||
show (Existential v) = "'" ++ show v
|
||||
|
||||
instance Var v => Var (TypeVar v) where
|
||||
|
@ -901,28 +901,36 @@ synthesizeClosed' :: Var v
|
||||
-> DataDeclarations v
|
||||
-> Term v
|
||||
-> M v (Type v)
|
||||
synthesizeClosed' abilities decls term | Set.null (ABT.freeVars term) =
|
||||
synthesizeClosed' abilities decls term
|
||||
| Set.null (ABT.freeVars term) =
|
||||
verifyDataDeclarations decls *>
|
||||
case runM (synthesize term) (MEnv env0 abilities decls True) of
|
||||
Left err -> M $ \_ -> Left err
|
||||
Right (t,env) -> pure $ generalizeExistentials (ctx env) t
|
||||
synthesizeClosed' _abilities _decls term =
|
||||
fail $ "cannot synthesize term with free variables: " ++ show (map Var.name $ Set.toList (ABT.freeVars term))
|
||||
fail $ "Unknown symbols: " ++ show (Set.toList . ABT.freeVars $ term)
|
||||
|
||||
checkClosed :: (Monad f, Var v) => Term v -> Noted f ()
|
||||
checkClosed t =
|
||||
let fvs = Set.toList $ Term.freeVars t
|
||||
fvts = Set.toList $ Term.freeTypeVars t
|
||||
in if null fvs && null fvts
|
||||
then pure ()
|
||||
else fail $ "Unknown symbols: " ++ intercalate ", " (Set.toList . Set.fromList $ map show fvs ++ map show fvts)
|
||||
|
||||
synthesizeClosedAnnotated :: (Monad f, Var v)
|
||||
=> [Type v]
|
||||
-> DataDeclarations v
|
||||
-> Term v
|
||||
-> Noted f (Type v)
|
||||
synthesizeClosedAnnotated abilities decls term | Set.null (ABT.freeVars term) = do
|
||||
synthesizeClosedAnnotated abilities decls term = do
|
||||
checkClosed term
|
||||
Note.fromEither $
|
||||
runM (verifyDataDeclarations decls *> synthesize term)
|
||||
(MEnv env0 abilities decls True)
|
||||
>>= \(t,env) ->
|
||||
-- we generalize over any remaining unsolved existentials
|
||||
pure $ generalizeExistentials (ctx env) t
|
||||
synthesizeClosedAnnotated _abilities _decls term =
|
||||
fail $ "cannot synthesize term with free variables: " ++ show (map Var.name $ Set.toList (ABT.freeVars term))
|
||||
|
||||
verifyDataDeclarations :: Var v => DataDeclarations v -> M v ()
|
||||
verifyDataDeclarations decls = forM_ (Map.toList decls) $ \(r, decl) -> do
|
||||
|
Loading…
Reference in New Issue
Block a user