d59db66 · rowtype-yoga/purescript-native

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

Use monad-unify package

commitd59db662e9cab6001850e71cbd86a53c389d3225 authorPhil Freeman <paf31@cantab.net> dateWed 29 Jan 2014, 23:10 (13 years ago) parent96f7566

10 files changed+161−307

compare with golang

unifiedsplit

purescript.cabal+2−3 src/Language/PureScript.hs+4−1 src/Language/PureScript/Kinds.hs+3−2 src/Language/PureScript/Pretty/Kinds.hs+2−2 src/Language/PureScript/Pretty/Types.hs+3−3 src/Language/PureScript/TypeChecker/Kinds.hs+32−37 src/Language/PureScript/TypeChecker/Monad.hs+17−119 src/Language/PureScript/TypeChecker/Types.hs+95−110 src/Language/PureScript/Types.hs+3−2 src/Language/PureScript/Unknown.hs−28

purescript.cabal+2−3

@@ -1,5 +1,5 @@

11name: purescript

2−version: 0.3.5

2+version: 0.3.6

33cabal-version: >=1.8

44build-type: Simple

55license: MIT

@@ -17,7 +17,7 @@ data-dir: ""

1717library

1818 build-depends: base >=4 && <5, cmdtheline -any, containers -any,

1919 directory -any, filepath -any, mtl -any, parsec -any, syb -any,

20− transformers -any, utf8-string -any, pattern-arrows -any

20+ transformers -any, utf8-string -any, pattern-arrows -any, monad-unify -any

2121 exposed-modules: Data.Generics.Extras

2222 Language.PureScript

2323 Language.PureScript.Options

@@ -25,7 +25,6 @@ library

2525 Language.PureScript.Kinds

2626 Language.PureScript.Names

2727 Language.PureScript.Types

28− Language.PureScript.Unknown

2928 Language.PureScript.Values

3029 Language.PureScript.Scope

3130 Language.PureScript.Sugar

src/Language/PureScript.hs+4−1

@@ -30,6 +30,7 @@ import Language.PureScript.ModuleDependencies as P

3030

3131import Data.List (intercalate)

3232import Control.Monad (when, forM)

33+import Control.Monad.State.Lazy

3334import Control.Applicative ((<$>))

3435import qualified Data.Map as M

3536

@@ -54,7 +55,9 @@ compile :: Options -> [Module] -> Either String (String, String, Environment)

5455compile opts ms = do

5556 sorted <- sortModules ms

5657 desugared <- desugar sorted

57− (elaborated, env) <- runCheck $ forM desugared $ \(Module moduleName decls) -> Module moduleName <$> typeCheckAll (ModuleName moduleName) decls

58+ (elaborated, env) <- runCheck $ forM desugared $ \(Module moduleName decls) -> do

59+ modify (\s -> s { checkCurrentModule = Just (ModuleName moduleName) })

60+ Module moduleName <$> typeCheckAll (ModuleName moduleName) decls

5861 regrouped <- createBindingGroupsModule . collapseBindingGroupsModule $ elaborated

5962 let js = concatMap (flip (moduleToJs opts) env) $ regrouped

6063 let exts = intercalate "\n" . map (flip moduleToPs env) $ regrouped

src/Language/PureScript/Kinds.hs+3−2

@@ -17,7 +17,8 @@

1717module Language.PureScript.Kinds where

1818

1919import Data.Data

20−import Language.PureScript.Unknown

20+

21+import Control.Monad.Unify (TypedUnknown(..))

2122

2223-- |

2324-- The data type of kinds

@@ -26,7 +27,7 @@ data Kind

2627 -- |

2728 -- Unification variable of type Kind

2829 --

29− = KUnknown (Unknown Kind)

30+ = KUnknown (TypedUnknown Kind)

3031 -- |

3132 -- The kind of types

3233 --

src/Language/PureScript/Pretty/Kinds.hs+2−2

@@ -21,17 +21,17 @@ import Data.Maybe (fromMaybe)

2121

2222import Control.Arrow (ArrowPlus(..))

2323import Control.PatternArrows

24+import Control.Monad.Unify

2425

2526import Language.PureScript.Kinds

2627import Language.PureScript.Pretty.Common

27−import Language.PureScript.Unknown

2828

2929typeLiterals :: Pattern () Kind String

3030typeLiterals = mkPattern match

3131 where

3232 match Star = Just "*"

3333 match Bang = Just "!"

34− match (KUnknown (Unknown u)) = Just $ 'u' : show u

34+ match (KUnknown (TypedUnknown (Unknown u))) = Just $ 'u' : show u

3535 match _ = Nothing

3636

3737matchRow :: Pattern () Kind ((), Kind)

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

@@ -23,10 +23,10 @@ import Data.List (intercalate)

2323

2424import Control.Arrow ((<+>))

2525import Control.PatternArrows

26+import Control.Monad.Unify

2627

2728import Language.PureScript.Types

2829import Language.PureScript.Pretty.Common

29−import Language.PureScript.Unknown

3030

3131typeLiterals :: Pattern () Type String

3232typeLiterals = mkPattern match

@@ -38,7 +38,7 @@ typeLiterals = mkPattern match

3838 match (Object row) = Just $ "{ " ++ prettyPrintType row ++ " }"

3939 match (TypeVar var) = Just var

4040 match (TypeConstructor ctor) = Just $ show ctor

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

41+ match (TUnknown (TypedUnknown (Unknown u))) = Just $ 'u' : show u

4242 match (Skolem s) = Just $ 's' : show s

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

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

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

5757 nameAndTypeToPs name ty = name ++ " :: " ++ prettyPrintType ty

5858 tailToPs :: Type -> String

5959 tailToPs REmpty = ""

60− tailToPs (TUnknown (Unknown u)) = " | u" ++ show u

60+ tailToPs (TUnknown (TypedUnknown (Unknown u))) = " | u" ++ show u

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

6262 tailToPs (Skolem s) = " | s" ++ show s

6363 tailToPs _ = error "Invalid row tail"

src/Language/PureScript/TypeChecker/Kinds.hs+32−37

@@ -15,6 +15,7 @@

1515

