1ae09f0 · rowtype-yoga/purescript-native

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

Merge pull request #1601 from purescript/tc-refactor

New approach to unification

commit1ae09f001261b812ede53237ca24e9ca3dde3680 authorPhil Freeman <paf31@cantab.net> dateSat 7 Nov 2015, 14:33 (11 years ago) parent7ce4667 fe69c1c

15 files changed+630−629

compare with golang

unifiedsplit

psci/PSCi.hs+7−5

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

3333import Control.Monad

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

3535import Control.Monad.Trans.Class

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

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

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

3838import Control.Monad.Trans.State.Strict

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

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

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

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

4241

4342import Options.Applicative as Opts

4443

@@ -422,8 +421,11 @@ handleKindOf typ = do

422421 Right env' ->

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

424423 Just (_, typ') -> do

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

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

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

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

426+

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

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

427429 case k of

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

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

purescript.cabal−1

@@ -174,7 +174,6 @@ library

174174 Language.PureScript.Publish.BoxesHelpers

175175

176176 Control.Monad.Logger

177− Control.Monad.Unify

178177 Control.Monad.Supply

179178 Control.Monad.Supply.Class

180179

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

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

2929import qualified Data.Map as M

3030

3131import Control.Monad

32−import Control.Monad.Unify

3332import Control.Monad.Writer

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

3534import Control.Monad.Trans.State.Lazy

@@ -177,12 +176,6 @@ data HintCategory

177176

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

179178

180−instance UnificationError Type ErrorMessage where

181− occursCheckFailed t = ErrorMessage [] $ InfiniteType t

182−

183−instance UnificationError Kind ErrorMessage where

184− occursCheckFailed k = ErrorMessage [] $ InfiniteKind k

185−

186179-- |

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

188181--

@@ -285,12 +278,6 @@ errorCode em = case unwrapErrorMessage em of

285278newtype MultipleErrors = MultipleErrors

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

287280

288−instance UnificationError Type MultipleErrors where

289− occursCheckFailed t = MultipleErrors [occursCheckFailed t]

290−

291−instance UnificationError Kind MultipleErrors where

292− occursCheckFailed k = MultipleErrors [occursCheckFailed k]

293−

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

295282nonEmpty :: MultipleErrors -> Bool

296283nonEmpty = not . null . runMultipleErrors

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

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

321308

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

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

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

324311

325312-- | How critical the issue is

326313data Level = Error | Warning deriving Show

@@ -334,7 +321,7 @@ unwrapErrorMessage (ErrorMessage _ se) = se

334321replaceUnknowns :: Type -> State UnknownMap Type

335322replaceUnknowns = everywhereOnTypesM replaceTypes

336323 where

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

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

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

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

340327 Just i -> (i, m)

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

@@ -23,8 +23,6 @@ import Prelude.Compat

2323import Data.Data

2424import qualified Data.Aeson.TH as A

2525

26−import Control.Monad.Unify (Unknown)

27−

2826-- |

2927-- The data type of kinds

3028--

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

3230 -- |

3331 -- Unification variable of type Kind

3432 --

35− = KUnknown Unknown

33+ = KUnknown Int

3634 -- |

3735 -- The kind of types

3836 --

src/Language/PureScript/TypeChecker.hs+95−29

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

1313--

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

1515

16+{-# LANGUAGE ScopedTypeVariables #-}

1617{-# LANGUAGE FlexibleInstances #-}

18+{-# LANGUAGE FlexibleContexts #-}

1719

1820module Language.PureScript.TypeChecker (

1921 module T,

@@ -34,8 +36,10 @@ import Data.Foldable (for_, traverse_)

3436

3537import qualified Data.Map as M

3638

37−import Control.Monad.State

39+import Control.Monad (when, unless, void, forM, forM_)

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

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

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

3943

4044import Language.PureScript.Crash

4145import Language.PureScript.Types

@@ -46,15 +50,31 @@ import Language.PureScript.TypeClassDictionaries

4650import Language.PureScript.Environment

4751import Language.PureScript.Errors

4852

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

53+addDataType ::

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

55+ ModuleName ->

56+ DataDeclType ->

57+ ProperName ->

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

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

60+ Kind ->

61+ m ()

5062addDataType moduleName dtype name args dctors ctorKind = do

5163 env <- getEnv

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

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

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

5466 warnAndRethrow (addHint (ErrorInDataConstructor dctor)) $

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

5668

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

69+addDataConstructor ::

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

71+ ModuleName ->

72+ DataDeclType ->

73+ ProperName ->

74+ [String] ->

75+ ProperName ->

76+ [Type] ->

77+ m ()

5878addDataConstructor moduleName dtype name args dctor tys = do

5979 env <- getEnv

6080 traverse_ checkTypeSynonyms tys

@@ -64,26 +84,50 @@ addDataConstructor moduleName dtype name args dctor tys = do

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

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

6686

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

87+addTypeSynonym ::

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

89+ ModuleName ->

90+ ProperName ->

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

92+ Type ->

93+ Kind ->

94+ m ()

6895addTypeSynonym moduleName name args ty kind = do

6996 env <- getEnv

7097 checkTypeSynonyms ty

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

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

73100

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

101+valueIsNotDefined ::

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

103+ ModuleName ->

104+ Ident ->

105+ m ()

75106valueIsNotDefined moduleName name = do

76107 env <- getEnv

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

78109 Just _ -> throwError . errorMessage $ RedefinedIdent name

79110 Nothing -> return ()

80111

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

112+addValue ::

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

114+ ModuleName ->

115+ Ident ->

116+ Type ->

117+ NameKind ->

118+ m ()

82119addValue moduleName name ty nameKind = do

83120 env <- getEnv

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

85122

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

123+addTypeClass ::

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

125+ ModuleName ->

126+ ProperName ->

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

128+ [Constraint] ->

129+ [Declaration] ->

130+ m ()

87131addTypeClass moduleName pn args implies ds =

88132 let members = map toPair ds in

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

@@ -92,19 +136,30 @@ addTypeClass moduleName pn args implies ds =

92136 toPair (PositionedDeclaration _ _ d) = toPair d

93137 toPair _ = internalError "Invalid declaration in TypeClassDeclaration"

94138

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

139+addTypeClassDictionaries ::

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

141+ Maybe ModuleName ->

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

143+ m ()

96144addTypeClassDictionaries mn entries =

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

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

99147

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

148+checkDuplicateTypeArguments ::

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

150+ [String] ->

151+ m ()

101152checkDuplicateTypeArguments args = for_ firstDup $ \dup ->

102153 throwError . errorMessage $ DuplicateTypeArgument dup

103154 where

104155 firstDup :: Maybe String

105156 firstDup = listToMaybe $ args \\ nub args

106157

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

158+checkTypeClassInstance ::

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

160+ ModuleName ->

161+ Type ->

162+ m ()

108163checkTypeClassInstance _ (TypeVar _) = return ()

109164checkTypeClassInstance _ (TypeConstructor ctor) = do

110165 env <- getEnv

@@ -116,7 +171,10 @@ checkTypeClassInstance _ ty = throwError . errorMessage $ InvalidInstanceHead ty

116171-- |

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

118173--

119−checkTypeSynonyms :: Type -> Check ()

174+checkTypeSynonyms ::

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

176+ Type ->

177+ m ()

120178checkTypeSynonyms = void . replaceAllTypeSynonyms

121179

122180-- |

@@ -132,10 +190,15 @@ checkTypeSynonyms = void . replaceAllTypeSynonyms

132190--

133191-- * Process module imports

134192--

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

193+typeCheckAll :: forall m.

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

195+ ModuleName ->

196+ [DeclarationRef] ->

197+ [Declaration] ->

198+ m [Declaration]

136199typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities ds

137200 where

138− go :: Declaration -> Check Declaration

201+ go :: Declaration -> m Declaration

139202 go (DataDeclaration dtype name args dctors) = do

140203 warnAndRethrow (addHint (ErrorInTypeConstructor name)) $ do

141204 when (dtype == Newtype) $ checkNewtype dctors

@@ -145,7 +208,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d

145208 addDataType moduleName dtype name args' dctors ctorKind

146209 return $ DataDeclaration dtype name args dctors

147210 where

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

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

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

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

151214 checkNewtype _ = throwError . errorMessage $ InvalidNewtype name

@@ -154,11 +217,11 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d

154217 let syns = mapMaybe toTypeSynonym tys

155218 let dataDecls = mapMaybe toDataDecl tys

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

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

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

158221 checkDuplicateTypeArguments $ map fst args

159222 let args' = args `withKinds` ctorKind

160223 addDataType moduleName dtype name args' dctors ctorKind

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

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

162225 checkDuplicateTypeArguments $ map fst args

163226 let args' = args `withKinds` kind

164227 addTypeSynonym moduleName name args' ty kind

@@ -187,7 +250,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d

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

188251 go (BindingGroupDeclaration vals) =

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

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

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

191254 valueIsNotDefined moduleName name

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

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

@@ -227,7 +290,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d

227290 go (PositionedDeclaration pos com d) =

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

229292

230− checkOrphanFixities :: Declaration -> Check ()

293+ checkOrphanFixities :: Declaration -> m ()

231294 checkOrphanFixities (FixityDeclaration _ name) = do

232295 env <- getEnv

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

@@ -235,7 +298,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d

235298 warnAndRethrowWithPosition pos $ checkOrphanFixities d

236299 checkOrphanFixities _ = return ()

237300

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

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

239302 checkInstanceMembers instDecls = do

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

241304 for_ (firstDuplicate idents) $ \ident ->

@@ -253,7 +316,7 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d

253316 | otherwise = firstDuplicate xs

254317 firstDuplicate _ = Nothing

255318

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

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

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

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

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

@@ -280,19 +343,22 @@ typeCheckAll moduleName _ ds = traverse go ds <* traverse_ checkOrphanFixities d

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

281344-- required by exported members are also exported.

282345--

283−typeCheckModule :: Module -> Check Module

346+typeCheckModule :: forall m.

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

348+ Module ->

349+ m Module

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

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

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

287353 decls' <- typeCheckAll mn exps decls

288− forM_ exps $ \e -> do

354+ for_ exps $ \e -> do

289355 checkTypesAreExported e

290356 checkClassMembersAreExported e

291357 checkClassesAreExported e

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

293359 where

294360

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

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

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

297363 env <- getEnv

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

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

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

301367 case dctors of

302368 Nothing -> return ()

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

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

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

305371 Nothing -> return ()

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

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

310376 checkExport dr extract ty

311377 checkMemberExport _ _ = return ()

312378

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

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

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

315381 [] -> return ()

316382 hidden -> throwError . errorMessage $ TransitiveExportError dr hidden

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

325391

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

327393 -- have also been exported from the module

328− checkTypesAreExported :: DeclarationRef -> Check ()

394+ checkTypesAreExported :: DeclarationRef -> m ()

329395 checkTypesAreExported = checkMemberExport findTcons

330396 where

331397 findTcons :: Type -> [DeclarationRef]

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

336402

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

338404 -- been exported from the module

339− checkClassesAreExported :: DeclarationRef -> Check ()

405+ checkClassesAreExported :: DeclarationRef -> m ()

340406 checkClassesAreExported = checkMemberExport findClasses

341407 where

342408 findClasses :: Type -> [DeclarationRef]

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

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

349415 extractCurrentModuleClass _ = Nothing

350416

351− checkClassMembersAreExported :: DeclarationRef -> Check ()

417+ checkClassMembersAreExported :: DeclarationRef -> m ()

352418 checkClassMembersAreExported dr@(TypeClassRef name) = do

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

354420 let missingMembers = members \\ exps

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

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

1313--

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

1515

16+{-# LANGUAGE ScopedTypeVariables #-}

17+{-# LANGUAGE FlexibleContexts #-}

18+

1619module Language.PureScript.TypeChecker.Entailment (

1720 entails

1821) where

@@ -28,13 +31,12 @@ import qualified Data.Map as M

2831import Control.Arrow (Arrow(..))

2932import Control.Monad.State

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

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

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

3235

3336import Language.PureScript.Crash

3437import Language.PureScript.AST

3538import Language.PureScript.Errors

3639import Language.PureScript.Names

37−import Language.PureScript.TypeChecker.Monad

3840import Language.PureScript.TypeChecker.Unify

3941import Language.PureScript.TypeClassDictionaries

4042import Language.PureScript.Types

@@ -44,7 +46,12 @@ import qualified Language.PureScript.Constants as C

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

4547-- return a type class dictionary reference.

4648--

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

49+entails :: forall m.

50+ (Functor m, Applicative m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

51+ ModuleName ->

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

53+ Constraint ->

54+ m Expr

4855entails moduleName context = solve

4956 where

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

@@ -60,12 +67,12 @@ entails moduleName context = solve

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

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

6269

63− solve :: Constraint -> Check Expr

70+ solve :: Constraint -> m Expr

6471 solve (className, tys) = do

6572 dict <- go 0 className tys

6673 return $ dictionaryValueToValue dict

6774 where

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

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

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

7077 go work className' tys' = do

7178 let instances = do

@@ -81,7 +88,7 @@ entails moduleName context = solve

8188 (tcdPath tcd)

8289 where

8390

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

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

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

8693 unique [a] = return a

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

@@ -104,7 +111,7 @@ entails moduleName context = solve

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

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

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

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

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

108115 solveSubgoals _ Nothing = return Nothing

109116 solveSubgoals subst (Just subgoals) = do

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

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

@@ -13,10 +13,12 @@

1313--

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

1515

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

1716{-# LANGUAGE MultiParamTypeClasses #-}

1817{-# LANGUAGE FlexibleInstances #-}

18+{-# LANGUAGE FlexibleContexts #-}

1919{-# LANGUAGE TupleSections #-}

20+{-# LANGUAGE ScopedTypeVariables #-}

21+{-# LANGUAGE RankNTypes #-}

2022

2123module Language.PureScript.TypeChecker.Kinds (

2224 kindOf,

@@ -28,16 +30,13 @@ module Language.PureScript.TypeChecker.Kinds (

2830import Prelude ()

2931import Prelude.Compat

3032

31−import Data.Maybe (fromMaybe)

32−

33−import qualified Data.HashMap.Strict as H

3433import qualified Data.Map as M

3534

3635import Control.Arrow (second)

3736import Control.Monad

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

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

3939import Control.Monad.State

40−import Control.Monad.Unify

4140

4241import Language.PureScript.Crash

4342import Language.PureScript.Environment

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

4746import Language.PureScript.TypeChecker.Monad

4847import Language.PureScript.Types

4948

50−instance Partial Kind where

51− unknown = KUnknown

52− isUnknown (KUnknown u) = Just u

53− isUnknown _ = Nothing

54− unknowns = everythingOnKinds (++) go

55− where

56− go (KUnknown u) = [u]

57− go _ = []

58− ($?) sub = everywhereOnKinds go

59− where

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

61− go other = other

62−

63−instance Unifiable Check Kind where

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

65− KUnknown u =?= k = u =:= k

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

67− Star =?= Star = return ()

68− Bang =?= Bang = return ()

69− Row k1 =?= Row k2 = k1 =?= k2

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

71− k1 =?= k3

72− k2 =?= k4

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

7455

75−-- |

76−-- Infer the kind of a single type

77−--

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

79107kindOf ty = fst <$> kindOfWithScopedVars ty

80108

81−-- |

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

83−--

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

85114kindOfWithScopedVars ty =

86115 rethrow (addHint (ErrorCheckingKind ty)) $

87116 fmap tidyUp . liftUnify $ infer ty

88117 where

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

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

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

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

91120 )

92121

93−-- |

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

95−--

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

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

98− tyCon <- fresh

99− kargs <- replicateM (length args) fresh

132+ tyCon <- freshKind

133+ kargs <- replicateM (length args) freshKind

100134 rest <- zipWithM freshKindVar args kargs

101135 let dict = (name, tyCon) : rest

102136 bindLocalTypeVariables moduleName dict $

103137 solveTypes isData ts kargs tyCon

104138 where

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

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

106140

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

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

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

110− kind =?= kind'

148+ unifyKinds kind kind'

111149 return (ProperName arg, kind')

112150

113−-- |

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

115−--

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

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

118− synVars <- replicateM (length syns) fresh

159+ synVars <- replicateM (length syns) freshKind

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

120161 bindLocalTypeVariables moduleName dict $ do

121− tyCons <- replicateM (length tys) fresh

162+ tyCons <- replicateM (length tys) freshKind

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

123164 bindLocalTypeVariables moduleName dict' $ do

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

125− kargs <- replicateM (length args) fresh

166+ kargs <- replicateM (length args) freshKind

126167 argDict <- zipWithM freshKindVar args kargs

127168 bindLocalTypeVariables moduleName argDict $

128169 solveTypes True ts kargs tyCon) tyCons tys

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

130− kargs <- replicateM (length args) fresh

171+ kargs <- replicateM (length args) freshKind

131172 argDict <- zipWithM freshKindVar args kargs

132173 bindLocalTypeVariables moduleName argDict $

133174 solveTypes False [ty] kargs synVar) synVars syns

134175 return (syn_ks, data_ks)

135176 where

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

137178

138−-- |

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

140−--

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

142181solveTypes isData ts kargs tyCon = do

143182 ks <- traverse (fmap fst . infer) ts

144183 when isData $ do

145− tyCon =?= foldr FunKind Star kargs

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

184+ unifyKinds tyCon (foldr FunKind Star kargs)

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

147186 unless isData $

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

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

149188 return tyCon

150189

151−-- |

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

153−--

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

154191starIfUnknown :: Kind -> Kind

155192starIfUnknown (KUnknown _) = Star

156193starIfUnknown (Row k) = Row (starIfUnknown k)

157194starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)

158195starIfUnknown k = k

159196

160−-- |

161−-- Infer a kind for a type

162−--

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

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

165200

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

167202infer' (ForAll ident ty _) = do

168− k1 <- fresh

203+ k1 <- freshKind

169204 Just moduleName <- checkCurrentModule <$> get

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

171− k2 =?= Star

206+ unifyKinds k2 Star

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

173208infer' (KindedType ty k) = do

174209 (k', args) <- infer ty

175− k =?= k'

210+ unifyKinds k k'

176211 return (k', args)

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

178213 where

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

214+ go :: Type -> m Kind

180215 go (ForAll ident ty _) = do

181− k1 <- fresh

216+ k1 <- freshKind

182217 Just moduleName <- checkCurrentModule <$> get

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

184− k2 =?= Star

219+ unifyKinds k2 Star

185220 return Star

186221 go (KindedType ty k) = do

187222 k' <- go ty

188− k =?= k'

223+ unifyKinds k k'

189224 return k'

190− go TypeWildcard = fresh

225+ go TypeWildcard = freshKind

191226 go (TypeVar v) = do

192227 Just moduleName <- checkCurrentModule <$> get

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

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

194229 go (Skolem v _ _) = do

195230 Just moduleName <- checkCurrentModule <$> get

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

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

197232 go (TypeConstructor v) = do

198− env <- liftCheck getEnv

233+ env <- getEnv

199234 case M.lookup v (types env) of

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

235+ Nothing -> throwError . errorMessage $ UnknownTypeConstructor v

201236 Just (kind, _) -> return kind

202237 go (TypeApp t1 t2) = do

203− k0 <- fresh

238+ k0 <- freshKind

204239 k1 <- go t1

205240 k2 <- go t2

206− k1 =?= FunKind k2 k0

241+ unifyKinds k1 (FunKind k2 k0)

207242 return k0

208243 go REmpty = do

209− k <- fresh

244+ k <- freshKind

210245 return $ Row k

211246 go (RCons _ ty row) = do

212247 k1 <- go ty

213248 k2 <- go row

214− k2 =?= Row k1

249+ unifyKinds k2 (Row k1)

215250 return $ Row k1

216251 go (ConstrainedType deps ty) = do

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

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

219− k =?= Star

254+ unifyKinds k Star

220255 k <- go ty

221− k =?= Star

256+ unifyKinds k Star

222257 return Star

223258 go _ = internalError "Invalid argument to infer"

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

@@ -26,14 +26,12 @@ import Prelude ()

2626import Prelude.Compat

2727

2828import Data.Maybe

29−import Data.Foldable (for_)

3029import qualified Data.Map as M

3130

31+import Control.Arrow (second)

3232import Control.Monad.State

33−import Control.Monad.Unify

34−import Control.Monad.Writer.Strict

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

36−import Control.Monad.Trans.Except

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

3735

3836import Language.PureScript.Environment

3937import Language.PureScript.Errors

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

4240import Language.PureScript.TypeClassDictionaries

4341import Language.PureScript.Types

4442

45−-- |

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

47−--

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

44+data Substitution = Substitution

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

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

47+ }

48+

49+-- | An empty substitution

50+emptySubstitution :: Substitution

51+emptySubstitution = Substitution M.empty M.empty

52+

53+-- | State required for type checking

54+data CheckState = CheckState

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

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

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

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

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

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

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

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

63+ }

64+

65+-- | Create an empty @CheckState@

66+emptyCheckState :: Environment -> CheckState

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

68+

69+-- | Unification variables

70+type Unknown = Int

71+

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

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

4974bindNames newNames action = do

5075 orig <- get

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

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

5479 return a

5580

56−-- |

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

58−--

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

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

6083bindTypes newNames action = do

6184 orig <- get

@@ -64,20 +87,16 @@ bindTypes newNames action = do

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

6588 return a

6689

67−-- |

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

69−--

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

7091withScopedTypeVars :: (Functor m, Applicative m, MonadState CheckState m, MonadWriter MultipleErrors m) => ModuleName -> [(String, Kind)] -> m a -> m a

7192withScopedTypeVars mn ks ma = do

7293 orig <- get

73− for_ ks $ \(name, _) ->

94+ forM_ ks $ \(name, _) ->

7495 when (Qualified (Just mn) (ProperName name) `M.member` types (checkEnv orig)) $

7596 tell . errorMessage $ ShadowedTypeVar name

7697 bindTypes (M.fromList (map (\(name, k) -> (Qualified (Just mn) (ProperName name), (k, ScopedTypeVar))) ks)) ma

7798

78−-- |

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

80−--

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

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

82101withTypeClassDictionaries entries action = do

83102 orig <- get

@@ -87,35 +106,30 @@ withTypeClassDictionaries entries action = do

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

88107 return a

89108

90−-- |

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

92−--

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

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

110+getTypeClassDictionaries ::

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

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

94113getTypeClassDictionaries = typeClassDictionaries . checkEnv <$> get

95114

96−-- |

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

98−--

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

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

116+lookupTypeClassDictionaries ::

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

118+ Maybe ModuleName ->

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

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

101121

102−-- |

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

104−--

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

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

106124bindLocalVariables moduleName bindings =

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

108126

109−-- |

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

111−--

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

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

113129bindLocalTypeVariables moduleName bindings =

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

115131

116−-- |

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

118−--

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

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

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

121135

@@ -131,9 +145,7 @@ preservingNames action = do

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

132146 return a

133147

134−-- |

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

136−--

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

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

138150lookupVariable currentModule (Qualified moduleName var) = do

139151 env <- getEnv

@@ -141,9 +153,7 @@ lookupVariable currentModule (Qualified moduleName var) = do

141153 Nothing -> throwError . errorMessage $ NameIsUndefined var

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

143155

144−-- |

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

146−--

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

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

148158getVisibility currentModule (Qualified moduleName var) = do

149159 env <- getEnv

@@ -151,9 +161,7 @@ getVisibility currentModule (Qualified moduleName var) = do

151161 Nothing -> throwError . errorMessage $ NameIsUndefined var

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

153163

154−-- |

155−-- Assert that a name is visible

156−--

164+-- | Assert that a name is visible

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

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

159167 vis <- getVisibility currentModule name

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

161169 Undefined -> throwError . errorMessage $ CycleInDeclaration var

162170 _ -> return ()

163171

164−-- |

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

166−--

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

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

168174lookupTypeVariable currentModule (Qualified moduleName name) = do

169175 env <- getEnv

@@ -171,113 +177,56 @@ lookupTypeVariable currentModule (Qualified moduleName name) = do

171177 Nothing -> throwError . errorMessage $ UndefinedTypeVariable name

172178 Just (k, _) -> return k

173179

174−-- |

175−-- State required for type checking:

176−--

177−data CheckState = CheckState {

178− -- |

179− -- The current @Environment@

180− --

181− checkEnv :: Environment

182− -- |

183− -- The next fresh unification variable name

184− --

185− , checkNextVar :: Int

186− -- |

187− -- The next type class dictionary name

188− --

189− , checkNextDictName :: Int

190− -- |

191− -- The current module

192− --

193− , checkCurrentModule :: Maybe ModuleName

194− }

195−

196−-- |

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

198−--

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

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

201−

202−-- |

203−-- Get the current @Environment@

204−--

180+-- | Get the current @Environment@

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

206182getEnv = checkEnv <$> get

207183

208−-- |

209−-- Update the @Environment@

210−--

184+-- | Update the @Environment@

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

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

213187

214−-- |

215−-- Modify the @Environment@

216−--

188+-- | Modify the @Environment@

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

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

219191

220−-- |

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

222−--

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

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

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

224194runCheck = runCheck' initEnvironment

225195

226−-- |

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

228−--

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

230−runCheck' env = interpretMultipleErrorsAndWarnings . unwrapCheckWithWarnings env

231− where

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

233− unwrapCheckWithWarnings e =

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

235− . runWriter

236− . runExceptT

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

238− . unCheck

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

240− envCheck rc = do

241− (a, s) <- rc

242− return (a, checkEnv s)

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

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

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

243199

244−-- |

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

246−--

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

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

248202guardWith _ True = return ()

249203guardWith e False = throwError e

250204

251−-- |

252−-- Generate new type class dictionary name

253−--

254−freshDictionaryName :: Check Int

205+-- | Generate new type class dictionary name

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

255207freshDictionaryName = do

256208 n <- checkNextDictName <$> get

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

258210 return n

259211

260−-- |

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

262−--

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

264−liftCheck = UnifyT . lift

265−

266−-- |

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

268−--

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

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

213+liftUnify ::

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

215+ m a ->

216+ m (a, Substitution)

270217liftUnify = liftUnifyWarnings (const id)

271218

272−-- |

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

274−--

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

276−liftUnifyWarnings replace unify = do

277− st <- get

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

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

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

281− let uust = unifyCurrentSubstitution ust

282− tell $ onErrorMessages (replace uust) w

283− return (a, uust)

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

220+liftUnifyWarnings ::

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

222+ (Substitution -> ErrorMessage -> ErrorMessage) ->

223+ m a ->

224+ m (a, Substitution)

225+liftUnifyWarnings replace ma = do

226+ orig <- get

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

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

229+ subst <- gets checkSubstitution

230+ tell . onErrorMessages (replace subst) $ w

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

232+ 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+15−7

@@ -13,6 +13,8 @@

1313--

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

1515

16+{-# LANGUAGE FlexibleContexts #-}

17+

1618module Language.PureScript.TypeChecker.Skolems (

1719 newSkolemConstant,

1820 introduceSkolemScope,

@@ -29,7 +31,7 @@ import Data.List (nub, (\\))

2931import Data.Monoid

3032

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

32−import Control.Monad.Unify

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

3335

3436import Language.PureScript.Crash

3537import Language.PureScript.AST

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

4042-- |

4143-- Generate a new skolem constant

4244--

43−newSkolemConstant :: UnifyT Type Check Int

44−newSkolemConstant = fresh'

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

46+newSkolemConstant = do

47+ s <- gets checkNextSkolem

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

49+ return s

4550

4651-- |

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

4853--

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

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

5055introduceSkolemScope = everywhereOnTypesM go

5156 where

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

@@ -55,8 +60,11 @@ introduceSkolemScope = everywhereOnTypesM go

5560-- |

5661-- Generate a new skolem scope

5762--

58−newSkolemScope :: UnifyT Type Check SkolemScope

59−newSkolemScope = SkolemScope <$> fresh'

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

64+newSkolemScope = do

65+ s <- gets checkNextSkolemScope

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

67+ return $ SkolemScope s

6068

6169-- |

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

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

8492-- |

8593-- Ensure skolem variables do not escape their scope

8694--

87−skolemEscapeCheck :: Expr -> Check ()

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

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

8997skolemEscapeCheck root@TypedValue{} =

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

@@ -46,10 +47,9 @@ import Data.Maybe (fromMaybe)

4647import qualified Data.Map as M

4748

4849import Control.Monad

49−import Control.Monad.State

50−import Control.Monad.Unify

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

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

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

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

5353

5454import Language.PureScript.Crash

5555import Language.PureScript.AST

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

6969import Language.PureScript.TypeClassDictionaries

7070import Language.PureScript.Types

7171

72−-- |

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

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

7473-- type class dictionaries and type annotations.

75−--

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

74+typesOf ::

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

76+ ModuleName ->

77+ [(Ident, Expr)] ->

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

7779typesOf moduleName vals = do

7880 tys <- fmap tidyUp . liftUnifyWarnings replace $ do

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

@@ -91,17 +93,21 @@ typesOf moduleName vals = do

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

9294 where

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

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

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

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

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

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

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

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

98100 replace _ em = em

99101

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

101103

102104type UntypedData = [(Ident, Type)]

103105

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

106+typeDictionaryForBindingGroup ::

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

108+ ModuleName ->

109+ [(Ident, Expr)] ->

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

105111typeDictionaryForBindingGroup moduleName vals = do

106112 let

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

@@ -113,7 +119,7 @@ typeDictionaryForBindingGroup moduleName vals = do

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

114120

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

116− untypedNames <- replicateM (length untyped) fresh

122+ untypedNames <- replicateM (length untyped) freshType

117123

118124 let

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

@@ -122,12 +128,17 @@ typeDictionaryForBindingGroup moduleName vals = do

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

123129 return (untyped, typed, dict, untypedDict)

124130

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

131+checkTypedBindingGroupElement ::

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

133+ ModuleName ->

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

135+ TypeData ->

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

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

127138 -- Replace type wildcards

128139 ty' <- replaceTypeWildcards ty

129140 -- Kind check

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

141+ (kind, args) <- kindOfWithScopedVars ty

131142 checkTypeKind ty kind

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

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

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

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

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

138149

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

150+typeForBindingGroupElement ::

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

152+ Bool ->

153+ (Ident, Expr) ->

154+ TypeData ->

155+ UntypedData ->

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

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

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

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

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

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

144161 when warn . tell . errorMessage $ MissingTypeDeclaration ident ty

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

146163

147−-- |

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

149−--

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

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

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

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

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

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

163178 g other = other

164179

165−-- |

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

167−--

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

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

181+replaceTypeClassDictionaries ::

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

183+ ModuleName ->

184+ Expr ->

185+ m Expr

169186replaceTypeClassDictionaries mn =

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

171188 in f

@@ -173,20 +190,24 @@ replaceTypeClassDictionaries mn =

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

174191 go other = return other

175192

176−-- |

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

178−--

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

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

194+checkTypeKind ::

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

196+ Type ->

197+ Kind ->

198+ m ()

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

181200

182−-- |

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

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

184202-- or TypeClassDictionary values.

185203--

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

187205-- unification variable.

188−--

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

206+instantiatePolyTypeWithUnknowns ::

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

208+ Expr ->

209+ Type ->

210+ m (Expr, Type)

190211instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do

191212 ty' <- replaceVarWithUnknown ident ty

192213 instantiatePolyTypeWithUnknowns val ty'

@@ -196,16 +217,18 @@ instantiatePolyTypeWithUnknowns val (ConstrainedType constraints ty) = do

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

197218instantiatePolyTypeWithUnknowns val ty = return (val, ty)

198219

199−-- |

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

201−--

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

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

221+infer ::

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

223+ Expr ->

224+ m Expr

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

204226

205−-- |

206−-- Infer a type for a value

207−--

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

227+-- | Infer a type for a value

228+infer' ::

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

230+ Expr ->

231+ m Expr

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

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

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

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

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

214237infer' (ArrayLiteral vals) = do

215238 ts <- traverse infer vals

216− els <- fresh

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

239+ els <- freshType

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

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

219242infer' (ObjectLiteral ps) = do

220243 ensureNoDuplicateProperties ps

@@ -224,20 +247,20 @@ infer' (ObjectLiteral ps) = do

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

225248infer' (ObjectUpdate o ps) = do

226249 ensureNoDuplicateProperties ps

227− row <- fresh

250+ row <- freshType

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

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

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

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

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

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

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

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

235− field <- fresh

236− rest <- fresh

258+ field <- freshType

259+ rest <- freshType

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

238261 return $ TypedValue True (Accessor prop typed) field

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

240− ty <- fresh

263+ ty <- freshType

241264 Just moduleName <- checkCurrentModule <$> get

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

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

@@ -264,7 +287,7 @@ infer' v@(Constructor c) = do

264287 return $ TypedValue True v' ty'

265288infer' (Case vals binders) = do

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

267− ret <- fresh

290+ ret <- freshType

268291 binders' <- checkBinders ts ret binders

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

270293infer' (IfThenElse cond th el) = do

@@ -281,7 +304,7 @@ infer' (SuperClassDictionary className tys) = do

281304 return $ TypeClassDictionary (className, tys) dicts

282305infer' (TypedValue checkType val ty) = do

283306 Just moduleName <- checkCurrentModule <$> get

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

307+ (kind, args) <- kindOfWithScopedVars ty

285308 checkTypeKind ty kind

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

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

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

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

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

291314

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

315+inferLetBinding ::

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

317+ [Declaration] ->

318+ [Declaration] ->

319+ Expr ->

320+ (Expr -> m Expr) ->

321+ m ([Declaration], Expr)

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

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

295324 Just moduleName <- checkCurrentModule <$> get

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

325+ (kind, args) <- kindOfWithScopedVars ty

297326 checkTypeKind ty kind

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

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

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

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

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

303− valTy <- fresh

332+ valTy <- freshType

304333 Just moduleName <- checkCurrentModule <$> get

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

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

307− valTy =?= valTy'

336+ unifyTypes valTy valTy'

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

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

310339 Just moduleName <- checkCurrentModule <$> get

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

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

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

322351

323−-- |

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

325−--

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

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

353+inferBinder :: forall m.

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

355+ Type ->

356+ Binder ->

357+ m (M.Map Ident Type)

327358inferBinder _ NullBinder = return M.empty

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

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

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

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

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

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

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

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

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

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

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

334365inferBinder val (ConstructorBinder ctor binders) = do

335366 env <- getEnv

@@ -339,7 +370,7 @@ inferBinder val (ConstructorBinder ctor binders) = do

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

340371 let (args, ret) = peelArgs fn'

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

342− ret =?= val

373+ unifyTypes ret val

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

344375 _ -> throwError . errorMessage $ UnknownDataConstructor ctor Nothing

345376 where

@@ -349,23 +380,23 @@ inferBinder val (ConstructorBinder ctor binders) = do

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

350381 go args ret = (args, ret)

351382inferBinder val (ObjectBinder props) = do

352− row <- fresh

353− rest <- fresh

383+ row <- freshType

384+ rest <- freshType

354385 m1 <- inferRowProperties row rest props

355− val =?= TypeApp tyObject row

386+ unifyTypes val (TypeApp tyObject row)

356387 return m1

357388 where

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

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

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

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

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

361− propTy <- fresh

392+ propTy <- freshType

362393 m1 <- inferBinder propTy binder

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

364395 return $ m1 `M.union` m2

365396inferBinder val (ArrayBinder binders) = do

366− el <- fresh

397+ el <- freshType

367398 m1 <- M.unions <$> traverse (inferBinder el) binders

368− val =?= TypeApp tyArray el

399+ unifyTypes val (TypeApp tyArray el)

369400 return m1

370401inferBinder val (NamedBinder name binder) = do

371402 m <- inferBinder val binder

@@ -377,9 +408,9 @@ inferBinder val (PositionedBinder pos _ binder) =

377408-- and use `kindOfWithScopedVars`.

378409inferBinder val (TypedBinder ty binder) = do

379410 ty1 <- replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

380− kind <- liftCheck $ kindOf ty1

411+ kind <- kindOf ty1

381412 checkTypeKind ty1 kind

382− val =?= ty1

413+ unifyTypes val ty1

383414 inferBinder val binder

384415

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

@@ -392,7 +423,11 @@ binderRequiresMonotype (PositionedBinder _ _ b) = binderRequiresMonotype b

392423binderRequiresMonotype _ = True

393424

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

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

426+instantiateForBinders ::

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

428+ [Expr] ->

429+ [CaseAlternative] ->

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

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

397432 TypedValue _ val' ty <- infer val

398433 if inst

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

405440-- |

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

407442--

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

443+checkBinders ::

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

445+ [Type] ->

446+ Type ->

447+ [CaseAlternative] ->

448+ m [CaseAlternative]

409449checkBinders _ _ [] = return []

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

411451 guardWith (errorMessage $ OverlappingArgNames Nothing) $

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

430470-- |

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

432472--

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

473+check ::

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

475+ Expr ->

476+ Type ->

477+ m Expr

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

435479

436480-- |

437481-- Check the type of a value

438482--

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

483+check' :: forall m.

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

485+ Expr ->

486+ Type ->

487+ m Expr

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

441489 scope <- newSkolemScope

442490 sko <- newSkolemConstant

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

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

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

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

449− n <- liftCheck freshDictionaryName

497+ n <- freshDictionaryName

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

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

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

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

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

454502 where

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

456− -- for all implies superclass instances.

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

504+ -- for all implied superclass instances.

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

458506 newDictionaries path name (className, instanceTy) = do

459507 tcs <- gets (typeClasses . checkEnv)

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

@@ -471,7 +519,7 @@ check' val u@(TUnknown _) = do

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

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

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

474− ty' =?= u

522+ unifyTypes ty' u

475523 return $ TypedValue True val'' ty'

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

477525 return $ TypedValue True v t

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

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

485533 return $ TypedValue True v t

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

487− a =?= tyArray

535+ unifyTypes a tyArray

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

489537 return $ TypedValue True array t

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

491− t =?= tyFunction

539+ unifyTypes t tyFunction

492540 Just moduleName <- checkCurrentModule <$> get

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

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

@@ -517,7 +565,7 @@ check' (SuperClassDictionary className tys) _ = do

517565 return $ TypeClassDictionary (className, tys) dicts

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

519567 Just moduleName <- checkCurrentModule <$> get

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

568+ (kind, args) <- kindOfWithScopedVars ty1

521569 checkTypeKind ty1 kind

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

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

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

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

550598 let (propsToCheck, rest) = rowToList row

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

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

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

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

554602 ps' <- checkProperties e ps row True

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

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

557− rest <- fresh

605+ rest <- freshType

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

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

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

@@ -588,12 +636,18 @@ check' val ty = do

588636--

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

590638--

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

639+checkProperties ::

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

641+ Expr ->

642+ [(String, Expr)] ->

643+ Type ->

644+ Bool ->

645+ m [(String, Expr)]

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

593647 go [] [] REmpty = return []

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

595649 | lax = return []

596− | otherwise = do u =?= REmpty

650+ | otherwise = do unifyTypes u REmpty

597651 return []

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

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

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

603657 case lookup p ts of

604658 Nothing -> do

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

606− rest <- fresh

607− r =?= RCons p ty rest

660+ rest <- freshType

661+ unifyTypes r (RCons p ty rest)

608662 ps'' <- go ps' ts rest

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

610664 Just ty -> do

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

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

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

615669

616−-- |

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

618−--

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

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

671+checkFunctionApplication ::

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

673+ Expr ->

674+ Type ->

675+ Expr ->

676+ Maybe Type ->

677+ m (Type, Expr)

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

621− subst <- unifyCurrentSubstitution <$> UnifyT get

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

623−

624−-- |

625−-- Check the type of a function application

626−--

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

679+ subst <- gets checkSubstitution

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

681+

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

683+checkFunctionApplication' ::

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

685+ Expr ->

686+ Type ->

687+ Expr ->

688+ Maybe Type ->

689+ m (Type, Expr)

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

629− tyFunction' =?= tyFunction

691+ unifyTypes tyFunction' tyFunction

630692 arg' <- check arg argTy

631693 case ret of

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

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

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

643705 return $ TypedValue True arg'' t'

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

645− ret' <- maybe fresh return ret

646− u =?= function ty ret'

707+ ret' <- maybe freshType return ret

708+ unifyTypes u (function ty ret')

647709 return (ret', App fn arg')

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

649711 checkFunctionApplication fn ty arg ret

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

654716 return (fnTy, App fn dict)

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

656718

657−-- |

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

659−-- TODO: handle constrained types

660−--

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

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

720+-- TODO: is this really needed?

721+meet ::

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

723+ Expr ->

724+ Expr ->

725+ Type ->

726+ Type ->

727+ m (Expr, Expr, Type)

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

663729 t1' <- replaceVarWithUnknown ident t1

664730 meet e1 e2 t1' t2

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

666732 t2' <- replaceVarWithUnknown ident t2

667733 meet e1 e2 t1 t2'

668734meet e1 e2 t1 t2 = do

669− t1 =?= t2

735+ unifyTypes t1 t2

670736 return (e1, e2, t1)

671737

672738-- |

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

@@ -28,7 +28,6 @@ import Data.Maybe (fromMaybe)

2828import qualified Data.Aeson as A

2929import qualified Data.Aeson.TH as A

3030

31−import Control.Monad.Unify

3231import Control.Arrow (second)

3332import Control.Monad ((<=<))

3433

@@ -48,7 +47,7 @@ data Type

4847 -- |

4948 -- A unification variable of type Type

5049 --

51− = TUnknown Unknown

50+ = TUnknown Int

5251 -- |

5352 -- A named type variable

5453 --