d59db66 · rowtype-yoga/purescript-native

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

on golang help sign in

Use monad-unify package

d59db66Phil Freeman13 years ago

purescript.cabal+2−3

compare with golang

unifiedsplit

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

1name: purescript

2−version: 0.3.5

2+version: 0.3.6

3cabal-version: >=1.8

4build-type: Simple

5license: MIT

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

17library

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

19 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

21 exposed-modules: Data.Generics.Extras

22 Language.PureScript

23 Language.PureScript.Options

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

25 Language.PureScript.Kinds

26 Language.PureScript.Names

27 Language.PureScript.Types

28− Language.PureScript.Unknown

29 Language.PureScript.Values

28 Language.PureScript.Values

30 Language.PureScript.Scope

29 Language.PureScript.Scope

31 Language.PureScript.Sugar

30 Language.PureScript.Sugar

src/Language/PureScript.hs+4−1

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

31import Data.List (intercalate)

32import Control.Monad (when, forM)

33+import Control.Monad.State.Lazy

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

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

34import qualified Data.Map as M

35import qualified Data.Map as M

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

54compile opts ms = do

55compile opts ms = do

55 sorted <- sortModules ms

56 sorted <- sortModules ms

56 desugared <- desugar sorted

57 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

58 regrouped <- createBindingGroupsModule . collapseBindingGroupsModule $ elaborated

61 regrouped <- createBindingGroupsModule . collapseBindingGroupsModule $ elaborated

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

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

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

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

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

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

17module Language.PureScript.Kinds where

19import Data.Data

20−import Language.PureScript.Unknown

20+

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

22-- |

23-- |

23-- The data type of kinds

24-- The data type of kinds

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

26 -- |

27 -- |

27 -- Unification variable of type Kind

28 -- Unification variable of type Kind

28 --

29 --

29− = KUnknown (Unknown Kind)

30+ = KUnknown (TypedUnknown Kind)

30 -- |

31 -- |

31 -- The kind of types

32 -- The kind of types

32 --

33 --

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

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

22import Control.Arrow (ArrowPlus(..))

23import Control.PatternArrows

24+import Control.Monad.Unify

25import Language.PureScript.Kinds

26import Language.PureScript.Kinds

26import Language.PureScript.Pretty.Common

27import Language.PureScript.Pretty.Common

27−import Language.PureScript.Unknown

29typeLiterals :: Pattern () Kind String

30typeLiterals = mkPattern match

31 where

32 match Star = Just "*"

33 match Bang = Just "!"

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

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

35 match _ = Nothing

37matchRow :: Pattern () Kind ((), Kind)

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

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

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

25import Control.PatternArrows

26+import Control.Monad.Unify

27import Language.PureScript.Types

28import Language.PureScript.Types

28import Language.PureScript.Pretty.Common

29import Language.PureScript.Pretty.Common

29−import Language.PureScript.Unknown

31typeLiterals :: Pattern () Type String

32typeLiterals = mkPattern match

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

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

39 match (TypeVar var) = Just var

40 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

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

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

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

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

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

58 tailToPs :: Type -> String

59 tailToPs REmpty = ""

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

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

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

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

63 tailToPs _ = error "Invalid row tail"

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

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

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

