64ea30a · rowtype-yoga/purescript-native

git.iko.soy/rowtype-yoga/purescript-native

on golang help sign in

First work on fixing the skolems bug #147

64ea30aPhil Freeman13 years ago

examples/failing/SkolemEscape2.pursnew file+9

compare with golang

unifiedsplit

@@ -0,0 +1,9 @@

1+module SkolemEscape where

3+import Prelude

4+import Eff

5+import ST

7+test _ = do

8+ r <- runST (newSTRef 0)

9+ ret 0

examples/passing/Eff.purs+3−3

@@ -10,10 +10,10 @@ test1 = catchError (\s -> ret 0) $ do

10 trace "Testing"

11 throwError "Error!"

13−test2 = runPure $ runST $ do

13+test2 = runST (do

14 ref <- newSTRef 0

15 modifySTRef ref $ \n -> n + 1

16− readSTRef ref

16+ readSTRef ref)

18module Main where

@@ -24,4 +24,4 @@ import TestEff

24main = do

25 n <- test1

26 Trace.print n

27− Trace.print test2

27+ --Trace.print test2

src/Language/PureScript/CodeGen/JS.hs+3−3

@@ -128,7 +128,7 @@ runtimeTypeChecks arg ty =

128 where

129 getFunctionArgumentType :: Type -> Maybe Type

130 getFunctionArgumentType (TypeApp (TypeApp t funArg) _) | t == tyFunction = Just funArg