1616{-# OPTIONS_GHC -fno-warn-orphans #-}

1717{-# LANGUAGE DeriveDataTypeable #-}

18+{-# LANGUAGE MultiParamTypeClasses #-}

1819

1920module Language.PureScript.TypeChecker.Kinds (

2021 kindOf,

@@ -27,48 +28,42 @@ import Language.PureScript.Kinds

2728import Language.PureScript.Names

2829import Language.PureScript.TypeChecker.Monad

2930import Language.PureScript.Pretty

30−import Language.PureScript.Unknown

3131

3232import Control.Monad.State

3333import Control.Monad.Error

3434import Control.Monad.Reader

35+import Control.Monad.Unify

3536

3637import Control.Applicative

3738

3839import qualified Data.Map as M

3940

40−instance Unifiable Kind where

41+instance Unifiable Check Kind where

4142 unknown = KUnknown

4243 isUnknown (KUnknown u) = Just u

4344 isUnknown _ = Nothing

44− KUnknown u1 ~~ KUnknown u2 | u1 == u2 = return ()

45− KUnknown u ~~ k = replace u k

46− k ~~ KUnknown u = replace u k

47− Star ~~ Star = return ()

48− Bang ~~ Bang = return ()

49− Row k1 ~~ Row k2 = k1 ~~ k2

50− FunKind k1 k2 ~~ FunKind k3 k4 = do

51− k1 ~~ k3

52− k2 ~~ k4

53− k1 ~~ k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."

54− apply s (KUnknown u) = runSubstitution s u

55− apply s (FunKind k1 k2) = FunKind (apply s k1) (apply s k2)

56− apply _ k = k

57− unknowns (KUnknown (Unknown u)) = [u]

58− unknowns (FunKind k1 k2) = unknowns k1 ++ unknowns k2

59− unknowns _ = []

45+ KUnknown u1 ?= KUnknown u2 | u1 == u2 = return ()

46+ KUnknown u ?= k = replace u k

47+ k ?= KUnknown u = replace u k

48+ Star ?= Star = return ()

49+ Bang ?= Bang = return ()

50+ Row k1 ?= Row k2 = k1 ?= k2

51+ FunKind k1 k2 ?= FunKind k3 k4 = do

52+ k1 ?= k3

53+ k2 ?= k4

54+ k1 ?= k2 = UnifyT . lift . throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."

6055

6156-- |

6257-- Infer the kind of a single type

6358--

6459kindOf :: ModuleName -> Type -> Check Kind

65−kindOf moduleName ty = fmap (\(k, s) -> apply s k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer ty

60+kindOf moduleName ty = liftUnify $ starIfUnknown <$> infer ty

6661

6762-- |

6863-- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors

6964--

7065kindsOf :: ModuleName -> ProperName -> [String] -> [Type] -> Check Kind

71−kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, s) -> apply s k)) . runSubst (SubstContext moduleName) $ do

66+kindsOf moduleName name args ts = fmap starIfUnknown . liftUnify $ do

7267 tyCon <- fresh

7368 kargs <- replicateM (length args) fresh

7469 let dict = (name, tyCon) : zip (map ProperName args) kargs

@@ -79,7 +74,7 @@ kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, s) -> apply s k))

7974-- Simultaneously infer the kinds of several mutually recursive type constructors

8075--

8176kindsOfAll :: ModuleName -> [(ProperName, [String], Type)] -> [(ProperName, [String], [Type])] -> Check ([Kind], [Kind])

82−kindsOfAll moduleName syns tys = fmap tidyUp . runSubst (SubstContext moduleName) $ do

77+kindsOfAll moduleName syns tys = fmap tidyUp . liftUnify $ do

8378 synVars <- replicateM (length syns) fresh

8479 let dict = zipWith (\(name, _, _) var -> (name, var)) syns synVars

8580 bindLocalTypeVariables moduleName dict $ do

@@ -98,16 +93,16 @@ kindsOfAll moduleName syns tys = fmap tidyUp . runSubst (SubstContext moduleName

9893 solveTypes [ty] kargs synVar) synVars syns

9994 return (syn_ks, data_ks)

10095 where

101− tidyUp ((ks1, ks2), s) = (map starIfUnknown $ apply s ks1, map starIfUnknown $ apply s ks2)

96+ tidyUp (ks1, ks2) = (map starIfUnknown ks1, map starIfUnknown ks2)

10297

10398-- |

10499-- Solve the set of kind constraints associated with the data constructors for a type constructor

105100--

106−solveTypes :: [Type] -> [Kind] -> Kind -> Subst Kind

101+solveTypes :: [Type] -> [Kind] -> Kind -> UnifyT Check Kind

107102solveTypes ts kargs tyCon = do

108103 ks <- mapM infer ts

109− tyCon ~~ foldr FunKind Star kargs

110− forM_ ks $ \k -> k ~~ Star

104+ tyCon ?= foldr FunKind Star kargs

105+ forM_ ks $ \k -> k ?= Star

111106 return tyCon

112107

113108-- |

@@ -121,39 +116,39 @@ starIfUnknown k = k

121116-- |

122117-- Infer a kind for a type

123118--

124−infer :: Type -> Subst Kind

119+infer :: Type -> UnifyT Check Kind

125120infer Number = return Star

126121infer String = return Star

127122infer Boolean = return Star

128123infer Array = return $ FunKind Star Star

129124infer (Object row) = do

130125 k <- infer row

131− k ~~ Row Star

126+ k ?= Row Star

132127 return Star

133128infer (Function args ret) = do

134129 ks <- mapM infer args

135130 k <- infer ret

136− k ~~ Star

137− forM_ ks (~~ Star)

131+ k ?= Star

132+ forM_ ks (?= Star)

138133 return Star

139134infer (TypeVar v) = do

140− moduleName <- substCurrentModule <$> ask

141− lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

135+ Just moduleName <- checkCurrentModule <$> get

136+ UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

142137infer (TypeConstructor v) = do

143138 env <- liftCheck getEnv

144− moduleName <- substCurrentModule `fmap` ask

139+ Just moduleName <- checkCurrentModule <$> get

145140 case M.lookup (qualify moduleName v) (types env) of

146− Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"

141+ Nothing -> UnifyT . lift . throwError $ "Unknown type constructor '" ++ show v ++ "'"

147142 Just (kind, _) -> return kind

148143infer (TypeApp t1 t2) = do

149144 k0 <- fresh

150145 k1 <- infer t1

151146 k2 <- infer t2

152− k1 ~~ FunKind k2 k0

147+ k1 ?= FunKind k2 k0

153148 return k0

154149infer (ForAll ident ty) = do

155150 k <- fresh

156− moduleName <- substCurrentModule <$> ask

151+ Just moduleName <- checkCurrentModule <$> get

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

158153infer REmpty = do

159154 k <- fresh

@@ -161,11 +156,11 @@ infer REmpty = do

161156infer (RCons _ ty row) = do

162157 k1 <- infer ty

163158 k2 <- infer row

164− k2 ~~ Row k1

159+ k2 ?= Row k1

165160 return $ Row k1

166161infer (ConstrainedType deps ty) = do

167162 mapM_ (infer . snd) deps

168163 k <- infer ty

169− k ~~ Star

164+ k ?= Star

170165 return Star

171166infer _ = error "Invalid argument to infer"

src/Language/PureScript/TypeChecker/Monad.hs+17−119

@@ -22,7 +22,6 @@ import Language.PureScript.Types