17{-# LANGUAGE DeriveDataTypeable #-}

18+{-# LANGUAGE MultiParamTypeClasses #-}

19module Language.PureScript.TypeChecker.Kinds (

20module Language.PureScript.TypeChecker.Kinds (

20 kindOf,

21 kindOf,

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

27import Language.PureScript.Names

28import Language.PureScript.Names

28import Language.PureScript.TypeChecker.Monad

29import Language.PureScript.TypeChecker.Monad

29import Language.PureScript.Pretty

30import Language.PureScript.Pretty

30−import Language.PureScript.Unknown

32import Control.Monad.State

33import Control.Monad.Error

34import Control.Monad.Reader

35+import Control.Monad.Unify

36import Control.Applicative

37import Control.Applicative

38import qualified Data.Map as M

39import qualified Data.Map as M

40−instance Unifiable Kind where

41+instance Unifiable Check Kind where

41 unknown = KUnknown

42 unknown = KUnknown

42 isUnknown (KUnknown u) = Just u

43 isUnknown (KUnknown u) = Just u

43 isUnknown _ = Nothing

44 isUnknown _ = Nothing

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

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

45− KUnknown u ~~ k = replace u k

46+ KUnknown u ?= k = replace u k

46− k ~~ KUnknown u = replace u k

47+ k ?= KUnknown u = replace u k

47− Star ~~ Star = return ()

48+ Star ?= Star = return ()

48− Bang ~~ Bang = return ()

49+ Bang ?= Bang = return ()

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

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

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

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

51− k1 ~~ k3

52+ k1 ?= k3

52− k2 ~~ k4

53+ k2 ?= k4

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

54+ k1 ?= k2 = UnifyT . lift . 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 _ = []

61-- |

56-- |

62-- Infer the kind of a single type

57-- Infer the kind of a single type

63--

58--

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

59kindOf :: 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

67-- |

62-- |

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

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

69--

64--

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

65kindsOf :: 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

72 tyCon <- fresh

67 tyCon <- fresh

73 kargs <- replicateM (length args) fresh

68 kargs <- replicateM (length args) fresh

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

69 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))

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

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

80--

75--

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

76kindsOfAll :: 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

83 synVars <- replicateM (length syns) fresh

78 synVars <- replicateM (length syns) fresh

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

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

85 bindLocalTypeVariables moduleName dict $ do

80 bindLocalTypeVariables moduleName dict $ do

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

98 solveTypes [ty] kargs synVar) synVars syns

93 solveTypes [ty] kargs synVar) synVars syns

99 return (syn_ks, data_ks)

94 return (syn_ks, data_ks)

100 where

95 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)

102

103-- |

98-- |

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

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

105--

100--

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

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

107solveTypes ts kargs tyCon = do

102solveTypes ts kargs tyCon = do

108 ks <- mapM infer ts

103 ks <- mapM infer ts

109− tyCon ~~ foldr FunKind Star kargs

104+ tyCon ?= foldr FunKind Star kargs

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

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

111 return tyCon

106 return tyCon

112

107

113-- |

108-- |

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

121-- |

116-- |

122-- Infer a kind for a type

117-- Infer a kind for a type

123--

118--

124−infer :: Type -> Subst Kind

119+infer :: Type -> UnifyT Check Kind

125infer Number = return Star

120infer Number = return Star

126infer String = return Star

121infer String = return Star

127infer Boolean = return Star

122infer Boolean = return Star

128infer Array = return $ FunKind Star Star

123infer Array = return $ FunKind Star Star

129infer (Object row) = do

124infer (Object row) = do

130 k <- infer row

125 k <- infer row

131− k ~~ Row Star

126+ k ?= Row Star

132 return Star

127 return Star

133infer (Function args ret) = do

128infer (Function args ret) = do

134 ks <- mapM infer args

129 ks <- mapM infer args

135 k <- infer ret

130 k <- infer ret

136− k ~~ Star

131+ k ?= Star

137− forM_ ks (~~ Star)

132+ forM_ ks (?= Star)

138 return Star

133 return Star

139infer (TypeVar v) = do

134infer (TypeVar v) = do

140− moduleName <- substCurrentModule <$> ask

135+ Just moduleName <- checkCurrentModule <$> get

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

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

142infer (TypeConstructor v) = do

137infer (TypeConstructor v) = do

143 env <- liftCheck getEnv

138 env <- liftCheck getEnv

144− moduleName <- substCurrentModule `fmap` ask

139+ Just moduleName <- checkCurrentModule <$> get

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

140 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 ++ "'"

147 Just (kind, _) -> return kind

142 Just (kind, _) -> return kind

148infer (TypeApp t1 t2) = do

143infer (TypeApp t1 t2) = do

149 k0 <- fresh

144 k0 <- fresh

150 k1 <- infer t1

145 k1 <- infer t1

151 k2 <- infer t2

146 k2 <- infer t2

152− k1 ~~ FunKind k2 k0

147+ k1 ?= FunKind k2 k0

153 return k0

148 return k0

154infer (ForAll ident ty) = do

149infer (ForAll ident ty) = do

155 k <- fresh

150 k <- fresh

156− moduleName <- substCurrentModule <$> ask

151+ Just moduleName <- checkCurrentModule <$> get

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

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

158infer REmpty = do

153infer REmpty = do

159 k <- fresh

154 k <- fresh

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

161infer (RCons _ ty row) = do

156infer (RCons _ ty row) = do

162 k1 <- infer ty

157 k1 <- infer ty

163 k2 <- infer row

158 k2 <- infer row

164− k2 ~~ Row k1

159+ k2 ?= Row k1

165 return $ Row k1

160 return $ Row k1