131− getFunctionArgumentType (ForAll _ ty') = getFunctionArgumentType ty'

131+ getFunctionArgumentType (ForAll _ ty' _) = getFunctionArgumentType ty'

132 getFunctionArgumentType _ = Nothing

133 argumentCheck :: JS -> Type -> [JS]

134 argumentCheck val t | t == tyNumber = [typeCheck val "number"]

@@ -141,7 +141,7 @@ runtimeTypeChecks arg ty =

141 in

142 typeCheck val "object" : concatMap (\(prop, ty') -> argumentCheck (JSAccessor prop val) ty') pairs

143 argumentCheck val (TypeApp (TypeApp t _) _) | t == tyFunction = [typeCheck val "function"]

144− argumentCheck val (ForAll _ ty') = argumentCheck val ty'

144+ argumentCheck val (ForAll _ ty' _) = argumentCheck val ty'

145 argumentCheck _ _ = []

146 typeCheck :: JS -> String -> JS

147 typeCheck js ty' = JSIfElse (JSBinary NotEqualTo (JSTypeOf js) (JSStringLiteral ty')) (JSBlock [JSThrow (JSStringLiteral $ ty' ++ " expected")]) Nothing

@@ -253,7 +253,7 @@ isOnlyConstructor m e ctor =

253 where

254 numConstructors ty = length $ filter (\(ty1, _) -> ((==) `on` typeConstructor) ty ty1) $ M.elems $ dataConstructors e

255 typeConstructor (TypeConstructor qual) = qualify m qual

256− typeConstructor (ForAll _ ty) = typeConstructor ty

256+ typeConstructor (ForAll _ ty _) = typeConstructor ty

257 typeConstructor (TypeApp (TypeApp t _) ty) | t == tyFunction = typeConstructor ty

258 typeConstructor (TypeApp ty _) = typeConstructor ty

259 typeConstructor fn = error $ "Invalid arguments to typeConstructor: " ++ show fn

src/Language/PureScript/Pretty/Types.hs+3−3

@@ -36,10 +36,10 @@ typeLiterals = mkPattern match

36 match (TypeApp arr ty) | arr == tyArray = Just $ "[" ++ prettyPrintType ty ++ "]"

37 match (TypeConstructor ctor) = Just $ show ctor

38 match (TUnknown (Unknown u)) = Just $ 'u' : show u

39− match (Skolem s) = Just $ 's' : show s

39+ match (Skolem s _) = Just $ 's' : show s

40 match (ConstrainedType deps ty) = Just $ "(" ++ intercalate "," (map (\(pn, ty') -> show pn ++ " (" ++ prettyPrintType ty' ++ ")") deps) ++ ") => " ++ prettyPrintType ty

41 match (SaturatedTypeSynonym name args) = Just $ show name ++ "<" ++ intercalate "," (map prettyPrintType args) ++ ">"

42− match (ForAll ident ty) = Just $ "forall " ++ ident ++ ". " ++ prettyPrintType ty

42+ match (ForAll ident ty _) = Just $ "forall " ++ ident ++ ". " ++ prettyPrintType ty

43 match REmpty = Just $ prettyPrintRow REmpty

44 match row@(RCons _ _ _) = Just $ prettyPrintRow row

45 match _ = Nothing

@@ -56,7 +56,7 @@ prettyPrintRow = (\(tys, rest) -> intercalate ", " (map (uncurry nameAndTypeToPs

56 tailToPs REmpty = ""

57 tailToPs (TUnknown (Unknown u)) = " | u" ++ show u

58 tailToPs (TypeVar var) = " | " ++ var

59− tailToPs (Skolem s) = " | s" ++ show s

59+ tailToPs (Skolem s _) = " | s" ++ show s

60 tailToPs _ = error "Invalid row tail"

61 toList :: [(String, Type)] -> Type -> ([(String, Type)], Type)

62 toList tys (RCons name ty row) = toList ((name, ty):tys) row

src/Language/PureScript/Sugar/TypeClasses.hs+2−2

@@ -74,7 +74,7 @@ typeClassMemberToDictionaryAccessor :: ProperName -> String -> Declaration -> De

74typeClassMemberToDictionaryAccessor name arg (TypeDeclaration ident ty) =

75 ExternDeclaration TypeClassAccessorImport ident

76 (Just (JSFunction (Just $ identToJs ident) ["dict"] (JSBlock [JSReturn (JSAccessor (identToJs ident) (JSVar "dict"))])))

77− (ForAll arg (ConstrainedType [(Qualified Nothing name, TypeVar arg)] ty))

77+ (ForAll arg (ConstrainedType [(Qualified Nothing name, TypeVar arg)] ty) Nothing)

78typeClassMemberToDictionaryAccessor _ _ _ = error "Invalid declaration in type class definition"

80typeInstanceDictionaryDeclaration :: ModuleName -> [(Qualified ProperName, Type)] -> Qualified ProperName -> Type -> [Declaration] -> Desugar Declaration

@@ -120,7 +120,7 @@ qualifiedToString mn (Qualified Nothing pn) = qualifiedToString mn (Qualified (J

120qualifiedToString _ (Qualified (Just (ModuleName mn)) pn) = runProperName mn ++ "_" ++ runProperName pn

121

122quantify :: Type -> Type

123−quantify ty' = foldr ForAll ty' tyVars

123+quantify ty' = foldr (\arg t -> ForAll arg t Nothing) ty' tyVars

124 where

125 tyVars = nub $ everything (++) (mkQ [] collect) ty'

126 collect (TypeVar v) = [v]

src/Language/PureScript/TypeChecker.hs+1−1

@@ -230,7 +230,7 @@ typeCheckAll currentModule (d@(ImportDeclaration moduleName idents) : rest) = do

230 addTypeClassDictionaries [tcd { tcdName = (Qualified (Just currentModule) ident), tcdType = TCDAlias (tcdName tcd) }]

231 constructs (TypeConstructor (Qualified (Just mn) pn')) pn

232 = mn == moduleName && pn' == pn

233− constructs (ForAll _ ty) pn = ty `constructs` pn

233+ constructs (ForAll _ ty _) pn = ty `constructs` pn

234 constructs (TypeApp (TypeApp t _) ty) pn | t == tyFunction = ty `constructs` pn

235 constructs (TypeApp ty _) pn = ty `constructs` pn

236 constructs fn _ = error $ "Invalid arguments to constructs: " ++ show fn

src/Language/PureScript/TypeChecker/Kinds.hs+1−1

@@ -142,7 +142,7 @@ infer (TypeApp t1 t2) = do

142 k2 <- infer t2

143 k1 =?= FunKind k2 k0

144 return k0

145−infer (ForAll ident ty) = do

145+infer (ForAll ident ty _) = do

146 k <- fresh

147 Just moduleName <- checkCurrentModule <$> get

148 bindLocalTypeVariables moduleName [(ProperName ident, k)] $ infer ty

src/Language/PureScript/TypeChecker/Types.hs+159−99

@@ -45,7 +45,8 @@ import Data.List

45import Data.Maybe (maybeToList, isNothing, isJust, fromMaybe)

46import qualified Data.Data as D

47import Data.Generics

48+ (everythingWithContext, mkM, everywhereM, everything, mkT,

48− (mkM, everywhereM, everything, mkT, something, everywhere, mkQ)

49+ something, everywhere, mkQ)

50import Language.PureScript.Values

51import Language.PureScript.Values

51import Language.PureScript.Types

52import Language.PureScript.Types

@@ -66,6 +67,7 @@ import Control.Arrow (Arrow(..))

67import qualified Data.Map as M

68import qualified Data.Map as M

68import Data.Function (on)

69import Data.Function (on)

70+import Debug.Trace (trace)

70instance Partial Type where

72instance Partial Type where

71 unknown = TUnknown

73 unknown = TUnknown

@@ -86,17 +88,23 @@ unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 +

86 unifyTypes' (TUnknown u) t = u =:= t

88 unifyTypes' (TUnknown u) t = u =:= t

87 unifyTypes' t (TUnknown u) = u =:= t

89 unifyTypes' t (TUnknown u) = u =:= t

88 unifyTypes' (SaturatedTypeSynonym name args) ty = do

90 unifyTypes' (SaturatedTypeSynonym name args) ty = do

89− ty1 <- expandTypeSynonym name args

91+ ty1 <- introduceSkolemScope <=< expandTypeSynonym name $ args

90 ty1 `unifyTypes` ty

92 ty1 `unifyTypes` ty

91 unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty

93 unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty

92− unifyTypes' (ForAll ident1 ty1) (ForAll ident2 ty2) = do

94+ unifyTypes' (ForAll ident1 ty1 sc1) (ForAll ident2 ty2 sc2) =

95+ case (sc1, sc2) of

96+ (Just sc1', Just sc2') -> do

97+ sko <- newSkolemConstant

93− sk <- skolemize ident1 ty1

98+ let sk1 = skolemize ident1 sko sc1' ty1

94− replaced <- replaceVarWithUnknown ident2 ty2

99+ let sk2 = skolemize ident2 sko sc2' ty2

95− sk `unifyTypes` replaced

100+ sk1 `unifyTypes` sk2

101+ _ -> throwError (prettyPrintType ty1)

96− unifyTypes' (ForAll ident ty1) ty2 = do

102+ unifyTypes' (ForAll ident ty1 (Just sc)) ty2 = do

103+ sko <- newSkolemConstant

97− sk <- skolemize ident ty1

104+ let sk = skolemize ident sko sc ty1

98 sk `unifyTypes` ty2

105 sk `unifyTypes` ty2

106+ unifyTypes' (ForAll _ _ _) _ = throwError "Skolem variable scope is unspecified"

99− unifyTypes' ty f@(ForAll _ _) = f `unifyTypes` ty

107+ unifyTypes' ty f@(ForAll _ _ _) = f `unifyTypes` ty

100 unifyTypes' (Object row1) (Object row2) = row1 =?= row2

108 unifyTypes' (Object row1) (Object row2) = row1 =?= row2

101 unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()

109 unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()

102 unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do

110 unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do

@@ -106,7 +114,7 @@ unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 +

106 unifyTypes' (TypeApp t3 t4) (TypeApp t5 t6) = do

114 unifyTypes' (TypeApp t3 t4) (TypeApp t5 t6) = do

107 t3 `unifyTypes` t5

115 t3 `unifyTypes` t5

108 t4 `unifyTypes` t6

116 t4 `unifyTypes` t6

109− unifyTypes' (Skolem s1) (Skolem s2) | s1 == s2 = return ()

117+ unifyTypes' (Skolem s1 _) (Skolem s2 _) | s1 == s2 = return ()

110 unifyTypes' r1@(RCons _ _ _) r2 = unifyRows r1 r2

118 unifyTypes' r1@(RCons _ _ _) r2 = unifyRows r1 r2

111 unifyTypes' r1 r2@(RCons _ _ _) = unifyRows r1 r2

119 unifyTypes' r1 r2@(RCons _ _ _) = unifyRows r1 r2

112 unifyTypes' r1@REmpty r2 = unifyRows r1 r2

120 unifyTypes' r1@REmpty r2 = unifyRows r1 r2

@@ -143,7 +151,7 @@ unifyRows r1 r2 =

143 unifyRows' row r others u'

151 unifyRows' row r others u'

144 unifyRows' [] REmpty [] REmpty = return ()

152 unifyRows' [] REmpty [] REmpty = return ()

145 unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()

153 unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()

146− unifyRows' [] (Skolem s1) [] (Skolem s2) | s1 == s2 = return ()

154+ unifyRows' [] (Skolem s1 _) [] (Skolem s2 _) | s1 == s2 = return ()

147 unifyRows' sd3 r3 sd4 r4 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd3, r3)) ++ " with " ++ prettyPrintRow (rowFromList (sd4, r4)) ++ "."

155 unifyRows' sd3 r3 sd4 r4 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd3, r3)) ++ " with " ++ prettyPrintRow (rowFromList (sd4, r4)) ++ "."

148

156

149-- |

157-- |

@@ -171,22 +179,24 @@ typesOf moduleName vals = do

171 (ident, (val, Just (ty, checkType))) -> do

179 (ident, (val, Just (ty, checkType))) -> do

172 kind <- liftCheck $ kindOf moduleName ty

180 kind <- liftCheck $ kindOf moduleName ty

173 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

181 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

174− ty' <- replaceAllTypeSynonyms ty

182+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty

175− val' <- bindNames dict $ if checkType then check val ty' else return val

183+ val' <- bindNames dict $ if checkType

184+ then TypedValue True <$> check val ty' <*> pure ty'

185+ else return (TypedValue False val ty')

176 return (ident, (val', ty'))

186 return (ident, (val', ty'))

177 (ident, (val, Nothing)) -> do

187 (ident, (val, Nothing)) -> do

178 TypedValue _ val' ty <- bindNames dict $ infer val

188 TypedValue _ val' ty <- bindNames dict $ infer val

179 ty =?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)

189 ty =?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)

180− return (ident, (val', ty))

190+ return (ident, (TypedValue True val' ty, ty))

181 when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do

191 when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do

182 [eff, a] <- replicateM 2 fresh

192 [eff, a] <- replicateM 2 fresh

183 ty =?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a

193 ty =?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a

184 escapeCheck val ty

194 escapeCheck val ty

185 return triple

195 return triple

186− forM_ tys $ skolemEscapeCheck . snd . snd

187 forM tys $ \(ident, (val, ty)) -> do

196 forM tys $ \(ident, (val, ty)) -> do

188 val' <- replaceTypeClassDictionaries moduleName val

197 val' <- replaceTypeClassDictionaries moduleName val

198+ rethrow (("Error in " ++ show ident ++ ": \n") ++) $ skolemEscapeCheck val'

189− return (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'

199+ return $ (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'

190 , varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty))

200 , varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty))

191 where

201 where

192 tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts

202 tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts

@@ -252,7 +262,7 @@ entails moduleName context goal@(className, ty) = do

252-- and return a substitution from type variables to types which makes the type heads unify.

262-- and return a substitution from type variables to types which makes the type heads unify.

253--

263--

254typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]

264typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]

255−typeHeadsAreEqual _ _ (Skolem s1) (Skolem s2) | s1 == s2 = Just []

265+typeHeadsAreEqual _ _ (Skolem s1 _) (Skolem s2 _) | s1 == s2 = Just []

256typeHeadsAreEqual m e (TypeConstructor c1) (TypeConstructor c2) | typeConstructorsAreEqual e m c1 c2 = Just []

266typeHeadsAreEqual m e (TypeConstructor c1) (TypeConstructor c2) | typeConstructorsAreEqual e m c1 c2 = Just []

257typeHeadsAreEqual m e (TypeApp h1 (TypeVar v)) (TypeApp h2 arg) = (:) (v, arg) <$> typeHeadsAreEqual m e h1 h2

267typeHeadsAreEqual m e (TypeApp h1 (TypeVar v)) (TypeApp h2 arg) = (:) (v, arg) <$> typeHeadsAreEqual m e h1 h2

258typeHeadsAreEqual m e t1@(TypeApp _ _) t2@(TypeApp _ (TypeVar _)) = typeHeadsAreEqual m e t2 t1

268typeHeadsAreEqual m e t1@(TypeApp _ _) t2@(TypeApp _ (TypeVar _)) = typeHeadsAreEqual m e t2 t1

@@ -268,7 +278,7 @@ escapeCheck value ty = do

268 let allUnknowns = findAllTypes value

278 let allUnknowns = findAllTypes value

269 forM_ allUnknowns $ \t -> do

279 forM_ allUnknowns $ \t -> do

270 let unsolvedUnknowns = nub . unknowns $ subst $? t

280 let unsolvedUnknowns = nub . unknowns $ subst $? t

271− guardWith ("Escape check fails" ++ show (subst $? ty, subst $? t)) $ null $ unsolvedUnknowns \\ visibleUnknowns

281+ guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns

272

282

273-- |

283-- |

274-- Find all type annotations occuring inside a value

284-- Find all type annotations occuring inside a value

@@ -282,14 +292,31 @@ findAllTypes = everything (++) (mkQ [] go)

282-- |

292-- |

283-- Ensure skolem variables do not escape their scope

293-- Ensure skolem variables do not escape their scope

284--

294--

285−skolemEscapeCheck :: Type -> Check ()

295+skolemEscapeCheck :: Value -> Check ()

286−skolemEscapeCheck ty =

296+skolemEscapeCheck (TypedValue False _ _) = return ()

287− case something (mkQ Nothing findSkolems) ty of

297+skolemEscapeCheck root@(TypedValue _ _ _) =

298+ case everythingWithContext [] (++) (mkQ ((,) []) go) root of

288− Nothing -> return ()

299+ [] -> return ()

289− Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature."

300+ ((binding, val) : _) -> throwError $ "Rigid/skolem type variable bound by " ++ prettyPrintValue binding ++ " has escaped at " ++ prettyPrintValue val

290 where

301 where

291− findSkolems (Skolem _) = return ()

302+ go :: Value -> [(SkolemScope, Value)] -> ([(Value, Value)], [(SkolemScope, Value)])

292− findSkolems _ = mzero

303+ go val@(TypedValue _ _ (ForAll _ _ (Just sco))) scos = ([], (sco, val) : scos)

304+ go val@(TypedValue _ _ ty) scos = case collectSkolems ty \\ map fst scos of

305+ (sco : _) -> ([(findBindingScope sco, val)], scos)

306+ _ -> ([], scos)

307+ where

308+ collectSkolems :: Type -> [SkolemScope]

309+ collectSkolems = nub . everything (++) (mkQ [] collect)

310+ where

311+ collect (Skolem _ scope) = [scope]

312+ collect _ = []

313+ go _ scos = ([], scos)

314+ findBindingScope :: SkolemScope -> Value

315+ findBindingScope sco = fromMaybe (error "No introducing ForAll for skolem variable.") $ something (mkQ Nothing go) root

316+ where

317+ go val@(TypedValue _ _ (ForAll _ _ (Just sco'))) | sco == sco' = Just val

318+ go _ = Nothing

319+skolemEscapeCheck val = throwError $ "Untyped value passed to skolemEscapeCheck: " ++ prettyPrintValue val

293

320

294-- |

321-- |

295-- Ensure a row contains no duplicate labels

322-- Ensure a row contains no duplicate labels

@@ -326,7 +353,7 @@ replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id

326-- Replace named type variables with new unification variables

353-- Replace named type variables with new unification variables

327--

354--

328replaceAllVarsWithUnknowns :: Type -> UnifyT Type Check Type

355replaceAllVarsWithUnknowns :: Type -> UnifyT Type Check Type

329−replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns

356+replaceAllVarsWithUnknowns (ForAll ident ty _) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns

330replaceAllVarsWithUnknowns ty = return ty

357replaceAllVarsWithUnknowns ty = return ty

331

358

332-- |

359-- |

@@ -404,7 +431,8 @@ infer' (ObjectUpdate o ps) = do

404 newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps

431 newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps

405 let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals

432 let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals

406 oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh

433 oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh

407− o' <- check o $ Object $ rowFromList (oldTys, row)

434+ let oldTy = Object $ rowFromList (oldTys, row)

435+ o' <- TypedValue True <$> check o oldTy <*> pure oldTy

408 return $ TypedValue True (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)

436 return $ TypedValue True (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)

409infer' (Accessor prop val) = do

437infer' (Accessor prop val) = do

410 typed@(TypedValue _ _ objTy) <- infer val

438 typed@(TypedValue _ _ objTy) <- infer val

@@ -424,19 +452,17 @@ infer' (Abs arg ret) = do

424 return $ TypedValue True (Abs arg body) $ function ty bodyTy

452 return $ TypedValue True (Abs arg body) $ function ty bodyTy

425infer' (App f arg) = do

453infer' (App f arg) = do

426 f'@(TypedValue _ _ ft) <- infer f

454 f'@(TypedValue _ _ ft) <- infer f

427− ret <- fresh

428− app <- checkFunctionApplication f' ft arg ret

455+ (ret, app) <- checkFunctionApplication f' ft arg

429 return $ TypedValue True app ret

456 return $ TypedValue True app ret

430infer' (Var var) = do

457infer' (Var var) = do

431 Just moduleName <- checkCurrentModule <$> get

458 Just moduleName <- checkCurrentModule <$> get

432− ty <- lookupVariable moduleName var

459+ ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var

433− ty' <- replaceAllTypeSynonyms ty

434− case ty' of

460+ case ty of

435 ConstrainedType constraints _ -> do

461 ConstrainedType constraints _ -> do

436 env <- getEnv

462 env <- getEnv

437 dicts <- getTypeClassDictionaries

463 dicts <- getTypeClassDictionaries

438− return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty'

464+ return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty

439− _ -> return $ TypedValue True (Var var) ty'

465+ _ -> return $ TypedValue True (Var var) ty

440infer' (Block ss) = do

466infer' (Block ss) = do

441 ret <- fresh

467 ret <- fresh

442 (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss

468 (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss

@@ -447,7 +473,7 @@ infer' v@(Constructor c) = do

447 Just moduleName <- checkCurrentModule <$> get

473 Just moduleName <- checkCurrentModule <$> get

448 case M.lookup (qualify moduleName c) (dataConstructors env) of

474 case M.lookup (qualify moduleName c) (dataConstructors env) of

449 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

475 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

450− Just (ty, _) -> do ty' <- replaceAllTypeSynonyms ty

476+ Just (ty, _) -> do ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty

451 return $ TypedValue True v ty'

477 return $ TypedValue True v ty'

452infer' (Case vals binders) = do

478infer' (Case vals binders) = do

453 ts <- mapM infer vals

479 ts <- mapM infer vals

@@ -464,9 +490,9 @@ infer' (TypedValue checkType val ty) = do

464 Just moduleName <- checkCurrentModule <$> get

490 Just moduleName <- checkCurrentModule <$> get

465 kind <- liftCheck $ kindOf moduleName ty

491 kind <- liftCheck $ kindOf moduleName ty

466 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

492 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star

467− ty' <- replaceAllTypeSynonyms ty

493+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty

468 val' <- if checkType then check val ty' else return val

494 val' <- if checkType then check val ty' else return val

469− return $ TypedValue True val' ty

495+ return $ TypedValue True val' ty'

470infer' _ = error "Invalid argument to infer"

496infer' _ = error "Invalid argument to infer"

471

497

472-- |

498-- |

@@ -477,9 +503,9 @@ inferProperty (Object row) prop = do

477 let (props, _) = rowToList row

503 let (props, _) = rowToList row

478 return $ lookup prop props

504 return $ lookup prop props

479inferProperty (SaturatedTypeSynonym name args) prop = do

505inferProperty (SaturatedTypeSynonym name args) prop = do

480− replaced <- expandTypeSynonym name args

506+ replaced <- introduceSkolemScope <=< expandTypeSynonym name $ args

481 inferProperty replaced prop

507 inferProperty replaced prop

482−inferProperty (ForAll ident ty) prop = do

508+inferProperty (ForAll ident ty _) prop = do

483 replaced <- replaceVarWithUnknown ident ty

509 replaced <- replaceVarWithUnknown ident ty

484 inferProperty replaced prop

510 inferProperty replaced prop

485inferProperty _ _ = return Nothing

511inferProperty _ _ = return Nothing

@@ -551,7 +577,7 @@ checkBinders nvals ret ((binders, grd, val):bs) = do

551 Just moduleName <- checkCurrentModule <$> get

577 Just moduleName <- checkCurrentModule <$> get

552 m1 <- M.unions <$> zipWithM inferBinder nvals binders

578 m1 <- M.unions <$> zipWithM inferBinder nvals binders

553 r <- bindLocalVariables moduleName (M.toList m1) $ do

579 r <- bindLocalVariables moduleName (M.toList m1) $ do

554− val' <- check val ret

580+ val' <- TypedValue True <$> check val ret <*> pure ret

555 case grd of

581 case grd of

556 Nothing -> return (binders, Nothing, val')

582 Nothing -> return (binders, Nothing, val')

557 Just g -> do

583 Just g -> do

@@ -602,7 +628,7 @@ checkStatement mass ret (For ident start end inner) = do

602 return (allCodePathsReturn, mass, For ident start' end' inner')

628 return (allCodePathsReturn, mass, For ident start' end' inner')

603checkStatement mass ret (Return val) = do

629checkStatement mass ret (Return val) = do

604 val' <- check val ret

630 val' <- check val ret

605− return (True, mass, Return val')

631+ return (True, mass, Return (TypedValue True val' ret))

606

632

607-- |

633-- |

608-- Check the type of an if-then-else statement

634-- Check the type of an if-then-else statement

@@ -642,13 +668,32 @@ checkBlock mass ret (s:ss) = do

642 (b, m, ss'') <- checkBlock mass1 ret ss'

668 (b, m, ss'') <- checkBlock mass1 ret ss'

643 return (b, m, s':ss'')

669 return (b, m, s':ss'')

644

670

671+-- |

672+-- Generate a new skolem constant

673+--

674+newSkolemConstant :: UnifyT Type Check Int

675+newSkolemConstant = runUnknown <$> fresh'

676+

677+-- |

678+-- Generate a new skolem scope

679+--

680+newSkolemScope :: UnifyT Type Check SkolemScope

681+newSkolemScope = SkolemScope . runUnknown <$> fresh'

682+

645-- |

683-- |

646-- Skolemize a type variable by replacing its instances with fresh skolem constants

684-- Skolemize a type variable by replacing its instances with fresh skolem constants

647--

685--

686+skolemize :: (D.Data d) => String -> Int -> SkolemScope -> d -> d

687+skolemize ident sko scope d = replaceTypeVars ident (Skolem sko scope) d

688+

689+-- |

690+-- Introduce skolem scope at every occurence of a ForAll

691+--

648−skolemize :: String -> Type -> UnifyT Type Check Type

692+introduceSkolemScope :: Type -> UnifyT Type Check Type

649−skolemize ident ty = do

693+introduceSkolemScope = everywhereM (mkM go)

650− tsk <- Skolem . runUnknown <$> fresh'

694+ where

651− return $ replaceTypeVars ident tsk ty

695+ go (ForAll ident ty Nothing) = ForAll ident ty <$> (Just <$> newSkolemScope)

696+ go other = return other

652

697

653-- |

698-- |

654-- Check the type of a value, rethrowing errors to provide a better error message

699-- Check the type of a value, rethrowing errors to provide a better error message

@@ -668,10 +713,13 @@ check val ty = rethrow errorMessage $ check' val ty

668-- Check the type of a value

713-- Check the type of a value

669--

714--

670check' :: Value -> Type -> UnifyT Type Check Value

715check' :: Value -> Type -> UnifyT Type Check Value

671−check' val (ForAll idents ty) = do

716+check' val t@(ForAll ident ty _) = do

717+ scope <- newSkolemScope

718+ sko <- newSkolemConstant

672− sk <- skolemize idents ty

719+ let sk = skolemize ident sko scope ty

673− check val sk

720+ val' <- check val sk

721+ return $ TypedValue True val' (ForAll ident ty (Just scope))

674−check' val (ConstrainedType constraints ty) = do

722+check' val t@(ConstrainedType constraints ty) = do

675 env <- getEnv

723 env <- getEnv

676 Just moduleName <- checkCurrentModule <$> get

724 Just moduleName <- checkCurrentModule <$> get

677 dictNames <- flip mapM constraints $ \(Qualified _ (ProperName className), _) -> do

725 dictNames <- flip mapM constraints $ \(Qualified _ (ProperName className), _) -> do

@@ -681,34 +729,39 @@ check' val (ConstrainedType constraints ty) = do

681 TypeClassDictionaryInScope name className instanceTy Nothing TCDRegular) (map (Qualified Nothing) dictNames)

729 TypeClassDictionaryInScope name className instanceTy Nothing TCDRegular) (map (Qualified Nothing) dictNames)

682 (qualifyAllUnqualifiedNames moduleName env constraints)) $

730 (qualifyAllUnqualifiedNames moduleName env constraints)) $

683 check val ty

731 check val ty

684− return $ foldr Abs val' dictNames

732+ return $ TypedValue True (foldr Abs val' dictNames) t

685check' val u@(TUnknown _) = do

733check' val u@(TUnknown _) = do

686 val'@(TypedValue _ _ ty) <- infer val

734 val'@(TypedValue _ _ ty) <- infer val

687 -- Don't unify an unknown with an inferred polytype

735 -- Don't unify an unknown with an inferred polytype

688 ty' <- replaceAllVarsWithUnknowns ty

736 ty' <- replaceAllVarsWithUnknowns ty

689 ty' =?= u

737 ty' =?= u

690− return val'

738+ return $ TypedValue True val' ty'

691−check' v@(NumericLiteral _) t | t == tyNumber = return v

739+check' v@(NumericLiteral _) t | t == tyNumber =

740+ return $ TypedValue True v t

692−check' v@(StringLiteral _) t | t == tyString = return v

741+check' v@(StringLiteral _) t | t == tyString =

742+ return $ TypedValue True v t

693−check' v@(BooleanLiteral _) t | t == tyBoolean = return v

743+check' v@(BooleanLiteral _) t | t == tyBoolean =

744+ return $ TypedValue True v t

694−check' (ArrayLiteral vals) (TypeApp a ty) | a == tyArray = ArrayLiteral <$> forM vals (\val -> check val ty)

745+check' (ArrayLiteral vals) t@(TypeApp a ty) | a == tyArray = do

746+ arr <- ArrayLiteral <$> forM vals (\val -> check val ty)

747+ return $ TypedValue True arr t

695−check' (Abs arg ret) (TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do

748+check' (Abs arg ret) ty@(TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do

696 Just moduleName <- checkCurrentModule <$> get

749 Just moduleName <- checkCurrentModule <$> get

697 ret' <- bindLocalVariables moduleName [(arg, argTy)] $ check ret retTy

750 ret' <- bindLocalVariables moduleName [(arg, argTy)] $ check ret retTy

698− return $ Abs arg ret'

751+ return $ TypedValue True (Abs arg ret') ty

699check' (App f arg) ret = do

752check' (App f arg) ret = do

700 f'@(TypedValue _ _ ft) <- infer f

753 f'@(TypedValue _ _ ft) <- infer f

701− app <- checkFunctionApplication f' ft arg ret

754+ (ret', app) <- checkFunctionApplication f' ft arg

755+ subsumes Nothing ret' ret

702− return $ app

756+ return $ TypedValue True app ret

703check' v@(Var var) ty = do

757check' v@(Var var) ty = do

704 Just moduleName <- checkCurrentModule <$> get

758 Just moduleName <- checkCurrentModule <$> get

705− ty1 <- lookupVariable moduleName var

759+ repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var

706− repl <- replaceAllTypeSynonyms ty1

707− ty' <- replaceAllTypeSynonyms ty

760+ ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty

708 v' <- subsumes (Just v) repl ty'

761 v' <- subsumes (Just v) repl ty'

709 case v' of

762 case v' of

710 Nothing -> throwError "Unable to check type subsumption"

763 Nothing -> throwError "Unable to check type subsumption"

711− Just v'' -> return v''

764+ Just v'' -> return $ TypedValue True v'' ty'

712check' (TypedValue checkType val ty1) ty2 = do

765check' (TypedValue checkType val ty1) ty2 = do

713 Just moduleName <- checkCurrentModule <$> get

766 Just moduleName <- checkCurrentModule <$> get

714 kind <- liftCheck $ kindOf moduleName ty1

767 kind <- liftCheck $ kindOf moduleName ty1

@@ -718,22 +771,22 @@ check' (TypedValue checkType val ty1) ty2 = do

718 Nothing -> throwError "Unable to check type subsumption"

771 Nothing -> throwError "Unable to check type subsumption"

719 Just val'' -> do

772 Just val'' -> do

720 val''' <- if checkType then check val'' ty1 else return val''

773 val''' <- if checkType then check val'' ty1 else return val''

721− return $ TypedValue True val''' ty1

774+ return $ TypedValue checkType (TypedValue True val''' ty1) ty2

722check' (Case vals binders) ret = do

775check' (Case vals binders) ret = do

723 vals' <- mapM infer vals

776 vals' <- mapM infer vals

724 let ts = map (\(TypedValue _ _ t) -> t) vals'

777 let ts = map (\(TypedValue _ _ t) -> t) vals'

725 binders' <- checkBinders ts ret binders

778 binders' <- checkBinders ts ret binders

726− return $ Case vals' binders'

779+ return $ TypedValue True (Case vals' binders') ret

727check' (IfThenElse cond th el) ty = do

780check' (IfThenElse cond th el) ty = do

728 cond' <- check cond tyBoolean

781 cond' <- check cond tyBoolean

729 th' <- check th ty

782 th' <- check th ty

730 el' <- check el ty

783 el' <- check el ty

731− return $ IfThenElse cond' th' el'

784+ return $ TypedValue True (IfThenElse cond' th' el') ty

732−check' (ObjectLiteral ps) (Object row) = do

785+check' (ObjectLiteral ps) t@(Object row) = do

733 ensureNoDuplicateProperties ps

786 ensureNoDuplicateProperties ps

734 ps' <- checkProperties ps row False

787 ps' <- checkProperties ps row False

735− return $ ObjectLiteral ps'

788+ return $ TypedValue True (ObjectLiteral ps') t

736−check' (ObjectUpdate obj ps) (Object row) = do

789+check' (ObjectUpdate obj ps) t@(Object row) = do

737 ensureNoDuplicateProperties ps

790 ensureNoDuplicateProperties ps

738 us <- zip (map fst ps) <$> replicateM (length ps) fresh

791 us <- zip (map fst ps) <$> replicateM (length ps) fresh

739 let (propsToCheck, rest) = rowToList row

792 let (propsToCheck, rest) = rowToList row

@@ -741,27 +794,28 @@ check' (ObjectUpdate obj ps) (Object row) = do

741 remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck

794 remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck

742 obj' <- check obj (Object (rowFromList (us ++ remainingProps, rest)))

795 obj' <- check obj (Object (rowFromList (us ++ remainingProps, rest)))

743 ps' <- checkProperties ps row True

796 ps' <- checkProperties ps row True

744− return $ ObjectUpdate obj' ps'

797+ return $ TypedValue True (ObjectUpdate obj' ps') t

745check' (Accessor prop val) ty = do

798check' (Accessor prop val) ty = do

746 rest <- fresh

799 rest <- fresh

747 val' <- check val (Object (RCons prop ty rest))

800 val' <- check val (Object (RCons prop ty rest))

748− return $ Accessor prop val'

801+ return $ TypedValue True (Accessor prop val') ty

749check' (Block ss) ret = do

802check' (Block ss) ret = do

750 (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss

803 (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss

751 guardWith "Block is missing a return statement" allCodePathsReturn

804 guardWith "Block is missing a return statement" allCodePathsReturn

752− return $ Block ss'

805+ return $ TypedValue True (Block ss') ret

753check' (Constructor c) ty = do

806check' (Constructor c) ty = do

754 env <- getEnv

807 env <- getEnv

755 Just moduleName <- checkCurrentModule <$> get

808 Just moduleName <- checkCurrentModule <$> get

756 case M.lookup (qualify moduleName c) (dataConstructors env) of

809 case M.lookup (qualify moduleName c) (dataConstructors env) of

757 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

810 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"

758 Just (ty1, _) -> do

811 Just (ty1, _) -> do

759− repl <- replaceAllTypeSynonyms ty1

812+ repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1

760 _ <- subsumes Nothing repl ty

813 _ <- subsumes Nothing repl ty

761− return $ Constructor c

814+ return $ TypedValue True (Constructor c) ty

762−check' val (SaturatedTypeSynonym name args) = do

815+check' val t@(SaturatedTypeSynonym name args) = do

763− ty <- expandTypeSynonym name args

816+ ty <- introduceSkolemScope <=< expandTypeSynonym name $ args

764− check val ty

817+ val' <- check val ty

818+ return $ TypedValue True val' ty

765check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty

819check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty

766

820

767-- |

821-- |

@@ -774,7 +828,7 @@ checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where

774 go [] [] REmpty = return []

828 go [] [] REmpty = return []

775 go [] [] u@(TUnknown _) = do u =?= REmpty

829 go [] [] u@(TUnknown _) = do u =?= REmpty

776 return []

830 return []

777− go [] [] (Skolem _) | lax = return []

831+ go [] [] (Skolem _ _) | lax = return []

778 go [] ((p, _): _) _ | lax = return []

832 go [] ((p, _): _) _ | lax = return []

779 | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p

833 | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p

780 go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row

834 go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row

@@ -801,8 +855,8 @@ checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where

801-- |

855-- |

802-- Check the type of a function application, rethrowing errors to provide a better error message

856-- Check the type of a function application, rethrowing errors to provide a better error message

803--

857--

804−checkFunctionApplication :: Value -> Type -> Value -> Type -> UnifyT Type Check Value

858+checkFunctionApplication :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)

805−checkFunctionApplication fn fnTy arg ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg ret

859+checkFunctionApplication fn fnTy arg = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg

806 where

860 where

807 errorMessage msg = "Error applying function of type "

861 errorMessage msg = "Error applying function of type "

808 ++ prettyPrintType fnTy

862 ++ prettyPrintType fnTy

@@ -812,34 +866,33 @@ checkFunctionApplication fn fnTy arg ret = rethrow errorMessage $ checkFunctionA

812-- |

866-- |

813-- Check the type of a function application

867-- Check the type of a function application

814--

868--

815−checkFunctionApplication' :: Value -> Type -> Value -> Type -> UnifyT Type Check Value

869+checkFunctionApplication' :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)

816−checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do

870+checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg = do

817 tyFunction' =?= tyFunction

871 tyFunction' =?= tyFunction

818 arg' <- check arg argTy

872 arg' <- check arg argTy

819− _ <- subsumes Nothing retTy ret

820− return $ App fn arg'

873+ return (retTy, App fn arg')

821−checkFunctionApplication' fn (ForAll ident ty) arg ret = do

874+checkFunctionApplication' fn (ForAll ident ty _) arg = do

822 replaced <- replaceVarWithUnknown ident ty

875 replaced <- replaceVarWithUnknown ident ty

823− checkFunctionApplication fn replaced arg ret

876+ checkFunctionApplication fn replaced arg

824−checkFunctionApplication' fn u@(TUnknown _) arg ret = do

877+checkFunctionApplication' fn u@(TUnknown _) arg = do

825 arg' <- do

878 arg' <- do

826 TypedValue _ v t <- infer arg

879 TypedValue _ v t <- infer arg

827 TypedValue True v <$> replaceAllVarsWithUnknowns t

880 TypedValue True v <$> replaceAllVarsWithUnknowns t

828 let ty = (\(TypedValue _ _ t) -> t) arg'

881 let ty = (\(TypedValue _ _ t) -> t) arg'

882+ ret <- fresh

829 u =?= function ty ret

883 u =?= function ty ret

830− return $ App fn arg'

884+ return (ret, App fn arg')

831−checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do

885+checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg = do

832− ty <- expandTypeSynonym name tyArgs

886+ ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs

833− checkFunctionApplication fn ty arg ret

887+ checkFunctionApplication fn ty arg

834−checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do

888+checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg = do

835 env <- getEnv

889 env <- getEnv

836 dicts <- getTypeClassDictionaries

890 dicts <- getTypeClassDictionaries

837 Just moduleName <- checkCurrentModule <$> get

891 Just moduleName <- checkCurrentModule <$> get

838− checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy arg ret

892+ checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy arg

839−checkFunctionApplication' _ fnTy arg ret = throwError $ "Applying a function of type "

893+checkFunctionApplication' _ fnTy arg = throwError $ "Cannot apply a function of type "

840 ++ prettyPrintType fnTy

894 ++ prettyPrintType fnTy

841− ++ " to argument(s) " ++ prettyPrintValue arg

895+ ++ " to argument " ++ prettyPrintValue arg

842− ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."

843

896

844-- |

897-- |

845-- Check whether one type subsumes another, rethrowing errors to provide a better error message

898-- Check whether one type subsumes another, rethrowing errors to provide a better error message

@@ -857,18 +910,25 @@ subsumes val ty1 ty2 = rethrow errorMessage $ subsumes' val ty1 ty2

857-- Check whether one type subsumes another

910-- Check whether one type subsumes another

858--

911--

859subsumes' :: Maybe Value -> Type -> Type -> UnifyT Type Check (Maybe Value)

912subsumes' :: Maybe Value -> Type -> Type -> UnifyT Type Check (Maybe Value)

860−subsumes' val (ForAll ident ty1) ty2 = do

913+subsumes' val (ForAll ident ty1 _) ty2 = do

861 replaced <- replaceVarWithUnknown ident ty1

914 replaced <- replaceVarWithUnknown ident ty1

862 subsumes val replaced ty2

915 subsumes val replaced ty2

916+subsumes' val ty1 (ForAll ident ty2 sco) =

917+ case sco of

918+ Just sco' -> do

919+ sko <- newSkolemConstant

920+ let sk = skolemize ident sko sco' ty2

921+ subsumes val ty1 sk

922+ Nothing -> throwError "Skolem variable scope is unspecified"

863subsumes' val (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do

923subsumes' val (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do

864 subsumes Nothing arg2 arg1

924 subsumes Nothing arg2 arg1

865 subsumes Nothing ret1 ret2

925 subsumes Nothing ret1 ret2

866 return val

926 return val

867subsumes' val (SaturatedTypeSynonym name tyArgs) ty2 = do

927subsumes' val (SaturatedTypeSynonym name tyArgs) ty2 = do

868− ty1 <- expandTypeSynonym name tyArgs

928+ ty1 <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs

869 subsumes val ty1 ty2

929 subsumes val ty1 ty2

870subsumes' val ty1 (SaturatedTypeSynonym name tyArgs) = do

930subsumes' val ty1 (SaturatedTypeSynonym name tyArgs) = do

871− ty2 <- expandTypeSynonym name tyArgs

931+ ty2 <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs

872 subsumes val ty1 ty2

932 subsumes val ty1 ty2

873subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do

933subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do

874 env <- getEnv

934 env <- getEnv

src/Language/PureScript/Types.hs+10−5

@@ -24,6 +24,11 @@ import Control.Monad.Unify

25import Language.PureScript.Names

27+-- |

28+-- An identifier for the scope of a skolem variable

29+--

30+newtype SkolemScope = SkolemScope { runSkolemScope :: Int } deriving (Show, Eq, Ord, Data, Typeable)

31+

27-- |

32-- |

28-- The type of types

33-- The type of types

29--

34--

@@ -55,7 +60,7 @@ data Type

55 -- |

60 -- |

56 -- Forall quantifier

61 -- Forall quantifier

57 --

62 --

58− | ForAll String Type

63+ | ForAll String Type (Maybe SkolemScope)

59 -- |

64 -- |

60 -- A type with a set of type class constraints

65 -- A type with a set of type class constraints

61 --

66 --

@@ -63,7 +68,7 @@ data Type

63 -- |

68 -- |

64 -- A skolem constant

69 -- A skolem constant

65 --

70 --

66− | Skolem Int

71+ | Skolem Int SkolemScope

67 -- |

72 -- |

68 -- An empty row

73 -- An empty row

69 --

74 --

@@ -128,14 +133,14 @@ rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))

128-- Check whether a type is a monotype

133-- Check whether a type is a monotype

129--

134--

130isMonoType :: Type -> Bool

135isMonoType :: Type -> Bool

131−isMonoType (ForAll _ _) = False

136+isMonoType (ForAll _ _ _) = False

132isMonoType ty = True

137isMonoType ty = True

133

138

134-- |

139-- |

135-- Universally quantify a type

140-- Universally quantify a type

136--

141--

137mkForAll :: [String] -> Type -> Type

142mkForAll :: [String] -> Type -> Type

138−mkForAll = flip . foldl . flip $ ForAll

143+mkForAll args ty = foldl (\t arg -> ForAll arg t Nothing) ty args

139

144

140-- |

145-- |

141-- The empty record type

146-- The empty record type

@@ -151,5 +156,5 @@ replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replaceTypeVa

151 where

156 where

152 replaceTypeVar (TypeVar v) | v == name = t

157 replaceTypeVar (TypeVar v) | v == name = t

153 replaceTypeVar other = other

158 replaceTypeVar other = other

154− isShadowed (ForAll v _) | v == name = True

159+ isShadowed (ForAll v _ _) | v == name = True

155 isShadowed _ = False

160 isShadowed _ = False