2222import Language.PureScript.Kinds

2323import Language.PureScript.Values

2424import Language.PureScript.Names

25−import Language.PureScript.Unknown

2625import Language.PureScript.Declarations

2726

2827import Data.Data

@@ -34,6 +33,7 @@ import Control.Applicative

3433import Control.Monad.State

3534import Control.Monad.Error

3635import Control.Monad.Reader

36+import Control.Monad.Unify

3737import Control.Arrow ((***))

3838

3939import qualified Data.Map as M

@@ -227,6 +227,10 @@ data CheckState = CheckState {

227227 -- The next type class dictionary name

228228 --

229229 , checkNextDictName :: Int

230+ -- |

231+ -- The current module

232+ --

233+ , checkCurrentModule :: Maybe ModuleName

230234 }

231235

232236-- |

@@ -258,7 +262,7 @@ modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })

258262--

259263runCheck :: Check a -> Either String (a, Environment)

260264runCheck c = do

261− (a, s) <- flip runStateT (CheckState emptyEnvironment 0 0) $ unCheck c

265+ (a, s) <- flip runStateT (CheckState emptyEnvironment 0 0 Nothing) $ unCheck c

262266 return (a, checkEnv s)

263267

264268-- |

@@ -283,130 +287,24 @@ freshDictionaryName = do

283287 modify $ \s -> s { checkNextDictName = succ (checkNextDictName s) }

284288 return n

285289

286−-- |

287−-- A substitution maintains a mapping from unification variables to their values, ensuring that

288−-- the type of a unification variable matches the type of its value.

289−--

290−newtype Substitution = Substitution { runSubstitution :: forall t. (Unifiable t) => Unknown t -> t }

291−

292−instance Monoid Substitution where

293− mempty = Substitution unknown

294− s1 `mappend` s2 = Substitution $ \u -> apply s1 (apply s2 (unknown u))

295−

296−-- |

297−-- State for the substitution monad, which contains the current substitution

298−--

299−data SubstState = SubstState { substSubst :: Substitution }

300−

301−-- |

302−-- Configuration for the substitution monad, constaining the current module

303−--

304−newtype SubstContext = SubstContext { substCurrentModule :: ModuleName } deriving (Show)

305−

306−-- |

307−-- The substitution monad, which provides the means to unify values to generate a substitution, in addition to

308−-- the actions supported by the type checking monad @Check@.

309−--

310−newtype Subst a = Subst { unSubst :: ReaderT SubstContext (StateT SubstState Check) a }

311− deriving (Functor, Monad, Applicative, MonadPlus, MonadReader SubstContext)

312−

313−instance MonadState CheckState Subst where

314− get = Subst . lift . lift $ get

315− put = Subst . lift . lift . put

316−

317−deriving instance MonadError String Subst

318−

319290-- |

320291-- Lift a computation in the @Check@ monad into the substitution monad.

321292--

322−liftCheck :: Check a -> Subst a

323−liftCheck = Subst . lift . lift

324−

325−-- |

326−-- Get the current substitution monad state

327−--

328−getSubstState :: Subst SubstState

329−getSubstState = Subst . lift $ get

293+liftCheck :: Check a -> UnifyT Check a

294+liftCheck = UnifyT . lift . lift

330295

331296-- |

332297-- Run a computation in the substitution monad, generating a return value and the final substitution.

333298--

334−runSubst :: SubstContext -> Subst a -> Check (a, Substitution)

335−runSubst context subst = do

336− (a, s) <- flip runStateT (SubstState mempty) . flip runReaderT context . unSubst $ subst

337− return (a, substSubst s)

338−

339−-- |

340−-- Generate a substitution from a substitution function for a single type

341−--

342−substituteWith :: (Typeable t) => (Unknown t -> t) -> Substitution

343−substituteWith f = Substitution $ \u -> fromMaybe (unknown u) $ do

344− u1 <- cast u

345− cast (f u1)

346−

347−-- |

348−-- Substitute a single unification variable

349−--

350−substituteOne :: (Unifiable t) => Unknown t -> t -> Substitution

351−substituteOne u t = substituteWith $ \u1 ->

352− case u1 of

353− u2 | u2 == u -> t

354− | otherwise -> unknown u2

355−

356−-- |

357−-- Replace a unification variable with the specified value in the current substitution

358−--

359−replace :: (Unifiable t) => Unknown t -> t -> Subst ()

360−replace u t' = do

361− sub <- substSubst <$> Subst get

362− let t = apply sub t'

363− occursCheck u t

364− let current = apply sub $ unknown u

365− case isUnknown current of

366− Just u1 | u1 == u -> return ()

367− _ -> current ~~ t

368− Subst . modify $ \s -> s { substSubst = substituteOne u t <> substSubst s }

369−

370−-- |

371−-- Identifies types which support unification

372−--

373−class (Typeable t, Data t, Show t) => Unifiable t where

374− unknown :: Unknown t -> t

375− (~~) :: t -> t -> Subst ()

376− isUnknown :: t -> Maybe (Unknown t)

377− apply :: Substitution -> t -> t

378− unknowns :: t -> [Int]

379−

380−instance (Unifiable a) => Unifiable [a] where

381− unknown _ = error "not supported"

382− (~~) = zipWithM_ (~~)

383− isUnknown _ = error "not supported"

384− apply s = map (apply s)

385− unknowns = concatMap unknowns

386−

387−-- |

388−-- Perform the occurs check, to make sure a unification variable does not occur inside a value

389−--

390−occursCheck :: (Unifiable t) => Unknown s -> t -> Subst ()

391−occursCheck (Unknown u) t =

392− case isUnknown t of

393− Nothing -> guardWith "Occurs check fails" (u `notElem` unknowns t)

394− _ -> return ()

395−

396−-- |

397−-- Generate a fresh untyped unification variable

398−--

399−fresh' :: Subst Int

400−fresh' = do

401− n <- checkNextVar <$> get

402− modify $ \s -> s { checkNextVar = succ (checkNextVar s) }

403− return n

404−

405−-- |

406−-- Generate a fresh unification variable at a specific type

407−--

408−fresh :: (Unifiable t) => Subst t

409−fresh = unknown . Unknown <$> fresh'

299+liftUnify :: (Data a) => UnifyT Check a -> Check a

300+liftUnify unify = do

301+ st <- get

302+ e <- runUnify (defaultUnifyState { unifyNextVar = checkNextVar st }) unify

303+ case e of

304+ Left err -> throwError err

305+ Right (a, ust) -> do

306+ modify $ \st -> st { checkNextVar = unifyNextVar ust }

307+ return $ runSubstitution (unifyCurrentSubstitution ust) a

410308

411309-- |

412310-- Replace any unqualified names in a type wit their qualified versionss

src/Language/PureScript/TypeChecker/Types.hs+95−110