166infer (ConstrainedType deps ty) = do

161infer (ConstrainedType deps ty) = do

167 mapM_ (infer . snd) deps

162 mapM_ (infer . snd) deps

168 k <- infer ty

163 k <- infer ty

169− k ~~ Star

164+ k ?= Star

170 return Star

165 return Star

171infer _ = error "Invalid argument to infer"

166infer _ = error "Invalid argument to infer"

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

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

22import Language.PureScript.Kinds

23import Language.PureScript.Values

24import Language.PureScript.Names

25−import Language.PureScript.Unknown

26import Language.PureScript.Declarations

25import Language.PureScript.Declarations

28import Data.Data

27import Data.Data

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

34import Control.Monad.State

33import Control.Monad.State

35import Control.Monad.Error

34import Control.Monad.Error

36import Control.Monad.Reader

35import Control.Monad.Reader

36+import Control.Monad.Unify

37import Control.Arrow ((***))

39import qualified Data.Map as M

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

227 -- The next type class dictionary name

228 --

229 , checkNextDictName :: Int

230+ -- |

231+ -- The current module

232+ --

233+ , checkCurrentModule :: Maybe ModuleName

230 }

234 }

231

235

232-- |

236-- |

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

258--

262--

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

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

260runCheck c = do

264runCheck 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

262 return (a, checkEnv s)

266 return (a, checkEnv s)

263

267

264-- |

268-- |

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

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

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

284 return n

288 return n

285

289

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−

319-- |

290-- |

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

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

321--

292--

322−liftCheck :: Check a -> Subst a

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

323−liftCheck = Subst . lift . lift

294+liftCheck = UnifyT . lift . lift

324−

325−-- |

326−-- Get the current substitution monad state

327−--

328−getSubstState :: Subst SubstState

329−getSubstState = Subst . lift $ get

330

295

331-- |

296-- |

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

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

333--

298--

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

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

335−runSubst context subst = do

300+liftUnify unify = do

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

301+ st <- get

337− return (a, substSubst s)

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

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

303+ case e of

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

304+ Left err -> throwError err

394− _ -> return ()

305+ Right (a, ust) -> do

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) }

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

403− return n

307+ return $ runSubstitution (unifyCurrentSubstitution ust) a

404−

405−-- |

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

407−--

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

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

410

308

411-- |

309-- |

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

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

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

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

14-----------------------------------------------------------------------------

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

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

