git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Prevent skolem variables from escaping
ce885efPhil Freeman
examples/failing/SkolemEscape.psnew file+3
compare with golang
unifiedsplit
@@ -0,0 +1,3 @@
1+foreign import foo :: (forall a. a -> a) -> Number
2+
3+test = \x -> foo x
src/Language/PureScript/TypeChecker/Types.hs+15−2
@@ -22,7 +22,9 @@ import Data.List
22import Data.Maybe (isJust, fromMaybe)
22import Data.Maybe (isJust, fromMaybe)
23import Data.Function
23import Data.Function
24import qualified Data.Data as D
24import qualified Data.Data as D
25+import Data.Generics
25−import Data.Generics (everywhere, everywhereM, everything, everywhereBut, mkT, mkM, mkQ, extM, extQ)
26+ (something, everywhere, everywhereM, everything, everywhereBut,
27+ mkT, mkM, mkQ, extM, extQ)
26
28
27import Language.PureScript.Values
29import Language.PureScript.Values
28import Language.PureScript.Types
30import Language.PureScript.Types
@@ -145,7 +147,6 @@ isFunction (Abs _ _) = True
145isFunction (TypedValue untyped _) = isFunction untyped
147isFunction (TypedValue untyped _) = isFunction untyped
146isFunction _ = False
148isFunction _ = False
147
149
148−-- TODO: check skolems don't escape
149typeOf :: Maybe Ident -> Value -> Check Type
150typeOf :: Maybe Ident -> Value -> Check Type
150typeOf name val = do
151typeOf name val = do
151 (ty, sub, checks) <- runSubst $ case name of
152 (ty, sub, checks) <- runSubst $ case name of
@@ -164,6 +165,7 @@ typeOf name val = do
164 return ty
165 return ty
165 _ -> infer M.empty val
166 _ -> infer M.empty val
166 escapeCheck checks ty sub
167 escapeCheck checks ty sub
168+ skolemEscapeCheck ty
167 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
169 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
168
170
169escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()
171escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()
@@ -176,6 +178,17 @@ escapeCheck checks ty sub =
176 let unsolvedUnknowns = nub . unknowns $ apply sub t
178 let unsolvedUnknowns = nub . unknowns $ apply sub t
177 guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
179 guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
178
180
181+skolemEscapeCheck :: Type -> Check ()
182+skolemEscapeCheck ty =
183+ case something (extQ (mkQ Nothing findSkolems) findRSkolems) ty of
184+ Nothing -> return ()
185+ Just _ -> throwError "Skolem variables cannot escape. Consider adding a type signature."
186+ where
187+ findSkolems (Skolem _) = return ()
188+ findSkolems _ = mzero
189+ findRSkolems (RSkolem _) = return ()
190+ findRSkolems _ = mzero
191+
179setify :: Row -> Row
192setify :: Row -> Row
180setify = rowFromList . first (M.toList . M.fromList) . rowToList
193setify = rowFromList . first (M.toList . M.fromList) . rowToList
181
194