@@ -14,7 +14,9 @@

1414-----------------------------------------------------------------------------

1515

1616{-# OPTIONS_GHC -fno-warn-orphans #-}

17−{-# LANGUAGE DeriveDataTypeable, FlexibleContexts #-}

17+{-# LANGUAGE DeriveDataTypeable #-}

18+{-# LANGUAGE FlexibleContexts #-}

19+{-# LANGUAGE MultiParamTypeClasses #-}

1820

1921module Language.PureScript.TypeChecker.Types (

2022 typesOf

@@ -53,11 +55,11 @@ import Language.PureScript.TypeChecker.Monad

5355import Language.PureScript.TypeChecker.Kinds

5456import Language.PureScript.TypeChecker.Synonyms

5557import Language.PureScript.Pretty

56−import Language.PureScript.Unknown

5758

5859import Control.Monad.State

5960import Control.Monad.Error

6061import Control.Monad.Reader

62+import Control.Monad.Unify

6163

6264import Control.Applicative

6365import Control.Arrow (Arrow(..))

@@ -65,32 +67,16 @@ import Control.Arrow (Arrow(..))

6567import qualified Data.Map as M

6668import Data.Function (on)

6769

68−instance Unifiable Type where

70+instance Unifiable Check Type where

6971 unknown = TUnknown

7072 isUnknown (TUnknown u) = Just u

7173 isUnknown _ = Nothing

72− (~~) = unifyTypes

73− apply s (TUnknown u) = runSubstitution s u

74− apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys

75− apply s (ForAll idents ty) = ForAll idents $ apply s ty

76− apply s (Object r) = Object (apply s r)

77− apply s (Function args ret) = Function (map (apply s) args) (apply s ret)

78− apply s (TypeApp t1 t2) = TypeApp (apply s t1) (apply s t2)

79− apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)

80− apply _ t = t

81− unknowns (TUnknown (Unknown u)) = [u]

82− unknowns (SaturatedTypeSynonym _ tys) = concatMap unknowns tys

83− unknowns (ForAll _ ty) = unknowns ty

84− unknowns (Object r) = unknowns r

85− unknowns (Function args ret) = concatMap unknowns args ++ unknowns ret

86− unknowns (TypeApp t1 t2) = unknowns t1 ++ unknowns t2

87− unknowns (RCons _ ty r) = unknowns ty ++ unknowns r

88− unknowns _ = []

74+ (?=) = unifyTypes

8975

9076-- |

9177-- Unify two types, updating the current substitution

9278--

93−unifyTypes :: Type -> Type -> Subst ()

79+unifyTypes :: Type -> Type -> UnifyT Check ()

9480unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 ++ " with type " ++ prettyPrintType t2 ++ ":\n" ++ e) $ do

9581 unifyTypes' t1 t2

9682 where

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

11399 unifyTypes' String String = return ()

114100 unifyTypes' Boolean Boolean = return ()

115101 unifyTypes' Array Array = return ()

116− unifyTypes' (Object row1) (Object row2) = row1 ~~ row2

102+ unifyTypes' (Object row1) (Object row2) = row1 ?= row2

117103 unifyTypes' (Function args1 ret1) (Function args2 ret2) = do

118104 guardWith "Function applied to incorrect number of args" $ length args1 == length args2

119105 zipWithM_ unifyTypes args1 args2

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

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

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

123109 env <- getEnv

124− moduleName <- substCurrentModule `fmap` ask

110+ Just moduleName <- checkCurrentModule <$> get

125111 guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (typeConstructorsAreEqual env moduleName c1 c2)

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

127113 t3 `unifyTypes` t5

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

140126-- trailing row unification variable, if appropriate, otherwise leftover labels result in a unification

141127-- error.

142128--

143−unifyRows :: Type -> Type -> Subst ()

129+unifyRows :: Type -> Type -> UnifyT Check ()

144130unifyRows r1 r2 =

145131 let

146132 (s1, r1') = rowToList r1

@@ -149,17 +135,17 @@ unifyRows r1 r2 =

149135 sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]

150136 sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]

151137 in do

152− forM_ int (uncurry (~~))

138+ forM_ int (uncurry (?=))

153139 unifyRows' sd1 r1' sd2 r2'

154140 where

155− unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Subst ()

141+ unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> UnifyT Check ()

156142 unifyRows' [] (TUnknown u) sd r = replace u (rowFromList (sd, r))

157143 unifyRows' sd r [] (TUnknown u) = replace u (rowFromList (sd, r))

158144 unifyRows' ((name, ty):row) r others u@(TUnknown un) = do

159145 occursCheck un ty

160146 forM_ row $ \(_, t) -> occursCheck un t

161147 u' <- fresh

162− u ~~ RCons name ty u'

148+ u ?= RCons name ty u'

163149 unifyRows' row r others u'

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

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

@@ -178,8 +164,7 @@ typeConstructorsAreEqual env moduleName = (==) `on` canonicalizeType moduleName

178164--

179165typesOf :: ModuleName -> [(Ident, Value)] -> Check [(Ident, (Value, Type))]

180166typesOf moduleName vals = do

181− tys <- fmap (\(tys, s) -> map (\(ident, (val, ty)) -> (ident, (overTypes (apply s) val, apply s ty))) tys)

182− . runSubst (SubstContext moduleName) $ do

167+ tys <- liftUnify $ do

183168 let es = map isTyped vals

184169 typed = filter (isJust . snd . snd) es

185170 untyped = filter (isNothing . snd . snd) es

@@ -197,11 +182,11 @@ typesOf moduleName vals = do

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

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

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

200− ty ~~ fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)

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

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

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

203188 [eff, a] <- replicateM 2 fresh

204− ty ~~ TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a

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

205190 escapeCheck val ty

206191 return triple

207192 forM_ tys $ skolemEscapeCheck . snd . snd

@@ -279,14 +264,14 @@ typeHeadsAreEqual _ _ _ _ = Nothing

279264-- |

280265-- Ensure unsolved unification variables do not escape

281266--

282−escapeCheck :: Value -> Type -> Subst ()

267+escapeCheck :: Value -> Type -> UnifyT Check ()

283268escapeCheck value ty = do

284− subst <- substSubst <$> getSubstState

285− let visibleUnknowns = nub $ unknowns $ apply subst ty

269+ subst <- unifyCurrentSubstitution <$> UnifyT get

270+ let visibleUnknowns = nub $ unknowns $ runSubstitution subst ty

286271 let allUnknowns = findAllTypes value

287272 forM_ allUnknowns $ \t -> do

288− let unsolvedUnknowns = nub . unknowns $ apply subst t

289− guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns

273+ let unsolvedUnknowns = nub . unknowns $ runSubstitution subst t

274+ guardWith ("Escape check fails" ++ show ( runSubstitution subst ty, runSubstitution subst t)) $ null $ unsolvedUnknowns \\ visibleUnknowns

290275

291276-- |

292277-- Find all type annotations occuring inside a value

@@ -304,7 +289,7 @@ skolemEscapeCheck :: Type -> Check ()

304289skolemEscapeCheck ty =

305290 case something (mkQ Nothing findSkolems) ty of

306291 Nothing -> return ()

307− Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature." ++ show ty

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

308293 where

309294 findSkolems (Skolem _) = return ()

310295 findSkolems _ = mzero

@@ -330,9 +315,9 @@ varIfUnknown ty =

330315 toName = (:) 't' . show

331316 ty' = everywhere (mkT typeToVar) $ ty

332317 typeToVar :: Type -> Type

333− typeToVar (TUnknown (Unknown u)) = TypeVar (toName u)

318+ typeToVar (TUnknown (TypedUnknown (Unknown u))) = TypeVar (toName u)

334319 typeToVar t = t

335− in mkForAll (sort . map toName $ unks) ty'

320+ in mkForAll (sort . map (toName . runUnknown) $ unks) ty'

336321

337322-- |

338323-- Replace named type variables with types

@@ -343,14 +328,14 @@ replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id

343328-- |

344329-- Replace named type variables with new unification variables

345330--

346−replaceAllVarsWithUnknowns :: Type -> Subst Type

331+replaceAllVarsWithUnknowns :: Type -> UnifyT Check Type

347332replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns

348333replaceAllVarsWithUnknowns ty = return ty

349334

350335-- |

351336-- Replace a single type variable with a new unification variable

352337--

353−replaceVarWithUnknown :: String -> Type -> Subst Type

338+replaceVarWithUnknown :: String -> Type -> UnifyT Check Type

354339replaceVarWithUnknown ident ty = do

355340 tu <- fresh

356341 return $ replaceTypeVars ident tu $ ty

@@ -359,10 +344,10 @@ replaceVarWithUnknown ident ty = do

359344-- Replace fully applied type synonyms with the @SaturatedTypeSynonym@ data constructor, which helps generate

360345-- better error messages during unification.

361346--

362−replaceAllTypeSynonyms :: (Functor m, MonadState CheckState m, MonadReader SubstContext m, MonadError String m) => (D.Data d) => d -> m d

347+replaceAllTypeSynonyms :: (Functor m, MonadState CheckState m, MonadError String m) => (D.Data d) => d -> m d

363348replaceAllTypeSynonyms d = do

364349 env <- getEnv

365− moduleName <- substCurrentModule <$> ask

350+ Just moduleName <- checkCurrentModule <$> get

366351 let syns = map (\((path, name), (args, _)) -> ((path, name), length args)) . M.toList $ typeSynonyms env

367352 either throwError return $ saturateAllTypeSynonyms env moduleName syns d

368353

@@ -378,10 +363,10 @@ desaturateAllTypeSynonyms = everywhere (mkT replaceSaturatedTypeSynonym)

378363-- |

379364-- Replace a type synonym and its arguments with the aliased type

380365--

381−expandTypeSynonym :: Qualified ProperName -> [Type] -> Subst Type

366+expandTypeSynonym :: Qualified ProperName -> [Type] -> UnifyT Check Type

382367expandTypeSynonym name args = do

383368 env <- getEnv

384− moduleName <- substCurrentModule `fmap` ask

369+ Just moduleName <- checkCurrentModule <$> get

385370 case M.lookup (canonicalizeType moduleName env name) (typeSynonyms env) of

386371 Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body

387372 Nothing -> error "Type synonym was not defined"

@@ -395,20 +380,20 @@ ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (

395380-- |

396381-- Infer a type for a value, rethrowing any error to provide a more useful error message

397382--

398−infer :: Value -> Subst Value

383+infer :: Value -> UnifyT Check Value

399384infer val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ infer' val

400385

401386-- |

402387-- Infer a type for a value

403388--

404−infer' :: Value -> Subst Value

389+infer' :: Value -> UnifyT Check Value

405390infer' v@(NumericLiteral _) = return $ TypedValue True v Number

406391infer' v@(StringLiteral _) = return $ TypedValue True v String

407392infer' v@(BooleanLiteral _) = return $ TypedValue True v Boolean

408393infer' (ArrayLiteral vals) = do

409394 ts <- mapM infer vals

410395 els <- fresh

411− forM_ ts $ \(TypedValue _ _ t) -> els ~~ TypeApp Array t

396+ forM_ ts $ \(TypedValue _ _ t) -> els ?= TypeApp Array t

412397 return $ TypedValue True (ArrayLiteral ts) els

413398infer' (Unary op val) = do

414399 v <- infer val

@@ -448,7 +433,7 @@ infer' (Accessor prop val) = do

448433 Just ty -> return $ TypedValue True (Accessor prop typed) ty

449434infer' (Abs args ret) = do

450435 ts <- replicateM (length args) fresh

451− moduleName <- substCurrentModule <$> ask

436+ Just moduleName <- checkCurrentModule <$> get

452437 bindLocalVariables moduleName (zip args ts) $ do

453438 body@(TypedValue _ _ bodyTy) <- infer' ret

454439 return $ TypedValue True (Abs args body) $ Function ts bodyTy

@@ -458,7 +443,7 @@ infer' (App f args) = do

458443 app <- checkFunctionApplication f' ft args ret

459444 return $ TypedValue True app ret

460445infer' (Var var) = do

461− moduleName <- substCurrentModule <$> ask

446+ Just moduleName <- checkCurrentModule <$> get

462447 ty <- lookupVariable moduleName var

463448 ty' <- replaceAllTypeSynonyms ty

464449 case ty' of

@@ -474,7 +459,7 @@ infer' (Block ss) = do

474459 return $ TypedValue True (Block ss') ret

475460infer' v@(Constructor c) = do

476461 env <- getEnv

477− moduleName <- substCurrentModule `fmap` ask

462+ Just moduleName <- checkCurrentModule <$> get

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

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

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

@@ -488,10 +473,10 @@ infer' (IfThenElse cond th el) = do

488473 cond' <- check cond Boolean

489474 v2@(TypedValue _ _ t2) <- infer th

490475 v3@(TypedValue _ _ t3) <- infer el

491− t2 ~~ t3

476+ t2 ?= t3

492477 return $ TypedValue True (IfThenElse cond' v2 v3) t2

493478infer' (TypedValue checkType val ty) = do

494− moduleName <- substCurrentModule <$> ask

479+ Just moduleName <- checkCurrentModule <$> get

495480 kind <- liftCheck $ kindOf moduleName ty

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

497482 ty' <- replaceAllTypeSynonyms ty

@@ -502,7 +487,7 @@ infer' _ = error "Invalid argument to infer"

502487-- |

503488-- Infer the type of a property inside a record with a given type

504489--

505−inferProperty :: Type -> String -> Subst (Maybe Type)

490+inferProperty :: Type -> String -> UnifyT Check (Maybe Type)

506491inferProperty (Object row) prop = do

507492 let (props, _) = rowToList row

508493 return $ lookup prop props

@@ -517,22 +502,22 @@ inferProperty _ _ = return Nothing

517502-- |

518503-- Infer the type of a unary operator application

519504--

520−inferUnary :: UnaryOperator -> Value -> Subst Value

505+inferUnary :: UnaryOperator -> Value -> UnifyT Check Value

521506inferUnary op (TypedValue _ val valTy) =

522507 case fromMaybe (error "Invalid operator") $ lookup op unaryOps of

523508 (valTy', resTy) -> do

524− valTy' ~~ valTy

509+ valTy' ?= valTy

525510 return $ TypedValue True (Unary op val) resTy

526511inferUnary _ _ = error "Invalid arguments to inferUnary"

527512

528513-- |

529514-- Check the type of a unary operator application

530515--

531−checkUnary :: UnaryOperator -> Value -> Type -> Subst Value

516+checkUnary :: UnaryOperator -> Value -> Type -> UnifyT Check Value

532517checkUnary op val res =

533518 case fromMaybe (error "Invalid operator") $ lookup op unaryOps of

534519 (valTy, resTy) -> do

535− res ~~ resTy

520+ res ?= resTy

536521 val' <- check val valTy

537522 return $ Unary op val'

538523

@@ -548,32 +533,32 @@ unaryOps = [ (Negate, (Number, Number))

548533-- |

549534-- Infer the type of a binary operator application

550535--

551−inferBinary :: BinaryOperator -> Value -> Value -> Subst Value

536+inferBinary :: BinaryOperator -> Value -> Value -> UnifyT Check Value

552537inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) | isEqualityTest op = do

553− leftTy ~~ rightTy

538+ leftTy ?= rightTy

554539 return $ TypedValue True (Binary op left right) Boolean

555540inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) =

556541 case fromMaybe (error "Invalid operator") $ lookup op binaryOps of

557542 (valTy, resTy) -> do

558− leftTy ~~ valTy

559− rightTy ~~ valTy

543+ leftTy ?= valTy

544+ rightTy ?= valTy

560545 return $ TypedValue True (Binary op left right) resTy

561546inferBinary _ _ _ = error "Invalid arguments to inferBinary"

562547

563548-- |

564549-- Check the type of a binary operator application

565550--

566−checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst Value

551+checkBinary :: BinaryOperator -> Value -> Value -> Type -> UnifyT Check Value

567552checkBinary op left right res | isEqualityTest op = do

568− res ~~ Boolean

553+ res ?= Boolean

569554 left'@(TypedValue _ _ t1) <- infer left

570555 right'@(TypedValue _ _ t2) <- infer right

571− t1 ~~ t2

556+ t1 ?= t2

572557 return $ Binary op left' right'

573558checkBinary op left right res =

574559 case fromMaybe (error "Invalid operator") $ lookup op binaryOps of

575560 (valTy, resTy) -> do

576− res ~~ resTy

561+ res ?= resTy

577562 left' <- check left valTy

578563 right' <- check right valTy

579564 return $ Binary op left' right'

@@ -613,15 +598,15 @@ binaryOps = [ (Add, (Number, Number))

613598-- |

614599-- Infer the types of variables brought into scope by a binder

615600--

616−inferBinder :: Type -> Binder -> Subst (M.Map Ident Type)

601+inferBinder :: Type -> Binder -> UnifyT Check (M.Map Ident Type)

617602inferBinder _ NullBinder = return M.empty

618−inferBinder val (StringBinder _) = val ~~ String >> return M.empty

619−inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty

620−inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty

603+inferBinder val (StringBinder _) = val ?= String >> return M.empty

604+inferBinder val (NumberBinder _) = val ?= Number >> return M.empty

605+inferBinder val (BooleanBinder _) = val ?= Boolean >> return M.empty

621606inferBinder val (VarBinder name) = return $ M.singleton name val

622607inferBinder val (NullaryBinder ctor) = do

623608 env <- getEnv

624− moduleName <- substCurrentModule <$> ask

609+ Just moduleName <- checkCurrentModule <$> get

625610 case M.lookup (qualify moduleName ctor) (dataConstructors env) of

626611 Just (ty, _) -> do

627612 ty `subsumes` val

@@ -629,7 +614,7 @@ inferBinder val (NullaryBinder ctor) = do

629614 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"

630615inferBinder val (UnaryBinder ctor binder) = do

631616 env <- getEnv

632− moduleName <- substCurrentModule <$> ask

617+ Just moduleName <- checkCurrentModule <$> get

633618 case M.lookup (qualify moduleName ctor) (dataConstructors env) of

634619 Just (ty, _) -> do

635620 fn <- replaceAllVarsWithUnknowns ty

@@ -643,11 +628,11 @@ inferBinder val (ObjectBinder props) = do

643628 row <- fresh

644629 rest <- fresh

645630 m1 <- inferRowProperties row rest props

646− val ~~ Object row

631+ val ?= Object row

647632 return m1

648633 where

649− inferRowProperties :: Type -> Type -> [(String, Binder)] -> Subst (M.Map Ident Type)

650− inferRowProperties nrow row [] = nrow ~~ row >> return M.empty

634+ inferRowProperties :: Type -> Type -> [(String, Binder)] -> UnifyT Check (M.Map Ident Type)

635+ inferRowProperties nrow row [] = nrow ?= row >> return M.empty

651636 inferRowProperties nrow row ((name, binder):binders) = do

652637 propTy <- fresh

653638 m1 <- inferBinder propTy binder

@@ -656,13 +641,13 @@ inferBinder val (ObjectBinder props) = do

656641inferBinder val (ArrayBinder binders) = do

657642 el <- fresh

658643 m1 <- M.unions <$> mapM (inferBinder el) binders

659− val ~~ TypeApp Array el

644+ val ?= TypeApp Array el

660645 return m1

661646inferBinder val (ConsBinder headBinder tailBinder) = do

662647 el <- fresh

663648 m1 <- inferBinder el headBinder

664649 m2 <- inferBinder val tailBinder

665− val ~~ TypeApp Array el

650+ val ?= TypeApp Array el

666651 return $ m1 `M.union` m2

667652inferBinder val (NamedBinder name binder) = do

668653 m <- inferBinder val binder

@@ -671,10 +656,10 @@ inferBinder val (NamedBinder name binder) = do

671656-- |

672657-- Check the types of the return values in a set of binders in a case statement

673658--

674−checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> Subst [([Binder], Maybe Guard, Value)]

659+checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> UnifyT Check [([Binder], Maybe Guard, Value)]

675660checkBinders _ _ [] = return []

676661checkBinders nvals ret ((binders, grd, val):bs) = do

677− moduleName <- substCurrentModule <$> ask

662+ Just moduleName <- checkCurrentModule <$> get

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

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

680665 val' <- check val ret

@@ -689,19 +674,19 @@ checkBinders nvals ret ((binders, grd, val):bs) = do

689674-- |

690675-- Check that a local variable name is not already used

691676--

692−assignVariable :: Ident -> Subst ()

677+assignVariable :: Ident -> UnifyT Check ()

693678assignVariable name = do

694679 env <- checkEnv <$> get

695− moduleName <- substCurrentModule <$> ask

680+ Just moduleName <- checkCurrentModule <$> get

696681 case M.lookup (moduleName, name) (names env) of

697− Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."

682+ Just _ -> UnifyT . lift . throwError $ "Variable with name " ++ show name ++ " already exists."

698683 _ -> return ()

699684

700685-- |

701686-- Check the type of the return values of a statement, returning whether or not the statement returns on

702687-- all code paths

703688--

704−checkStatement :: M.Map Ident Type -> Type -> Statement -> Subst (Bool, M.Map Ident Type, Statement)

689+checkStatement :: M.Map Ident Type -> Type -> Statement -> UnifyT Check (Bool, M.Map Ident Type, Statement)

705690checkStatement mass _ (VariableIntroduction name val) = do

706691 assignVariable name

707692 val'@(TypedValue _ _ t) <- infer val

@@ -710,7 +695,7 @@ checkStatement mass _ (Assignment ident val) = do

710695 val'@(TypedValue _ _ t) <- infer val

711696 case M.lookup ident mass of

712697 Nothing -> throwError $ "No local variable with name " ++ show ident

713− Just ty -> do t ~~ ty

698+ Just ty -> do t ?= ty

714699 return (False, mass, Assignment ident val')

715700checkStatement mass ret (While val inner) = do

716701 val' <- check val Boolean

@@ -720,7 +705,7 @@ checkStatement mass ret (If ifst) = do

720705 (allCodePathsReturn, ifst') <- checkIfStatement mass ret ifst

721706 return (allCodePathsReturn, mass, If ifst')

722707checkStatement mass ret (For ident start end inner) = do

723− moduleName <- substCurrentModule <$> ask

708+ Just moduleName <- checkCurrentModule <$> get

724709 assignVariable ident

725710 start' <- check start Number

726711 end' <- check end Number

@@ -733,7 +718,7 @@ checkStatement mass ret (Return val) = do

733718-- |

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

735720--

736−checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> Subst (Bool, IfStatement)

721+checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> UnifyT Check (Bool, IfStatement)

737722checkIfStatement mass ret (IfStatement val thens Nothing) = do

738723 val' <- check val Boolean

739724 (_, _, thens') <- checkBlock mass ret thens

@@ -747,7 +732,7 @@ checkIfStatement mass ret (IfStatement val thens (Just elses)) = do

747732-- |

748733-- Check the type of an else statement

749734--

750−checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> Subst (Bool, ElseStatement)

735+checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> UnifyT Check (Bool, ElseStatement)

751736checkElseStatement mass ret (Else elses) = do

752737 (allCodePathsReturn, _, elses') <- checkBlock mass ret elses

753738 return (allCodePathsReturn, Else elses')

@@ -756,10 +741,10 @@ checkElseStatement mass ret (ElseIf ifst) = (id *** ElseIf) <$> checkIfStatement

756741-- |

757742-- Check the type of the return value of a block of statements

758743--

759−checkBlock :: M.Map Ident Type -> Type -> [Statement] -> Subst (Bool, M.Map Ident Type, [Statement])

744+checkBlock :: M.Map Ident Type -> Type -> [Statement] -> UnifyT Check (Bool, M.Map Ident Type, [Statement])

760745checkBlock mass _ [] = return (False, mass, [])

761746checkBlock mass ret (s:ss) = do

762− moduleName <- substCurrentModule <$> ask

747+ Just moduleName <- checkCurrentModule <$> get

763748 (b1, mass1, s') <- checkStatement mass ret s

764749 bindLocalVariables moduleName (M.toList mass1) $ case (b1, ss) of

765750 (True, []) -> return (True, mass1, [s'])

@@ -771,15 +756,15 @@ checkBlock mass ret (s:ss) = do

771756-- |

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

773758--

774−skolemize :: String -> Type -> Subst Type

759+skolemize :: String -> Type -> UnifyT Check Type

775760skolemize ident ty = do

776− tsk <- Skolem <$> fresh'

761+ tsk <- Skolem . runUnknown <$> fresh'

777762 return $ replaceTypeVars ident tsk ty

778763

779764-- |

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

781766--

782−check :: Value -> Type -> Subst Value

767+check :: Value -> Type -> UnifyT Check Value

783768check val ty = rethrow errorMessage $ check' val ty

784769 where

785770 errorMessage msg =

@@ -793,13 +778,13 @@ check val ty = rethrow errorMessage $ check' val ty

793778-- |

794779-- Check the type of a value

795780--

796−check' :: Value -> Type -> Subst Value

781+check' :: Value -> Type -> UnifyT Check Value

797782check' val (ForAll idents ty) = do

798783 sk <- skolemize idents ty

799784 check val sk

800785check' val (ConstrainedType constraints ty) = do

801786 env <- getEnv

802− moduleName <- substCurrentModule <$> ask

787+ Just moduleName <- checkCurrentModule <$> get

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

804789 n <- liftCheck freshDictionaryName

805790 return $ Ident $ "__dict_" ++ className ++ "_" ++ show n

@@ -812,7 +797,7 @@ check' val u@(TUnknown _) = do

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

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

814799 ty' <- replaceAllVarsWithUnknowns ty

815− ty' ~~ u

800+ ty' ?= u

816801 return val'

817802check' v@(NumericLiteral _) Number = return v

818803check' v@(StringLiteral _) String = return v

@@ -825,7 +810,7 @@ check' (Indexer index vals) ty = do

825810 vals' <- check vals (TypeApp Array ty)

826811 return $ Indexer index' vals'

827812check' (Abs args ret) (Function argTys retTy) = do

828− moduleName <- substCurrentModule <$> ask

813+ Just moduleName <- checkCurrentModule <$> get

829814 guardWith "Incorrect number of function arguments" (length args == length argTys)

830815 ret' <- bindLocalVariables moduleName (zip args argTys) $ check ret retTy

831816 return $ Abs args ret'

@@ -834,13 +819,13 @@ check' (App f args) ret = do

834819 app <- checkFunctionApplication f' ft args ret

835820 return $ app

836821check' (Var var) ty = do

837− moduleName <- substCurrentModule <$> ask

822+ Just moduleName <- checkCurrentModule <$> get

838823 ty1 <- lookupVariable moduleName var

839824 repl <- replaceAllTypeSynonyms ty1

840825 repl `subsumes` ty

841826 return $ Var var

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

843− moduleName <- substCurrentModule <$> ask

828+ Just moduleName <- checkCurrentModule <$> get

844829 kind <- liftCheck $ kindOf moduleName ty1

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

846831 ty1 `subsumes` ty2

@@ -879,7 +864,7 @@ check' (Block ss) ret = do

879864 return $ Block ss'

880865check' (Constructor c) ty = do

881866 env <- getEnv

882− moduleName <- substCurrentModule <$> ask

867+ Just moduleName <- checkCurrentModule <$> get

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

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

885870 Just (ty1, _) -> do

@@ -896,10 +881,10 @@ check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ p

896881--

897882-- The @lax@ parameter controls whether or not every record member has to be provided. For object updates, this is not the case.

898883--

899−checkProperties :: [(String, Value)] -> Type -> Bool -> Subst [(String, Value)]

884+checkProperties :: [(String, Value)] -> Type -> Bool -> UnifyT Check [(String, Value)]

900885checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where

901886 go [] [] REmpty = return []

902− go [] [] u@(TUnknown _) = do u ~~ REmpty

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

903888 return []

904889 go [] [] (Skolem _) | lax = return []

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

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

908893 go ((p,v):ps') [] u@(TUnknown _) = do

909894 v'@(TypedValue _ _ ty) <- infer v

910895 rest <- fresh

911− u ~~ RCons p ty rest

896+ u ?= RCons p ty rest

912897 ps'' <- go ps' [] rest

913898 return $ (p, v') : ps''

914899 go ((p,v):ps') ts r =

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

916901 Nothing -> do

917902 v'@(TypedValue _ _ ty) <- infer v

918903 rest <- fresh

919− r ~~ RCons p ty rest

904+ r ?= RCons p ty rest

920905 ps'' <- go ps' ts rest

921906 return $ (p, v') : ps''

922907 Just ty -> do

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

928913-- |

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

930915--

931−checkFunctionApplication :: Value -> Type -> [Value] -> Type -> Subst Value

916+checkFunctionApplication :: Value -> Type -> [Value] -> Type -> UnifyT Check Value

932917checkFunctionApplication fn fnTy args ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy args ret

933918 where

934919 errorMessage msg = "Error applying function of type "

@@ -939,7 +924,7 @@ checkFunctionApplication fn fnTy args ret = rethrow errorMessage $ checkFunction

939924-- |

940925-- Check the type of a function application

941926--

942−checkFunctionApplication' :: Value -> Type -> [Value] -> Type -> Subst Value

927+checkFunctionApplication' :: Value -> Type -> [Value] -> Type -> UnifyT Check Value

943928checkFunctionApplication' fn (Function argTys retTy) args ret = do

944929 guardWith "Incorrect number of function arguments" (length args == length argTys)

945930 args' <- zipWithM check args argTys

@@ -951,7 +936,7 @@ checkFunctionApplication' fn (ForAll ident ty) args ret = do

951936checkFunctionApplication' fn u@(TUnknown _) args ret = do

952937 args' <- mapM (\arg -> infer arg >>= \(TypedValue _ v t) -> TypedValue True v <$> replaceAllVarsWithUnknowns t) args

953938 let tys = map (\(TypedValue _ _ t) -> t) args'

954− u ~~ Function tys ret

939+ u ?= Function tys ret

955940 return $ App fn args'

956941checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) args ret = do

957942 ty <- expandTypeSynonym name tyArgs

@@ -959,7 +944,7 @@ checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) args ret = do

959944checkFunctionApplication' fn (ConstrainedType constraints fnTy) args ret = do

960945 env <- getEnv

961946 dicts <- getTypeClassDictionaries

962− moduleName <- substCurrentModule <$> ask

947+ Just moduleName <- checkCurrentModule <$> get

963948 checkFunctionApplication' (App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy args ret

964949checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of type "

965950 ++ prettyPrintType fnTy

@@ -969,7 +954,7 @@ checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of

969954-- |

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

971956--

972−subsumes :: Type -> Type -> Subst ()

957+subsumes :: Type -> Type -> UnifyT Check ()

973958subsumes ty1 ty2 = rethrow errorMessage $ subsumes' ty1 ty2

974959 where

975960 errorMessage msg = "Error checking that type "

@@ -981,12 +966,12 @@ subsumes ty1 ty2 = rethrow errorMessage $ subsumes' ty1 ty2

981966-- |

982967-- Check whether one type subsumes another

983968--

984−subsumes' :: Type -> Type -> Subst ()

969+subsumes' :: Type -> Type -> UnifyT Check ()

985970subsumes' (ForAll ident ty1) ty2 = do

986971 replaced <- replaceVarWithUnknown ident ty1

987972 replaced `subsumes` ty2

988973subsumes' (Function args1 ret1) (Function args2 ret2) = do

989974 zipWithM_ subsumes args2 args1

990975 ret1 `subsumes` ret2

991−subsumes' ty1 ty2 = ty1 ~~ ty2

976+subsumes' ty1 ty2 = ty1 ?= ty2

992977

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

@@ -20,8 +20,9 @@ module Language.PureScript.Types where

2020import Data.Data

2121import Data.Generics (mkT, mkQ, everywhereBut)

2222

23+import Control.Monad.Unify

24+

2325import Language.PureScript.Names

24−import Language.PureScript.Unknown (Unknown(..))

2526

2627-- |

2728-- The type of types

@@ -30,7 +31,7 @@ data Type

3031 -- |

3132 -- A unification variable of type Type

3233 --

33− = TUnknown (Unknown Type)

34+ = TUnknown (TypedUnknown Type)

3435 -- |

3536 -- Javascript numbers

3637 --

src/Language/PureScript/Unknown.hsdeleted−28

@@ -1,28 +0,0 @@

1−-----------------------------------------------------------------------------

2−--

3−-- Module : Language.PureScript.Unknown

4−-- Copyright : (c) Phil Freeman 2013

5−-- License : MIT

6−--

7−-- Maintainer : Phil Freeman <paf31@cantab.net>

8−-- Stability : experimental

9−-- Portability :

10−--

11−-- |

12−-- Data type for unification variables

13−--

14−-----------------------------------------------------------------------------

15−

16−{-# LANGUAGE DeriveDataTypeable #-}

17−

18−module Language.PureScript.Unknown where

19−

20−import Data.Data

21−

22−-- |

23−-- The type of typed unification variables

24−--

25−newtype Unknown t = Unknown { runUnknown :: Int } deriving (Show, Eq, Ord, Data, Typeable)

26−

27−

28−