purescript 0.6.6 → 0.6.7

raw patch · 19 files changed

+364/−111 lines, 19 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• examples/passing/Operators.purs +6/−0
• examples/passing/RowPolyInstanceContext.purs +20/−0
• examples/passing/ScopedTypeVariables.purs +34/−0
• examples/passing/UnknownInInstance.purs +8/−0
• prelude/prelude.purs +17/−0
• psc-docs/Main.hs +66/−31
• psci/Commands.hs +1/−1
• psci/Main.hs +26/−14
• psci/Parser.hs +1/−1
• purescript.cabal +1/−1
• src/Language/PureScript/CodeGen/JS/Common.hs +42/−2
• src/Language/PureScript/Environment.hs +6/−1
• src/Language/PureScript/Parser/Lexer.hs +1/−0
• src/Language/PureScript/TypeChecker/Entailment.hs +26/−3
• src/Language/PureScript/TypeChecker/Kinds.hs +69/−42
• src/Language/PureScript/TypeChecker/Monad.hs +6/−0
• src/Language/PureScript/TypeChecker/Skolems.hs +1/−0
• src/Language/PureScript/TypeChecker/Types.hs +16/−15
• src/Language/PureScript/TypeChecker/Unify.hs +17/−0

@@ -73,6 +73,11 @@   test19 :: Number   test19 = negate $ negate (-1) +  test20 :: Number+  test20 = 1 @ 2+    where+    (@) x y = x + y * y+   main = do     let t1 = test1 1 2 (\x y -> x + y)     let t2 = test2@@ -93,4 +98,5 @@     let t17 = test17     let t18 = test18     let t19 = test19+    let t20 = test20     trace "Done"

@@ -0,0 +1,20 @@+module Main where++class T s m where+  state :: (s -> s) -> m Unit++data S s a = S (s -> { new :: s, ret :: a })++instance st :: T s (S s) where+  state f = S $ \s -> { new: f s, ret: unit }++test1 :: forall r . S { foo :: String | r } Unit+test1 = state $ \o -> o { foo = o.foo ++ "!" }++test2 :: forall m r . (T { foo :: String | r } m) => m Unit+test2 = state $ \o -> o { foo = o.foo ++ "!" }++main = do+  let t1 = test1+  let t2 = test2+  Debug.Trace.trace "Done"

@@ -0,0 +1,34 @@+module Main where++test1 :: forall a. (a -> a) -> a -> a+test1 f x = g (g x)+  where+  g :: a -> a+  g y = f (f y)++test2 :: forall a. (a -> a) -> a -> a+test2 = h+  where+  h :: forall b. (b -> b) -> b -> b+  h f x = g (g x)+    where+    g :: b -> b+    g y = f (f y)++test3 :: Number +test3 = ((\b -> b :: b) :: forall b. b -> b) 0++test4 :: forall a. (a -> a) -> a -> a+test4 = h+  where+  h :: forall b. (b -> b) -> b -> b+  h f x = g (g x)+    where+    g :: b -> b+    g y = j (f (f y))+      where+      j :: forall b. b -> b+      j x = x+++main = Debug.Trace.trace "Done"

@@ -0,0 +1,8 @@+module Main where++data Proxy a = Proxy++test :: forall a. (Show (Proxy a)) => String+test = show Proxy++main = Debug.Trace.trace "Done"

@@ -24,15 +24,32 @@   , Unit(..), unit   ) where +  -- | An alias for `true`, which can be useful in guard clauses: +  -- | +  -- | E.g.+  -- | +  -- |     max x y | x >= y = x +  -- |             | otherwise = y   otherwise :: Boolean   otherwise = true +  -- | Flips the order of the arguments to a function of two arguments.    flip :: forall a b c. (a -> b -> c) -> b -> a -> c   flip f b a = f a b +  -- | Returns its first argument and ignores its second.    const :: forall a b. a -> b -> a   const a _ = a +  -- | This function returns its first argument, and can be used to assert type equalities.+  -- | This can be useful when types are otherwise ambiguous. +  -- | +  -- | E.g.+  -- | +  -- |     main = print $ [] `asTypeOf` [0]+  -- |+  -- | If instead, we had written `main = print []`, the type of the argument `[]` would have+  -- | been ambiguous, resulting in a compile-time error.   asTypeOf :: forall a. a -> a -> a   asTypeOf x _ = x 

