d0af878 · rowtype-yoga/purescript-native

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

Merge branch 'master' into pure11

commitd0af878cb25dbe9f854f0f955442428686cd5d08 authorAndy Arvanitis <andyarvanitis@gmail.com> dateSun 8 Nov 2015, 17:47 (11 years ago) parent6dd8b1d 6bedebe

33 files changed+1026−990

compare with golang

unifiedsplit

examples/failing/1175.pursnew file+11

@@ -0,0 +1,11 @@

1+-- @shouldFailWith TypesDoNotUnify

2+module X where

4+class Foo where

5+ foo :: String

7+instance f :: Foo where

8+ foo = "a"

9+ where

10+ bar :: String

11+ bar = 1

examples/passing/1335.pursnew file+12

@@ -0,0 +1,12 @@

1+module Main where

3+import Prelude

4+import Control.Monad.Eff.Console (log)

6+x :: forall a. a -> String

7+x a = y "Done"

8+ where

9+ y :: forall a. (Show a) => a -> String

10+ y a = show (a :: a)

11+

12+main = log (x 0)

psc-bundle/Main.hs+13−14

@@ -12,7 +12,6 @@

1212--

1313-----------------------------------------------------------------------------

1414

15−{-# LANGUAGE PatternGuards #-}

1615{-# LANGUAGE FlexibleContexts #-}

1716{-# LANGUAGE ScopedTypeVariables #-}

1817{-# LANGUAGE TupleSections #-}

@@ -53,16 +52,16 @@ data Options = Options

5352

5453-- | Given a filename, assuming it is in the correct place on disk, infer a ModuleIdentifier.

5554guessModuleIdentifier :: (Applicative m, MonadError ErrorMessage m) => FilePath -> m ModuleIdentifier

56−guessModuleIdentifier filename = ModuleIdentifier (takeFileName (takeDirectory filename)) <$> (guessModuleType (takeFileName filename))

55+guessModuleIdentifier filename = ModuleIdentifier (takeFileName (takeDirectory filename)) <$> guessModuleType (takeFileName filename)

5756 where

5857 guessModuleType "index.js" = pure Regular

59− guessModuleType "foreign.js" = pure Foreign

58+ guessModuleType "foreign.js" = pure Foreign

6059 guessModuleType name = throwError $ UnsupportedModulePath name

6160

6261-- | The main application function.

6362-- This function parses the input files, performs dead code elimination, filters empty modules

6463-- and generates and prints the final Javascript bundle.

65−app :: forall m. (Applicative m, MonadError ErrorMessage m, MonadIO m) => Options -> m String

64+app :: (Applicative m, MonadError ErrorMessage m, MonadIO m) => Options -> m String

6665app Options{..} = do

6766 inputFiles <- concat <$> mapM (liftIO . glob) optionsInputFiles

6867 when (null inputFiles) . liftIO $ do

@@ -72,11 +71,11 @@ app Options{..} = do

7271 js <- liftIO (readFile filename)

7372 mid <- guessModuleIdentifier filename

7473 return (mid, js)

75−

76− let entryIds = (map (`ModuleIdentifier` Regular) optionsEntryPoints)

74+

75+ let entryIds = map (`ModuleIdentifier` Regular) optionsEntryPoints

7776

7877 bundle input entryIds optionsMainModule optionsNamespace optionsRequirePath

79−

78+

8079-- | Command line options parser.

8180options :: Parser Options

8281options = Options <$> some inputFile

@@ -85,29 +84,29 @@ options = Options <$> some inputFile

8584 <*> optional mainModule

8685 <*> namespace

8786 <*> optional requirePath

88− where

87+ where

8988 inputFile :: Parser FilePath

9089 inputFile = strArgument $

9190 metavar "FILE"

9291 <> help "The input .js file(s)"

93−

92+

9493 outputFile :: Parser FilePath

9594 outputFile = strOption $

9695 short 'o'

9796 <> long "output"

9897 <> help "The output .js file"

99−

98+

10099 entryPoint :: Parser String

101100 entryPoint = strOption $

102101 short 'm'

103102 <> long "module"

104103 <> help "Entry point module name(s). All code which is not a transitive dependency of an entry point module will be removed."

105−

104+

106105 mainModule :: Parser String

107106 mainModule = strOption $

108107 long "main"

109108 <> help "Generate code to run the main method in the specified module."

110−

109+

111110 namespace :: Parser String

112111 namespace = strOption $

113112 short 'n'

@@ -122,8 +121,8 @@ options = Options <$> some inputFile

122121 <> long "require-path"

123122 <> Opts.value ""

124123 <> help "The path prefix used in require() calls in the generated JavaScript"

125−

126−-- | Make it go.

124+

125+-- | Make it go.

127126main :: IO ()

128127main = do

129128 opts <- execParser (info (version <*> helper <*> options) infoModList)

psc-docs/Ctags.hs+1−1

@@ -5,7 +5,7 @@ import Tags

55import Data.List (sort)

77dumpCtags :: [(String, P.Module)] -> [String]

8−dumpCtags = sort . concat . (map renderModCtags)

8+dumpCtags = sort . concatMap renderModCtags

1010renderModCtags :: (String, P.Module) -> [String]

1111renderModCtags (path, mdl) = sort tagLines

psc-docs/Etags.hs+1−3

@@ -4,12 +4,10 @@ import qualified Language.PureScript as P

44import Tags

66dumpEtags :: [(String, P.Module)] -> [String]

7−dumpEtags = concat . (map renderModEtags)

7+dumpEtags = concatMap renderModEtags

99renderModEtags :: (String, P.Module) -> [String]

1010renderModEtags (path, mdl) = ["\x0c", path ++ "," ++ show tagsLen] ++ tagLines

1111 where tagsLen = sum $ map length tagLines

1212 tagLines = map tagLine $ tags mdl

1313 tagLine (name, line) = "\x7f" ++ name ++ "\x01" ++ show line ++ ","

14−

15−

psc-publish/tests/Test.hs+2−2

@@ -46,8 +46,8 @@ clonePackage = do

4646 readProcess "git" ["tag", "v999.0.0"] "" >>= putStr

4747

4848bowerInstall :: IO ()

49−bowerInstall = do

50− pushd packageDir $ do

49+bowerInstall =

50+ pushd packageDir $

5151 readProcess "bower" ["install"] "" >>= putStr

5252

5353getPackage :: IO UploadedPackage

psci/Completion.hs+2−6

@@ -172,12 +172,8 @@ getAllQualifications sho m (declName, decl) = do

172172 let q = qualifyWith asQ'

173173 in case importType of

174174 P.Implicit -> [q]

175− P.Explicit refs -> if referencedBy refs

176− then [q]

177− else []

178− P.Hiding refs -> if referencedBy refs

179− then []

180− else [q]

175+ P.Explicit refs -> [q | referencedBy refs]

176+ P.Hiding refs -> [q | not $ referencedBy refs]

181177

182178

183179-- | Returns all the ImportedModule values referring to imports of a particular

psci/PSCi.hs+10−9

@@ -29,17 +29,15 @@ import Data.Tuple (swap)

2929import Data.Version (showVersion)

3030import qualified Data.Map as M

3131

32−import Control.Applicative

3332import Control.Arrow (first)

3433import Control.Monad

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

3635import Control.Monad.Trans.Class

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

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

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

3938import Control.Monad.Trans.State.Strict

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

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

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

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

4341

4442import Options.Applicative as Opts

4543

@@ -253,7 +251,7 @@ modulesDir = ".psci_modules" ++ pathSeparator : "node_modules"

253251-- | This is different than the runMake in 'Language.PureScript.Make' in that it specifies the

254252-- options and ignores the warning messages.

255253runMake :: P.Make a -> IO (Either P.MultipleErrors a)

256−runMake mk = fmap fst $ P.runMake P.defaultOptions mk

254+runMake mk = fst <$> P.runMake P.defaultOptions mk

257255

258256makeIO :: (IOError -> P.ErrorMessage) -> IO a -> P.Make a

259257makeIO f io = do

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

423421 Right env' ->

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

425423 Just (_, typ') -> do

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

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

428429 case k of

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

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

@@ -441,8 +442,8 @@ getCommand singleLineMode = handleInterrupt (return (Right Nothing)) $ do

441442 case firstLine of

442443 Nothing -> return (Right (Just QuitPSCi)) -- Ctrl-D when input is empty

443444 Just "" -> return (Right Nothing)

444− Just s | singleLineMode || head s == ':' -> return . either Left (Right . Just) $ parseCommand s

445− Just s -> either Left (Right . Just) . parseCommand <$> go [s]

445+ Just s | singleLineMode || head s == ':' -> return .fmap Just $ parseCommand s

446+ Just s -> fmap Just . parseCommand <$> go [s]

446447 where

447448 go :: [String] -> InputT (StateT PSCiState IO) String

448449 go ls = maybe (return . unlines $ reverse ls) (go . (:ls)) =<< getInputLine " "

purescript.cabal−1

@@ -190,7 +190,6 @@ library

190190 Language.PureScript.Publish.BoxesHelpers

191191

192192 Control.Monad.Logger

193− Control.Monad.Unify

194193 Control.Monad.Supply

195194 Control.Monad.Supply.Class

196195

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.hs−1

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

1515

1616{-# LANGUAGE DataKinds #-}

1717{-# LANGUAGE FlexibleContexts #-}

18−{-# LANGUAGE RecordWildCards #-}

1918{-# LANGUAGE ScopedTypeVariables #-}

2019

2120module Language.PureScript

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

@@ -19,7 +19,6 @@

1919{-# LANGUAGE FlexibleContexts #-}

2020{-# LANGUAGE ScopedTypeVariables #-}

2121{-# LANGUAGE TupleSections #-}

22−{-# LANGUAGE RecordWildCards #-}

2322

2423module Language.PureScript.Bundle (

2524 bundle

@@ -531,7 +530,7 @@ codeGen optionsMainModule optionsNamespace ms = renderToString (NN (JSSourceElem

531530-- | The bundling function.

532531-- This function performs dead code elimination, filters empty modules

533532-- and generates and prints the final Javascript bundle.

534−bundle :: forall m. (Applicative m, MonadError ErrorMessage m)

533+bundle :: (Applicative m, MonadError ErrorMessage m)

535534 => [(ModuleIdentifier, String)] -- ^ The input modules. Each module should be javascript rendered from 'Language.PureScript.Make' or @psc@.

536535 -> [ModuleIdentifier] -- ^ Entry points. These module identifiers are used as the roots for dead-code elimination

537536 -> Maybe String -- ^ An optional main module.

src/Language/PureScript/Docs/Render.hs+1−3

@@ -49,9 +49,7 @@ renderDeclarationWithOptions opts Declaration{..} =

4949 [ keywordClass ]

5050 ++ maybeToList superclasses

5151 ++ [renderType' (typeApp declTitle args)]

52− ++ if any (isTypeClassMember . cdeclInfo) declChildren

53− then [keywordWhere]

54− else []

52+ ++ [keywordWhere | any (isTypeClassMember . cdeclInfo) declChildren]

5553

5654 where

5755 superclasses

src/Language/PureScript/Errors.hs+17−26

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

@@ -526,7 +513,7 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError

526513 renderSimpleErrorMessage (EscapedSkolem binding) =

527514 paras $ [ line "A type variable has escaped its scope." ]

528515 <> foldMap (\expr -> [ line "Relevant expression: "

529− , indent $ prettyPrintValue expr

516+ , indent $ prettyPrintValue valueDepth expr

530517 ]) binding

531518 renderSimpleErrorMessage (TypesDoNotUnify t1 t2)

532519 = paras [ line "Could not match type"

@@ -581,7 +568,7 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError

581568 renderSimpleErrorMessage (DuplicateLabel l expr) =

582569 paras $ [ line $ "Label " ++ show l ++ " appears more than once in a row type." ]

583570 <> foldMap (\expr' -> [ line "Relevant expression: "

584− , indent $ prettyPrintValue expr'

571+ , indent $ prettyPrintValue valueDepth expr'

585572 ]) expr

586573 renderSimpleErrorMessage (DuplicateTypeArgument name) =

587574 line $ "Type argument " ++ show name ++ " appears more than once."

@@ -590,7 +577,7 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError

590577 renderSimpleErrorMessage (ArgListLengthsDiffer ident) =

591578 line $ "Argument list lengths differ in declaration " ++ showIdent ident

592579 renderSimpleErrorMessage (OverlappingArgNames ident) =

593− line $ "Overlapping names in function/binder" ++ foldMap ((" in declaration" ++) . showIdent) ident

580+ line $ "Overlapping names in function/binder" ++ foldMap ((" in declaration " ++) . showIdent) ident

594581 renderSimpleErrorMessage (MissingClassMember ident) =

595582 line $ "Type class member " ++ showIdent ident ++ " has not been implemented."

596583 renderSimpleErrorMessage (ExtraneousClassMember ident className) =

@@ -607,7 +594,7 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError

607594 line $ "Data constructor " ++ showQualified runProperName nm ++ " was given the wrong number of arguments in a case expression."

608595 renderSimpleErrorMessage (ExprDoesNotHaveType expr ty) =

609596 paras [ line "Expression"

610− , indent $ prettyPrintValue expr

597+ , indent $ prettyPrintValue valueDepth expr

611598 , line "does not have type"

612599 , indent $ typeAsBox ty

613600 ]

@@ -619,7 +606,7 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError

619606 paras [ line "A function of type"

620607 , indent $ typeAsBox fn

621608 , line "can not be applied to the argument"

622− , indent $ prettyPrintValue arg

609+ , indent $ prettyPrintValue valueDepth arg

623610 ]

624611 renderSimpleErrorMessage TypeSynonymInstance =

625612 line "Type class instances for type synonyms are disallowed."

@@ -706,7 +693,7 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError

706693 renderHint (ErrorInExpression expr) detail =

707694 paras [ detail

708695 , Box.hsep 1 Box.top [ Box.text "in the expression"

709− , prettyPrintValue expr

696+ , prettyPrintValue valueDepth expr

710697 ]

711698 ]

712699 renderHint (ErrorInModule mn) detail =

@@ -742,13 +729,13 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError

742729 renderHint (ErrorInferringType expr) detail =

743730 paras [ detail

744731 , Box.hsep 1 Box.top [ line "while inferring the type of"

745− , prettyPrintValue expr

732+ , prettyPrintValue valueDepth expr

746733 ]

747734 ]

748735 renderHint (ErrorCheckingType expr ty) detail =

749736 paras [ detail

750737 , Box.hsep 1 Box.top [ line "while checking that expression"

751− , prettyPrintValue expr

738+ , prettyPrintValue valueDepth expr

752739 ]

753740 , Box.moveRight 2 $ Box.hsep 1 Box.top [ line "has type"

754741 , typeAsBox ty

@@ -757,19 +744,19 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError

757744 renderHint (ErrorCheckingAccessor expr prop) detail =

758745 paras [ detail

759746 , Box.hsep 1 Box.top [ line "while checking type of property accessor"

760− , prettyPrintValue (Accessor prop expr)

747+ , prettyPrintValue valueDepth (Accessor prop expr)

761748 ]

762749 ]

763750 renderHint (ErrorInApplication f t a) detail =

764751 paras [ detail

765752 , Box.hsep 1 Box.top [ line "while applying a function"

766− , prettyPrintValue f

753+ , prettyPrintValue valueDepth f

767754 ]

768755 , Box.moveRight 2 $ Box.hsep 1 Box.top [ line "of type"

769756 , typeAsBox t

770757 ]

771758 , Box.moveRight 2 $ Box.hsep 1 Box.top [ line "to argument"

772− , prettyPrintValue a

759+ , prettyPrintValue valueDepth a

773760 ]

774761 ]

775762 renderHint (ErrorInDataConstructor nm) detail =

@@ -809,6 +796,10 @@ prettyPrintSingleError full level e = prettyPrintErrorMessage <$> onTypesInError

809796 , detail

810797 ]

811798

799+ valueDepth :: Int

800+ valueDepth | full = 1000

801+ | otherwise = 3

802+

812803 levelText :: String

813804 levelText = case level of

814805 Error -> "error"

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/Linter.hs−1

@@ -12,7 +12,6 @@

1212--

1313-----------------------------------------------------------------------------

1414

15−{-# LANGUAGE GeneralizedNewtypeDeriving #-}

1615{-# LANGUAGE FlexibleContexts #-}

1716{-# LANGUAGE ScopedTypeVariables #-}

1817

src/Language/PureScript/Parser/Lexer.hs+1−1

@@ -158,7 +158,7 @@ instance Show PositionedToken where

158158 show = prettyPrintToken . ptToken

159159

160160lex :: FilePath -> String -> Either P.ParseError [PositionedToken]

161−lex filePath input = P.parse parseTokens filePath input

161+lex = P.parse parseTokens

162162

163163parseTokens :: P.Parsec String u [PositionedToken]

164164parseTokens = whitespace *> P.many parsePositionedToken <* P.skipMany parseComment <* P.eof

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

@@ -133,7 +133,7 @@ matchType = buildPrettyPrinter operators matchTypeAtom

133133 ]

134134 , [ Wrap constrained $ \deps ty -> constraintsAsBox deps ty ]

135135 , [ Wrap forall_ $ \idents ty -> text ("forall " ++ unwords idents ++ ". ") <> ty ]

136− , [ Wrap kinded $ \k ty -> ty `before` (text (" :: " ++ prettyPrintKind k)) ]

136+ , [ Wrap kinded $ \k ty -> ty `before` text (" :: " ++ prettyPrintKind k) ]

137137 ]

138138

139139forall_ :: Pattern () Type ([String], Type)

src/Language/PureScript/Pretty/Values.hs+74−68

@@ -38,101 +38,107 @@ list open close f xs = vcat left (zipWith toLine [0 :: Int ..] xs ++ [ text [ cl

3838 where

3939 toLine i a = text [ if i == 0 then open else ',', ' ' ] <> f a

4040

41−prettyPrintObject :: [(String, Maybe Expr)] -> Box

42−prettyPrintObject = list '{' '}' prettyPrintObjectProperty

41+ellipsis :: Box

42+ellipsis = text "..."

43+

44+prettyPrintObject :: Int -> [(String, Maybe Expr)] -> Box

45+prettyPrintObject d = list '{' '}' prettyPrintObjectProperty

4346 where

4447 prettyPrintObjectProperty :: (String, Maybe Expr) -> Box

45− prettyPrintObjectProperty (key, value) = text (prettyPrintObjectKey key ++ ": ") <> maybe (text "_") prettyPrintValue value

48+ prettyPrintObjectProperty (key, value) = text (prettyPrintObjectKey key ++ ": ") <> maybe (text "_") (prettyPrintValue (d - 1)) value

4649

4750-- | Pretty-print an expression

48−prettyPrintValue :: Expr -> Box

49−prettyPrintValue (IfThenElse cond th el) =

50− (text "if " <> prettyPrintValueAtom cond)

51− // moveRight 2 (vcat left [ text "then " <> prettyPrintValueAtom th

52− , text "else " <> prettyPrintValueAtom el

51+prettyPrintValue :: Int -> Expr -> Box

52+prettyPrintValue d _ | d < 0 = text "..."

53+prettyPrintValue d (IfThenElse cond th el) =

54+ (text "if " <> prettyPrintValueAtom (d - 1) cond)

55+ // moveRight 2 (vcat left [ text "then " <> prettyPrintValueAtom (d - 1) th

56+ , text "else " <> prettyPrintValueAtom (d - 1) el

5357 ])

54−prettyPrintValue (Accessor prop val) = prettyPrintValueAtom val <> text ("." ++ show prop)

55−prettyPrintValue (ObjectUpdate o ps) = prettyPrintValueAtom o <> text " " <> list '{' '}' (\(key, val) -> text (key ++ " = ") <> prettyPrintValue val) ps

56−prettyPrintValue (ObjectUpdater o ps) = maybe (text "_") prettyPrintValueAtom o <> text " " <> list '{' '}' (\(key, val) -> text (key ++ " = ") <> maybe (text "_") prettyPrintValue val) ps

57−prettyPrintValue (App val arg) = prettyPrintValueAtom val `beforeWithSpace` prettyPrintValueAtom arg

58−prettyPrintValue (Abs (Left arg) val) = text ('\\' : showIdent arg ++ " -> ") // moveRight 2 (prettyPrintValue val)

59−prettyPrintValue (TypeClassDictionaryConstructorApp className ps) =

60− text (runProperName (disqualify className) ++ " ") <> prettyPrintValueAtom ps

61−prettyPrintValue (Case values binders) =

62− (text "case " <> foldl1 beforeWithSpace (map prettyPrintValueAtom values) <> text " of") //

63− moveRight 2 (vcat left (map prettyPrintCaseAlternative binders))

64−prettyPrintValue (Let ds val) =

58+prettyPrintValue d (Accessor prop val) = prettyPrintValueAtom (d - 1) val <> text ("." ++ show prop)

59+prettyPrintValue d (ObjectUpdate o ps) = prettyPrintValueAtom (d - 1) o <> text " " <> list '{' '}' (\(key, val) -> text (key ++ " = ") <> prettyPrintValue (d - 1) val) ps

60+prettyPrintValue d (ObjectUpdater o ps) = maybe (text "_") (prettyPrintValueAtom (d - 1)) o <> text " " <> list '{' '}' (\(key, val) -> text (key ++ " = ") <> maybe (text "_") (prettyPrintValue (d - 1)) val) ps

61+prettyPrintValue d (App val arg) = prettyPrintValueAtom (d - 1) val `beforeWithSpace` prettyPrintValueAtom (d - 1) arg

62+prettyPrintValue d (Abs (Left arg) val) = text ('\\' : showIdent arg ++ " -> ") // moveRight 2 (prettyPrintValue (d - 1) val)

63+prettyPrintValue d (TypeClassDictionaryConstructorApp className ps) =

64+ text (runProperName (disqualify className) ++ " ") <> prettyPrintValueAtom (d - 1) ps

65+prettyPrintValue d (Case values binders) =

66+ (text "case " <> foldl1 beforeWithSpace (map (prettyPrintValueAtom (d - 1)) values) <> text " of") //

67+ moveRight 2 (vcat left (map (prettyPrintCaseAlternative (d - 1)) binders))

68+prettyPrintValue d (Let ds val) =

6569 text "let" //

66− moveRight 2 (vcat left (map prettyPrintDeclaration ds)) //

67− (text "in " <> prettyPrintValue val)

68−prettyPrintValue (Do els) =

69− text "do " <> vcat left (map prettyPrintDoNotationElement els)

70−prettyPrintValue (TypeClassDictionary (name, tys) _) = foldl1 beforeWithSpace $ text ("#dict " ++ runProperName (disqualify name)) : map typeAtomAsBox tys

71−prettyPrintValue (SuperClassDictionary name _) = text $ "#dict " ++ runProperName (disqualify name)

72−prettyPrintValue (TypedValue _ val _) = prettyPrintValue val

73−prettyPrintValue (PositionedValue _ _ val) = prettyPrintValue val

74−prettyPrintValue expr = prettyPrintValueAtom expr

70+ moveRight 2 (vcat left (map (prettyPrintDeclaration (d - 1)) ds)) //

71+ (text "in " <> prettyPrintValue (d - 1) val)

72+prettyPrintValue d (Do els) =

73+ text "do " <> vcat left (map (prettyPrintDoNotationElement (d - 1)) els)

74+prettyPrintValue _ (TypeClassDictionary (name, tys) _) = foldl1 beforeWithSpace $ text ("#dict " ++ runProperName (disqualify name)) : map typeAtomAsBox tys

75+prettyPrintValue _ (SuperClassDictionary name _) = text $ "#dict " ++ runProperName (disqualify name)

76+prettyPrintValue d (TypedValue _ val _) = prettyPrintValue d val

77+prettyPrintValue d (PositionedValue _ _ val) = prettyPrintValue d val

78+prettyPrintValue d expr = prettyPrintValueAtom d expr

7579

7680-- | Pretty-print an atomic expression, adding parentheses if necessary.

77−prettyPrintValueAtom :: Expr -> Box

78−prettyPrintValueAtom (NumericLiteral n) = text $ either show show n

79−prettyPrintValueAtom (StringLiteral s) = text $ show s

80−prettyPrintValueAtom (CharLiteral c) = text $ show c

81−prettyPrintValueAtom (BooleanLiteral True) = text "true"

82−prettyPrintValueAtom (BooleanLiteral False) = text "false"

83−prettyPrintValueAtom (ArrayLiteral xs) = list '[' ']' prettyPrintValue xs

84−prettyPrintValueAtom (ObjectLiteral ps) = prettyPrintObject $ second Just `map` ps

85−prettyPrintValueAtom (ObjectConstructor ps) = prettyPrintObject ps

86−prettyPrintValueAtom (ObjectGetter prop) = text $ "_." ++ show prop

87−prettyPrintValueAtom (Constructor name) = text $ runProperName (disqualify name)

88−prettyPrintValueAtom (Var ident) = text $ showIdent (disqualify ident)

89−prettyPrintValueAtom (OperatorSection op (Right val)) = ((text "(" <> prettyPrintValue op) `beforeWithSpace` prettyPrintValue val) `before` text ")"

90−prettyPrintValueAtom (OperatorSection op (Left val)) = ((text "(" <> prettyPrintValue val) `beforeWithSpace` prettyPrintValue op) `before` text ")"

91−prettyPrintValueAtom (TypedValue _ val _) = prettyPrintValueAtom val

92−prettyPrintValueAtom (PositionedValue _ _ val) = prettyPrintValueAtom val

93−prettyPrintValueAtom expr = (text "(" <> prettyPrintValue expr) `before` text ")"

94−

95−prettyPrintDeclaration :: Declaration -> Box

96−prettyPrintDeclaration (TypeDeclaration ident ty) =

81+prettyPrintValueAtom :: Int -> Expr -> Box

82+prettyPrintValueAtom _ (NumericLiteral n) = text $ either show show n

83+prettyPrintValueAtom _ (StringLiteral s) = text $ show s

84+prettyPrintValueAtom _ (CharLiteral c) = text $ show c

85+prettyPrintValueAtom _ (BooleanLiteral True) = text "true"

86+prettyPrintValueAtom _ (BooleanLiteral False) = text "false"

87+prettyPrintValueAtom d (ArrayLiteral xs) = list '[' ']' (prettyPrintValue (d - 1)) xs

88+prettyPrintValueAtom d (ObjectLiteral ps) = prettyPrintObject (d - 1) $ second Just `map` ps

89+prettyPrintValueAtom d (ObjectConstructor ps) = prettyPrintObject (d - 1) ps

90+prettyPrintValueAtom _ (ObjectGetter prop) = text $ "_." ++ show prop

91+prettyPrintValueAtom _ (Constructor name) = text $ runProperName (disqualify name)

92+prettyPrintValueAtom _ (Var ident) = text $ showIdent (disqualify ident)

93+prettyPrintValueAtom d (OperatorSection op (Right val)) = ((text "(" <> prettyPrintValue (d - 1) op) `beforeWithSpace` prettyPrintValue (d - 1) val) `before` text ")"

94+prettyPrintValueAtom d (OperatorSection op (Left val)) = ((text "(" <> prettyPrintValue (d - 1) val) `beforeWithSpace` prettyPrintValue (d - 1) op) `before` text ")"

95+prettyPrintValueAtom d (TypedValue _ val _) = prettyPrintValueAtom d val

96+prettyPrintValueAtom d (PositionedValue _ _ val) = prettyPrintValueAtom d val

97+prettyPrintValueAtom d expr = (text "(" <> prettyPrintValue d expr) `before` text ")"

98+

99+prettyPrintDeclaration :: Int -> Declaration -> Box

100+prettyPrintDeclaration d _ | d < 0 = ellipsis

101+prettyPrintDeclaration _ (TypeDeclaration ident ty) =

97102 text (showIdent ident ++ " :: ") <> typeAsBox ty

98−prettyPrintDeclaration (ValueDeclaration ident _ [] (Right val)) =

99− text (showIdent ident ++ " = ") <> prettyPrintValue val

100−prettyPrintDeclaration (BindingGroupDeclaration ds) =

101− vsep 1 left (map (prettyPrintDeclaration . toDecl) ds)

103+prettyPrintDeclaration d (ValueDeclaration ident _ [] (Right val)) =

104+ text (showIdent ident ++ " = ") <> prettyPrintValue (d - 1) val

105+prettyPrintDeclaration d (BindingGroupDeclaration ds) =

106+ vsep 1 left (map (prettyPrintDeclaration (d - 1) . toDecl) ds)

102107 where

103108 toDecl (nm, t, e) = ValueDeclaration nm t [] (Right e)

104−prettyPrintDeclaration (PositionedDeclaration _ _ d) = prettyPrintDeclaration d

105−prettyPrintDeclaration _ = internalError "Invalid argument to prettyPrintDeclaration"

109+prettyPrintDeclaration d (PositionedDeclaration _ _ decl) = prettyPrintDeclaration d decl

110+prettyPrintDeclaration _ _ = internalError "Invalid argument to prettyPrintDeclaration"

106111

107−prettyPrintCaseAlternative :: CaseAlternative -> Box

108−prettyPrintCaseAlternative (CaseAlternative binders result) =

112+prettyPrintCaseAlternative :: Int -> CaseAlternative -> Box

113+prettyPrintCaseAlternative d _ | d < 0 = ellipsis

114+prettyPrintCaseAlternative d (CaseAlternative binders result) =

109115 text (unwords (map prettyPrintBinderAtom binders)) <> prettyPrintResult result

110116 where

111117 prettyPrintResult :: Either [(Guard, Expr)] Expr -> Box

112118 prettyPrintResult (Left gs) =

113119 vcat left (map prettyPrintGuardedValue gs)

114− prettyPrintResult (Right v) = text " -> " <> prettyPrintValue v

120+ prettyPrintResult (Right v) = text " -> " <> prettyPrintValue (d - 1) v

115121

116122 prettyPrintGuardedValue :: (Guard, Expr) -> Box

117123 prettyPrintGuardedValue (grd, val) = foldl1 before

118124 [ text " | "

119− , prettyPrintValue grd

125+ , prettyPrintValue (d - 1) grd

120126 , text " -> "

121− , prettyPrintValue val

127+ , prettyPrintValue (d - 1) val

122128 ]

123129

124−prettyPrintDoNotationElement :: DoNotationElement -> Box

125−prettyPrintDoNotationElement (DoNotationValue val) =

126− prettyPrintValue val

127−prettyPrintDoNotationElement (DoNotationBind binder val) =

128− text (prettyPrintBinder binder ++ " <- ") <> prettyPrintValue val

129−prettyPrintDoNotationElement (DoNotationLet ds) =

130+prettyPrintDoNotationElement :: Int -> DoNotationElement -> Box

131+prettyPrintDoNotationElement d _ | d < 0 = ellipsis

132+prettyPrintDoNotationElement d (DoNotationValue val) =

133+ prettyPrintValue d val

134+prettyPrintDoNotationElement d (DoNotationBind binder val) =

135+ text (prettyPrintBinder binder ++ " <- ") <> prettyPrintValue d val

136+prettyPrintDoNotationElement d (DoNotationLet ds) =

130137 text "let" //

131− moveRight 2 (vcat left (map prettyPrintDeclaration ds))

132−prettyPrintDoNotationElement (PositionedDoNotationElement _ _ el) = prettyPrintDoNotationElement el

138+ moveRight 2 (vcat left (map (prettyPrintDeclaration (d - 1)) ds))

139+prettyPrintDoNotationElement d (PositionedDoNotationElement _ _ el) = prettyPrintDoNotationElement d el

133140

134141prettyPrintBinderAtom :: Binder -> String

135−

136142prettyPrintBinderAtom NullBinder = "_"

137143prettyPrintBinderAtom (StringBinder str) = show str

138144prettyPrintBinderAtom (CharBinder c) = show c

src/Language/PureScript/Sugar/Operators.hs+1−1

@@ -66,7 +66,7 @@ removeSignedLiterals (Module ss coms mn ds exts) = Module ss coms mn (map f' ds)

6666 where

6767 (f', _, _) = everywhereOnValues id go id

6868

69− go (UnaryMinus val) = App (Var (Qualified (Just (ModuleName [ProperName C.prelude])) (Ident C.negate))) val

69+ go (UnaryMinus val) = App (Var (Qualified Nothing (Ident C.negate))) val

7070 go other = other

7171

7272rebracketModule :: (Applicative m, MonadError MultipleErrors m) => [[(Qualified Ident, Expr -> Expr -> Expr, Associativity)]] -> Module -> m Module

src/Language/PureScript/Sugar/TypeClasses/Deriving.hs+232−232

@@ -1,232 +1,232 @@

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

2−--

3−-- Module : Language.PureScript.Sugar.TypeClasses.Deriving

4−-- Copyright : (c) Gershom Bazerman 2015

5−-- License : MIT (http://opensource.org/licenses/MIT)

6−--

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

8−-- Stability : experimental

9−-- Portability :

10−--

11−-- |

12−-- This module implements the generic deriving elaboration that takes place during desugaring.

13−--

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

15−

16−{-# LANGUAGE FlexibleContexts #-}

17−{-# LANGUAGE MultiParamTypeClasses #-}

18−{-# LANGUAGE OverloadedStrings #-}

19−{-# LANGUAGE PatternGuards #-}

20−{-# LANGUAGE RankNTypes #-}

21−{-# LANGUAGE ScopedTypeVariables #-}

22−

23−module Language.PureScript.Sugar.TypeClasses.Deriving (

24− deriveInstances

25−) where

26−

27−import Prelude ()

28−import Prelude.Compat

29−

30−import Data.List (foldl', find, sortBy)

31−import Data.Maybe (fromMaybe)

32−import Data.Ord (comparing)

33−

34−import Control.Monad (replicateM)

35−import Control.Monad.Supply.Class (MonadSupply, freshName)

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

37−

38−import Language.PureScript.Crash

39−import Language.PureScript.AST

40−import Language.PureScript.Environment

41−import Language.PureScript.Errors

42−import Language.PureScript.Names

43−import Language.PureScript.Types

44−import qualified Language.PureScript.Constants as C

45−

46−-- | Elaborates deriving instance declarations by code generation.

47−deriveInstances :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadSupply m) => Module -> m Module

48−deriveInstances (Module ss coms mn ds exts) = Module ss coms mn <$> mapM (deriveInstance mn ds) ds <*> pure exts

49−

50−-- | Takes a declaration, and if the declaration is a deriving TypeInstanceDeclaration,

51−-- elaborates that into an instance declaration via code generation.

52−deriveInstance :: (Functor m, MonadError MultipleErrors m, MonadSupply m) => ModuleName -> [Declaration] -> Declaration -> m Declaration

53−deriveInstance mn ds (TypeInstanceDeclaration nm deps className tys@[ty] DerivedInstance)

54− | className == Qualified (Just dataGeneric) (ProperName C.generic)

55− , Just (Qualified mn' tyCon) <- unwrapTypeConstructor ty

56− , mn == fromMaybe mn mn'

57− = TypeInstanceDeclaration nm deps className tys . ExplicitInstance <$> deriveGeneric mn ds tyCon

58−deriveInstance _ _ (TypeInstanceDeclaration _ _ className tys DerivedInstance)

59− = throwError . errorMessage $ CannotDerive className tys

60−deriveInstance mn ds (PositionedDeclaration pos com d) = PositionedDeclaration pos com <$> deriveInstance mn ds d

61−deriveInstance _ _ e = return e

62−

63−unwrapTypeConstructor :: Type -> Maybe (Qualified ProperName)

64−unwrapTypeConstructor (TypeConstructor tyCon) = Just tyCon

65−unwrapTypeConstructor (TypeApp ty (TypeVar _)) = unwrapTypeConstructor ty

66−unwrapTypeConstructor _ = Nothing

67−

68−dataGeneric :: ModuleName

69−dataGeneric = ModuleName [ ProperName "Data", ProperName "Generic" ]

70−

71−dataMaybe :: ModuleName

72−dataMaybe = ModuleName [ ProperName "Data", ProperName "Maybe" ]

73−

74−deriveGeneric :: (Functor m, MonadError MultipleErrors m, MonadSupply m) => ModuleName -> [Declaration] -> ProperName -> m [Declaration]

75−deriveGeneric mn ds tyConNm = do

76− tyCon <- findTypeDecl tyConNm ds

77− toSpine <- mkSpineFunction mn tyCon

78− fromSpine <- mkFromSpineFunction mn tyCon

79− let toSignature = mkSignatureFunction mn tyCon

80− return [ ValueDeclaration (Ident C.toSpine) Public [] (Right toSpine)

81− , ValueDeclaration (Ident C.fromSpine) Public [] (Right fromSpine)

82− , ValueDeclaration (Ident C.toSignature) Public [] (Right toSignature)

83− ]

84−

85−findTypeDecl :: (Functor m, MonadError MultipleErrors m) => ProperName -> [Declaration] -> m Declaration

86−findTypeDecl tyConNm = maybe (throwError . errorMessage $ CannotFindDerivingType tyConNm) return . find isTypeDecl

87− where

88− isTypeDecl :: Declaration -> Bool

89− isTypeDecl (DataDeclaration _ nm _ _) | nm == tyConNm = True

90− isTypeDecl (PositionedDeclaration _ _ d) = isTypeDecl d

91− isTypeDecl _ = False

92−

93−mkSpineFunction :: forall m. (Functor m, MonadSupply m) => ModuleName -> Declaration -> m Expr

94−mkSpineFunction mn (DataDeclaration _ _ _ args) = lamCase "$x" <$> mapM mkCtorClause args

95− where

96− prodConstructor :: Expr -> Expr

97− prodConstructor = App (Constructor (Qualified (Just dataGeneric) (ProperName "SProd")))

98−

99− recordConstructor :: Expr -> Expr

100− recordConstructor = App (Constructor (Qualified (Just dataGeneric) (ProperName "SRecord")))

101−

102− mkCtorClause :: (ProperName, [Type]) -> m CaseAlternative

103− mkCtorClause (ctorName, tys) = do

104− idents <- replicateM (length tys) (fmap Ident freshName)

105− return $ CaseAlternative [ConstructorBinder (Qualified (Just mn) ctorName) (map VarBinder idents)] (Right (caseResult idents))

106− where

107− caseResult idents =

108− App (prodConstructor (StringLiteral . runProperName $ ctorName))

109− . ArrayLiteral

110− $ zipWith toSpineFun (map (Var . Qualified Nothing) idents) tys

111−

112− toSpineFun :: Expr -> Type -> Expr

113− toSpineFun i r | Just rec <- objectType r =

114− lamNull . recordConstructor . ArrayLiteral .

115− map (\(str,typ) -> ObjectLiteral [("recLabel", StringLiteral str), ("recValue", toSpineFun (Accessor str i) typ)])

116− $ decomposeRec rec

117− toSpineFun i _ = lamNull $ App (mkGenVar C.toSpine) i

118−mkSpineFunction mn (PositionedDeclaration _ _ d) = mkSpineFunction mn d

119−mkSpineFunction _ _ = internalError "mkSpineFunction: expected DataDeclaration"

120−

121−mkSignatureFunction :: ModuleName -> Declaration -> Expr

122−mkSignatureFunction _ (DataDeclaration _ _ _ args) = lamNull . mkSigProd $ map mkProdClause args

123− where

124− mkSigProd :: [Expr] -> Expr

125− mkSigProd = App (Constructor (Qualified (Just dataGeneric) (ProperName "SigProd"))) . ArrayLiteral

126−

127− mkSigRec :: [Expr] -> Expr

128− mkSigRec = App (Constructor (Qualified (Just dataGeneric) (ProperName "SigRecord"))) . ArrayLiteral

129−

130− proxy :: Type -> Type

131− proxy = TypeApp (TypeConstructor (Qualified (Just dataGeneric) (ProperName "Proxy")))

132−

133− mkProdClause :: (ProperName, [Type]) -> Expr

134− mkProdClause (ctorName, tys) = ObjectLiteral [ ("sigConstructor", StringLiteral (runProperName ctorName))

135− , ("sigValues", ArrayLiteral . map mkProductSignature $ tys)

136− ]

137−

138− mkProductSignature :: Type -> Expr

139− mkProductSignature r | Just rec <- objectType r =

140− lamNull . mkSigRec $ [ ObjectLiteral [ ("recLabel", StringLiteral str)

141− , ("recValue", mkProductSignature typ)

142− ]

143− | (str, typ) <- decomposeRec rec

144− ]

145− mkProductSignature typ = lamNull $ App (mkGenVar C.toSignature)

146− (TypedValue False (mkGenVar "anyProxy") (proxy typ))

147−mkSignatureFunction mn (PositionedDeclaration _ _ d) = mkSignatureFunction mn d

148−mkSignatureFunction _ _ = internalError "mkSignatureFunction: expected DataDeclaration"

149−

150−mkFromSpineFunction :: forall m. (Functor m, MonadSupply m) => ModuleName -> Declaration -> m Expr

151−mkFromSpineFunction mn (DataDeclaration _ _ _ args) = lamCase "$x" <$> (addCatch <$> mapM mkAlternative args)

152− where

153− mkJust :: Expr -> Expr

154− mkJust = App (Constructor (Qualified (Just dataMaybe) (ProperName "Just")))

155−

156− mkNothing :: Expr

157− mkNothing = Constructor (Qualified (Just dataMaybe) (ProperName "Nothing"))

158−

159− prodBinder :: [Binder] -> Binder

160− prodBinder = ConstructorBinder (Qualified (Just dataGeneric) (ProperName "SProd"))

161−

162− recordBinder :: [Binder] -> Binder

163− recordBinder = ConstructorBinder (Qualified (Just dataGeneric) (ProperName "SRecord"))

164−

165− mkAlternative :: (ProperName, [Type]) -> m CaseAlternative

166− mkAlternative (ctorName, tys) = do

167− idents <- replicateM (length tys) (fmap Ident freshName)

168− return $ CaseAlternative [ prodBinder [ StringBinder (runProperName ctorName), ArrayBinder (map VarBinder idents)]]

169− . Right

170− $ liftApplicative (mkJust $ Constructor (Qualified (Just mn) ctorName))

171− (zipWith fromSpineFun (map (Var . (Qualified Nothing)) idents) tys)

172−

173− addCatch :: [CaseAlternative] -> [CaseAlternative]

174− addCatch = (++ [catchAll])

175− where

176− catchAll = CaseAlternative [NullBinder] (Right mkNothing)

177−

178− fromSpineFun e r

179− | Just rec <- objectType r

180− = App (lamCase "r" [ mkRecCase (decomposeRec rec)

181− , CaseAlternative [NullBinder] (Right mkNothing)

182− ])

183− (App e (mkPrelVar "unit"))

184−

185− fromSpineFun e _ = App (mkGenVar C.fromSpine) (App e (mkPrelVar "unit"))

186−

187− mkRecCase rs = CaseAlternative [ recordBinder [ ArrayBinder (map (VarBinder . Ident . fst) rs)

188− ]

189− ]

190− . Right

191− $ liftApplicative (mkRecFun rs) (map (\(x, y) -> fromSpineFun (Accessor "recValue" (mkVar x)) y) rs)

192−

193− mkRecFun :: [(String, Type)] -> Expr

194− mkRecFun xs = mkJust $ foldr (\s e -> lam s e) recLiteral (map fst xs)

195− where recLiteral = ObjectLiteral $ map (\(s,_) -> (s,mkVar s)) xs

196−mkFromSpineFunction mn (PositionedDeclaration _ _ d) = mkFromSpineFunction mn d

197−mkFromSpineFunction _ _ = internalError "mkFromSpineFunction: expected DataDeclaration"

198−

199−-- Helpers

200−

201−objectType :: Type -> Maybe Type

202−objectType (TypeApp (TypeConstructor (Qualified (Just (ModuleName [ProperName "Prim"])) (ProperName "Object"))) rec) = Just rec

203−objectType _ = Nothing

204−

205−lam :: String -> Expr -> Expr

206−lam s = Abs (Left (Ident s))

207−

208−lamNull :: Expr -> Expr

209−lamNull = lam "$q"

210−

211−lamCase :: String -> [CaseAlternative] -> Expr

212−lamCase s = lam s . Case [mkVar s]

213−

214−liftApplicative :: Expr -> [Expr] -> Expr

215−liftApplicative = foldl' (\x e -> App (App (mkPrelVar "apply") x) e)

216−

217−mkVarMn :: Maybe ModuleName -> String -> Expr

218−mkVarMn mn s = Var (Qualified mn (Ident s))

219−

220−mkVar :: String -> Expr

221−mkVar s = mkVarMn Nothing s

222−

223−mkPrelVar :: String -> Expr

224−mkPrelVar s = mkVarMn (Just (ModuleName [ProperName C.prelude])) s

225−

226−mkGenVar :: String -> Expr

227−mkGenVar s = mkVarMn (Just (ModuleName [ProperName "Data", ProperName C.generic])) s

228−

229−decomposeRec :: Type -> [(String, Type)]

230−decomposeRec = sortBy (comparing fst) . go

231− where go (RCons str typ typs) = (str, typ) : decomposeRec typs

232− go _ = []

1+-----------------------------------------------------------------------------

2+--

3+-- Module : Language.PureScript.Sugar.TypeClasses.Deriving

4+-- Copyright : (c) Gershom Bazerman 2015

5+-- License : MIT (http://opensource.org/licenses/MIT)

6+--

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

8+-- Stability : experimental

9+-- Portability :

10+--

11+-- |

12+-- This module implements the generic deriving elaboration that takes place during desugaring.

13+--

14+-----------------------------------------------------------------------------

15+

16+{-# LANGUAGE FlexibleContexts #-}

17+{-# LANGUAGE MultiParamTypeClasses #-}

18+{-# LANGUAGE OverloadedStrings #-}

19+{-# LANGUAGE PatternGuards #-}

20+{-# LANGUAGE RankNTypes #-}

21+{-# LANGUAGE ScopedTypeVariables #-}

22+

23+module Language.PureScript.Sugar.TypeClasses.Deriving (

24+ deriveInstances

25+) where

26+

27+import Prelude ()

28+import Prelude.Compat

29+

30+import Data.List (foldl', find, sortBy)

31+import Data.Maybe (fromMaybe)

32+import Data.Ord (comparing)

33+

34+import Control.Monad (replicateM)

35+import Control.Monad.Supply.Class (MonadSupply, freshName)

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

37+

38+import Language.PureScript.Crash

39+import Language.PureScript.AST

40+import Language.PureScript.Environment

41+import Language.PureScript.Errors

42+import Language.PureScript.Names

43+import Language.PureScript.Types

44+import qualified Language.PureScript.Constants as C

45+

46+-- | Elaborates deriving instance declarations by code generation.

47+deriveInstances :: (Functor m, Applicative m, MonadError MultipleErrors m, MonadSupply m) => Module -> m Module

48+deriveInstances (Module ss coms mn ds exts) = Module ss coms mn <$> mapM (deriveInstance mn ds) ds <*> pure exts

49+

50+-- | Takes a declaration, and if the declaration is a deriving TypeInstanceDeclaration,

51+-- elaborates that into an instance declaration via code generation.

52+deriveInstance :: (Functor m, MonadError MultipleErrors m, MonadSupply m) => ModuleName -> [Declaration] -> Declaration -> m Declaration

53+deriveInstance mn ds (TypeInstanceDeclaration nm deps className tys@[ty] DerivedInstance)

54+ | className == Qualified (Just dataGeneric) (ProperName C.generic)

55+ , Just (Qualified mn' tyCon) <- unwrapTypeConstructor ty

56+ , mn == fromMaybe mn mn'

57+ = TypeInstanceDeclaration nm deps className tys . ExplicitInstance <$> deriveGeneric mn ds tyCon

58+deriveInstance _ _ (TypeInstanceDeclaration _ _ className tys DerivedInstance)

59+ = throwError . errorMessage $ CannotDerive className tys

60+deriveInstance mn ds (PositionedDeclaration pos com d) = PositionedDeclaration pos com <$> deriveInstance mn ds d

61+deriveInstance _ _ e = return e

62+

63+unwrapTypeConstructor :: Type -> Maybe (Qualified ProperName)

64+unwrapTypeConstructor (TypeConstructor tyCon) = Just tyCon

65+unwrapTypeConstructor (TypeApp ty (TypeVar _)) = unwrapTypeConstructor ty

66+unwrapTypeConstructor _ = Nothing

67+

68+dataGeneric :: ModuleName

69+dataGeneric = ModuleName [ ProperName "Data", ProperName "Generic" ]

70+

71+dataMaybe :: ModuleName

72+dataMaybe = ModuleName [ ProperName "Data", ProperName "Maybe" ]

73+

74+deriveGeneric :: (Functor m, MonadError MultipleErrors m, MonadSupply m) => ModuleName -> [Declaration] -> ProperName -> m [Declaration]

75+deriveGeneric mn ds tyConNm = do

76+ tyCon <- findTypeDecl tyConNm ds

77+ toSpine <- mkSpineFunction mn tyCon

78+ fromSpine <- mkFromSpineFunction mn tyCon

79+ let toSignature = mkSignatureFunction mn tyCon

80+ return [ ValueDeclaration (Ident C.toSpine) Public [] (Right toSpine)

81+ , ValueDeclaration (Ident C.fromSpine) Public [] (Right fromSpine)

82+ , ValueDeclaration (Ident C.toSignature) Public [] (Right toSignature)

83+ ]

84+

85+findTypeDecl :: (Functor m, MonadError MultipleErrors m) => ProperName -> [Declaration] -> m Declaration

86+findTypeDecl tyConNm = maybe (throwError . errorMessage $ CannotFindDerivingType tyConNm) return . find isTypeDecl

87+ where

88+ isTypeDecl :: Declaration -> Bool

89+ isTypeDecl (DataDeclaration _ nm _ _) | nm == tyConNm = True

90+ isTypeDecl (PositionedDeclaration _ _ d) = isTypeDecl d

91+ isTypeDecl _ = False

92+

93+mkSpineFunction :: forall m. (Functor m, MonadSupply m) => ModuleName -> Declaration -> m Expr

94+mkSpineFunction mn (DataDeclaration _ _ _ args) = lamCase "$x" <$> mapM mkCtorClause args

95+ where

96+ prodConstructor :: Expr -> Expr

97+ prodConstructor = App (Constructor (Qualified (Just dataGeneric) (ProperName "SProd")))

98+

99+ recordConstructor :: Expr -> Expr

100+ recordConstructor = App (Constructor (Qualified (Just dataGeneric) (ProperName "SRecord")))

101+

102+ mkCtorClause :: (ProperName, [Type]) -> m CaseAlternative

103+ mkCtorClause (ctorName, tys) = do

104+ idents <- replicateM (length tys) (fmap Ident freshName)

105+ return $ CaseAlternative [ConstructorBinder (Qualified (Just mn) ctorName) (map VarBinder idents)] (Right (caseResult idents))

106+ where

107+ caseResult idents =

108+ App (prodConstructor (StringLiteral . runProperName $ ctorName))

109+ . ArrayLiteral

110+ $ zipWith toSpineFun (map (Var . Qualified Nothing) idents) tys

111+

112+ toSpineFun :: Expr -> Type -> Expr

113+ toSpineFun i r | Just rec <- objectType r =

114+ lamNull . recordConstructor . ArrayLiteral .

115+ map (\(str,typ) -> ObjectLiteral [("recLabel", StringLiteral str), ("recValue", toSpineFun (Accessor str i) typ)])

116+ $ decomposeRec rec

117+ toSpineFun i _ = lamNull $ App (mkGenVar C.toSpine) i

118+mkSpineFunction mn (PositionedDeclaration _ _ d) = mkSpineFunction mn d

119+mkSpineFunction _ _ = internalError "mkSpineFunction: expected DataDeclaration"

120+

121+mkSignatureFunction :: ModuleName -> Declaration -> Expr

122+mkSignatureFunction _ (DataDeclaration _ _ _ args) = lamNull . mkSigProd $ map mkProdClause args

123+ where

124+ mkSigProd :: [Expr] -> Expr

125+ mkSigProd = App (Constructor (Qualified (Just dataGeneric) (ProperName "SigProd"))) . ArrayLiteral

126+

127+ mkSigRec :: [Expr] -> Expr

128+ mkSigRec = App (Constructor (Qualified (Just dataGeneric) (ProperName "SigRecord"))) . ArrayLiteral

129+

130+ proxy :: Type -> Type

131+ proxy = TypeApp (TypeConstructor (Qualified (Just dataGeneric) (ProperName "Proxy")))

132+

133+ mkProdClause :: (ProperName, [Type]) -> Expr

134+ mkProdClause (ctorName, tys) = ObjectLiteral [ ("sigConstructor", StringLiteral (runProperName ctorName))

135+ , ("sigValues", ArrayLiteral . map mkProductSignature $ tys)

136+ ]

137+

138+ mkProductSignature :: Type -> Expr

139+ mkProductSignature r | Just rec <- objectType r =

140+ lamNull . mkSigRec $ [ ObjectLiteral [ ("recLabel", StringLiteral str)

141+ , ("recValue", mkProductSignature typ)

142+ ]

143+ | (str, typ) <- decomposeRec rec

144+ ]

145+ mkProductSignature typ = lamNull $ App (mkGenVar C.toSignature)

146+ (TypedValue False (mkGenVar "anyProxy") (proxy typ))

147+mkSignatureFunction mn (PositionedDeclaration _ _ d) = mkSignatureFunction mn d

148+mkSignatureFunction _ _ = internalError "mkSignatureFunction: expected DataDeclaration"

149+

150+mkFromSpineFunction :: forall m. (Functor m, MonadSupply m) => ModuleName -> Declaration -> m Expr

151+mkFromSpineFunction mn (DataDeclaration _ _ _ args) = lamCase "$x" <$> (addCatch <$> mapM mkAlternative args)

152+ where

153+ mkJust :: Expr -> Expr

154+ mkJust = App (Constructor (Qualified (Just dataMaybe) (ProperName "Just")))

155+

156+ mkNothing :: Expr

157+ mkNothing = Constructor (Qualified (Just dataMaybe) (ProperName "Nothing"))

158+

159+ prodBinder :: [Binder] -> Binder

160+ prodBinder = ConstructorBinder (Qualified (Just dataGeneric) (ProperName "SProd"))

161+

162+ recordBinder :: [Binder] -> Binder

163+ recordBinder = ConstructorBinder (Qualified (Just dataGeneric) (ProperName "SRecord"))

164+

165+ mkAlternative :: (ProperName, [Type]) -> m CaseAlternative

166+ mkAlternative (ctorName, tys) = do

167+ idents <- replicateM (length tys) (fmap Ident freshName)

168+ return $ CaseAlternative [ prodBinder [ StringBinder (runProperName ctorName), ArrayBinder (map VarBinder idents)]]

169+ . Right

170+ $ liftApplicative (mkJust $ Constructor (Qualified (Just mn) ctorName))

171+ (zipWith fromSpineFun (map (Var . Qualified Nothing) idents) tys)

172+

173+ addCatch :: [CaseAlternative] -> [CaseAlternative]

174+ addCatch = (++ [catchAll])

175+ where

176+ catchAll = CaseAlternative [NullBinder] (Right mkNothing)

177+

178+ fromSpineFun e r

179+ | Just rec <- objectType r

180+ = App (lamCase "r" [ mkRecCase (decomposeRec rec)

181+ , CaseAlternative [NullBinder] (Right mkNothing)

182+ ])

183+ (App e (mkPrelVar "unit"))

184+

185+ fromSpineFun e _ = App (mkGenVar C.fromSpine) (App e (mkPrelVar "unit"))

186+

187+ mkRecCase rs = CaseAlternative [ recordBinder [ ArrayBinder (map (VarBinder . Ident . fst) rs)

188+ ]

189+ ]

190+ . Right

191+ $ liftApplicative (mkRecFun rs) (map (\(x, y) -> fromSpineFun (Accessor "recValue" (mkVar x)) y) rs)

192+

193+ mkRecFun :: [(String, Type)] -> Expr

194+ mkRecFun xs = mkJust $ foldr lam recLiteral (map fst xs)

195+ where recLiteral = ObjectLiteral $ map (\(s,_) -> (s,mkVar s)) xs

196+mkFromSpineFunction mn (PositionedDeclaration _ _ d) = mkFromSpineFunction mn d

197+mkFromSpineFunction _ _ = internalError "mkFromSpineFunction: expected DataDeclaration"

198+

199+-- Helpers

200+

201+objectType :: Type -> Maybe Type

202+objectType (TypeApp (TypeConstructor (Qualified (Just (ModuleName [ProperName "Prim"])) (ProperName "Object"))) rec) = Just rec

203+objectType _ = Nothing

204+

205+lam :: String -> Expr -> Expr

206+lam s = Abs (Left (Ident s))

207+

208+lamNull :: Expr -> Expr

209+lamNull = lam "$q"

210+

211+lamCase :: String -> [CaseAlternative] -> Expr

212+lamCase s = lam s . Case [mkVar s]

213+

214+liftApplicative :: Expr -> [Expr] -> Expr

215+liftApplicative = foldl' (\x e -> App (App (mkPrelVar "apply") x) e)

216+

217+mkVarMn :: Maybe ModuleName -> String -> Expr

218+mkVarMn mn s = Var (Qualified mn (Ident s))

219+

220+mkVar :: String -> Expr

221+mkVar = mkVarMn Nothing

222+

223+mkPrelVar :: String -> Expr

224+mkPrelVar = mkVarMn (Just (ModuleName [ProperName C.prelude]))

225+

226+mkGenVar :: String -> Expr

227+mkGenVar = mkVarMn (Just (ModuleName [ProperName "Data", ProperName C.generic]))

228+

229+decomposeRec :: Type -> [(String, Type)]

230+decomposeRec = sortBy (comparing fst) . go

231+ where go (RCons str typ typs) = (str, typ) : decomposeRec typs

232+ go _ = []

src/Language/PureScript/Sugar/TypeDeclarations.hs+5−1

@@ -61,9 +61,13 @@ desugarTypeDeclarationsModule ms = forM ms $ \(Module ss coms name ds exps) ->

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

6262 f' (Left gs) = Left <$> mapM (pairM return f) gs

6363 f' (Right v) = Right <$> f v

64− (:) <$> (ValueDeclaration name nameKind bs <$> f' val) <*> desugarTypeDeclarations rest

64+ (:) <$> (ValueDeclaration name nameKind bs <$> f' val)

65+ <*> desugarTypeDeclarations rest

6566 where

6667 go (Let ds val') = Let <$> desugarTypeDeclarations ds <*> pure val'

6768 go other = return other

69+ desugarTypeDeclarations (TypeInstanceDeclaration nm deps cls args (ExplicitInstance ds) : rest) =

70+ (:) <$> (TypeInstanceDeclaration nm deps cls args . ExplicitInstance <$> desugarTypeDeclarations ds)

71+ <*> desugarTypeDeclarations rest

6872 desugarTypeDeclarations (d:ds) = (:) d <$> desugarTypeDeclarations ds

6973 desugarTypeDeclarations [] = return []

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

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

1313--

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

1515

16+{-# LANGUAGE FlexibleContexts #-}

17+

1618module Language.PureScript.TypeChecker.Skolems (

1719 newSkolemConstant,

1820 introduceSkolemScope,

@@ -27,26 +29,31 @@ import Prelude.Compat

2729

2830import Data.List (nub, (\\))

2931import Data.Monoid

32+import Data.Functor.Identity (Identity(), runIdentity)

3033

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

32−import Control.Monad.Unify

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

3336

3437import Language.PureScript.Crash

3538import Language.PureScript.AST

3639import Language.PureScript.Errors

3740import Language.PureScript.TypeChecker.Monad

3841import Language.PureScript.Types

42+import Language.PureScript.Traversals (defS)

3943

4044-- |

4145-- Generate a new skolem constant

4246--

43−newSkolemConstant :: UnifyT Type Check Int

44−newSkolemConstant = fresh'

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

48+newSkolemConstant = do

49+ s <- gets checkNextSkolem

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

51+ return s

4552

4653-- |

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

4855--

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

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

5057introduceSkolemScope = everywhereOnTypesM go

5158 where

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

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

5562-- |

5663-- Generate a new skolem scope

5764--

58−newSkolemScope :: UnifyT Type Check SkolemScope

59−newSkolemScope = SkolemScope <$> fresh'

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

66+newSkolemScope = do

67+ s <- gets checkNextSkolemScope

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

69+ return $ SkolemScope s

6070

6171-- |

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

@@ -70,21 +80,31 @@ skolemize ident sko scope = replaceTypeVars ident (Skolem ident sko scope)

7080-- only example of scoped type variables.

7181--

7282skolemizeTypesInValue :: String -> Int -> SkolemScope -> Expr -> Expr

73−skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id onExpr onBinder in f

83+skolemizeTypesInValue ident sko scope =

84+ let

85+ (_, f, _, _, _) = everywhereWithContextOnValuesM [] defS onExpr onBinder defS defS

86+ in runIdentity . f

7487 where

75− onExpr :: Expr -> Expr

76− onExpr (SuperClassDictionary c ts) = SuperClassDictionary c (map (skolemize ident sko scope) ts)

77− onExpr (TypedValue check val ty) = TypedValue check val (skolemize ident sko scope ty)

78− onExpr other = other

88+ onExpr :: [String] -> Expr -> Identity ([String], Expr)

89+ onExpr sco (SuperClassDictionary c ts)

90+ | ident `notElem` sco = return (sco, SuperClassDictionary c (map (skolemize ident sko scope) ts))

91+ onExpr sco (TypedValue check val ty)

92+ | ident `notElem` sco = return (sco ++ peelTypeVars ty, TypedValue check val (skolemize ident sko scope ty))

93+ onExpr sco other = return (sco, other)

94+

95+ onBinder :: [String] -> Binder -> Identity ([String], Binder)

96+ onBinder sco (TypedBinder ty b)

97+ | ident `notElem` sco = return (sco ++ peelTypeVars ty, TypedBinder (skolemize ident sko scope ty) b)

98+ onBinder sco other = return (sco, other)

7999

80− onBinder :: Binder -> Binder

81− onBinder (TypedBinder ty b) = TypedBinder (skolemize ident sko scope ty) b

82− onBinder other = other

100+ peelTypeVars :: Type -> [String]

101+ peelTypeVars (ForAll i ty _) = i : peelTypeVars ty

102+ peelTypeVars _ = []

83103

84104-- |

85105-- Ensure skolem variables do not escape their scope

86106--

87−skolemEscapeCheck :: Expr -> Check ()

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

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

89109skolemEscapeCheck root@TypedValue{} =

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

tests/Main.hs−1

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

1414{-# LANGUAGE DataKinds #-}

1515{-# LANGUAGE DoAndIfThenElse #-}

1616{-# LANGUAGE TupleSections #-}

17−{-# LANGUAGE GeneralizedNewtypeDeriving #-}

1817{-# LANGUAGE FlexibleInstances #-}

1918

2019-- Failing tests can specify the kind of error that should be thrown with a