117d5d3 · rowtype-yoga/purescript-native

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

New approach to unification

commit117d5d3cd25122aa3859f0425f196e623aa08490 authorPhil Freeman <paf31@cantab.net> dateSun 1 Nov 2015, 11:10 (11 years ago) parent80fb351

15 files changed+635−633

compare with golang

unifiedsplit

psci/PSCi.hs+7−5

@@ -35,12 +35,11 @@ import Control.Arrow (first)

3535import Control.Monad

3636import Control.Monad.Error.Class (MonadError(..))

3737import Control.Monad.Trans.Class

38−import Control.Monad.Trans.Except (runExceptT)

38+import Control.Monad.Trans.Except (ExceptT(), runExceptT)

3939import Control.Monad.Trans.Maybe (MaybeT(..), runMaybeT)

4040import Control.Monad.Trans.State.Strict

4141import Control.Monad.IO.Class (liftIO)

42−import Control.Monad.Writer.Strict (runWriter)

43−import qualified Control.Monad.Trans.State.Lazy as L

42+import Control.Monad.Writer.Strict (Writer(), runWriter)

4443

4544import Options.Applicative as Opts

4645

@@ -424,8 +423,11 @@ handleKindOf typ = do

424423 Right env' ->

425424 case M.lookup (P.Qualified (Just mName) $ P.ProperName "IT") (P.typeSynonyms env') of

426425 Just (_, typ') -> do

427− let chk = P.CheckState env' 0 0 (Just mName)

428− k = fst . runWriter . runExceptT $ L.runStateT (P.unCheck (P.kindOf typ')) chk

426+ let chk = (P.emptyCheckState env') { P.checkCurrentModule = Just mName }

427+ k = check (P.kindOf typ') chk

428+

429+ check :: StateT P.CheckState (ExceptT P.MultipleErrors (Writer P.MultipleErrors)) a -> P.CheckState -> Either P.MultipleErrors (a, P.CheckState)

430+ check sew cs = fst . runWriter . runExceptT . runStateT sew $ cs

429431 case k of

430432 Left errStack -> PSCI . outputStrLn . P.prettyPrintMultipleErrors False $ errStack

431433 Right (kind, _) -> PSCI . outputStrLn . P.prettyPrintKind $ kind

purescript.cabal−1

@@ -173,7 +173,6 @@ library

173173 Language.PureScript.Publish.BoxesHelpers

174174

175175 Control.Monad.Logger

176− Control.Monad.Unify

177176 Control.Monad.Supply

178177 Control.Monad.Supply.Class

179178

src/Control/Monad/Unify.hsdeleted−160

@@ -1,160 +0,0 @@

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

2−--

3−-- Module : Control.Monad.Unify

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−--

13−--

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

15−

16−{-# LANGUAGE GeneralizedNewtypeDeriving #-}

17−{-# LANGUAGE FlexibleInstances #-}

18−{-# LANGUAGE FlexibleContexts #-}

19−{-# LANGUAGE DeriveDataTypeable #-}

20−{-# LANGUAGE MultiParamTypeClasses #-}

21−{-# LANGUAGE FunctionalDependencies #-}

22−{-# LANGUAGE UndecidableInstances #-}

23−

24−module Control.Monad.Unify where

25−

26−import Data.Monoid

27−

28−import Control.Applicative

29−import Control.Monad.State

30−import Control.Monad.Error.Class (MonadError(..))

31−import Control.Monad.Writer.Class (MonadWriter(..))

32−

33−import Data.HashMap.Strict as M

34−

35−-- |

36−-- Untyped unification variables

37−--

38−type Unknown = Int

39−

40−-- |

41−-- A type which can contain unification variables

42−--

43−class Partial t where

44− unknown :: Unknown -> t

45− isUnknown :: t -> Maybe Unknown

46− unknowns :: t -> [Unknown]

47− ($?) :: Substitution t -> t -> t

48−

49−-- |

50−-- Identifies types which support unification

51−--

52−class (Partial t) => Unifiable m t | t -> m where

53− (=?=) :: t -> t -> UnifyT t m ()

54−

55−-- |

56−-- A substitution maintains a mapping from unification variables to their values

57−--

58−data Substitution t = Substitution { runSubstitution :: M.HashMap Int t }

59−

60−instance (Partial t) => Monoid (Substitution t) where

61− mempty = Substitution M.empty

62− s1 `mappend` s2 = Substitution $

63− M.map (s2 $?) (runSubstitution s1) `M.union`

64− M.map (s1 $?) (runSubstitution s2)

65−

66−-- |

67−-- State required for type checking

68−--

69−data UnifyState t = UnifyState {

70− -- |

71− -- The next fresh unification variable

72− --

73− unifyNextVar :: Int

74− -- |

75− -- The current substitution

76− --

77− , unifyCurrentSubstitution :: Substitution t

78− }

79−

80−-- |

81−-- An empty @UnifyState@

82−--

83−defaultUnifyState :: (Partial t) => UnifyState t

84−defaultUnifyState = UnifyState 0 mempty

85−

86−-- |

87−-- A class for errors which support unification errors

88−--

89−class UnificationError t e where

90− occursCheckFailed :: t -> e

91−

92−-- |

93−-- The type checking monad, which provides the state of the type checker, and error reporting capabilities

94−--

95−newtype UnifyT t m a = UnifyT { unUnify :: StateT (UnifyState t) m a }

96− deriving (Functor, Monad, Applicative, Alternative, MonadPlus, MonadWriter w)

97−

98−instance (MonadState s m) => MonadState s (UnifyT t m) where

99− get = UnifyT . lift $ get

100− put = UnifyT . lift . put

101−

102−instance (MonadError e m) => MonadError e (UnifyT t m) where

103− throwError = UnifyT . throwError

104− catchError e f = UnifyT $ catchError (unUnify e) (unUnify . f)

105−

106−-- |

107−-- Run a computation in the Unify monad, failing with an error, or succeeding with a return value and the new next unification variable

108−--

109−runUnify :: UnifyState t -> UnifyT t m a -> m (a, UnifyState t)

110−runUnify s = flip runStateT s . unUnify

111−

112−-- |

113−-- Substitute a single unification variable

114−--

115−substituteOne :: (Partial t) => Unknown -> t -> Substitution t

116−substituteOne u t = Substitution $ M.singleton u t

117−

118−-- |

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

120−--

121−(=:=) :: (UnificationError t e, Monad m, MonadError e m, Unifiable m t) => Unknown -> t -> UnifyT t m ()

122−(=:=) u t' = do

123− st <- UnifyT get

124− let sub = unifyCurrentSubstitution st

125− let t = sub $? t'

126− occursCheck u t

127− let current = sub $? unknown u

128− case isUnknown current of

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

130− _ -> current =?= t

131− UnifyT $ modify $ \s -> s { unifyCurrentSubstitution = substituteOne u t <> unifyCurrentSubstitution s }

132−

133−-- |

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

135−--

136−occursCheck :: (UnificationError t e, Monad m, MonadError e m, Partial t) => Unknown -> t -> UnifyT t m ()

137−occursCheck u t =

138− case isUnknown t of

139− Nothing -> when (u `elem` unknowns t) $ UnifyT . lift . throwError $ occursCheckFailed t

140− _ -> return ()

141−

142−-- |

143−-- Generate a fresh untyped unification variable

144−--

145−fresh' :: (Monad m) => UnifyT t m Unknown

146−fresh' = do

147− st <- UnifyT get

148− UnifyT $ modify $ \s -> s { unifyNextVar = succ (unifyNextVar s) }

149− return $ unifyNextVar st

150−

151−-- |

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

153−--

154−fresh :: (Monad m, Partial t) => UnifyT t m t

155−fresh = do

156− u <- fresh'

157− return $ unknown u

158−

159−

160−

src/Language/PureScript/Errors.hs+2−15

@@ -32,7 +32,6 @@ import Data.Foldable (fold)

3232import qualified Data.Map as M

3333

3434import Control.Monad

35−import Control.Monad.Unify

3635import Control.Monad.Writer

3736import Control.Monad.Error.Class (MonadError(..))

3837#if __GLASGOW_HASKELL__ < 710

@@ -183,12 +182,6 @@ data HintCategory

183182

184183data ErrorMessage = ErrorMessage [ErrorMessageHint] SimpleErrorMessage deriving (Show)

185184

186−instance UnificationError Type ErrorMessage where

187− occursCheckFailed t = ErrorMessage [] $ InfiniteType t

188−

189−instance UnificationError Kind ErrorMessage where

190− occursCheckFailed k = ErrorMessage [] $ InfiniteKind k

191−

192185-- |

193186-- Get the error code for a particular error type

194187--

@@ -291,12 +284,6 @@ errorCode em = case unwrapErrorMessage em of

291284newtype MultipleErrors = MultipleErrors

292285 { runMultipleErrors :: [ErrorMessage] } deriving (Show, Monoid)

293286

294−instance UnificationError Type MultipleErrors where

295− occursCheckFailed t = MultipleErrors [occursCheckFailed t]

296−

297−instance UnificationError Kind MultipleErrors where

298− occursCheckFailed k = MultipleErrors [occursCheckFailed k]

299−

300287-- | Check whether a collection of errors is empty or not.

301288nonEmpty :: MultipleErrors -> Bool

302289nonEmpty = not . null . runMultipleErrors

@@ -326,7 +313,7 @@ addHint hint = onErrorMessages $ \(ErrorMessage hints se) -> ErrorMessage (hint

326313data LabelType = TypeLabel | SkolemLabel String deriving (Show, Read, Eq, Ord)

327314

328315-- | A map from rigid type variable name/unknown variable pairs to new variables.

329−type UnknownMap = M.Map (LabelType, Unknown) Unknown

316+type UnknownMap = M.Map (LabelType, Int) Int

330317

331318-- | How critical the issue is

332319data Level = Error | Warning deriving Show

@@ -340,7 +327,7 @@ unwrapErrorMessage (ErrorMessage _ se) = se

340327replaceUnknowns :: Type -> State UnknownMap Type

341328replaceUnknowns = everywhereOnTypesM replaceTypes

342329 where

343− lookupTable :: (LabelType, Unknown) -> UnknownMap -> (Unknown, UnknownMap)

330+ lookupTable :: (LabelType, Int) -> UnknownMap -> (Int, UnknownMap)

344331 lookupTable x m = case M.lookup x m of

345332 Nothing -> let i = length (filter (on (==) fst x) (M.keys m)) in (i, M.insert x i m)

346333 Just i -> (i, m)

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

@@ -24,7 +24,6 @@ import qualified Data.Aeson.TH as A

2424#if __GLASGOW_HASKELL__ < 710

2525import Control.Applicative

2626#endif

27−import Control.Monad.Unify (Unknown)

2827

2928-- |

3029-- The data type of kinds

@@ -33,7 +32,7 @@ data Kind

3332 -- |

3433 -- Unification variable of type Kind

3534 --

36− = KUnknown Unknown

35+ = KUnknown Int

3736 -- |

3837 -- The kind of types

3938 --

src/Language/PureScript/TypeChecker.hs+103−36

@@ -13,7 +13,9 @@

1313--

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

1515

16+{-# LANGUAGE ScopedTypeVariables #-}

1617{-# LANGUAGE FlexibleInstances #-}

18+{-# LANGUAGE FlexibleContexts #-}

1719{-# LANGUAGE CPP #-}

1820

1921module Language.PureScript.TypeChecker (

@@ -29,14 +31,17 @@ import Language.PureScript.TypeChecker.Synonyms as T

2931import Data.Maybe

3032import Data.List (nub, (\\), sort, group)

3133import Data.Foldable (for_)

34+import Data.Traversable (for)

3235

3336import qualified Data.Map as M

3437

3538#if __GLASGOW_HASKELL__ < 710

36−import Control.Applicative ((<$>), (<*))

39+import Control.Applicative

3740#endif

38−import Control.Monad.State

41+import Control.Monad (when, unless, void)

42+import Control.Monad.State.Class (MonadState(..), modify)

3943import Control.Monad.Error.Class (MonadError(..))

44+import Control.Monad.Writer.Class (MonadWriter(..))

4045

4146import Language.PureScript.Crash

4247import Language.PureScript.Types

@@ -47,15 +52,31 @@ import Language.PureScript.TypeClassDictionaries

4752import Language.PureScript.Environment

4853import Language.PureScript.Errors

4954

50−addDataType :: ModuleName -> DataDeclType -> ProperName -> [(String, Maybe Kind)] -> [(ProperName, [Type])] -> Kind -> Check ()

55+addDataType ::

56+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

57+ ModuleName ->

58+ DataDeclType ->

59+ ProperName ->

60+ [(String, Maybe Kind)] ->

61+ [(ProperName, [Type])] ->

62+ Kind ->

63+ m ()

5164addDataType moduleName dtype name args dctors ctorKind = do

5265 env <- getEnv

5366 putEnv $ env { types = M.insert (Qualified (Just moduleName) name) (ctorKind, DataType args dctors) (types env) }

54− forM_ dctors $ \(dctor, tys) ->

67+ for_ dctors $ \(dctor, tys) ->

5568 warnAndRethrow (addHint (ErrorInDataConstructor dctor)) $

5669 addDataConstructor moduleName dtype name (map fst args) dctor tys

5770

58−addDataConstructor :: ModuleName -> DataDeclType -> ProperName -> [String] -> ProperName -> [Type] -> Check ()

71+addDataConstructor ::

72+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

73+ ModuleName ->

74+ DataDeclType ->

75+ ProperName ->

76+ [String] ->

77+ ProperName ->

78+ [Type] ->

79+ m ()

5980addDataConstructor moduleName dtype name args dctor tys = do

6081 env <- getEnv

6182 mapM_ checkTypeSynonyms tys

@@ -65,26 +86,50 @@ addDataConstructor moduleName dtype name args dctor tys = do

6586 let fields = [Ident ("value" ++ show n) | n <- [0..(length tys - 1)]]

6687 putEnv $ env { dataConstructors = M.insert (Qualified (Just moduleName) dctor) (dtype, name, polyType, fields) (dataConstructors env) }

6788

68−addTypeSynonym :: ModuleName -> ProperName -> [(String, Maybe Kind)] -> Type -> Kind -> Check ()

89+addTypeSynonym ::

90+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

91+ ModuleName ->

92+ ProperName ->

93+ [(String, Maybe Kind)] ->

94+ Type ->

95+ Kind ->

96+ m ()

6997addTypeSynonym moduleName name args ty kind = do

7098 env <- getEnv

7199 checkTypeSynonyms ty

72100 putEnv $ env { types = M.insert (Qualified (Just moduleName) name) (kind, TypeSynonym) (types env)

73101 , typeSynonyms = M.insert (Qualified (Just moduleName) name) (args, ty) (typeSynonyms env) }

74102

75−valueIsNotDefined :: ModuleName -> Ident -> Check ()

103+valueIsNotDefined ::

104+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

105+ ModuleName ->

106+ Ident ->

107+ m ()

76108valueIsNotDefined moduleName name = do

77109 env <- getEnv

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

79111 Just _ -> throwError . errorMessage $ RedefinedIdent name

80112 Nothing -> return ()

81113

82−addValue :: ModuleName -> Ident -> Type -> NameKind -> Check ()

114+addValue ::

115+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

116+ ModuleName ->

117+ Ident ->

118+ Type ->

119+ NameKind ->

120+ m ()

83121addValue moduleName name ty nameKind = do

84122 env <- getEnv

85123 putEnv (env { names = M.insert (moduleName, name) (ty, nameKind, Defined) (names env) })

86124

87−addTypeClass :: ModuleName -> ProperName -> [(String, Maybe Kind)] -> [Constraint] -> [Declaration] -> Check ()

125+addTypeClass ::

126+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

127+ ModuleName ->

128+ ProperName ->

129+ [(String, Maybe Kind)] ->

130+ [Constraint] ->

131+ [Declaration] ->

132+ m ()

88133addTypeClass moduleName pn args implies ds =

89134 let members = map toPair ds in

90135 modify $ \st -> st { checkEnv = (checkEnv st) { typeClasses = M.insert (Qualified (Just moduleName) pn) (args, members, implies) (typeClasses . checkEnv $ st) } }

@@ -93,19 +138,30 @@ addTypeClass moduleName pn args implies ds =

93138 toPair (PositionedDeclaration _ _ d) = toPair d

94139 toPair _ = internalError "Invalid declaration in TypeClassDeclaration"

95140

96−addTypeClassDictionaries :: Maybe ModuleName -> M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope) -> Check ()

141+addTypeClassDictionaries ::

142+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

143+ Maybe ModuleName ->

144+ M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope) ->

145+ m ()

97146addTypeClassDictionaries mn entries =

98147 modify $ \st -> st { checkEnv = (checkEnv st) { typeClassDictionaries = insertState st } }

99148 where insertState st = M.insertWith (M.unionWith M.union) mn entries (typeClassDictionaries . checkEnv $ st)

100149

101−checkDuplicateTypeArguments :: [String] -> Check ()

150+checkDuplicateTypeArguments ::

151+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

152+ [String] ->

153+ m ()

102154checkDuplicateTypeArguments args = for_ firstDup $ \dup ->

103155 throwError . errorMessage $ DuplicateTypeArgument dup

104156 where

105157 firstDup :: Maybe String

106158 firstDup = listToMaybe $ args \\ nub args

107159

108−checkTypeClassInstance :: ModuleName -> Type -> Check ()

160+checkTypeClassInstance ::

161+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

162+ ModuleName ->

163+ Type ->

164+ m ()

109165checkTypeClassInstance _ (TypeVar _) = return ()

110166checkTypeClassInstance _ (TypeConstructor ctor) = do

111167 env <- getEnv

@@ -117,7 +173,10 @@ checkTypeClassInstance _ ty = throwError . errorMessage $ InvalidInstanceHead ty

117173-- |

118174-- Check that type synonyms are fully-applied in a type

119175--

120−checkTypeSynonyms :: Type -> Check ()

176+checkTypeSynonyms ::

177+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

178+ Type ->

179+ m ()

121180checkTypeSynonyms = void . replaceAllTypeSynonyms

122181

123182-- |

@@ -133,10 +192,15 @@ checkTypeSynonyms = void . replaceAllTypeSynonyms

133192--

134193-- * Process module imports

135194--

136−typeCheckAll :: ModuleName -> [DeclarationRef] -> [Declaration] -> Check [Declaration]

195+typeCheckAll :: forall m.

196+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

197+ ModuleName ->

198+ [DeclarationRef] ->

199+ [Declaration] ->

200+ m [Declaration]

137201typeCheckAll moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds

138202 where

139− go :: Declaration -> Check Declaration

203+ go :: Declaration -> m Declaration

140204 go (DataDeclaration dtype name args dctors) = do

141205 warnAndRethrow (addHint (ErrorInTypeConstructor name)) $ do

142206 when (dtype == Newtype) $ checkNewtype dctors

@@ -146,7 +210,7 @@ typeCheckAll moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds

146210 addDataType moduleName dtype name args' dctors ctorKind

147211 return $ DataDeclaration dtype name args dctors

148212 where

149− checkNewtype :: [(ProperName, [Type])] -> Check ()

213+ checkNewtype :: [(ProperName, [Type])] -> m ()

150214 checkNewtype [(_, [_])] = return ()

151215 checkNewtype [(_, _)] = throwError . errorMessage $ InvalidNewtype name

152216 checkNewtype _ = throwError . errorMessage $ InvalidNewtype name

@@ -155,11 +219,11 @@ typeCheckAll moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds

155219 let syns = mapMaybe toTypeSynonym tys

156220 let dataDecls = mapMaybe toDataDecl tys

157221 (syn_ks, data_ks) <- kindsOfAll moduleName syns (map (\(_, name, args, dctors) -> (name, args, concatMap snd dctors)) dataDecls)

158− forM_ (zip dataDecls data_ks) $ \((dtype, name, args, dctors), ctorKind) -> do

222+ for_ (zip dataDecls data_ks) $ \((dtype, name, args, dctors), ctorKind) -> do

159223 checkDuplicateTypeArguments $ map fst args

160224 let args' = args `withKinds` ctorKind

161225 addDataType moduleName dtype name args' dctors ctorKind

162− forM_ (zip syns syn_ks) $ \((name, args, ty), kind) -> do

226+ for_ (zip syns syn_ks) $ \((name, args, ty), kind) -> do

163227 checkDuplicateTypeArguments $ map fst args

164228 let args' = args `withKinds` kind

165229 addTypeSynonym moduleName name args' ty kind

@@ -188,14 +252,14 @@ typeCheckAll moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds

188252 go (ValueDeclaration{}) = internalError "Binders were not desugared"

189253 go (BindingGroupDeclaration vals) =

190254 warnAndRethrow (addHint (ErrorInBindingGroup (map (\(ident, _, _) -> ident) vals))) $ do

191− forM_ (map (\(ident, _, _) -> ident) vals) $ \name ->

255+ for_ (map (\(ident, _, _) -> ident) vals) $ \name ->

192256 valueIsNotDefined moduleName name

193257 tys <- typesOf moduleName $ map (\(ident, _, ty) -> (ident, ty)) vals

194− vals' <- forM [ (name, val, nameKind, ty)

195− | (name, nameKind, _) <- vals

196− , (name', (val, ty)) <- tys

197− , name == name'

198− ] $ \(name, val, nameKind, ty) -> do

258+ vals' <- for [ (name, val, nameKind, ty)

259+ | (name, nameKind, _) <- vals

260+ , (name', (val, ty)) <- tys

261+ , name == name'

262+ ] $ \(name, val, nameKind, ty) -> do

199263 addValue moduleName name ty nameKind

200264 return (name, nameKind, val)

201265 return $ BindingGroupDeclaration vals'

@@ -219,7 +283,7 @@ typeCheckAll moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds

219283 return d

220284 go (d@(TypeInstanceDeclaration dictName deps className tys body)) = rethrow (addHint (ErrorInInstance className tys)) $ do

221285 mapM_ (checkTypeClassInstance moduleName) tys

222− forM_ deps $ mapM_ (checkTypeClassInstance moduleName) . snd

286+ for_ deps $ mapM_ (checkTypeClassInstance moduleName) . snd

223287 checkOrphanInstance dictName className tys

224288 _ <- traverseTypeInstanceBody checkInstanceMembers body

225289 let dict = TypeClassDictionaryInScope (Qualified (Just moduleName) dictName) [] className tys (Just deps)

@@ -228,7 +292,7 @@ typeCheckAll moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds

228292 go (PositionedDeclaration pos com d) =

229293 warnAndRethrowWithPosition pos $ PositionedDeclaration pos com <$> go d

230294

231− checkOrphanFixities :: Declaration -> Check ()

295+ checkOrphanFixities :: Declaration -> m ()

232296 checkOrphanFixities (FixityDeclaration _ name) = do

233297 env <- getEnv

234298 guardWith (errorMessage (OrphanFixityDeclaration name)) $ M.member (moduleName, Op name) $ names env

@@ -236,7 +300,7 @@ typeCheckAll moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds

236300 warnAndRethrowWithPosition pos $ checkOrphanFixities d

237301 checkOrphanFixities _ = return ()

238302

239− checkInstanceMembers :: [Declaration] -> Check [Declaration]

303+ checkInstanceMembers :: [Declaration] -> m [Declaration]

240304 checkInstanceMembers instDecls = do

241305 let idents = sort . map head . group . map memberName $ instDecls

242306 for_ (firstDuplicate idents) $ \ident ->

@@ -254,7 +318,7 @@ typeCheckAll moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds

254318 | otherwise = firstDuplicate xs

255319 firstDuplicate _ = Nothing

256320

257− checkOrphanInstance :: Ident -> Qualified ProperName -> [Type] -> Check ()

321+ checkOrphanInstance :: Ident -> Qualified ProperName -> [Type] -> m ()

258322 checkOrphanInstance dictName className@(Qualified (Just mn') _) tys'

259323 | moduleName == mn' || any checkType tys' = return ()

260324 | otherwise = throwError . errorMessage $ OrphanInstance dictName className tys'

@@ -281,19 +345,22 @@ typeCheckAll moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds

281345-- Type check an entire module and ensure all types and classes defined within the module that are

282346-- required by exported members are also exported.

283347--

284−typeCheckModule :: Module -> Check Module

348+typeCheckModule :: forall m.

349+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

350+ Module ->

351+ m Module

285352typeCheckModule (Module _ _ _ _ Nothing) = internalError "exports should have been elaborated"

286353typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint (ErrorInModule mn)) $ do

287354 modify (\s -> s { checkCurrentModule = Just mn })

288355 decls' <- typeCheckAll mn exps decls

289− forM_ exps $ \e -> do

356+ for_ exps $ \e -> do

290357 checkTypesAreExported e

291358 checkClassMembersAreExported e

292359 checkClassesAreExported e

293360 return $ Module ss coms mn decls' (Just exps)

294361 where

295362

296− checkMemberExport :: (Type -> [DeclarationRef]) -> DeclarationRef -> Check ()

363+ checkMemberExport :: (Type -> [DeclarationRef]) -> DeclarationRef -> m ()

297364 checkMemberExport extract dr@(TypeRef name dctors) = do

298365 env <- getEnv

299366 case M.lookup (Qualified (Just mn) name) (typeSynonyms env) of

@@ -301,7 +368,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint

301368 Just (_, ty) -> checkExport dr extract ty

302369 case dctors of

303370 Nothing -> return ()

304− Just dctors' -> forM_ dctors' $ \dctor ->

371+ Just dctors' -> for_ dctors' $ \dctor ->

305372 case M.lookup (Qualified (Just mn) dctor) (dataConstructors env) of

306373 Nothing -> return ()

307374 Just (_, _, ty, _) -> checkExport dr extract ty

@@ -311,7 +378,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint

311378 checkExport dr extract ty

312379 checkMemberExport _ _ = return ()

313380

314− checkExport :: DeclarationRef -> (Type -> [DeclarationRef]) -> Type -> Check ()

381+ checkExport :: DeclarationRef -> (Type -> [DeclarationRef]) -> Type -> m ()

315382 checkExport dr extract ty = case filter (not . exported) (extract ty) of

316383 [] -> return ()

317384 hidden -> throwError . errorMessage $ TransitiveExportError dr hidden

@@ -326,7 +393,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint

326393

327394 -- Check that all the type constructors defined in the current module that appear in member types

328395 -- have also been exported from the module

329− checkTypesAreExported :: DeclarationRef -> Check ()

396+ checkTypesAreExported :: DeclarationRef -> m ()

330397 checkTypesAreExported = checkMemberExport findTcons

331398 where

332399 findTcons :: Type -> [DeclarationRef]

@@ -337,7 +404,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint

337404

338405 -- Check that all the classes defined in the current module that appear in member types have also

339406 -- been exported from the module

340− checkClassesAreExported :: DeclarationRef -> Check ()

407+ checkClassesAreExported :: DeclarationRef -> m ()

341408 checkClassesAreExported = checkMemberExport findClasses

342409 where

343410 findClasses :: Type -> [DeclarationRef]

@@ -349,7 +416,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) = warnAndRethrow (addHint

349416 extractCurrentModuleClass (Qualified (Just mn') name) | mn == mn' = Just name

350417 extractCurrentModuleClass _ = Nothing

351418

352− checkClassMembersAreExported :: DeclarationRef -> Check ()

419+ checkClassMembersAreExported :: DeclarationRef -> m ()

353420 checkClassMembersAreExported dr@(TypeClassRef name) = do

354421 let members = ValueRef `map` head (mapMaybe findClassMembers decls)

355422 let missingMembers = members \\ exps

src/Language/PureScript/TypeChecker/Entailment.hs+13−7

@@ -14,6 +14,8 @@

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

1515

1616{-# LANGUAGE CPP #-}

17+{-# LANGUAGE ScopedTypeVariables #-}

18+{-# LANGUAGE FlexibleContexts #-}

1719

1820module Language.PureScript.TypeChecker.Entailment (

1921 entails

@@ -33,13 +35,12 @@ import Control.Applicative

3335import Control.Arrow (Arrow(..))

3436import Control.Monad.State

3537import Control.Monad.Error.Class (MonadError(..))

36−import Control.Monad.Writer.Class (tell)

38+import Control.Monad.Writer.Class (MonadWriter(..))

3739

3840import Language.PureScript.Crash

3941import Language.PureScript.AST

4042import Language.PureScript.Errors

4143import Language.PureScript.Names

42−import Language.PureScript.TypeChecker.Monad

4344import Language.PureScript.TypeChecker.Unify

4445import Language.PureScript.TypeClassDictionaries

4546import Language.PureScript.Types

@@ -49,7 +50,12 @@ import qualified Language.PureScript.Constants as C

4950-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,

5051-- return a type class dictionary reference.

5152--

52−entails :: ModuleName -> M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)) -> Constraint -> Check Expr

53+entails :: forall m.

54+ (MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

55+ ModuleName ->

56+ M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)) ->

57+ Constraint ->

58+ m Expr

5359entails moduleName context = solve

5460 where

5561 forClassName :: Qualified ProperName -> [Type] -> [TypeClassDictionaryInScope]

@@ -65,12 +71,12 @@ entails moduleName context = solve

6571 findDicts :: Qualified ProperName -> Maybe ModuleName -> [TypeClassDictionaryInScope]

6672 findDicts cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup context

6773

68− solve :: Constraint -> Check Expr

74+ solve :: Constraint -> m Expr

6975 solve (className, tys) = do

7076 dict <- go 0 className tys

7177 return $ dictionaryValueToValue dict

7278 where

73− go :: Int -> Qualified ProperName -> [Type] -> Check DictionaryValue

79+ go :: Int -> Qualified ProperName -> [Type] -> m DictionaryValue

7480 go work className' tys' | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'

7581 go work className' tys' = do

7682 let instances = do

@@ -86,7 +92,7 @@ entails moduleName context = solve

8692 (tcdPath tcd)

8793 where

8894

89− unique :: [(a, TypeClassDictionaryInScope)] -> Check (a, TypeClassDictionaryInScope)

95+ unique :: [(a, TypeClassDictionaryInScope)] -> m (a, TypeClassDictionaryInScope)

9096 unique [] = throwError . errorMessage $ NoInstanceFound className' tys'

9197 unique [a] = return a

9298 unique tcds | pairwise overlapping (map snd tcds) = do

@@ -109,7 +115,7 @@ entails moduleName context = solve

109115 -- Create dictionaries for subgoals which still need to be solved by calling go recursively

110116 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type

111117 -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.

112− solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> Check (Maybe [DictionaryValue])

118+ solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> m (Maybe [DictionaryValue])

113119 solveSubgoals _ Nothing = return Nothing

114120 solveSubgoals subst (Just subgoals) = do

115121 dict <- mapM (uncurry (go (work + 1)) . second (map (replaceAllTypeVars subst))) subgoals

src/Language/PureScript/TypeChecker/Kinds.hs+124−90

@@ -13,10 +13,11 @@

1313--

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

1515

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

1716{-# LANGUAGE MultiParamTypeClasses #-}

1817{-# LANGUAGE FlexibleInstances #-}

18+{-# LANGUAGE FlexibleContexts #-}

1919{-# LANGUAGE TupleSections #-}

20+{-# LANGUAGE ScopedTypeVariables #-}

2021{-# LANGUAGE CPP #-}

2122

2223module Language.PureScript.TypeChecker.Kinds (

@@ -26,9 +27,6 @@ module Language.PureScript.TypeChecker.Kinds (

2627 kindsOfAll

2728) where

2829

29−import Data.Maybe (fromMaybe)

30−

31−import qualified Data.HashMap.Strict as H

3230import qualified Data.Map as M

3331

3432import Control.Arrow (second)

@@ -37,8 +35,8 @@ import Control.Applicative

3735#endif

3836import Control.Monad

3937import Control.Monad.Error.Class (MonadError(..))

38+import Control.Monad.Writer.Class (MonadWriter(..))

4039import Control.Monad.State

41−import Control.Monad.Unify

4240

4341import Language.PureScript.Crash

4442import Language.PureScript.Environment

@@ -48,177 +46,213 @@ import Language.PureScript.Names

4846import Language.PureScript.TypeChecker.Monad

4947import Language.PureScript.Types

5048

51−instance Partial Kind where

52− unknown = KUnknown

53− isUnknown (KUnknown u) = Just u

54− isUnknown _ = Nothing

55− unknowns = everythingOnKinds (++) go

56− where

57− go (KUnknown u) = [u]

58− go _ = []

59− ($?) sub = everywhereOnKinds go

60− where

61− go t@(KUnknown u) = fromMaybe t $ H.lookup u (runSubstitution sub)

62− go other = other

63−

64−instance Unifiable Check Kind where

65− KUnknown u1 =?= KUnknown u2 | u1 == u2 = return ()

66− KUnknown u =?= k = u =:= k

67− k =?= KUnknown u = u =:= k

68− Star =?= Star = return ()

69− Bang =?= Bang = return ()

70− Row k1 =?= Row k2 = k1 =?= k2

71− FunKind k1 k2 =?= FunKind k3 k4 = do

72− k1 =?= k3

73− k2 =?= k4

74− k1 =?= k2 = UnifyT . lift . throwError . errorMessage $ KindsDoNotUnify k1 k2

49+-- | Generate a fresh kind variable

50+freshKind :: (MonadState CheckState m) => m Kind

51+freshKind = do

52+ k <- gets checkNextKind

53+ modify $ \st -> st { checkNextKind = k + 1 }

54+ return $ KUnknown k

7555

76−-- |

77−-- Infer the kind of a single type

78−--

79−kindOf :: Type -> Check Kind

56+-- | Update the substitution to solve a kind constraint

57+solveKind :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Int -> Kind -> m ()

58+solveKind u k = do

59+ occursCheck u k

60+ modify $ \cs -> cs { checkSubstitution =

61+ (checkSubstitution cs) { substKind =

62+ M.insert u k $ substKind $ checkSubstitution cs

63+ }

64+ }

65+

66+-- | Apply a substitution to a kind

67+substituteKind :: Substitution -> Kind -> Kind

68+substituteKind sub = everywhereOnKinds go

69+ where

70+ go (KUnknown u) =

71+ case M.lookup u (substKind sub) of

72+ Nothing -> KUnknown u

73+ Just (KUnknown u1) | u1 == u -> KUnknown u1

74+ Just t -> substituteKind sub t

75+ go other = other

76+

77+-- | Make sure that an unknown does not occur in a kind

78+occursCheck :: (Functor m, Applicative m, MonadError MultipleErrors m) => Int -> Kind -> m ()

79+occursCheck _ KUnknown{} = return ()

80+occursCheck u k = void $ everywhereOnKindsM go k

81+ where

82+ go (KUnknown u') | u == u' = throwError . errorMessage . InfiniteKind $ k

83+ go other = return other

84+

85+-- | Unify two kinds

86+unifyKinds :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Kind -> Kind -> m ()

87+unifyKinds k1 k2 = do

88+ sub <- gets checkSubstitution

89+ go (substituteKind sub k1) (substituteKind sub k2)

90+ where

91+ go (KUnknown u1) (KUnknown u2) | u1 == u2 = return ()

92+ go (KUnknown u) k = solveKind u k

93+ go k (KUnknown u) = solveKind u k

94+ go Star Star = return ()

95+ go Bang Bang = return ()

96+ go (Row k1') (Row k2') = go k1' k2'

97+ go (FunKind k1' k2') (FunKind k3 k4) = do

98+ go k1' k3

99+ go k2' k4

100+ go k1' k2' = throwError . errorMessage $ KindsDoNotUnify k1' k2'

101+

102+-- | Infer the kind of a single type

103+kindOf ::

104+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m) =>

105+ Type ->

106+ m Kind

80107kindOf ty = fst <$> kindOfWithScopedVars ty

81108

82−-- |

83−-- Infer the kind of a single type, returning the kinds of any scoped type variables

84−--

85−kindOfWithScopedVars :: Type -> Check (Kind, [(String, Kind)])

109+-- | Infer the kind of a single type, returning the kinds of any scoped type variables

110+kindOfWithScopedVars ::

111+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m) =>

112+ Type ->

113+ m (Kind, [(String, Kind)])

86114kindOfWithScopedVars ty =

87115 rethrow (addHint (ErrorCheckingKind ty)) $

88116 fmap tidyUp . liftUnify $ infer ty

89117 where

90− tidyUp ((k, args), sub) = ( starIfUnknown (sub $? k)

91− , map (second (starIfUnknown . (sub $?))) args

118+ tidyUp ((k, args), sub) = ( starIfUnknown (substituteKind sub k)

119+ , map (second (starIfUnknown . substituteKind sub)) args

92120 )

93121

94−-- |

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

96−--

97−kindsOf :: Bool -> ModuleName -> ProperName -> [(String, Maybe Kind)] -> [Type] -> Check Kind

122+-- | Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors

123+kindsOf ::

124+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m) =>

125+ Bool ->

126+ ModuleName ->

127+ ProperName ->

128+ [(String, Maybe Kind)] ->

129+ [Type] ->

130+ m Kind

98131kindsOf isData moduleName name args ts = fmap tidyUp . liftUnify $ do

99− tyCon <- fresh

100− kargs <- replicateM (length args) fresh

132+ tyCon <- freshKind

133+ kargs <- replicateM (length args) freshKind

101134 rest <- zipWithM freshKindVar args kargs

102135 let dict = (name, tyCon) : rest

103136 bindLocalTypeVariables moduleName dict $

104137 solveTypes isData ts kargs tyCon

105138 where

106− tidyUp (k, sub) = starIfUnknown $ sub $? k

139+ tidyUp (k, sub) = starIfUnknown $ substituteKind sub k

107140

108−freshKindVar :: (String, Maybe Kind) -> Kind -> UnifyT Kind Check (ProperName, Kind)

141+freshKindVar ::

142+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) =>

143+ (String, Maybe Kind) ->

144+ Kind ->

145+ m (ProperName, Kind)

109146freshKindVar (arg, Nothing) kind = return (ProperName arg, kind)

110147freshKindVar (arg, Just kind') kind = do

111− kind =?= kind'

148+ unifyKinds kind kind'

112149 return (ProperName arg, kind')

113150

114−-- |

115−-- Simultaneously infer the kinds of several mutually recursive type constructors

116−--

117−kindsOfAll :: ModuleName -> [(ProperName, [(String, Maybe Kind)], Type)] -> [(ProperName, [(String, Maybe Kind)], [Type])] -> Check ([Kind], [Kind])

151+-- | Simultaneously infer the kinds of several mutually recursive type constructors

152+kindsOfAll ::

153+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m) =>

154+ ModuleName ->

155+ [(ProperName, [(String, Maybe Kind)], Type)] ->

156+ [(ProperName, [(String, Maybe Kind)], [Type])] ->

157+ m ([Kind], [Kind])

118158kindsOfAll moduleName syns tys = fmap tidyUp . liftUnify $ do

119− synVars <- replicateM (length syns) fresh

159+ synVars <- replicateM (length syns) freshKind

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

121161 bindLocalTypeVariables moduleName dict $ do

122− tyCons <- replicateM (length tys) fresh

162+ tyCons <- replicateM (length tys) freshKind

123163 let dict' = zipWith (\(name, _, _) tyCon -> (name, tyCon)) tys tyCons

124164 bindLocalTypeVariables moduleName dict' $ do

125165 data_ks <- zipWithM (\tyCon (_, args, ts) -> do

126− kargs <- replicateM (length args) fresh

166+ kargs <- replicateM (length args) freshKind

127167 argDict <- zipWithM freshKindVar args kargs

128168 bindLocalTypeVariables moduleName argDict $

129169 solveTypes True ts kargs tyCon) tyCons tys

130170 syn_ks <- zipWithM (\synVar (_, args, ty) -> do

131− kargs <- replicateM (length args) fresh

171+ kargs <- replicateM (length args) freshKind

132172 argDict <- zipWithM freshKindVar args kargs

133173 bindLocalTypeVariables moduleName argDict $

134174 solveTypes False [ty] kargs synVar) synVars syns

135175 return (syn_ks, data_ks)

136176 where

137− tidyUp ((ks1, ks2), sub) = (map (starIfUnknown . (sub $?)) ks1, map (starIfUnknown . (sub $?)) ks2)

177+ tidyUp ((ks1, ks2), sub) = (map (starIfUnknown . substituteKind sub) ks1, map (starIfUnknown . substituteKind sub) ks2)

138178

139−-- |

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

141−--

142−solveTypes :: Bool -> [Type] -> [Kind] -> Kind -> UnifyT Kind Check Kind

179+-- | Solve the set of kind constraints associated with the data constructors for a type constructor

180+solveTypes :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Bool -> [Type] -> [Kind] -> Kind -> m Kind

143181solveTypes isData ts kargs tyCon = do

144182 ks <- mapM (fmap fst . infer) ts

145183 when isData $ do

146− tyCon =?= foldr FunKind Star kargs

147− forM_ ks $ \k -> k =?= Star

184+ unifyKinds tyCon (foldr FunKind Star kargs)

185+ forM_ ks $ \k -> unifyKinds k Star

148186 unless isData $

149− tyCon =?= foldr FunKind (head ks) kargs

187+ unifyKinds tyCon (foldr FunKind (head ks) kargs)

150188 return tyCon

151189

152−-- |

153−-- Default all unknown kinds to the Star kind of types

154−--

190+-- | Default all unknown kinds to the Star kind of types

155191starIfUnknown :: Kind -> Kind

156192starIfUnknown (KUnknown _) = Star

157193starIfUnknown (Row k) = Row (starIfUnknown k)

158194starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)

159195starIfUnknown k = k

160196

161−-- |

162−-- Infer a kind for a type

163−--

164−infer :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])

197+-- | Infer a kind for a type

198+infer :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Type -> m (Kind, [(String, Kind)])

165199infer ty = rethrow (addHint (ErrorCheckingKind ty)) $ infer' ty

166200

167−infer' :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])

201+infer' :: forall m. (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Type -> m (Kind, [(String, Kind)])

168202infer' (ForAll ident ty _) = do

169− k1 <- fresh

203+ k1 <- freshKind

170204 Just moduleName <- checkCurrentModule <$> get

171205 (k2, args) <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty

172− k2 =?= Star

206+ unifyKinds k2 Star

173207 return (Star, (ident, k1) : args)

174208infer' (KindedType ty k) = do

175209 (k', args) <- infer ty

176− k =?= k'

210+ unifyKinds k k'

177211 return (k', args)

178212infer' other = (, []) <$> go other

179213 where

180− go :: Type -> UnifyT Kind Check Kind

214+ go :: Type -> m Kind

181215 go (ForAll ident ty _) = do

182− k1 <- fresh

216+ k1 <- freshKind

183217 Just moduleName <- checkCurrentModule <$> get

184218 k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ go ty

185− k2 =?= Star

219+ unifyKinds k2 Star

186220 return Star

187221 go (KindedType ty k) = do

188222 k' <- go ty

189− k =?= k'

223+ unifyKinds k k'

190224 return k'

191− go TypeWildcard = fresh

225+ go TypeWildcard = freshKind

192226 go (TypeVar v) = do

193227 Just moduleName <- checkCurrentModule <$> get

194− UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

228+ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

195229 go (Skolem v _ _) = do

196230 Just moduleName <- checkCurrentModule <$> get

197− UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

231+ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))

198232 go (TypeConstructor v) = do

199− env <- liftCheck getEnv

233+ env <- getEnv

200234 case M.lookup v (types env) of

201− Nothing -> UnifyT . lift . throwError . errorMessage $ UnknownTypeConstructor v

235+ Nothing -> throwError . errorMessage $ UnknownTypeConstructor v

202236 Just (kind, _) -> return kind

203237 go (TypeApp t1 t2) = do

204− k0 <- fresh

238+ k0 <- freshKind

205239 k1 <- go t1

206240 k2 <- go t2

207− k1 =?= FunKind k2 k0

241+ unifyKinds k1 (FunKind k2 k0)

208242 return k0

209243 go REmpty = do

210− k <- fresh

244+ k <- freshKind

211245 return $ Row k

212246 go (RCons _ ty row) = do

213247 k1 <- go ty

214248 k2 <- go row

215− k2 =?= Row k1

249+ unifyKinds k2 (Row k1)

216250 return $ Row k1

217251 go (ConstrainedType deps ty) = do

218252 forM_ deps $ \(className, tys) -> do

219253 k <- go $ foldl TypeApp (TypeConstructor className) tys

220− k =?= Star

254+ unifyKinds k Star

221255 k <- go ty

222− k =?= Star

256+ unifyKinds k Star

223257 return Star

224258 go _ = internalError "Invalid argument to infer"

src/Language/PureScript/TypeChecker/Monad.hs+82−131

@@ -27,13 +27,13 @@ import Data.Maybe

2727import qualified Data.Map as M

2828

2929#if __GLASGOW_HASKELL__ < 710

30+import Data.Monoid

3031import Control.Applicative

3132#endif

33+import Control.Arrow (second)

3234import Control.Monad.State

33−import Control.Monad.Unify

34−import Control.Monad.Writer.Strict

3535import Control.Monad.Error.Class (MonadError(..))

36−import Control.Monad.Trans.Except

36+import Control.Monad.Writer.Class (MonadWriter(..), listen, censor)

3737

3838import Language.PureScript.Environment

3939import Language.PureScript.Errors

@@ -42,9 +42,36 @@ import Language.PureScript.Names

4242import Language.PureScript.TypeClassDictionaries

4343import Language.PureScript.Types

4444

45−-- |

46−-- Temporarily bind a collection of names to values

47−--

45+-- | A substitution of unification variables for types or kinds

46+data Substitution = Substitution

47+ { substType :: M.Map Int Type -- ^ Type substitution

48+ , substKind :: M.Map Int Kind -- ^ Kind substitution

49+ }

50+

51+-- | An empty substitution

52+emptySubstitution :: Substitution

53+emptySubstitution = Substitution M.empty M.empty

54+

55+-- | State required for type checking

56+data CheckState = CheckState

57+ { checkEnv :: Environment -- ^ The current @Environment@

58+ , checkNextType :: Int -- ^ The next type unification variable

59+ , checkNextKind :: Int -- ^ The next kind unification variable

60+ , checkNextSkolem :: Int -- ^ The next skolem variable

61+ , checkNextSkolemScope :: Int -- ^ The next skolem scope constant

62+ , checkNextDictName :: Int -- ^ The next type class dictionary name

63+ , checkCurrentModule :: Maybe ModuleName -- ^ The current module

64+ , checkSubstitution :: Substitution -- ^ The current substitution

65+ }

66+

67+-- | Create an empty @CheckState@

68+emptyCheckState :: Environment -> CheckState

69+emptyCheckState env = CheckState env 0 0 0 0 0 Nothing emptySubstitution

70+

71+-- | Unification variables

72+type Unknown = Int

73+

74+-- | Temporarily bind a collection of names to values

4875bindNames :: (MonadState CheckState m) => M.Map (ModuleName, Ident) (Type, NameKind, NameVisibility) -> m a -> m a

4976bindNames newNames action = do

5077 orig <- get

@@ -53,9 +80,7 @@ bindNames newNames action = do

5380 modify $ \st -> st { checkEnv = (checkEnv st) { names = names . checkEnv $ orig } }

5481 return a

5582

56−-- |

57−-- Temporarily bind a collection of names to types

58−--

83+-- | Temporarily bind a collection of names to types

5984bindTypes :: (MonadState CheckState m) => M.Map (Qualified ProperName) (Kind, TypeKind) -> m a -> m a

6085bindTypes newNames action = do

6186 orig <- get

@@ -64,15 +89,11 @@ bindTypes newNames action = do

6489 modify $ \st -> st { checkEnv = (checkEnv st) { types = types . checkEnv $ orig } }

6590 return a

6691

67−-- |

68−-- Temporarily bind a collection of names to types

69−--

92+-- | Temporarily bind a collection of names to types

7093withScopedTypeVars :: (Functor m, MonadState CheckState m) => ModuleName -> [(String, Kind)] -> m a -> m a

7194withScopedTypeVars mn ks = bindTypes (M.fromList (map (\(name, k) -> (Qualified (Just mn) (ProperName name), (k, ScopedTypeVar))) ks))

7295

73−-- |

74−-- Temporarily make a collection of type class dictionaries available

75−--

96+-- | Temporarily make a collection of type class dictionaries available

7697withTypeClassDictionaries :: (MonadState CheckState m) => [TypeClassDictionaryInScope] -> m a -> m a

7798withTypeClassDictionaries entries action = do

7899 orig <- get

@@ -82,35 +103,30 @@ withTypeClassDictionaries entries action = do

82103 modify $ \st -> st { checkEnv = (checkEnv st) { typeClassDictionaries = typeClassDictionaries . checkEnv $ orig } }

83104 return a

84105

85−-- |

86−-- Get the currently available map of type class dictionaries

87−--

88−getTypeClassDictionaries :: (Functor m, MonadState CheckState m) => m (M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)))

106+-- | Get the currently available map of type class dictionaries

107+getTypeClassDictionaries ::

108+ (Functor m, MonadState CheckState m) =>

109+ m (M.Map (Maybe ModuleName) (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope)))

89110getTypeClassDictionaries = typeClassDictionaries . checkEnv <$> get

90111

91−-- |

92−-- Lookup type class dictionaries in a module.

93−--

94−lookupTypeClassDictionaries :: (Functor m, MonadState CheckState m) => Maybe ModuleName -> m (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope))

112+-- | Lookup type class dictionaries in a module.

113+lookupTypeClassDictionaries ::

114+ (Functor m, MonadState CheckState m) =>

115+ Maybe ModuleName ->

116+ m (M.Map (Qualified ProperName) (M.Map (Qualified Ident) TypeClassDictionaryInScope))

95117lookupTypeClassDictionaries mn = fromMaybe M.empty . M.lookup mn . typeClassDictionaries . checkEnv <$> get

96118

97−-- |

98−-- Temporarily bind a collection of names to local variables

99−--

119+-- | Temporarily bind a collection of names to local variables

100120bindLocalVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(Ident, Type, NameVisibility)] -> m a -> m a

101121bindLocalVariables moduleName bindings =

102122 bindNames (M.fromList $ flip map bindings $ \(name, ty, visibility) -> ((moduleName, name), (ty, Private, visibility)))

103123

104−-- |

105−-- Temporarily bind a collection of names to local type variables

106−--

124+-- | Temporarily bind a collection of names to local type variables

107125bindLocalTypeVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(ProperName, Kind)] -> m a -> m a

108126bindLocalTypeVariables moduleName bindings =

109127 bindTypes (M.fromList $ flip map bindings $ \(pn, kind) -> (Qualified (Just moduleName) pn, (kind, LocalTypeVariable)))

110128

111−-- |

112−-- Update the visibility of all names to Defined

113−--

129+-- | Update the visibility of all names to Defined

114130makeBindingGroupVisible :: (Functor m, MonadState CheckState m) => m ()

115131makeBindingGroupVisible = modifyEnv $ \e -> e { names = M.map (\(ty, nk, _) -> (ty, nk, Defined)) (names e) }

116132

@@ -126,9 +142,7 @@ preservingNames action = do

126142 modifyEnv $ \e -> e { names = orig }

127143 return a

128144

129−-- |

130−-- Lookup the type of a value by name in the @Environment@

131−--

145+-- | Lookup the type of a value by name in the @Environment@

132146lookupVariable :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified Ident -> m Type

133147lookupVariable currentModule (Qualified moduleName var) = do

134148 env <- getEnv

@@ -136,9 +150,7 @@ lookupVariable currentModule (Qualified moduleName var) = do

136150 Nothing -> throwError . errorMessage $ NameIsUndefined var

137151 Just (ty, _, _) -> return ty

138152

139−-- |

140−-- Lookup the visibility of a value by name in the @Environment@

141−--

153+-- | Lookup the visibility of a value by name in the @Environment@

142154getVisibility :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified Ident -> m NameVisibility

143155getVisibility currentModule (Qualified moduleName var) = do

144156 env <- getEnv

@@ -146,9 +158,7 @@ getVisibility currentModule (Qualified moduleName var) = do

146158 Nothing -> throwError . errorMessage $ NameIsUndefined var

147159 Just (_, _, vis) -> return vis

148160

149−-- |

150−-- Assert that a name is visible

151−--

161+-- | Assert that a name is visible

152162checkVisibility :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified Ident -> m ()

153163checkVisibility currentModule name@(Qualified _ var) = do

154164 vis <- getVisibility currentModule name

@@ -156,9 +166,7 @@ checkVisibility currentModule name@(Qualified _ var) = do

156166 Undefined -> throwError . errorMessage $ CycleInDeclaration var

157167 _ -> return ()

158168

159−-- |

160−-- Lookup the kind of a type by name in the @Environment@

161−--

169+-- | Lookup the kind of a type by name in the @Environment@

162170lookupTypeVariable :: (e ~ MultipleErrors, Functor m, MonadState CheckState m, MonadError e m) => ModuleName -> Qualified ProperName -> m Kind

163171lookupTypeVariable currentModule (Qualified moduleName name) = do

164172 env <- getEnv

@@ -166,113 +174,56 @@ lookupTypeVariable currentModule (Qualified moduleName name) = do

166174 Nothing -> throwError . errorMessage $ UndefinedTypeVariable name

167175 Just (k, _) -> return k

168176

169−-- |

170−-- State required for type checking:

171−--

172−data CheckState = CheckState {

173− -- |

174− -- The current @Environment@

175− --

176− checkEnv :: Environment

177− -- |

178− -- The next fresh unification variable name

179− --

180− , checkNextVar :: Int

181− -- |

182− -- The next type class dictionary name

183− --

184− , checkNextDictName :: Int

185− -- |

186− -- The current module

187− --

188− , checkCurrentModule :: Maybe ModuleName

189− }

190−

191−-- |

192−-- The type checking monad, which provides the state of the type checker, and error reporting capabilities

193−--

194−newtype Check a = Check { unCheck :: StateT CheckState (ExceptT MultipleErrors (Writer MultipleErrors)) a }

195− deriving (Functor, Monad, Applicative, MonadState CheckState, MonadError MultipleErrors, MonadWriter MultipleErrors)

196−

197−-- |

198−-- Get the current @Environment@

199−--

177+-- | Get the current @Environment@

200178getEnv :: (Functor m, MonadState CheckState m) => m Environment

201179getEnv = checkEnv <$> get

202180

203−-- |

204−-- Update the @Environment@

205−--

181+-- | Update the @Environment@

206182putEnv :: (MonadState CheckState m) => Environment -> m ()

207183putEnv env = modify (\s -> s { checkEnv = env })

208184

209−-- |

210−-- Modify the @Environment@

211−--

185+-- | Modify the @Environment@

212186modifyEnv :: (MonadState CheckState m) => (Environment -> Environment) -> m ()

213187modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })

214188

215−-- |

216−-- Run a computation in the Check monad, starting with an empty @Environment@

217−--

218−runCheck :: (MonadError MultipleErrors m, MonadWriter MultipleErrors m) => Check a -> m (a, Environment)

189+-- | Run a computation in the typechecking monad, starting with an empty @Environment@

190+runCheck :: (Functor m) => StateT CheckState m a -> m (a, Environment)

219191runCheck = runCheck' initEnvironment

220192

221−-- |

222−-- Run a computation in the Check monad, failing with an error, or succeeding with a return value and the final @Environment@.

223−--

224−runCheck' :: (MonadError MultipleErrors m, MonadWriter MultipleErrors m) => Environment -> Check a -> m (a, Environment)

225−runCheck' env = interpretMultipleErrorsAndWarnings . unwrapCheckWithWarnings env

226− where

227− unwrapCheckWithWarnings :: Environment -> Check a -> (Either MultipleErrors (a, Environment), MultipleErrors)

228− unwrapCheckWithWarnings e =

229− (\(rc, w) -> (envCheck rc, w))

230− . runWriter

231− . runExceptT

232− . flip runStateT (CheckState e 0 0 Nothing)

233− . unCheck

234− envCheck :: Either MultipleErrors (a, CheckState) -> Either MultipleErrors (a, Environment)

235− envCheck rc = do

236− (a, s) <- rc

237− return (a, checkEnv s)

193+-- | Run a computation in the typechecking monad, failing with an error, or succeeding with a return value and the final @Environment@.

194+runCheck' :: (Functor m) => Environment -> StateT CheckState m a -> m (a, Environment)

195+runCheck' env check = fmap (second checkEnv) $ runStateT check (emptyCheckState env)

238196

239−-- |

240−-- Make an assertion, failing with an error message

241−--

197+-- | Make an assertion, failing with an error message

242198guardWith :: (MonadError e m) => e -> Bool -> m ()

243199guardWith _ True = return ()

244200guardWith e False = throwError e

245201

246−-- |

247−-- Generate new type class dictionary name

248−--

249−freshDictionaryName :: Check Int

202+-- | Generate new type class dictionary name

203+freshDictionaryName :: (Functor m, MonadState CheckState m) => m Int

250204freshDictionaryName = do

251205 n <- checkNextDictName <$> get

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

253207 return n

254208

255−-- |

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

257−--

258−liftCheck :: Check a -> UnifyT t Check a

259−liftCheck = UnifyT . lift

260−

261−-- |

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

263−--

264−liftUnify :: (Partial t) => UnifyT t Check a -> Check (a, Substitution t)

209+-- | Run a computation in the substitution monad, generating a return value and the final substitution.

210+liftUnify ::

211+ (MonadState CheckState m, MonadWriter MultipleErrors m) =>

212+ m a ->

213+ m (a, Substitution)

265214liftUnify = liftUnifyWarnings (const id)

266215

267−-- |

268−-- Run a computation in the substitution monad, generating a return value, the final substitution and updating warnings values.

269−--

270−liftUnifyWarnings :: (Partial t) => (Substitution t -> ErrorMessage -> ErrorMessage) -> UnifyT t Check a -> Check (a, Substitution t)

271−liftUnifyWarnings replace unify = do

272− st <- get

273− let ru = runUnify (defaultUnifyState { unifyNextVar = checkNextVar st }) unify

274− ((a, ust), w) <- censor (const mempty) . listen $ ru

275− modify $ \st' -> st' { checkNextVar = unifyNextVar ust }

276− let uust = unifyCurrentSubstitution ust

277− tell $ onErrorMessages (replace uust) w

278− return (a, uust)

216+-- | Run a computation in the substitution monad, generating a return value, the final substitution and updating warnings values.

217+liftUnifyWarnings ::

218+ (MonadState CheckState m, MonadWriter MultipleErrors m) =>

219+ (Substitution -> ErrorMessage -> ErrorMessage) ->

220+ m a ->

221+ m (a, Substitution)

222+liftUnifyWarnings replace ma = do

223+ orig <- get

224+ modify $ \st -> st { checkSubstitution = emptySubstitution }

225+ (a, w) <- censor (const mempty) . listen $ ma

226+ subst <- gets checkSubstitution

227+ tell . onErrorMessages (replace subst) $ w

228+ modify $ \st -> st { checkSubstitution = checkSubstitution orig }

229+ return (a, subst)

src/Language/PureScript/TypeChecker/Rows.hs+13−7

@@ -13,38 +13,44 @@

1313--

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

1515

16+{-# LANGUAGE ScopedTypeVariables #-}

17+{-# LANGUAGE FlexibleContexts #-}

18+{-# LANGUAGE CPP #-}

19+

1620module Language.PureScript.TypeChecker.Rows (

1721 checkDuplicateLabels

1822) where

1923

2024import Data.List

2125

26+#if __GLASGOW_HASKELL__ < 710

27+import Control.Applicative

28+#endif

2229import Control.Monad

2330import Control.Monad.Error.Class (MonadError(..))

31+import Control.Monad.State.Class (MonadState(..))

2432

2533import Language.PureScript.AST

2634import Language.PureScript.Errors

2735import Language.PureScript.TypeChecker.Monad

2836import Language.PureScript.Types

2937

30−-- |

31−-- Ensure rows do not contain duplicate labels

32−--

33−checkDuplicateLabels :: Expr -> Check ()

38+-- | Ensure rows do not contain duplicate labels

39+checkDuplicateLabels :: forall m. (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Expr -> m ()

3440checkDuplicateLabels =

3541 let (_, f, _) = everywhereOnValuesM def go def

3642 in void . f

3743 where

38− def :: a -> Check a

44+ def :: a -> m a

3945 def = return

4046

41− go :: Expr -> Check Expr

47+ go :: Expr -> m Expr

4248 go e@(TypedValue _ val ty) = do

4349 checkDups ty

4450 return e

4551

4652 where

47− checkDups :: Type -> Check ()

53+ checkDups :: Type -> m ()

4854 checkDups (TypeApp t1 t2) = checkDups t1 >> checkDups t2

4955 checkDups (ForAll _ t _) = checkDups t

5056 checkDups (ConstrainedType args t) = do

src/Language/PureScript/TypeChecker/Skolems.hs+14−7

@@ -14,6 +14,7 @@

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

1515

1616{-# LANGUAGE CPP #-}

17+{-# LANGUAGE FlexibleContexts #-}

1718

1819module Language.PureScript.TypeChecker.Skolems (

1920 newSkolemConstant,

@@ -31,7 +32,7 @@ import Data.Monoid

3132import Control.Applicative

3233#endif

3334import Control.Monad.Error.Class (MonadError(..))

34−import Control.Monad.Unify

35+import Control.Monad.State.Class (MonadState(..), gets, modify)

3536

3637import Language.PureScript.Crash

3738import Language.PureScript.AST

@@ -42,13 +43,16 @@ import Language.PureScript.Types

4243-- |

4344-- Generate a new skolem constant

4445--

45−newSkolemConstant :: UnifyT Type Check Int

46−newSkolemConstant = fresh'

46+newSkolemConstant :: (MonadState CheckState m) => m Int

47+newSkolemConstant = do

48+ s <- gets checkNextSkolem

49+ modify $ \st -> st { checkNextSkolem = s + 1 }

50+ return s

4751

4852-- |

4953-- Introduce skolem scope at every occurence of a ForAll

5054--

51−introduceSkolemScope :: Type -> UnifyT Type Check Type

55+introduceSkolemScope :: (Functor m, Applicative m, MonadState CheckState m) => Type -> m Type

5256introduceSkolemScope = everywhereOnTypesM go

5357 where

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

@@ -57,8 +61,11 @@ introduceSkolemScope = everywhereOnTypesM go

5761-- |

5862-- Generate a new skolem scope

5963--

60−newSkolemScope :: UnifyT Type Check SkolemScope

61−newSkolemScope = SkolemScope <$> fresh'

64+newSkolemScope :: (MonadState CheckState m) => m SkolemScope

65+newSkolemScope = do

66+ s <- gets checkNextSkolemScope

67+ modify $ \st -> st { checkNextSkolemScope = s + 1 }

68+ return $ SkolemScope s

6269

6370-- |

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

@@ -86,7 +93,7 @@ skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id on

8693-- |

8794-- Ensure skolem variables do not escape their scope

8895--

89−skolemEscapeCheck :: Expr -> Check ()

96+skolemEscapeCheck :: (MonadError MultipleErrors m, MonadState CheckState m) => Expr -> m ()

9097skolemEscapeCheck (TypedValue False _ _) = return ()

9198skolemEscapeCheck root@TypedValue{} =

9299 -- Every skolem variable is created when a ForAll type is skolemized.

src/Language/PureScript/TypeChecker/Subsumption.hs+23−17

@@ -13,6 +13,9 @@

1313--

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

1515

16+{-# LANGUAGE FlexibleContexts #-}

17+{-# LANGUAGE CPP #-}

18+

1619module Language.PureScript.TypeChecker.Subsumption (

1720 subsumes

1821) where

@@ -20,8 +23,11 @@ module Language.PureScript.TypeChecker.Subsumption (

2023import Data.List (sortBy)

2124import Data.Ord (comparing)

2225

23−import Control.Monad.Unify

24−import Control.Monad.Error.Class (throwError)

26+#if __GLASGOW_HASKELL__ < 710

27+import Control.Applicative

28+#endif

29+import Control.Monad.Error.Class (MonadError(..))

30+import Control.Monad.State.Class (MonadState(..))

2531

2632import Language.PureScript.Crash

2733import Language.PureScript.AST

@@ -32,16 +38,16 @@ import Language.PureScript.TypeChecker.Skolems

3238import Language.PureScript.TypeChecker.Unify

3339import Language.PureScript.Types

3440

35−-- |

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

37−--

38−subsumes :: Maybe Expr -> Type -> Type -> UnifyT Type Check (Maybe Expr)

41+-- | Check that one type subsumes another, rethrowing errors to provide a better error message

42+subsumes :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Maybe Expr -> Type -> Type -> m (Maybe Expr)

3943subsumes val ty1 ty2 = rethrow (addHint (ErrorInSubsumption ty1 ty2)) $ subsumes' val ty1 ty2

4044

41−-- |

42−-- Check whether one type subsumes another

43−--

44−subsumes' :: Maybe Expr -> Type -> Type -> UnifyT Type Check (Maybe Expr)

45+-- | Check tahat one type subsumes another

46+subsumes' :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) =>

47+ Maybe Expr ->

48+ Type ->

49+ Type ->

50+ m (Maybe Expr)

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

4652 replaced <- replaceVarWithUnknown ident ty1

4753 subsumes val replaced ty2

@@ -72,25 +78,25 @@ subsumes' val (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyObject && f2 == tyObject

7278 go ts1' ts2' r1' r2'

7379 return val

7480 where

75− go [] ts2 r1' r2' = r1' =?= rowFromList (ts2, r2')

76− go ts1 [] r1' r2' = r2' =?= rowFromList (ts1, r1')

81+ go [] ts2 r1' r2' = unifyTypes r1' (rowFromList (ts2, r2'))

82+ go ts1 [] r1' r2' = unifyTypes r2' (rowFromList (ts1, r1'))

7783 go ((p1, ty1) : ts1) ((p2, ty2) : ts2) r1' r2'

7884 | p1 == p2 = do _ <- subsumes Nothing ty1 ty2

7985 go ts1 ts2 r1' r2'

80− | p1 < p2 = do rest <- fresh

86+ | p1 < p2 = do rest <- freshType

8187 -- What happens next is a bit of a hack.

8288 -- TODO: in the new type checker, object properties will probably be restricted to being monotypes

8389 -- in which case, this branch of the subsumes function should not even be necessary.

8490 case r2' of

8591 REmpty -> throwError . errorMessage $ AdditionalProperty p1

86− _ -> r2' =?= RCons p1 ty1 rest

92+ _ -> unifyTypes r2' (RCons p1 ty1 rest)

8793 go ts1 ((p2, ty2) : ts2) r1' rest

88− | otherwise = do rest <- fresh

94+ | otherwise = do rest <- freshType

8995 case r1' of

9096 REmpty -> throwError . errorMessage $ PropertyIsMissing p2

91− _ -> r1' =?= RCons p2 ty2 rest

97+ _ -> unifyTypes r1' (RCons p2 ty2 rest)

9298 go ((p1, ty1) : ts1) ts2 rest r2'

9399subsumes' val ty1 ty2@(TypeApp obj _) | obj == tyObject = subsumes val ty2 ty1

94100subsumes' val ty1 ty2 = do

95− ty1 =?= ty2

101+ unifyTypes ty1 ty2

96102 return val

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

@@ -14,6 +14,7 @@

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

1515

1616{-# LANGUAGE FlexibleContexts #-}

17+{-# LANGUAGE ScopedTypeVariables #-}

1718{-# LANGUAGE MultiParamTypeClasses #-}

1819{-# LANGUAGE OverloadedStrings #-}

1920{-# LANGUAGE CPP #-}

@@ -47,10 +48,9 @@ import qualified Data.Map as M

4748import Control.Applicative

4849#endif

4950import Control.Monad

50−import Control.Monad.State

51−import Control.Monad.Unify

51+import Control.Monad.State.Class (MonadState(..), gets)

5252import Control.Monad.Error.Class (MonadError(..))

53−import Control.Monad.Writer.Class (tell)

53+import Control.Monad.Writer.Class (MonadWriter(..))

5454

5555import Language.PureScript.Crash

5656import Language.PureScript.AST

@@ -70,11 +70,13 @@ import Language.PureScript.TypeChecker.Unify

7070import Language.PureScript.TypeClassDictionaries

7171import Language.PureScript.Types

7272

73−-- |

74−-- Infer the types of multiple mutually-recursive values, and return elaborated values including

73+-- | Infer the types of multiple mutually-recursive values, and return elaborated values including

7574-- type class dictionaries and type annotations.

76−--

77−typesOf :: ModuleName -> [(Ident, Expr)] -> Check [(Ident, (Expr, Type))]

75+typesOf ::

76+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

77+ ModuleName ->

78+ [(Ident, Expr)] ->

79+ m [(Ident, (Expr, Type))]

7880typesOf moduleName vals = do

7981 tys <- fmap tidyUp . liftUnifyWarnings replace $ do

8082 (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName vals

@@ -92,17 +94,21 @@ typesOf moduleName vals = do

9294 return (ident, (val', varIfUnknown ty))

9395 where

9496 -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values

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

97+ tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (substituteType sub) val, substituteType sub ty))) ts

9698 -- Replace all the wildcards types with their inferred types

97− replace sub (ErrorMessage hints (WildcardInferredType ty)) = ErrorMessage hints $ WildcardInferredType (sub $? ty)

98− replace sub (ErrorMessage hints (MissingTypeDeclaration name ty)) = ErrorMessage hints $ MissingTypeDeclaration name (varIfUnknown (sub $? ty))

99+ replace sub (ErrorMessage hints (WildcardInferredType ty)) = ErrorMessage hints . WildcardInferredType $ substituteType sub ty

100+ replace sub (ErrorMessage hints (MissingTypeDeclaration name ty)) = ErrorMessage hints $ MissingTypeDeclaration name (varIfUnknown (substituteType sub ty))

99101 replace _ em = em

100102

101103type TypeData = M.Map (ModuleName, Ident) (Type, NameKind, NameVisibility)

102104

103105type UntypedData = [(Ident, Type)]

104106

105−typeDictionaryForBindingGroup :: ModuleName -> [(Ident, Expr)] -> UnifyT Type Check ([(Ident, Expr)], [(Ident, (Expr, Type, Bool))], TypeData, UntypedData)

107+typeDictionaryForBindingGroup ::

108+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

109+ ModuleName ->

110+ [(Ident, Expr)] ->

111+ m ([(Ident, Expr)], [(Ident, (Expr, Type, Bool))], TypeData, UntypedData)

106112typeDictionaryForBindingGroup moduleName vals = do

107113 let

108114 -- Map each declaration to a name/value pair, with an optional type, if the declaration is typed

@@ -114,7 +120,7 @@ typeDictionaryForBindingGroup moduleName vals = do

114120 typedDict = map (\(ident, (_, ty, _)) -> (ident, ty)) typed

115121

116122 -- Create fresh unification variables for the types of untyped declarations

117− untypedNames <- replicateM (length untyped) fresh

123+ untypedNames <- replicateM (length untyped) freshType

118124

119125 let

120126 -- Make a map of names to the unification variables of untyped declarations

@@ -123,12 +129,17 @@ typeDictionaryForBindingGroup moduleName vals = do

123129 dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, Private, Undefined))) $ typedDict ++ untypedDict)

124130 return (untyped, typed, dict, untypedDict)

125131

126−checkTypedBindingGroupElement :: ModuleName -> (Ident, (Expr, Type, Bool)) -> TypeData -> UnifyT Type Check (Ident, (Expr, Type))

132+checkTypedBindingGroupElement ::

133+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

134+ ModuleName ->

135+ (Ident, (Expr, Type, Bool)) ->

136+ TypeData ->

137+ m (Ident, (Expr, Type))

127138checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do

128139 -- Replace type wildcards

129140 ty' <- replaceTypeWildcards ty

130141 -- Kind check

131− (kind, args) <- liftCheck $ kindOfWithScopedVars ty

142+ (kind, args) <- kindOfWithScopedVars ty

132143 checkTypeKind ty kind

133144 -- Check the type with the new names in scope

134145 ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'

@@ -137,17 +148,21 @@ checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do

137148 else return (TypedValue False val' ty'')

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

139150

140−typeForBindingGroupElement :: Bool -> (Ident, Expr) -> TypeData -> UntypedData -> UnifyT Type Check (Ident, (Expr, Type))

151+typeForBindingGroupElement ::

152+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

153+ Bool ->

154+ (Ident, Expr) ->

155+ TypeData ->

156+ UntypedData ->

157+ m (Ident, (Expr, Type))

141158typeForBindingGroupElement warn (ident, val) dict untypedDict = do

142159 -- Infer the type with the new names in scope

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

144− ty =?= fromMaybe (internalError "name not found in dictionary") (lookup ident untypedDict)

161+ unifyTypes ty $ fromMaybe (internalError "name not found in dictionary") (lookup ident untypedDict)

145162 when warn . tell . errorMessage $ MissingTypeDeclaration ident ty

146163 return (ident, (TypedValue True val' ty, ty))

147164

148−-- |

149−-- Check if a value contains a type annotation

150−--

165+-- | Check if a value contains a type annotation

151166isTyped :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))

152167isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))

153168isTyped (name, value) = Left (name, value)

@@ -163,10 +178,12 @@ overTypes f = let (_, f', _) = everywhereOnValues id g id in f'

163178 g (TypeClassDictionary (nm, tys) sco) = TypeClassDictionary (nm, map f tys) sco

164179 g other = other

165180

166−-- |

167−-- Replace type class dictionary placeholders with inferred type class dictionaries

168−--

169−replaceTypeClassDictionaries :: ModuleName -> Expr -> Check Expr

181+-- | Replace type class dictionary placeholders with inferred type class dictionaries

182+replaceTypeClassDictionaries ::

183+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

184+ ModuleName ->

185+ Expr ->

186+ m Expr

170187replaceTypeClassDictionaries mn =

171188 let (_, f, _) = everywhereOnValuesTopDownM return go return

172189 in f

@@ -174,20 +191,24 @@ replaceTypeClassDictionaries mn =

174191 go (TypeClassDictionary constraint dicts) = entails mn dicts constraint

175192 go other = return other

176193

177−-- |

178−-- Check the kind of a type, failing if it is not of kind *.

179−--

180−checkTypeKind :: Type -> Kind -> UnifyT t Check ()

194+-- | Check the kind of a type, failing if it is not of kind *.

195+checkTypeKind ::

196+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>

197+ Type ->

198+ Kind ->

199+ m ()

181200checkTypeKind ty kind = guardWith (errorMessage (ExpectedType ty kind)) $ kind == Star

182201

183−-- |

184−-- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns

202+-- | Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns

185203-- or TypeClassDictionary values.

186204--

187205-- This is necessary during type checking to avoid unifying a polymorphic type with a

188206-- unification variable.

189−--

190−instantiatePolyTypeWithUnknowns :: Expr -> Type -> UnifyT Type Check (Expr, Type)

207+instantiatePolyTypeWithUnknowns ::

208+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>

209+ Expr ->

210+ Type ->

211+ m (Expr, Type)

191212instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do

192213 ty' <- replaceVarWithUnknown ident ty

193214 instantiatePolyTypeWithUnknowns val ty'

@@ -197,16 +218,18 @@ instantiatePolyTypeWithUnknowns val (ConstrainedType constraints ty) = do

197218 return (foldl App val (map (flip TypeClassDictionary dicts) constraints), ty')

198219instantiatePolyTypeWithUnknowns val ty = return (val, ty)

199220

200−-- |

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

202−--

203−infer :: Expr -> UnifyT Type Check Expr

221+-- | Infer a type for a value, rethrowing any error to provide a more useful error message

222+infer ::

223+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

224+ Expr ->

225+ m Expr

204226infer val = rethrow (addHint (ErrorInferringType val)) $ infer' val

205227

206−-- |

207−-- Infer a type for a value

208−--

209−infer' :: Expr -> UnifyT Type Check Expr

228+-- | Infer a type for a value

229+infer' ::

230+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

231+ Expr ->

232+ m Expr

210233infer' v@(NumericLiteral (Left _)) = return $ TypedValue True v tyInt

211234infer' v@(NumericLiteral (Right _)) = return $ TypedValue True v tyNumber

212235infer' v@(StringLiteral _) = return $ TypedValue True v tyString

@@ -214,8 +237,8 @@ infer' v@(CharLiteral _) = return $ TypedValue True v tyChar

214237infer' v@(BooleanLiteral _) = return $ TypedValue True v tyBoolean

215238infer' (ArrayLiteral vals) = do

216239 ts <- mapM infer vals

217− els <- fresh

218− forM_ ts $ \(TypedValue _ _ t) -> els =?= t

240+ els <- freshType

241+ forM_ ts $ \(TypedValue _ _ t) -> unifyTypes els t

219242 return $ TypedValue True (ArrayLiteral ts) (TypeApp tyArray els)

220243infer' (ObjectLiteral ps) = do

221244 ensureNoDuplicateProperties ps

@@ -225,20 +248,20 @@ infer' (ObjectLiteral ps) = do

225248 return $ TypedValue True (ObjectLiteral (zip (map fst ps) ts)) ty

226249infer' (ObjectUpdate o ps) = do

227250 ensureNoDuplicateProperties ps

228− row <- fresh

251+ row <- freshType

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

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

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

254+ oldTys <- zip (map fst ps) <$> replicateM (length ps) freshType

232255 let oldTy = TypeApp tyObject $ rowFromList (oldTys, row)

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

234257 return $ TypedValue True (ObjectUpdate o' newVals) $ TypeApp tyObject $ rowFromList (newTys, row)

235258infer' (Accessor prop val) = rethrow (addHint (ErrorCheckingAccessor val prop)) $ do

236− field <- fresh

237− rest <- fresh

259+ field <- freshType

260+ rest <- freshType

238261 typed <- check val (TypeApp tyObject (RCons prop field rest))

239262 return $ TypedValue True (Accessor prop typed) field

240263infer' (Abs (Left arg) ret) = do

241− ty <- fresh

264+ ty <- freshType

242265 Just moduleName <- checkCurrentModule <$> get

243266 withBindingGroupVisible $ bindLocalVariables moduleName [(arg, ty, Defined)] $ do

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

@@ -265,7 +288,7 @@ infer' v@(Constructor c) = do

265288 return $ TypedValue True v' ty'

266289infer' (Case vals binders) = do

267290 (vals', ts) <- instantiateForBinders vals binders

268− ret <- fresh

291+ ret <- freshType

269292 binders' <- checkBinders ts ret binders

270293 return $ TypedValue True (Case vals' binders') ret

271294infer' (IfThenElse cond th el) = do

@@ -282,7 +305,7 @@ infer' (SuperClassDictionary className tys) = do

282305 return $ TypeClassDictionary (className, tys) dicts

283306infer' (TypedValue checkType val ty) = do

284307 Just moduleName <- checkCurrentModule <$> get

285− (kind, args) <- liftCheck $ kindOfWithScopedVars ty

308+ (kind, args) <- kindOfWithScopedVars ty

286309 checkTypeKind ty kind

287310 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

288311 val' <- if checkType then withScopedTypeVars moduleName args (check val ty') else return val

@@ -290,22 +313,28 @@ infer' (TypedValue checkType val ty) = do

290313infer' (PositionedValue pos _ val) = warnAndRethrowWithPosition pos $ infer' val

291314infer' _ = internalError "Invalid argument to infer"

292315

293−inferLetBinding :: [Declaration] -> [Declaration] -> Expr -> (Expr -> UnifyT Type Check Expr) -> UnifyT Type Check ([Declaration], Expr)

316+inferLetBinding ::

317+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

318+ [Declaration] ->

319+ [Declaration] ->

320+ Expr ->

321+ (Expr -> m Expr) ->

322+ m ([Declaration], Expr)

294323inferLetBinding seen [] ret j = (,) seen <$> withBindingGroupVisible (j ret)

295324inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do

296325 Just moduleName <- checkCurrentModule <$> get

297− (kind, args) <- liftCheck $ kindOfWithScopedVars ty

326+ (kind, args) <- kindOfWithScopedVars ty

298327 checkTypeKind ty kind

299328 let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)

300329 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

301330 TypedValue _ val' ty'' <- if checkType then withScopedTypeVars moduleName args (bindNames dict (check val ty')) else return tv

302331 bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right (TypedValue checkType val' ty''))]) rest ret j

303332inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret j = do

304− valTy <- fresh

333+ valTy <- freshType

305334 Just moduleName <- checkCurrentModule <$> get

306335 let dict = M.singleton (moduleName, ident) (valTy, nameKind, Undefined)

307336 TypedValue _ val' valTy' <- bindNames dict $ infer val

308− valTy =?= valTy'

337+ unifyTypes valTy valTy'

309338 bindNames (M.singleton (moduleName, ident) (valTy', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right val')]) rest ret j

310339inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do

311340 Just moduleName <- checkCurrentModule <$> get

@@ -321,16 +350,18 @@ inferLetBinding seen (PositionedDeclaration pos com d : ds) ret j = warnAndRethr

321350 return (PositionedDeclaration pos com d' : ds', val')

322351inferLetBinding _ _ _ _ = internalError "Invalid argument to inferLetBinding"

323352

324−-- |

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

326−--

327−inferBinder :: Type -> Binder -> UnifyT Type Check (M.Map Ident Type)

353+-- | Infer the types of variables brought into scope by a binder

354+inferBinder :: forall m.

355+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

356+ Type ->

357+ Binder ->

358+ m (M.Map Ident Type)

328359inferBinder _ NullBinder = return M.empty

329−inferBinder val (StringBinder _) = val =?= tyString >> return M.empty

330−inferBinder val (CharBinder _) = val =?= tyChar >> return M.empty

331−inferBinder val (NumberBinder (Left _)) = val =?= tyInt >> return M.empty

332−inferBinder val (NumberBinder (Right _)) = val =?= tyNumber >> return M.empty

333−inferBinder val (BooleanBinder _) = val =?= tyBoolean >> return M.empty

360+inferBinder val (StringBinder _) = unifyTypes val tyString >> return M.empty

361+inferBinder val (CharBinder _) = unifyTypes val tyChar >> return M.empty

362+inferBinder val (NumberBinder (Left _)) = unifyTypes val tyInt >> return M.empty

363+inferBinder val (NumberBinder (Right _)) = unifyTypes val tyNumber >> return M.empty

364+inferBinder val (BooleanBinder _) = unifyTypes val tyBoolean >> return M.empty

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

335366inferBinder val (ConstructorBinder ctor binders) = do

336367 env <- getEnv

@@ -340,7 +371,7 @@ inferBinder val (ConstructorBinder ctor binders) = do

340371 fn' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ fn

341372 let (args, ret) = peelArgs fn'

342373 unless (length args == length binders) . throwError . errorMessage $ IncorrectConstructorArity ctor

343− ret =?= val

374+ unifyTypes ret val

344375 M.unions <$> zipWithM inferBinder (reverse args) binders

345376 _ -> throwError . errorMessage $ UnknownDataConstructor ctor Nothing

346377 where

@@ -350,23 +381,23 @@ inferBinder val (ConstructorBinder ctor binders) = do

350381 go args (TypeApp (TypeApp fn arg) ret) | fn == tyFunction = go (arg : args) ret

351382 go args ret = (args, ret)

352383inferBinder val (ObjectBinder props) = do

353− row <- fresh

354− rest <- fresh

384+ row <- freshType

385+ rest <- freshType

355386 m1 <- inferRowProperties row rest props

356− val =?= TypeApp tyObject row

387+ unifyTypes val (TypeApp tyObject row)

357388 return m1

358389 where

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

360− inferRowProperties nrow row [] = nrow =?= row >> return M.empty

390+ inferRowProperties :: Type -> Type -> [(String, Binder)] -> m (M.Map Ident Type)

391+ inferRowProperties nrow row [] = unifyTypes nrow row >> return M.empty

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

362− propTy <- fresh

393+ propTy <- freshType

363394 m1 <- inferBinder propTy binder

364395 m2 <- inferRowProperties nrow (RCons name propTy row) binders

365396 return $ m1 `M.union` m2

366397inferBinder val (ArrayBinder binders) = do

367− el <- fresh

398+ el <- freshType

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

369− val =?= TypeApp tyArray el

400+ unifyTypes val (TypeApp tyArray el)

370401 return m1

371402inferBinder val (NamedBinder name binder) = do

372403 m <- inferBinder val binder

@@ -378,9 +409,9 @@ inferBinder val (PositionedBinder pos _ binder) =

378409-- and use `kindOfWithScopedVars`.

379410inferBinder val (TypedBinder ty binder) = do

380411 ty1 <- replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

381− kind <- liftCheck $ kindOf ty1

412+ kind <- kindOf ty1

382413 checkTypeKind ty1 kind

383− val =?= ty1

414+ unifyTypes val ty1

384415 inferBinder val binder

385416

386417-- | Returns true if a binder requires its argument type to be a monotype.

@@ -393,7 +424,11 @@ binderRequiresMonotype (PositionedBinder _ _ b) = binderRequiresMonotype b

393424binderRequiresMonotype _ = True

394425

395426-- | Instantiate polytypes only when necessitated by a binder.

396−instantiateForBinders :: [Expr] -> [CaseAlternative] -> UnifyT Type Check ([Expr], [Type])

427+instantiateForBinders ::

428+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

429+ [Expr] ->

430+ [CaseAlternative] ->

431+ m ([Expr], [Type])

397432instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do

398433 TypedValue _ val' ty <- infer val

399434 if inst

@@ -406,7 +441,12 @@ instantiateForBinders vals cas = unzip <$> zipWithM (\val inst -> do

406441-- |

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

408443--

409−checkBinders :: [Type] -> Type -> [CaseAlternative] -> UnifyT Type Check [CaseAlternative]

444+checkBinders ::

445+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

446+ [Type] ->

447+ Type ->

448+ [CaseAlternative] ->

449+ m [CaseAlternative]

410450checkBinders _ _ [] = return []

411451checkBinders nvals ret (CaseAlternative binders result : bs) = do

412452 guardWith (errorMessage $ OverlappingArgNames Nothing) $

@@ -431,13 +471,21 @@ checkBinders nvals ret (CaseAlternative binders result : bs) = do

431471-- |

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

433473--

434−check :: Expr -> Type -> UnifyT Type Check Expr

474+check ::

475+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

476+ Expr ->

477+ Type ->

478+ m Expr

435479check val ty = rethrow (addHint (ErrorCheckingType val ty)) $ check' val ty

436480

437481-- |

438482-- Check the type of a value

439483--

440−check' :: Expr -> Type -> UnifyT Type Check Expr

484+check' :: forall m.

485+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

486+ Expr ->

487+ Type ->

488+ m Expr

441489check' val (ForAll ident ty _) = do

442490 scope <- newSkolemScope

443491 sko <- newSkolemConstant

@@ -447,15 +495,15 @@ check' val (ForAll ident ty _) = do

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

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

449497 dictNames <- forM constraints $ \(Qualified _ (ProperName className), _) -> do

450− n <- liftCheck freshDictionaryName

498+ n <- freshDictionaryName

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

452− dicts <- join <$> liftCheck (zipWithM (newDictionaries []) (map (Qualified Nothing) dictNames) constraints)

500+ dicts <- join <$> zipWithM (newDictionaries []) (map (Qualified Nothing) dictNames) constraints

453501 val' <- withBindingGroupVisible $ withTypeClassDictionaries dicts $ check val ty

454502 return $ TypedValue True (foldr (Abs . Left) val' dictNames) t

455503 where

456504 -- | Add a dictionary for the constraint to the scope, and dictionaries

457− -- for all implies superclass instances.

458− newDictionaries :: [(Qualified ProperName, Integer)] -> Qualified Ident -> (Qualified ProperName, [Type]) -> Check [TypeClassDictionaryInScope]

505+ -- for all implied superclass instances.

506+ newDictionaries :: [(Qualified ProperName, Integer)] -> Qualified Ident -> (Qualified ProperName, [Type]) -> m [TypeClassDictionaryInScope]

459507 newDictionaries path name (className, instanceTy) = do

460508 tcs <- gets (typeClasses . checkEnv)

461509 let (args, _, superclasses) = fromMaybe (internalError "newDictionaries: type class lookup failed") $ M.lookup className tcs

@@ -472,7 +520,7 @@ check' val u@(TUnknown _) = do

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

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

474522 (val'', ty') <- instantiatePolyTypeWithUnknowns val' ty

475− ty' =?= u

523+ unifyTypes ty' u

476524 return $ TypedValue True val'' ty'

477525check' v@(NumericLiteral (Left _)) t | t == tyInt =

478526 return $ TypedValue True v t

@@ -485,11 +533,11 @@ check' v@(CharLiteral _) t | t == tyChar =

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

486534 return $ TypedValue True v t

487535check' (ArrayLiteral vals) t@(TypeApp a ty) = do

488− a =?= tyArray

536+ unifyTypes a tyArray

489537 array <- ArrayLiteral <$> forM vals (`check` ty)

490538 return $ TypedValue True array t

491539check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) = do

492− t =?= tyFunction

540+ unifyTypes t tyFunction

493541 Just moduleName <- checkCurrentModule <$> get

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

495543 return $ TypedValue True (Abs (Left arg) ret') ty

@@ -518,7 +566,7 @@ check' (SuperClassDictionary className tys) _ = do

518566 return $ TypeClassDictionary (className, tys) dicts

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

520568 Just moduleName <- checkCurrentModule <$> get

521− (kind, args) <- liftCheck $ kindOfWithScopedVars ty1

569+ (kind, args) <- kindOfWithScopedVars ty1

522570 checkTypeKind ty1 kind

523571 ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1

524572 ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2

@@ -550,12 +598,12 @@ check' e@(ObjectUpdate obj ps) t@(TypeApp o row) | o == tyObject = do

550598 -- We check _obj_ against the type _t_ with the types in _ps_ replaced with unknowns.

551599 let (propsToCheck, rest) = rowToList row

552600 (removedProps, remainingProps) = partition (\(p, _) -> p `elem` map fst ps) propsToCheck

553− us <- zip (map fst removedProps) <$> replicateM (length ps) fresh

601+ us <- zip (map fst removedProps) <$> replicateM (length ps) freshType

554602 obj' <- check obj (TypeApp tyObject (rowFromList (us ++ remainingProps, rest)))

555603 ps' <- checkProperties e ps row True

556604 return $ TypedValue True (ObjectUpdate obj' ps') t

557605check' (Accessor prop val) ty = rethrow (addHint (ErrorCheckingAccessor val prop)) $ do

558− rest <- fresh

606+ rest <- freshType

559607 val' <- check val (TypeApp tyObject (RCons prop ty rest))

560608 return $ TypedValue True (Accessor prop val') ty

561609check' v@(Constructor c) ty = do

@@ -589,12 +637,18 @@ check' val ty = do

589637--

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

591639--

592−checkProperties :: Expr -> [(String, Expr)] -> Type -> Bool -> UnifyT Type Check [(String, Expr)]

640+checkProperties ::

641+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

642+ Expr ->

643+ [(String, Expr)] ->

644+ Type ->

645+ Bool ->

646+ m [(String, Expr)]

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

594648 go [] [] REmpty = return []

595649 go [] [] u@(TUnknown _)

596650 | lax = return []

597− | otherwise = do u =?= REmpty

651+ | otherwise = do unifyTypes u REmpty

598652 return []

599653 go [] [] Skolem{} | lax = return []

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

@@ -604,8 +658,8 @@ checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' wh

604658 case lookup p ts of

605659 Nothing -> do

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

607− rest <- fresh

608− r =?= RCons p ty rest

661+ rest <- freshType

662+ unifyTypes r (RCons p ty rest)

609663 ps'' <- go ps' ts rest

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

611665 Just ty -> do

@@ -614,20 +668,28 @@ checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' wh

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

615669 go _ _ _ = throwError . errorMessage $ ExprDoesNotHaveType expr (TypeApp tyObject row)

616670

617−-- |

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

619−--

620−checkFunctionApplication :: Expr -> Type -> Expr -> Maybe Type -> UnifyT Type Check (Type, Expr)

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

672+checkFunctionApplication ::

673+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

674+ Expr ->

675+ Type ->

676+ Expr ->

677+ Maybe Type ->

678+ m (Type, Expr)

621679checkFunctionApplication fn fnTy arg ret = rethrow (addHint (ErrorInApplication fn fnTy arg)) $ do

622− subst <- unifyCurrentSubstitution <$> UnifyT get

623− checkFunctionApplication' fn (subst $? fnTy) arg (($?) subst <$> ret)

624−

625−-- |

626−-- Check the type of a function application

627−--

628−checkFunctionApplication' :: Expr -> Type -> Expr -> Maybe Type -> UnifyT Type Check (Type, Expr)

680+ subst <- gets checkSubstitution

681+ checkFunctionApplication' fn (substituteType subst fnTy) arg (substituteType subst <$> ret)

682+

683+-- | Check the type of a function application

684+checkFunctionApplication' ::

685+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

686+ Expr ->

687+ Type ->

688+ Expr ->

689+ Maybe Type ->

690+ m (Type, Expr)

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

630− tyFunction' =?= tyFunction

692+ unifyTypes tyFunction' tyFunction

631693 arg' <- check arg argTy

632694 case ret of

633695 Nothing -> return (retTy, App fn arg')

@@ -643,8 +705,8 @@ checkFunctionApplication' fn u@(TUnknown _) arg ret = do

643705 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t

644706 return $ TypedValue True arg'' t'

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

646− ret' <- maybe fresh return ret

647− u =?= function ty ret'

708+ ret' <- maybe freshType return ret

709+ unifyTypes u (function ty ret')

648710 return (ret', App fn arg')

649711checkFunctionApplication' fn (KindedType ty _) arg ret =

650712 checkFunctionApplication fn ty arg ret

@@ -655,11 +717,15 @@ checkFunctionApplication' fn fnTy dict@TypeClassDictionary{} _ =

655717 return (fnTy, App fn dict)

656718checkFunctionApplication' _ fnTy arg _ = throwError . errorMessage $ CannotApplyFunction fnTy arg

657719

658−-- |

659−-- Compute the meet of two types, i.e. the most general type which both types subsume.

660−-- TODO: handle constrained types

661−--

662−meet :: Expr -> Expr -> Type -> Type -> UnifyT Type Check (Expr, Expr, Type)

720+-- | Compute the meet of two types, i.e. the most general type which both types subsume.

721+-- TODO: is this really needed?

722+meet ::

723+ (Functor m, Applicative m, MonadState CheckState m, MonadError MultipleErrors m) =>

724+ Expr ->

725+ Expr ->

726+ Type ->

727+ Type ->

728+ m (Expr, Expr, Type)

663729meet e1 e2 (ForAll ident t1 _) t2 = do

664730 t1' <- replaceVarWithUnknown ident t1

665731 meet e1 e2 t1' t2

@@ -667,7 +733,7 @@ meet e1 e2 t1 (ForAll ident t2 _) = do

667733 t2' <- replaceVarWithUnknown ident t2

668734 meet e1 e2 t1 t2'

669735meet e1 e2 t1 t2 = do

670− t1 =?= t2

736+ unifyTypes t1 t2

671737 return (e1, e2, t1)

672738

673739-- |

src/Language/PureScript/TypeChecker/Unify.hs+76−43

@@ -13,12 +13,16 @@

1313--

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

1515

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

1716{-# LANGUAGE FlexibleInstances #-}

1817{-# LANGUAGE FlexibleContexts #-}

1918{-# LANGUAGE MultiParamTypeClasses #-}

19+{-# LANGUAGE ScopedTypeVariables #-}

20+{-# LANGUAGE CPP #-}

2021

2122module Language.PureScript.TypeChecker.Unify (

23+ freshType,

24+ solveType,

25+ substituteType,

2226 unifyTypes,

2327 unifyRows,

2428 unifiesWith,

@@ -28,13 +32,15 @@ module Language.PureScript.TypeChecker.Unify (

2832) where

2933

3034import Data.List (nub, sort)

31−import Data.Maybe (fromMaybe)

32−import qualified Data.HashMap.Strict as H

35+import qualified Data.Map as M

3336

37+#if __GLASGOW_HASKELL__ < 710

38+import Control.Applicative

39+#endif

3440import Control.Monad

35−import Control.Monad.Unify

36−import Control.Monad.Writer

3741import Control.Monad.Error.Class (MonadError(..))

42+import Control.Monad.Writer.Class (MonadWriter(..))

43+import Control.Monad.State.Class (MonadState(..), gets, modify)

3844

3945import Language.PureScript.Crash

4046import Language.PureScript.Errors

@@ -42,32 +48,59 @@ import Language.PureScript.TypeChecker.Monad

4248import Language.PureScript.TypeChecker.Skolems

4349import Language.PureScript.Types

4450

45−instance Partial Type where

46− unknown = TUnknown

47− isUnknown (TUnknown u) = Just u

48− isUnknown _ = Nothing

49− unknowns = everythingOnTypes (++) go

50− where

51− go (TUnknown u) = [u]

52− go _ = []

53− ($?) sub = everywhereOnTypes go

54− where

55− go t@(TUnknown u) = fromMaybe t $ H.lookup u (runSubstitution sub)

56− go other = other

57−

58−instance Unifiable Check Type where

59− (=?=) = unifyTypes

51+-- | Generate a fresh type variable

52+freshType :: (MonadState CheckState m) => m Type

53+freshType = do

54+ t <- gets checkNextType

55+ modify $ \st -> st { checkNextType = t + 1 }

56+ return $ TUnknown t

6057

61−-- |

62−-- Unify two types, updating the current substitution

63−--

64−unifyTypes :: Type -> Type -> UnifyT Type Check ()

65−unifyTypes t1 t2 = rethrow (addHint (ErrorUnifyingTypes t1 t2)) $

66− unifyTypes' t1 t2

58+-- | Update the substitution to solve a type constraint

59+solveType :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Int -> Type -> m ()

60+solveType u t = do

61+ occursCheck u t

62+ modify $ \cs -> cs { checkSubstitution =

63+ (checkSubstitution cs) { substType =

64+ M.insert u t $ substType $ checkSubstitution cs

65+ }

66+ }

67+

68+-- | Apply a substitution to a type

69+substituteType :: Substitution -> Type -> Type

70+substituteType sub = everywhereOnTypes go

71+ where

72+ go (TUnknown u) =

73+ case M.lookup u (substType sub) of

74+ Nothing -> TUnknown u

75+ Just (TUnknown u1) | u1 == u -> TUnknown u1

76+ Just t -> substituteType sub t

77+ go other = other

78+

79+-- | Make sure that an unknown does not occur in a type

80+occursCheck :: (Functor m, Applicative m, MonadError MultipleErrors m) => Int -> Type -> m ()

81+occursCheck _ TUnknown{} = return ()

82+occursCheck u t = void $ everywhereOnTypesM go t

83+ where

84+ go (TUnknown u') | u == u' = throwError . errorMessage . InfiniteType $ t

85+ go other = return other

86+

87+-- | Compute a list of all unknowns appearing in a type

88+unknownsInType :: Type -> [Int]

89+unknownsInType t = everythingOnTypes (.) go t []

90+ where

91+ go :: Type -> [Int] -> [Int]

92+ go (TUnknown u) = (u :)

93+ go _ = id

94+

95+-- | Unify two types, updating the current substitution

96+unifyTypes :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Type -> Type -> m ()

97+unifyTypes t1 t2 = do

98+ sub <- gets checkSubstitution

99+ rethrow (addHint (ErrorUnifyingTypes t1 t2)) $ unifyTypes' (substituteType sub t1) (substituteType sub t2)

67100 where

68101 unifyTypes' (TUnknown u1) (TUnknown u2) | u1 == u2 = return ()

69− unifyTypes' (TUnknown u) t = u =:= t

70− unifyTypes' t (TUnknown u) = u =:= t

102+ unifyTypes' (TUnknown u) t = solveType u t

103+ unifyTypes' t (TUnknown u) = solveType u t

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

72105 case (sc1, sc2) of

73106 (Just sc1', Just sc2') -> do

@@ -106,7 +139,7 @@ unifyTypes t1 t2 = rethrow (addHint (ErrorUnifyingTypes t1 t2)) $

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

107140-- error.

108141--

109−unifyRows :: Type -> Type -> UnifyT Type Check ()

142+unifyRows :: forall m. (Functor m, Applicative m, MonadError MultipleErrors m, MonadState CheckState m) => Type -> Type -> m ()

110143unifyRows r1 r2 =

111144 let

112145 (s1, r1') = rowToList r1

@@ -115,18 +148,18 @@ unifyRows r1 r2 =

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

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

117150 in do

118− forM_ int (uncurry (=?=))

151+ forM_ int (uncurry unifyTypes)

119152 unifyRows' sd1 r1' sd2 r2'

120153 where

121− unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> UnifyT Type Check ()

122− unifyRows' [] (TUnknown u) sd r = u =:= rowFromList (sd, r)

123− unifyRows' sd r [] (TUnknown u) = u =:= rowFromList (sd, r)

154+ unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> m ()

155+ unifyRows' [] (TUnknown u) sd r = solveType u (rowFromList (sd, r))

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

124157 unifyRows' sd1 (TUnknown u1) sd2 (TUnknown u2) = do

125158 forM_ sd1 $ \(_, t) -> occursCheck u2 t

126159 forM_ sd2 $ \(_, t) -> occursCheck u1 t

127− rest <- fresh

128− u1 =:= rowFromList (sd2, rest)

129− u2 =:= rowFromList (sd1, rest)

160+ rest <- freshType

161+ solveType u1 (rowFromList (sd2, rest))

162+ solveType u2 (rowFromList (sd1, rest))

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

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

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

@@ -164,21 +197,21 @@ unifiesWith _ _ = False

164197-- |

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

166199--

167−replaceVarWithUnknown :: String -> Type -> UnifyT Type Check Type

200+replaceVarWithUnknown :: (MonadState CheckState m) => String -> Type -> m Type

168201replaceVarWithUnknown ident ty = do

169− tu <- fresh

202+ tu <- freshType

170203 return $ replaceTypeVars ident tu ty

171204

172205-- |

173206-- Replace type wildcards with unknowns

174207--

175−replaceTypeWildcards :: Type -> UnifyT t Check Type

208+replaceTypeWildcards :: (Functor m, Applicative m, MonadWriter MultipleErrors m, MonadState CheckState m) => Type -> m Type

176209replaceTypeWildcards = everywhereOnTypesM replace

177210 where

178211 replace TypeWildcard = do

179− u <- fresh'

180− liftCheck . tell $ errorMessage . WildcardInferredType $ TUnknown u

181− return $ TUnknown u

212+ t <- freshType

213+ tell . errorMessage $ WildcardInferredType t

214+ return t

182215 replace other = return other

183216

184217-- |

@@ -186,7 +219,7 @@ replaceTypeWildcards = everywhereOnTypesM replace

186219--

187220varIfUnknown :: Type -> Type

188221varIfUnknown ty =

189− let unks = nub $ unknowns ty

222+ let unks = nub $ unknownsInType ty

190223 toName = (:) 't' . show

191224 ty' = everywhereOnTypes typeToVar ty

192225 typeToVar :: Type -> Type

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

@@ -26,7 +26,6 @@ import Data.Maybe (fromMaybe)

2626import qualified Data.Aeson as A

2727import qualified Data.Aeson.TH as A

2828

29−import Control.Monad.Unify

3029import Control.Arrow (second)

3130#if __GLASGOW_HASKELL__ < 710

3231import Control.Applicative

@@ -49,7 +48,7 @@ data Type

4948 -- |

5049 -- A unification variable of type Type

5150 --

52− = TUnknown Unknown

51+ = TUnknown Int

5352 -- |

5453 -- A named type variable

5554 --