@@ -22,6 +22,7 @@ import Data.List import Data.Maybe (fromMaybe) import Data.Version (showVersion)+import Data.Foldable (traverse_)  import Options.Applicative @@ -30,13 +31,11 @@ import System.Exit (exitSuccess, exitFailure) import System.IO (hPutStrLn, stderr) - data PSCDocsOptions = PSCDocsOptions   { pscdIncludeHeir :: Bool   , pscdInputFiles  :: [FilePath]   } - docgen :: PSCDocsOptions -> IO () docgen (PSCDocsOptions showHierarchy input) = do   e <- P.parseModulesFromFiles (fromMaybe "") <$> mapM (fmap (first Just) . parseFile) (nub input)@@ -62,11 +61,17 @@ headerLevel :: Int -> String -> Docs headerLevel level hdr = tell [replicate level '#' ++ ' ' : hdr] +withIndent :: Int -> Docs -> Docs+withIndent indent = censor (map (replicate indent ' ' ++ ))+ atIndent :: Int -> String -> Docs atIndent indent text =   let ls = lines text in-  forM_ ls $ \l -> tell [replicate indent ' ' ++ l]+  withIndent indent (tell ls) +ticks :: String -> String+ticks = ("`" ++) . (++ "`")+ renderModules :: Bool -> [P.Module] -> Docs renderModules showHierarchy ms = do   headerLevel 1 "Module Documentation"@@ -109,61 +114,91 @@  renderTopLevel :: Maybe [P.DeclarationRef] -> [P.Declaration] -> Docs renderTopLevel exps decls = forM_ (sortBy (compare `on` getName) decls) $ \decl -> do-  renderDeclaration 4 exps decl+  traverse_ (headerLevel 4) (ticks `fmap` getDeclarationTitle decl)   spacer+  renderDeclaration exps decl+  spacer  renderTypeclassImage :: P.ModuleName -> Docs renderTypeclassImage name =   let name' = P.runModuleName name   in tell ["![" ++ name' ++ "](images/" ++ name' ++ ".png)"] -renderDeclaration :: Int -> Maybe [P.DeclarationRef] -> P.Declaration -> Docs-renderDeclaration n _ (P.TypeDeclaration ident ty) =-  atIndent n $ show ident ++ " :: " ++ prettyPrintType' ty-renderDeclaration n _ (P.ExternDeclaration _ ident _ ty) =-  atIndent n $ show ident ++ " :: " ++ prettyPrintType' ty-renderDeclaration n exps (P.DataDeclaration dtype name args ctors) = do+getDeclarationTitle :: P.Declaration -> Maybe String+getDeclarationTitle (P.TypeDeclaration name _)                      = Just (show name)+getDeclarationTitle (P.ExternDeclaration _ name _ _)                = Just (show name)+getDeclarationTitle (P.DataDeclaration _ name _ _)                  = Just (show name)+getDeclarationTitle (P.ExternDataDeclaration name _)                = Just (show name)+getDeclarationTitle (P.TypeSynonymDeclaration name _ _)             = Just (show name)+getDeclarationTitle (P.TypeClassDeclaration name _ _ _)   = Just (show name)+getDeclarationTitle (P.TypeInstanceDeclaration name _ _ _ _)        = Just (show name)+getDeclarationTitle (P.PositionedDeclaration _ _ d)                 = getDeclarationTitle d+getDeclarationTitle _                                               = Nothing++renderDeclaration :: Maybe [P.DeclarationRef] -> P.Declaration -> Docs+renderDeclaration _ (P.TypeDeclaration ident ty) =+  atIndent 4 $ show ident ++ " :: " ++ prettyPrintType' ty+renderDeclaration _ (P.ExternDeclaration _ ident _ ty) =+  atIndent 4 $ show ident ++ " :: " ++ prettyPrintType' ty+renderDeclaration exps (P.DataDeclaration dtype name args ctors) = do   let     typeApp  = foldl P.TypeApp (P.TypeConstructor (P.Qualified Nothing name)) (map toTypeVar args)     typeName = prettyPrintType' typeApp     exported = filter (P.isDctorExported name exps . fst) ctors-  atIndent n $ show dtype ++ " " ++ typeName ++ (if null exported then "" else " where")-  forM_ exported $ \(ctor, tys) ->-    let ctorTy = foldr P.function typeApp tys-    in atIndent (n + 2) $ P.runProperName ctor ++ " :: " ++ prettyPrintType' ctorTy-renderDeclaration n _ (P.ExternDataDeclaration name kind) =-  atIndent n $ "data " ++ P.runProperName name ++ " :: " ++ P.prettyPrintKind kind-renderDeclaration n _ (P.TypeSynonymDeclaration name args ty) = do+  atIndent 4 $ show dtype ++ " " ++ typeName+  zipWithM_ (\isFirst (ctor, tys) ->+              atIndent 6 $ (if isFirst then "= " else "| ") ++ P.runProperName ctor ++ " " ++ unwords (map P.prettyPrintTypeAtom tys))+            (True : repeat False) exported+renderDeclaration _ (P.ExternDataDeclaration name kind) =+  atIndent 4 $ "data " ++ P.runProperName name ++ " :: " ++ P.prettyPrintKind kind+renderDeclaration _ (P.TypeSynonymDeclaration name args ty) = do   let     typeApp  = foldl P.TypeApp (P.TypeConstructor (P.Qualified Nothing name)) (map toTypeVar args)     typeName = prettyPrintType' typeApp-  atIndent n $ "type " ++ typeName ++ " = " ++ prettyPrintType' ty-renderDeclaration n exps (P.TypeClassDeclaration name args implies ds) = do+  atIndent 4 $ "type " ++ typeName ++ " = " ++ prettyPrintType' ty+renderDeclaration _ (P.TypeClassDeclaration name args implies ds) = do   let impliesText = case implies of                       [] -> ""                       is -> "(" ++ intercalate ", " (map (\(pn, tys') -> show pn ++ " " ++ unwords (map P.prettyPrintTypeAtom tys')) is) ++ ") <= "       classApp  = foldl P.TypeApp (P.TypeConstructor (P.Qualified Nothing name)) (map toTypeVar args)       className = prettyPrintType' classApp-  atIndent n $ "class " ++ impliesText ++ className ++ " where"-  mapM_ (renderDeclaration (n + 2) exps) ds-renderDeclaration n _ (P.TypeInstanceDeclaration name constraints className tys _) = do+  atIndent 4 $ "class " ++ impliesText ++ className ++ " where"+  mapM_ renderClassMember ds+  where+    renderClassMember (P.PositionedDeclaration _ _ d) = renderClassMember d+    renderClassMember (P.TypeDeclaration ident ty) = atIndent 6 $ show ident ++ " :: " ++ prettyPrintType' ty+    renderClassMember _ = error "Invalid argument to renderClassMember."+renderDeclaration _ (P.TypeInstanceDeclaration name constraints className tys _) = do   let constraintsText = case constraints of                           [] -> ""                           cs -> "(" ++ intercalate ", " (map (\(pn, tys') -> show pn ++ " " ++ unwords (map P.prettyPrintTypeAtom tys')) cs) ++ ") => "-  atIndent n $ "instance " ++ show name ++ " :: " ++ constraintsText ++ show className ++ " " ++ unwords (map P.prettyPrintTypeAtom tys)-renderDeclaration n exps (P.PositionedDeclaration _ com d) = do-  renderComments n com-  spacer-  renderDeclaration n exps d-renderDeclaration _ _ _ = return ()+  atIndent 4 $ "instance " ++ show name ++ " :: " ++ constraintsText ++ show className ++ " " ++ unwords (map P.prettyPrintTypeAtom tys)+renderDeclaration exps (P.PositionedDeclaration _ com d) = do+  renderComments com+  renderDeclaration exps d+renderDeclaration _ _ = return () -renderComments :: Int -> [P.Comment] -> Docs-renderComments n cs = mapM_ (atIndent n) ls+renderComments :: [P.Comment] -> Docs+renderComments cs = do+  let raw = concatMap toLines cs+  +  if all hasPipe raw+    then atIndent 0 . unlines . map stripPipes $ raw+    else atIndent 4 $ unlines raw+  +  unless (null raw) spacer   where-  ls = concatMap toLines cs    toLines (P.LineComment s) = [s]   toLines (P.BlockComment s) = lines s+  +  hasPipe s = case dropWhile (== ' ') s of { ('|':_) -> True; _ -> False }+  +  stripPipes = dropPipe . dropWhile (== ' ')++  dropPipe ('|':' ':s) = s+  dropPipe ('|':s) = s+  dropPipe s = s  toTypeVar :: (String, Maybe P.Kind) -> P.Type toTypeVar (s, Nothing) = P.TypeVar s