17+{-# LANGUAGE DeriveDataTypeable #-}

18+{-# LANGUAGE FlexibleContexts #-}

19+{-# LANGUAGE MultiParamTypeClasses #-}

19module Language.PureScript.TypeChecker.Types (

21module Language.PureScript.TypeChecker.Types (

20 typesOf

22 typesOf

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

53import Language.PureScript.TypeChecker.Kinds

55import Language.PureScript.TypeChecker.Kinds

54import Language.PureScript.TypeChecker.Synonyms

56import Language.PureScript.TypeChecker.Synonyms

55import Language.PureScript.Pretty

57import Language.PureScript.Pretty

56−import Language.PureScript.Unknown

58import Control.Monad.State

59import Control.Monad.State

59import Control.Monad.Error

60import Control.Monad.Error

60import Control.Monad.Reader

61import Control.Monad.Reader

62+import Control.Monad.Unify

62import Control.Applicative

64import Control.Applicative

63import Control.Arrow (Arrow(..))

65import Control.Arrow (Arrow(..))

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

65import qualified Data.Map as M

67import qualified Data.Map as M

66import Data.Function (on)

68import Data.Function (on)

68−instance Unifiable Type where

70+instance Unifiable Check Type where

69 unknown = TUnknown

71 unknown = TUnknown

70 isUnknown (TUnknown u) = Just u

72 isUnknown (TUnknown u) = Just u

71 isUnknown _ = Nothing

73 isUnknown _ = Nothing

72− (~~) = unifyTypes

74+ (?=) = 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 _ = []

90-- |

76-- |

91-- Unify two types, updating the current substitution

77-- Unify two types, updating the current substitution

92--

78--

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

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

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

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

95 unifyTypes' t1 t2

81 unifyTypes' t1 t2

96 where

82 where

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

113 unifyTypes' String String = return ()

99 unifyTypes' String String = return ()

114 unifyTypes' Boolean Boolean = return ()

100 unifyTypes' Boolean Boolean = return ()

115 unifyTypes' Array Array = return ()

101 unifyTypes' Array Array = return ()

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

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

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

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

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

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

119 zipWithM_ unifyTypes args1 args2

105 zipWithM_ unifyTypes args1 args2

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

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

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

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

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

123 env <- getEnv

109 env <- getEnv

124− moduleName <- substCurrentModule `fmap` ask

110+ Just moduleName <- checkCurrentModule <$> get

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

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

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

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

127 t3 `unifyTypes` t5

113 t3 `unifyTypes` t5

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

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

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

141-- error.

127-- error.

142--

128--

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

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

144unifyRows r1 r2 =

130unifyRows r1 r2 =

145 let

131 let

146 (s1, r1') = rowToList r1

132 (s1, r1') = rowToList r1

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

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

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

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

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

151 in do

137 in do

152− forM_ int (uncurry (~~))

138+ forM_ int (uncurry (?=))

153 unifyRows' sd1 r1' sd2 r2'

139 unifyRows' sd1 r1' sd2 r2'

154 where

140 where

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

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

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

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

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

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

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

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

159 occursCheck un ty

145 occursCheck un ty

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

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

161 u' <- fresh

147 u' <- fresh

162− u ~~ RCons name ty u'

148+ u ?= RCons name ty u'

163 unifyRows' row r others u'

149 unifyRows' row r others u'

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

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

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

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

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

178--

164--

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

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

180typesOf moduleName vals = do

166typesOf moduleName vals = do

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

167+ tys <- liftUnify $ do

182− . runSubst (SubstContext moduleName) $ do

183 let es = map isTyped vals

168 let es = map isTyped vals

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

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

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

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

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

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

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

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

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

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

184 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)

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

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

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

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

203 [eff, a] <- replicateM 2 fresh

188 [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

205 escapeCheck val ty

190 escapeCheck val ty

206 return triple

191 return triple

207 forM_ tys $ skolemEscapeCheck . snd . snd

192 forM_ tys $ skolemEscapeCheck . snd . snd

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

279-- |

264-- |

280-- Ensure unsolved unification variables do not escape

265-- Ensure unsolved unification variables do not escape

281--

266--

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

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

283escapeCheck value ty = do

268escapeCheck value ty = do

284− subst <- substSubst <$> getSubstState

269+ subst <- unifyCurrentSubstitution <$> UnifyT get

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

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

286 let allUnknowns = findAllTypes value

271 let allUnknowns = findAllTypes value

287 forM_ allUnknowns $ \t -> do

272 forM_ allUnknowns $ \t -> do

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

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

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

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

290

275

291-- |

276-- |

292-- Find all type annotations occuring inside a value

277-- Find all type annotations occuring inside a value

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

304skolemEscapeCheck ty =

289skolemEscapeCheck ty =

305 case something (mkQ Nothing findSkolems) ty of

290 case something (mkQ Nothing findSkolems) ty of

306 Nothing -> return ()

291 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."

308 where

293 where

309 findSkolems (Skolem _) = return ()

294 findSkolems (Skolem _) = return ()

310 findSkolems _ = mzero

295 findSkolems _ = mzero

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

330 toName = (:) 't' . show

315 toName = (:) 't' . show

331 ty' = everywhere (mkT typeToVar) $ ty

316 ty' = everywhere (mkT typeToVar) $ ty

332 typeToVar :: Type -> Type

317 typeToVar :: Type -> Type

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

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

334 typeToVar t = t

319 typeToVar t = t

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

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

336

321

337-- |

322-- |

338-- Replace named type variables with types

323-- Replace named type variables with types

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

343-- |

328-- |

344-- Replace named type variables with new unification variables

329-- Replace named type variables with new unification variables

345--

330--

346−replaceAllVarsWithUnknowns :: Type -> Subst Type

331+replaceAllVarsWithUnknowns :: Type -> UnifyT Check Type

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

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

348replaceAllVarsWithUnknowns ty = return ty

333replaceAllVarsWithUnknowns ty = return ty

349

334

350-- |

335-- |

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

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

352--

337--

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

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

354replaceVarWithUnknown ident ty = do

339replaceVarWithUnknown ident ty = do

355 tu <- fresh

340 tu <- fresh

356 return $ replaceTypeVars ident tu $ ty

341 return $ replaceTypeVars ident tu $ ty

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

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

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

360-- better error messages during unification.

345-- better error messages during unification.

361--

346--

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

363replaceAllTypeSynonyms d = do

348replaceAllTypeSynonyms d = do

364 env <- getEnv

349 env <- getEnv

365− moduleName <- substCurrentModule <$> ask

350+ Just moduleName <- checkCurrentModule <$> get

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

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

367 either throwError return $ saturateAllTypeSynonyms env moduleName syns d

352 either throwError return $ saturateAllTypeSynonyms env moduleName syns d

368

353

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

378-- |

363-- |

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

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

380--

365--

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

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

382expandTypeSynonym name args = do

367expandTypeSynonym name args = do

383 env <- getEnv

368 env <- getEnv

384− moduleName <- substCurrentModule `fmap` ask

369+ Just moduleName <- checkCurrentModule <$> get

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

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

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

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

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

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

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

395-- |

380-- |

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

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

397--

382--

398−infer :: Value -> Subst Value

383+infer :: Value -> UnifyT Check Value

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

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

400

385

401-- |

386-- |

402-- Infer a type for a value

387-- Infer a type for a value

403--

388--

404−infer' :: Value -> Subst Value

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

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

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

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

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

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

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

408infer' (ArrayLiteral vals) = do

393infer' (ArrayLiteral vals) = do

409 ts <- mapM infer vals

394 ts <- mapM infer vals

410 els <- fresh

395 els <- fresh

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

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

412 return $ TypedValue True (ArrayLiteral ts) els

397 return $ TypedValue True (ArrayLiteral ts) els

413infer' (Unary op val) = do

398infer' (Unary op val) = do

414 v <- infer val

399 v <- infer val

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

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

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

449infer' (Abs args ret) = do

434infer' (Abs args ret) = do

450 ts <- replicateM (length args) fresh

435 ts <- replicateM (length args) fresh

451− moduleName <- substCurrentModule <$> ask

436+ Just moduleName <- checkCurrentModule <$> get

452 bindLocalVariables moduleName (zip args ts) $ do

437 bindLocalVariables moduleName (zip args ts) $ do

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

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

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

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

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

458 app <- checkFunctionApplication f' ft args ret

443 app <- checkFunctionApplication f' ft args ret

459 return $ TypedValue True app ret

444 return $ TypedValue True app ret

460infer' (Var var) = do

445infer' (Var var) = do

461− moduleName <- substCurrentModule <$> ask

446+ Just moduleName <- checkCurrentModule <$> get

462 ty <- lookupVariable moduleName var

447 ty <- lookupVariable moduleName var

463 ty' <- replaceAllTypeSynonyms ty

448 ty' <- replaceAllTypeSynonyms ty

464 case ty' of

449 case ty' of

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

474 return $ TypedValue True (Block ss') ret

459 return $ TypedValue True (Block ss') ret

475infer' v@(Constructor c) = do

460infer' v@(Constructor c) = do

476 env <- getEnv

461 env <- getEnv

477− moduleName <- substCurrentModule `fmap` ask

462+ Just moduleName <- checkCurrentModule <$> get

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

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

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

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

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

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

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

488 cond' <- check cond Boolean

473 cond' <- check cond Boolean

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

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

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

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

491− t2 ~~ t3

476+ t2 ?= t3

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

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

493infer' (TypedValue checkType val ty) = do

478infer' (TypedValue checkType val ty) = do

494− moduleName <- substCurrentModule <$> ask

479+ Just moduleName <- checkCurrentModule <$> get

495 kind <- liftCheck $ kindOf moduleName ty

480 kind <- liftCheck $ kindOf moduleName ty

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

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

497 ty' <- replaceAllTypeSynonyms ty

482 ty' <- replaceAllTypeSynonyms ty

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

502-- |

487-- |

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

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

504--

489--

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

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

506inferProperty (Object row) prop = do

491inferProperty (Object row) prop = do

507 let (props, _) = rowToList row

492 let (props, _) = rowToList row

508 return $ lookup prop props

493 return $ lookup prop props

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

517-- |

502-- |

518-- Infer the type of a unary operator application

503-- Infer the type of a unary operator application

519--

504--

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

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

521inferUnary op (TypedValue _ val valTy) =

506inferUnary op (TypedValue _ val valTy) =

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

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

523 (valTy', resTy) -> do

508 (valTy', resTy) -> do

524− valTy' ~~ valTy

509+ valTy' ?= valTy

525 return $ TypedValue True (Unary op val) resTy

510 return $ TypedValue True (Unary op val) resTy

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

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

527

512

528-- |

513-- |

529-- Check the type of a unary operator application

514-- Check the type of a unary operator application

530--

515--

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

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

532checkUnary op val res =

517checkUnary op val res =

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

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

534 (valTy, resTy) -> do

519 (valTy, resTy) -> do

535− res ~~ resTy

520+ res ?= resTy

536 val' <- check val valTy

521 val' <- check val valTy

537 return $ Unary op val'

522 return $ Unary op val'

538

523

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

548-- |

533-- |

549-- Infer the type of a binary operator application

534-- Infer the type of a binary operator application

550--

535--

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

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

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

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

553− leftTy ~~ rightTy

538+ leftTy ?= rightTy

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

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

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

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

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

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

557 (valTy, resTy) -> do

542 (valTy, resTy) -> do

558− leftTy ~~ valTy

543+ leftTy ?= valTy

559− rightTy ~~ valTy

544+ rightTy ?= valTy

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

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

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

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

562

547

563-- |

548-- |

564-- Check the type of a binary operator application

549-- Check the type of a binary operator application

565--

550--

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

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

567checkBinary op left right res | isEqualityTest op = do

552checkBinary op left right res | isEqualityTest op = do

568− res ~~ Boolean

553+ res ?= Boolean

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

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

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

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

571− t1 ~~ t2

556+ t1 ?= t2

572 return $ Binary op left' right'

557 return $ Binary op left' right'

573checkBinary op left right res =

558checkBinary op left right res =

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

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

575 (valTy, resTy) -> do

560 (valTy, resTy) -> do

576− res ~~ resTy

561+ res ?= resTy

577 left' <- check left valTy

562 left' <- check left valTy

578 right' <- check right valTy

563 right' <- check right valTy

579 return $ Binary op left' right'

564 return $ Binary op left' right'

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

613-- |

598-- |

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

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

615--

600--

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

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

617inferBinder _ NullBinder = return M.empty

602inferBinder _ NullBinder = return M.empty

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

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

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

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

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

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

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

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

622inferBinder val (NullaryBinder ctor) = do

607inferBinder val (NullaryBinder ctor) = do

623 env <- getEnv

608 env <- getEnv

624− moduleName <- substCurrentModule <$> ask

609+ Just moduleName <- checkCurrentModule <$> get

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

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

626 Just (ty, _) -> do

611 Just (ty, _) -> do

627 ty `subsumes` val

612 ty `subsumes` val

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

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

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

630inferBinder val (UnaryBinder ctor binder) = do

615inferBinder val (UnaryBinder ctor binder) = do

631 env <- getEnv

616 env <- getEnv

632− moduleName <- substCurrentModule <$> ask

617+ Just moduleName <- checkCurrentModule <$> get

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

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

634 Just (ty, _) -> do

619 Just (ty, _) -> do

635 fn <- replaceAllVarsWithUnknowns ty

620 fn <- replaceAllVarsWithUnknowns ty

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

643 row <- fresh

628 row <- fresh

644 rest <- fresh

629 rest <- fresh

645 m1 <- inferRowProperties row rest props

630 m1 <- inferRowProperties row rest props

646− val ~~ Object row

631+ val ?= Object row

647 return m1

632 return m1

648 where

633 where

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

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

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

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

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

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

652 propTy <- fresh

637 propTy <- fresh

653 m1 <- inferBinder propTy binder

638 m1 <- inferBinder propTy binder

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

656inferBinder val (ArrayBinder binders) = do

641inferBinder val (ArrayBinder binders) = do

657 el <- fresh

642 el <- fresh

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

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

659− val ~~ TypeApp Array el

644+ val ?= TypeApp Array el

660 return m1

645 return m1

661inferBinder val (ConsBinder headBinder tailBinder) = do

646inferBinder val (ConsBinder headBinder tailBinder) = do

662 el <- fresh

647 el <- fresh

663 m1 <- inferBinder el headBinder

648 m1 <- inferBinder el headBinder

664 m2 <- inferBinder val tailBinder

649 m2 <- inferBinder val tailBinder

665− val ~~ TypeApp Array el

650+ val ?= TypeApp Array el

666 return $ m1 `M.union` m2

651 return $ m1 `M.union` m2

667inferBinder val (NamedBinder name binder) = do

652inferBinder val (NamedBinder name binder) = do

668 m <- inferBinder val binder

653 m <- inferBinder val binder

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

671-- |

656-- |

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

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

673--

658--

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)]

675checkBinders _ _ [] = return []

660checkBinders _ _ [] = return []

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

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

677− moduleName <- substCurrentModule <$> ask

662+ Just moduleName <- checkCurrentModule <$> get

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

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

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

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

680 val' <- check val ret

665 val' <- check val ret

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

689-- |

674-- |

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

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

691--

676--

692−assignVariable :: Ident -> Subst ()

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

693assignVariable name = do

678assignVariable name = do

694 env <- checkEnv <$> get

679 env <- checkEnv <$> get

695− moduleName <- substCurrentModule <$> ask

680+ Just moduleName <- checkCurrentModule <$> get

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

681 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."

698 _ -> return ()

683 _ -> return ()

699

684

700-- |

685-- |

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

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

702-- all code paths

687-- all code paths

703--

688--

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)

705checkStatement mass _ (VariableIntroduction name val) = do

690checkStatement mass _ (VariableIntroduction name val) = do

706 assignVariable name

691 assignVariable name

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

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

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

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

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

711 case M.lookup ident mass of

696 case M.lookup ident mass of

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

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

713− Just ty -> do t ~~ ty

698+ Just ty -> do t ?= ty

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

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

715checkStatement mass ret (While val inner) = do

700checkStatement mass ret (While val inner) = do

716 val' <- check val Boolean

701 val' <- check val Boolean

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

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

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

721 return (allCodePathsReturn, mass, If ifst')

706 return (allCodePathsReturn, mass, If ifst')

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

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

723− moduleName <- substCurrentModule <$> ask

708+ Just moduleName <- checkCurrentModule <$> get

724 assignVariable ident

709 assignVariable ident

725 start' <- check start Number

710 start' <- check start Number

726 end' <- check end Number

711 end' <- check end Number

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

733-- |

718-- |

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

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

735--

720--

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

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

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

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

738 val' <- check val Boolean

723 val' <- check val Boolean

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

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

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

747-- |

732-- |

748-- Check the type of an else statement

733-- Check the type of an else statement

749--

734--

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

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

751checkElseStatement mass ret (Else elses) = do

736checkElseStatement mass ret (Else elses) = do

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

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

753 return (allCodePathsReturn, Else elses')

738 return (allCodePathsReturn, Else elses')

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

756-- |

741-- |

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

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

758--

743--

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])

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

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

761checkBlock mass ret (s:ss) = do

746checkBlock mass ret (s:ss) = do

762− moduleName <- substCurrentModule <$> ask

747+ Just moduleName <- checkCurrentModule <$> get

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

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

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

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

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

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

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

771-- |

756-- |

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

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

773--

758--

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

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

775skolemize ident ty = do

760skolemize ident ty = do

776− tsk <- Skolem <$> fresh'

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

777 return $ replaceTypeVars ident tsk ty

762 return $ replaceTypeVars ident tsk ty

778

763

779-- |

764-- |

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

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

781--

766--

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

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

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

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

784 where

769 where

785 errorMessage msg =

770 errorMessage msg =

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

793-- |

778-- |

794-- Check the type of a value

779-- Check the type of a value

795--

780--

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

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

797check' val (ForAll idents ty) = do

782check' val (ForAll idents ty) = do

798 sk <- skolemize idents ty

783 sk <- skolemize idents ty

799 check val sk

784 check val sk

800check' val (ConstrainedType constraints ty) = do

785check' val (ConstrainedType constraints ty) = do

801 env <- getEnv

786 env <- getEnv

802− moduleName <- substCurrentModule <$> ask

787+ Just moduleName <- checkCurrentModule <$> get

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

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

804 n <- liftCheck freshDictionaryName

789 n <- liftCheck freshDictionaryName

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

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

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

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

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

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

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

814 ty' <- replaceAllVarsWithUnknowns ty

799 ty' <- replaceAllVarsWithUnknowns ty

815− ty' ~~ u

800+ ty' ?= u

816 return val'

801 return val'

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

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

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

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

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

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

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

826 return $ Indexer index' vals'

811 return $ Indexer index' vals'

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

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

828− moduleName <- substCurrentModule <$> ask

813+ Just moduleName <- checkCurrentModule <$> get

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

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

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

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

831 return $ Abs args ret'

816 return $ Abs args ret'

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

834 app <- checkFunctionApplication f' ft args ret

819 app <- checkFunctionApplication f' ft args ret

835 return $ app

820 return $ app

836check' (Var var) ty = do

821check' (Var var) ty = do

837− moduleName <- substCurrentModule <$> ask

822+ Just moduleName <- checkCurrentModule <$> get

838 ty1 <- lookupVariable moduleName var

823 ty1 <- lookupVariable moduleName var

839 repl <- replaceAllTypeSynonyms ty1

824 repl <- replaceAllTypeSynonyms ty1

840 repl `subsumes` ty

825 repl `subsumes` ty

841 return $ Var var

826 return $ Var var

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

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

843− moduleName <- substCurrentModule <$> ask

828+ Just moduleName <- checkCurrentModule <$> get

844 kind <- liftCheck $ kindOf moduleName ty1

829 kind <- liftCheck $ kindOf moduleName ty1

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

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

846 ty1 `subsumes` ty2

831 ty1 `subsumes` ty2

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

879 return $ Block ss'

864 return $ Block ss'

880check' (Constructor c) ty = do

865check' (Constructor c) ty = do

881 env <- getEnv

866 env <- getEnv

882− moduleName <- substCurrentModule <$> ask

867+ Just moduleName <- checkCurrentModule <$> get

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

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

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

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

885 Just (ty1, _) -> do

870 Just (ty1, _) -> do

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

896--

881--

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

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

898--

883--

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

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

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

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

901 go [] [] REmpty = return []

886 go [] [] REmpty = return []

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

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

903 return []

888 return []

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

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

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

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

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

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

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

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

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

910 rest <- fresh

895 rest <- fresh

911− u ~~ RCons p ty rest

896+ u ?= RCons p ty rest

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

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

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

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

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

899 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

916 Nothing -> do

901 Nothing -> do

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

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

918 rest <- fresh

903 rest <- fresh

919− r ~~ RCons p ty rest

904+ r ?= RCons p ty rest

920 ps'' <- go ps' ts rest

905 ps'' <- go ps' ts rest

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

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

922 Just ty -> do

907 Just ty -> do

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

928-- |

913-- |

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

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

930--

915--

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

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

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

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

933 where

918 where

934 errorMessage msg = "Error applying function of type "

919 errorMessage msg = "Error applying function of type "

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

939-- |

924-- |

940-- Check the type of a function application

925-- Check the type of a function application

941--

926--

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

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

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

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

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

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

945 args' <- zipWithM check args argTys

930 args' <- zipWithM check args argTys

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

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

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

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

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

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

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

954− u ~~ Function tys ret

939+ u ?= Function tys ret

955 return $ App fn args'

940 return $ App fn args'

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

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

957 ty <- expandTypeSynonym name tyArgs

942 ty <- expandTypeSynonym name tyArgs

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

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

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

960 env <- getEnv

945 env <- getEnv

961 dicts <- getTypeClassDictionaries

946 dicts <- getTypeClassDictionaries

962− moduleName <- substCurrentModule <$> ask

947+ Just moduleName <- checkCurrentModule <$> get

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

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

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

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

965 ++ prettyPrintType fnTy

950 ++ prettyPrintType fnTy

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

969-- |

954-- |

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

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

971--

956--

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

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

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

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

974 where

959 where

975 errorMessage msg = "Error checking that type "

960 errorMessage msg = "Error checking that type "

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

981-- |

966-- |

982-- Check whether one type subsumes another

967-- Check whether one type subsumes another

983--

968--

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

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

985subsumes' (ForAll ident ty1) ty2 = do

970subsumes' (ForAll ident ty1) ty2 = do

986 replaced <- replaceVarWithUnknown ident ty1

971 replaced <- replaceVarWithUnknown ident ty1

987 replaced `subsumes` ty2

972 replaced `subsumes` ty2

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

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

989 zipWithM_ subsumes args2 args1

974 zipWithM_ subsumes args2 args1

990 ret1 `subsumes` ret2

975 ret1 `subsumes` ret2

991−subsumes' ty1 ty2 = ty1 ~~ ty2

976+subsumes' ty1 ty2 = ty1 ?= ty2

992

977

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

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

20import Data.Data

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

23+import Control.Monad.Unify

24+

23import Language.PureScript.Names

25import Language.PureScript.Names

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

26-- |

27-- |

27-- The type of types

28-- The type of types

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

30 -- |

31 -- |

31 -- A unification variable of type Type

32 -- A unification variable of type Type

32 --

33 --

33− = TUnknown (Unknown Type)

34+ = TUnknown (TypedUnknown Type)

34 -- |

35 -- |

35 -- Javascript numbers

36 -- Javascript numbers

36 --

37 --

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−