@@ -52,7 +52,7 @@   -- |   -- Binds a value to a name   ---  | Let (Expr -> Expr)+  | Let [Declaration]   -- |   -- Find the type of an expression   --

@@ -69,7 +69,7 @@   { psciImportedFilenames   :: [FilePath]   , psciImportedModuleNames :: [P.ModuleName]   , psciLoadedModules       :: [(Either P.RebuildPolicy FilePath, P.Module)]-  , psciLetBindings         :: [P.Expr -> P.Expr]+  , psciLetBindings         :: [P.Declaration]   }  -- State helpers@@ -95,8 +95,8 @@ -- | -- Updates the state to have more let bindings. ---updateLets :: (P.Expr -> P.Expr) -> PSCiState -> PSCiState-updateLets name st = st { psciLetBindings = name : psciLetBindings st }+updateLets :: [P.Declaration] -> PSCiState -> PSCiState+updateLets ds st = st { psciLetBindings = ds ++ psciLetBindings st }  -- File helpers -- |@@ -141,6 +141,16 @@     return (Right filename, content)   return $ P.parseModulesFromFiles (either (const "") id) $ (Left P.RebuildNever, P.prelude) : filesAndContent +-- |+-- Load all modules, updating the application state+--+loadAllImportedModules :: PSCI ()+loadAllImportedModules = do+  files <- PSCI . lift $ fmap psciImportedFilenames get+  modulesOrFirstError <- psciIO $ loadAllModules files+  case modulesOrFirstError of+    Left err -> psciIO $ print err+    Right modules -> PSCI . lift . modify $ \st -> st { psciLoadedModules = modules }   -- | -- Expands tilde in path.@@ -348,14 +358,14 @@     importDecl m = P.ImportDeclaration m P.Unqualified Nothing     traceModule = P.ModuleName [P.ProperName "Debug", P.ProperName "Trace"]     trace = P.Var (P.Qualified (Just traceModule) (P.Ident "print"))-    itValue = foldl (\x f -> f x) val lets     mainValue = P.App trace (P.Var (P.Qualified Nothing (P.Ident "it")))-    itDecl = P.ValueDeclaration (P.Ident "it") P.Value [] $ Right itValue+    itDecl = P.ValueDeclaration (P.Ident "it") P.Value [] $ Right val     mainDecl = P.ValueDeclaration (P.Ident "main") P.Value [] $ Right mainValue     decls = if exec then [itDecl, mainDecl] else [itDecl]   in-    P.Module moduleName ((importDecl `map` imports) ++ decls) Nothing+    P.Module moduleName ((importDecl `map` imports) ++ lets ++ decls) Nothing + -- | -- Makes a volatile module to hold a non-qualified type synonym for a fully-qualified data type declaration. --@@ -408,10 +418,10 @@ -- Takes a let declaration and updates the environment, then run a make. If the declaration fails, -- restore the pre-let environment. ---handleLet :: (P.Expr -> P.Expr) -> PSCI ()-handleLet l = do+handleLet :: [P.Declaration] -> PSCI ()+handleLet ds = do   st <- PSCI $ lift get-  let st' = updateLets l st+  let st' = updateLets ds st   let m = createTemporaryModule False st' (P.ObjectLiteral [])   e <- psciIO . runMake $ P.make modulesDir options (psciLoadedModules st' ++ [(Left P.RebuildAlways, m)]) []   case e of@@ -561,10 +571,12 @@     PSCI . outputStrLn $ "Couldn't locate: " ++ filePath handleCommand Reset = do   files <- psciImportedFilenames <$> PSCI (lift get)-  modulesOrFirstError <- psciIO $ loadAllModules files-  case modulesOrFirstError of-    Left err -> psciIO $ print err >> exitFailure-    Right modules -> PSCI . lift $ put (PSCiState files defaultImports modules [])+  PSCI . lift . modify $ \st -> st +    { psciImportedFilenames   = files+    , psciImportedModuleNames = defaultImports+    , psciLetBindings         = []+    }+  loadAllImportedModules handleCommand (TypeOf val) = handleTypeOf val handleCommand (KindOf typ) = handleKindOf typ handleCommand (Browse moduleName) = handleBrowse moduleName@@ -609,7 +621,7 @@             Left err -> outputStrLn err >> go             Right Nothing -> go             Right (Just Quit) -> outputStrLn quitMessage-            Right (Just c') -> runPSCI (handleCommand c') >> go+            Right (Just c') -> runPSCI (loadAllImportedModules >> handleCommand c') >> go  singleLineFlag :: Parser Bool singleLineFlag = switch $

@@ -76,7 +76,7 @@   -- we actually want the normal @let@.   --   psciLet :: P.TokenParser Command-  psciLet = Let <$> (P.Let <$> (P.reserved "let" *> P.indented *> manyDecls))+  psciLet = Let <$> (P.reserved "let" *> P.indented *> manyDecls)     where     manyDecls :: P.TokenParser [P.Declaration]     manyDecls = C.mark (many1 (C.same *> P.parseDeclaration))

@@ -1,5 +1,5 @@ name: purescript-version: 0.6.6+version: 0.6.7 cabal-version: >=1.8 build-type: Simple license: MIT

@@ -135,7 +135,47 @@               , "volatile"               , "while"               , "with"-              , "yield" ]+              , "yield" ] || properNameIsJsReserved name  moduleNameToJs :: ModuleName -> String-moduleNameToJs (ModuleName pns) = intercalate "_" (runProperName `map` pns)+moduleNameToJs (ModuleName pns) =+  let name = intercalate "_" (runProperName `map` pns)+  in if properNameIsJsReserved name then "$$" ++ name else name++-- |+-- Checks whether a proper name is reserved in Javascript.+--+properNameIsJsReserved :: String -> Bool+properNameIsJsReserved name =+  name `elem` [ "Infinity"+              , "NaN"+              , "Object"+              , "Function"+              , "Boolean"+              , "Error"+              , "EvalError"+              , "InternalError"+              , "RangeError"+              , "ReferenceError"+              , "SyntaxError"+              , "TypeError"+              , "URIError"+              , "Number"+              , "Math"+              , "Date"+              , "String"+              , "RegExp"+              , "Array"+              , "Int8Array"+              , "Uint8Array"+              , "Uint8ClampedArray"+              , "Int16Array"+              , "Uint16Array"+              , "Int32Array"+              , "Uint32Array"+              , "Float32Array"+              , "Float64Array"+              , "ArrayBuffer"+              , "DataView"+              , "JSON"+              , "Intl" ]

@@ -136,7 +136,12 @@   -- |   -- A local type variable   ---  | LocalTypeVariable deriving (Show, Eq, Data, Typeable)+  | LocalTypeVariable+  -- |+  -- A scoped type variable+  --+  | ScopedTypeVar+   deriving (Show, Eq, Data, Typeable)  -- | -- The type ('data' or 'newtype') of a data type declaration

@@ -422,6 +422,7 @@   go (Symbol s) = Just s   go Colon      = Just ":"   go LFatArrow  = Just "<="+  go At         = Just "@"   go _ = Nothing  symbol' :: String -> TokenParser ()

@@ -20,6 +20,7 @@ import Data.Function (on) import Data.List import Data.Maybe (maybeToList)+import Data.Foldable (foldMap) import qualified Data.Map as M  import Control.Applicative@@ -199,13 +200,35 @@ -- and return a substitution from type variables to types which makes the type heads unify. -- typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]-typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []-typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]+typeHeadsAreEqual _ _ (Skolem _ s1 _)      (Skolem _ s2 _)      | s1 == s2 = Just []+typeHeadsAreEqual _ _ t                    (TypeVar v)                     = Just [(v, t)]+-- In this case, we might want type information to flow back to the typechecker.+-- TODO: run this function in the UnifyT monad.+typeHeadsAreEqual _ _ (TUnknown _)         _                    = Just [] typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []-typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2 <*> typeHeadsAreEqual m e t1 t2+typeHeadsAreEqual m e (TypeApp h1 t1)      (TypeApp h2 t2)                 = (++) <$> typeHeadsAreEqual m e h1 h2 +                                                                                  <*> typeHeadsAreEqual m e t1 t2 typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of   Left  _  -> Nothing   Right t1 -> typeHeadsAreEqual m e t1 t2+typeHeadsAreEqual _ _ REmpty REmpty = Just []+typeHeadsAreEqual m e r1@(RCons _ _ _) r2@(RCons _ _ _) =+  let (s1, r1') = rowToList r1+      (s2, r2') = rowToList r2+      +      int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]+      sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]+      sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]+  in (++) <$> foldMap (\(t1, t2) -> typeHeadsAreEqual m e t1 t2) int +          <*> go sd1 r1' sd2 r2'+  where+  go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Maybe [(String, Type)]+  go [] REmpty          [] REmpty          = Just [] +  go [] (TUnknown _)    _  _               = Just [] +  go [] (TypeVar v1)    [] (TypeVar v2)    | v1 == v2 = Just []+  go [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = Just []+  go sd r               [] (TypeVar v)     = Just [(v, rowFromList (sd, r))]+  go _  _               _  _               = Nothing typeHeadsAreEqual _ _ _ _ = Nothing  -- |

@@ -14,19 +14,22 @@ -----------------------------------------------------------------------------  {-# OPTIONS_GHC -fno-warn-orphans #-}-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TupleSections #-}  module Language.PureScript.TypeChecker.Kinds (     kindOf,+    kindOfWithScopedVars,     kindsOf,     kindsOfAll ) where  import Data.Maybe (fromMaybe) import Data.Monoid ((<>))+ import qualified Data.HashMap.Strict as H import qualified Data.Map as M +import Control.Arrow (second) import Control.Applicative import Control.Monad.Error import Control.Monad.State@@ -69,11 +72,19 @@ -- Infer the kind of a single type -- kindOf :: ModuleName -> Type -> Check Kind-kindOf _ ty =+kindOf _ ty = fst <$> kindOfWithScopedVars ty+    +-- |+-- Infer the kind of a single type, returning the kinds of any scoped type variables+--+kindOfWithScopedVars :: Type -> Check (Kind, [(String, Kind)])   +kindOfWithScopedVars ty =    rethrow (mkErrorStack "Error checking kind" (Just (TypeError ty)) <>) $-    fmap (starIfUnknown . tidyUp) . liftUnify $ infer ty+    fmap tidyUp . liftUnify $ infer ty   where-  tidyUp (k, sub) = sub $? k+  tidyUp ((k, args), sub) = ( starIfUnknown (sub $? k)+                            , map (second (starIfUnknown . (sub $?))) args+                            )  -- | -- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors@@ -125,7 +136,7 @@ -- solveTypes :: Bool -> [Type] -> [Kind] -> Kind -> UnifyT Kind Check Kind solveTypes isData ts kargs tyCon = do-  ks <- mapM infer ts+  ks <- mapM (fmap fst . infer) ts   when isData $ do     tyCon =?= foldr FunKind Star kargs     forM_ ks $ \k -> k =?= Star@@ -145,48 +156,64 @@ -- | -- Infer a kind for a type ---infer :: Type -> UnifyT Kind Check Kind+infer :: Type -> UnifyT Kind Check (Kind, [(String, Kind)]) infer ty = rethrow (mkErrorStack "Error inferring type of value" (Just (TypeError ty)) <>) $ infer' ty -infer' :: Type -> UnifyT Kind Check Kind-infer' TypeWildcard = fresh-infer' (TypeVar v) = do-  Just moduleName <- checkCurrentModule <$> get-  UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))-infer' c@(TypeConstructor v) = do-  env <- liftCheck getEnv-  case M.lookup v (types env) of-    Nothing -> UnifyT . lift . throwError $ mkErrorStack "Unknown type constructor" (Just (TypeError c))-    Just (kind, _) -> return kind-infer' (TypeApp t1 t2) = do-  k0 <- fresh-  k1 <- infer t1-  k2 <- infer t2-  k1 =?= FunKind k2 k0-  return k0+infer' :: Type -> UnifyT Kind Check (Kind, [(String, Kind)]) infer' (ForAll ident ty _) = do   k1 <- fresh   Just moduleName <- checkCurrentModule <$> get-  k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty+  (k2, args) <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty   k2 =?= Star-  return Star-infer' REmpty = do-  k <- fresh-  return $ Row k-infer' (RCons _ ty row) = do-  k1 <- infer ty-  k2 <- infer row-  k2 =?= Row k1-  return $ Row k1-infer' (ConstrainedType deps ty) = do-  forM_ deps $ \(className, tys) -> do-    _ <- infer $ foldl TypeApp (TypeConstructor className) tys-    return ()-  k <- infer ty-  k =?= Star-  return Star+  return (Star, (ident, k1) : args) infer' (KindedType ty k) = do-  k' <- infer ty+  (k', args) <- infer ty   k =?= k'-  return k'-infer' _ = error "Invalid argument to infer"+  return (k', args)+infer' other = (, []) <$> go other+  where+  go :: Type -> UnifyT Kind Check Kind+  go (ForAll ident ty _) = do+    k1 <- fresh+    Just moduleName <- checkCurrentModule <$> get+    k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ go ty+    k2 =?= Star+    return Star+  go (KindedType ty k) = do+    k' <- go ty+    k =?= k'+    return k'+  go TypeWildcard = fresh+  go (TypeVar v) = do+    Just moduleName <- checkCurrentModule <$> get+    UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))+  go (Skolem v _ _) = do+    Just moduleName <- checkCurrentModule <$> get+    UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))+  go c@(TypeConstructor v) = do+    env <- liftCheck getEnv+    case M.lookup v (types env) of+      Nothing -> UnifyT . lift . throwError $ mkErrorStack "Unknown type constructor" (Just (TypeError c))+      Just (kind, _) -> return kind+  go (TypeApp t1 t2) = do+    k0 <- fresh+    k1 <- go t1+    k2 <- go t2+    k1 =?= FunKind k2 k0+    return k0+  go REmpty = do+    k <- fresh+    return $ Row k+  go (RCons _ ty row) = do+    k1 <- go ty+    k2 <- go row+    k2 =?= Row k1+    return $ Row k1+  go (ConstrainedType deps ty) = do+    forM_ deps $ \(className, tys) -> do+      _ <- go $ foldl TypeApp (TypeConstructor className) tys+      return ()+    k <- go ty+    k =?= Star+    return Star+  go _ = error "Invalid argument to infer"

@@ -57,6 +57,12 @@   return a  -- |+-- Temporarily bind a collection of names to types+--+withScopedTypeVars :: (Functor m, MonadState CheckState m) => ModuleName -> [(String, Kind)] -> m a -> m a+withScopedTypeVars mn ks = bindTypes (M.fromList (map (\(name, k) -> (Qualified (Just mn) (ProperName name), (k, ScopedTypeVar))) ks))++-- | -- Temporarily make a collection of type class dictionaries available -- withTypeClassDictionaries :: (MonadState CheckState m) => [TypeClassDictionaryInScope] -> m a -> m a

@@ -71,6 +71,7 @@ skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id go id in f   where   go (SuperClassDictionary c ts) = SuperClassDictionary c (map (skolemize ident sko scope) ts)+  go (TypedValue check val ty) = TypedValue check val (skolemize ident sko scope ty)   go other = other  -- |

@@ -129,16 +129,16 @@   return (untyped, typed, dict, untypedDict)  checkTypedBindingGroupElement :: ModuleName -> (Ident, (Expr, Type, Bool)) -> TypeData ->  UnifyT Type Check (Ident, (Expr, Type))-checkTypedBindingGroupElement moduleName (ident, (val', ty, checkType)) dict = do+checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do   -- Replace type wildcards   ty' <- replaceTypeWildcards ty   -- Kind check-  kind <- liftCheck $ kindOf moduleName ty-  guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star+  (kind, args) <- liftCheck $ kindOfWithScopedVars ty+  checkTypeKind kind   -- Check the type with the new names in scope   ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'   val'' <- if checkType-           then bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''+           then withScopedTypeVars mn args $ bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''            else return (TypedValue False val' ty'')   return (ident, (val'', ty'')) @@ -183,10 +183,8 @@ -- | -- Check the kind of a type, failing if it is not of kind *. ---checkTypeKind :: ModuleName -> Type -> UnifyT t Check ()-checkTypeKind moduleName ty = do-  kind <- liftCheck $ kindOf moduleName ty-  guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star+checkTypeKind :: Kind -> UnifyT t Check ()+checkTypeKind kind = guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star  -- | -- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns@@ -293,9 +291,10 @@   return $ TypeClassDictionary False (className, tys) dicts infer' (TypedValue checkType val ty) = do   Just moduleName <- checkCurrentModule <$> get-  checkTypeKind moduleName ty+  (kind, args) <- liftCheck $ kindOfWithScopedVars ty+  checkTypeKind kind   ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty-  val' <- if checkType then check val ty' else return val+  val' <- if checkType then withScopedTypeVars moduleName args (check val ty') else return val   return $ TypedValue True val' ty' infer' (PositionedValue pos _ val) = rethrowWithPosition pos $ infer' val infer' _ = error "Invalid argument to infer"@@ -304,10 +303,11 @@ inferLetBinding seen [] ret j = (,) seen <$> makeBindingGroupVisible (j ret) inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do   Just moduleName <- checkCurrentModule <$> get-  checkTypeKind moduleName ty+  (kind, args) <- liftCheck $ kindOfWithScopedVars ty+  checkTypeKind kind   let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)   ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty-  TypedValue _ val' ty'' <- if checkType then bindNames dict (check val ty') else return tv+  TypedValue _ val' ty'' <- if checkType then withScopedTypeVars moduleName args (bindNames dict (check val ty')) else return tv   bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right (TypedValue checkType val' ty''))]) rest ret j inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret j = do   valTy <- fresh@@ -507,14 +507,15 @@   return $ TypeClassDictionary False (className, tys) dicts check' (TypedValue checkType val ty1) ty2 = do   Just moduleName <- checkCurrentModule <$> get-  checkTypeKind moduleName ty1+  (kind, args) <- liftCheck $ kindOfWithScopedVars ty1+  checkTypeKind kind   ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1   ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2   val' <- subsumes (Just val) ty1' ty2'   case val' of     Nothing -> throwError . strMsg $ "Unable to check type subsumption"     Just val'' -> do-      val''' <- if checkType then check val'' ty2' else return val''+      val''' <- if checkType then withScopedTypeVars moduleName args (check val'' ty2') else return val''       return $ TypedValue checkType (TypedValue True val''' ty1') ty2' check' (Case vals binders) ret = do   vals' <- mapM infer vals@@ -562,7 +563,7 @@   ty' <- introduceSkolemScope <=< expandAllTypeSynonyms <=< replaceTypeWildcards $ ty   check val ty' check' val kt@(KindedType ty kind) = do-  guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star+  checkTypeKind kind   val' <- check' val ty   return $ TypedValue True val' kt check' (PositionedValue pos _ val) ty =

@@ -153,6 +153,23 @@     Left  _  -> False     Right t1 -> unifiesWith e t1 t2 unifiesWith e t1 t2@(SaturatedTypeSynonym _ _) = unifiesWith e t2 t1+unifiesWith _ REmpty REmpty = True+unifiesWith e r1@(RCons _ _ _) r2@(RCons _ _ _) =+  let (s1, r1') = rowToList r1+      (s2, r2') = rowToList r2+      +      int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]+      sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]+      sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]+  in all (\(t1, t2) -> unifiesWith e t1 t2) int && go sd1 r1' sd2 r2'+  where+  go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Bool+  go [] REmpty          [] REmpty          = True +  go [] (TypeVar v1)    [] (TypeVar v2)    = v1 == v2+  go [] (Skolem _ s1 _) [] (Skolem _ s2 _) = s1 == s2+  go _  (TUnknown _)    _  _               = True+  go _  _               _  (TUnknown _)    = True+  go _  _               _  _               = False unifiesWith _ _ _ = False  -- |