packages feed

purescript 0.3.5 → 0.3.6

raw patch · 10 files changed

+161/−307 lines, 10 filesdep +monad-unifydep ~cmdtheline

Dependencies added: monad-unify

Dependency ranges changed: cmdtheline

Files

purescript.cabal view
@@ -1,5 +1,5 @@ name: purescript-version: 0.3.5+version: 0.3.6 cabal-version: >=1.8 build-type: Simple license: MIT@@ -17,7 +17,7 @@ library     build-depends: base >=4 && <5, cmdtheline -any, containers -any,                    directory -any, filepath -any, mtl -any, parsec -any, syb -any,-                   transformers -any, utf8-string -any, pattern-arrows -any+                   transformers -any, utf8-string -any, pattern-arrows -any, monad-unify -any     exposed-modules: Data.Generics.Extras                      Language.PureScript                      Language.PureScript.Options@@ -25,7 +25,6 @@                      Language.PureScript.Kinds                      Language.PureScript.Names                      Language.PureScript.Types-                     Language.PureScript.Unknown                      Language.PureScript.Values                      Language.PureScript.Scope                      Language.PureScript.Sugar
src/Language/PureScript.hs view
@@ -30,6 +30,7 @@  import Data.List (intercalate) import Control.Monad (when, forM)+import Control.Monad.State.Lazy import Control.Applicative ((<$>)) import qualified Data.Map as M @@ -54,7 +55,9 @@ compile opts ms = do   sorted <- sortModules ms   desugared <- desugar sorted-  (elaborated, env) <- runCheck $ forM desugared $ \(Module moduleName decls) -> Module moduleName <$> typeCheckAll (ModuleName moduleName) decls+  (elaborated, env) <- runCheck $ forM desugared $ \(Module moduleName decls) -> do+    modify (\s -> s { checkCurrentModule = Just (ModuleName moduleName) })+    Module moduleName <$> typeCheckAll (ModuleName moduleName) decls   regrouped <- createBindingGroupsModule . collapseBindingGroupsModule $ elaborated   let js = concatMap (flip (moduleToJs opts) env) $ regrouped   let exts = intercalate "\n" . map (flip moduleToPs env) $ regrouped
src/Language/PureScript/Kinds.hs view
@@ -17,8 +17,9 @@ module Language.PureScript.Kinds where  import Data.Data-import Language.PureScript.Unknown +import Control.Monad.Unify (TypedUnknown(..))+ -- | -- The data type of kinds --@@ -26,7 +27,7 @@   -- |   -- Unification variable of type Kind   ---  = KUnknown (Unknown Kind)+  = KUnknown (TypedUnknown Kind)   -- |   -- The kind of types   --
src/Language/PureScript/Pretty/Kinds.hs view
@@ -21,17 +21,17 @@  import Control.Arrow (ArrowPlus(..)) import Control.PatternArrows+import Control.Monad.Unify  import Language.PureScript.Kinds import Language.PureScript.Pretty.Common-import Language.PureScript.Unknown  typeLiterals :: Pattern () Kind String typeLiterals = mkPattern match   where   match Star = Just "*"   match Bang = Just "!"-  match (KUnknown (Unknown u)) = Just $ 'u' : show u+  match (KUnknown (TypedUnknown (Unknown u))) = Just $ 'u' : show u   match _ = Nothing  matchRow :: Pattern () Kind ((), Kind)
src/Language/PureScript/Pretty/Types.hs view
@@ -23,10 +23,10 @@  import Control.Arrow ((<+>)) import Control.PatternArrows+import Control.Monad.Unify  import Language.PureScript.Types import Language.PureScript.Pretty.Common-import Language.PureScript.Unknown  typeLiterals :: Pattern () Type String typeLiterals = mkPattern match@@ -38,7 +38,7 @@   match (Object row) = Just $ "{ " ++ prettyPrintType row ++ " }"   match (TypeVar var) = Just var   match (TypeConstructor ctor) = Just $ show ctor-  match (TUnknown (Unknown u)) = Just $ 'u' : show u+  match (TUnknown (TypedUnknown (Unknown u))) = Just $ 'u' : show u   match (Skolem s) = Just $ 's' : show s   match (ConstrainedType deps ty) = Just $ "(" ++ intercalate "," (map (\(pn, ty') -> show pn ++ " (" ++ prettyPrintType ty' ++ ")") deps) ++ ") => " ++ prettyPrintType ty   match (SaturatedTypeSynonym name args) = Just $ show name ++ "<" ++ intercalate "," (map prettyPrintType args) ++ ">"@@ -57,7 +57,7 @@   nameAndTypeToPs name ty = name ++ " :: " ++ prettyPrintType ty   tailToPs :: Type -> String   tailToPs REmpty = ""-  tailToPs (TUnknown (Unknown u)) = " | u" ++ show u+  tailToPs (TUnknown (TypedUnknown (Unknown u))) = " | u" ++ show u   tailToPs (TypeVar var) = " | " ++ var   tailToPs (Skolem s) = " | s" ++ show s   tailToPs _ = error "Invalid row tail"
src/Language/PureScript/TypeChecker/Kinds.hs view
@@ -15,6 +15,7 @@  {-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE MultiParamTypeClasses #-}  module Language.PureScript.TypeChecker.Kinds (     kindOf,@@ -27,48 +28,42 @@ import Language.PureScript.Names import Language.PureScript.TypeChecker.Monad import Language.PureScript.Pretty-import Language.PureScript.Unknown  import Control.Monad.State import Control.Monad.Error import Control.Monad.Reader+import Control.Monad.Unify  import Control.Applicative  import qualified Data.Map as M -instance Unifiable Kind where+instance Unifiable Check Kind where   unknown = KUnknown   isUnknown (KUnknown u) = Just u   isUnknown _ = Nothing-  KUnknown u1 ~~ KUnknown u2 | u1 == u2 = return ()-  KUnknown u ~~ k = replace u k-  k ~~ KUnknown u = replace u k-  Star ~~ Star = return ()-  Bang ~~ Bang = return ()-  Row k1 ~~ Row k2 = k1 ~~ k2-  FunKind k1 k2 ~~ FunKind k3 k4 = do-    k1 ~~ k3-    k2 ~~ k4-  k1 ~~ k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."-  apply s (KUnknown u) = runSubstitution s u-  apply s (FunKind k1 k2) = FunKind (apply s k1) (apply s k2)-  apply _ k = k-  unknowns (KUnknown (Unknown u)) = [u]-  unknowns (FunKind k1 k2) = unknowns k1 ++ unknowns k2-  unknowns _ = []+  KUnknown u1 ?= KUnknown u2 | u1 == u2 = return ()+  KUnknown u ?= k = replace u k+  k ?= KUnknown u = replace u k+  Star ?= Star = return ()+  Bang ?= Bang = return ()+  Row k1 ?= Row k2 = k1 ?= k2+  FunKind k1 k2 ?= FunKind k3 k4 = do+    k1 ?= k3+    k2 ?= k4+  k1 ?= k2 = UnifyT . lift . throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."  -- | -- Infer the kind of a single type -- kindOf :: ModuleName -> Type -> Check Kind-kindOf moduleName ty = fmap (\(k, s) -> apply s k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer ty+kindOf moduleName ty = liftUnify $ starIfUnknown <$> infer ty  -- | -- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors -- kindsOf :: ModuleName -> ProperName -> [String] -> [Type] -> Check Kind-kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, s) -> apply s k)) . runSubst (SubstContext moduleName) $ do+kindsOf moduleName name args ts = fmap starIfUnknown . liftUnify $ do   tyCon <- fresh   kargs <- replicateM (length args) fresh   let dict = (name, tyCon) : zip (map ProperName args) kargs@@ -79,7 +74,7 @@ -- Simultaneously infer the kinds of several mutually recursive type constructors -- kindsOfAll :: ModuleName -> [(ProperName, [String], Type)] -> [(ProperName, [String], [Type])] -> Check ([Kind], [Kind])-kindsOfAll moduleName syns tys = fmap tidyUp . runSubst (SubstContext moduleName) $ do+kindsOfAll moduleName syns tys = fmap tidyUp . liftUnify $ do   synVars <- replicateM (length syns) fresh   let dict = zipWith (\(name, _, _) var -> (name, var)) syns synVars   bindLocalTypeVariables moduleName dict $ do@@ -98,16 +93,16 @@           solveTypes [ty] kargs synVar) synVars syns       return (syn_ks, data_ks)   where-  tidyUp ((ks1, ks2), s) = (map starIfUnknown $ apply s ks1, map starIfUnknown $ apply s ks2)+  tidyUp (ks1, ks2) = (map starIfUnknown ks1, map starIfUnknown ks2)  -- | -- Solve the set of kind constraints associated with the data constructors for a type constructor ---solveTypes :: [Type] -> [Kind] -> Kind -> Subst Kind+solveTypes :: [Type] -> [Kind] -> Kind -> UnifyT Check Kind solveTypes ts kargs tyCon = do   ks <- mapM infer ts-  tyCon ~~ foldr FunKind Star kargs-  forM_ ks $ \k -> k ~~ Star+  tyCon ?= foldr FunKind Star kargs+  forM_ ks $ \k -> k ?= Star   return tyCon  -- |@@ -121,39 +116,39 @@ -- | -- Infer a kind for a type ---infer :: Type -> Subst Kind+infer :: Type -> UnifyT Check Kind infer Number = return Star infer String = return Star infer Boolean = return Star infer Array = return $ FunKind Star Star infer (Object row) = do   k <- infer row-  k ~~ Row Star+  k ?= Row Star   return Star infer (Function args ret) = do   ks <- mapM infer args   k <- infer ret-  k ~~ Star-  forM_ ks (~~ Star)+  k ?= Star+  forM_ ks (?= Star)   return Star infer (TypeVar v) = do-  moduleName <- substCurrentModule <$> ask-  lookupTypeVariable moduleName (Qualified Nothing (ProperName v))+  Just moduleName <- checkCurrentModule <$> get+  UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v)) infer (TypeConstructor v) = do   env <- liftCheck getEnv-  moduleName <- substCurrentModule `fmap` ask+  Just moduleName <- checkCurrentModule <$> get   case M.lookup (qualify moduleName v) (types env) of-    Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"+    Nothing -> UnifyT . lift . throwError $ "Unknown type constructor '" ++ show v ++ "'"     Just (kind, _) -> return kind infer (TypeApp t1 t2) = do   k0 <- fresh   k1 <- infer t1   k2 <- infer t2-  k1 ~~ FunKind k2 k0+  k1 ?= FunKind k2 k0   return k0 infer (ForAll ident ty) = do   k <- fresh-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   bindLocalTypeVariables moduleName [(ProperName ident, k)] $ infer ty infer REmpty = do   k <- fresh@@ -161,11 +156,11 @@ infer (RCons _ ty row) = do   k1 <- infer ty   k2 <- infer row-  k2 ~~ Row k1+  k2 ?= Row k1   return $ Row k1 infer (ConstrainedType deps ty) = do   mapM_ (infer . snd) deps   k <- infer ty-  k ~~ Star+  k ?= Star   return Star infer _ = error "Invalid argument to infer"
src/Language/PureScript/TypeChecker/Monad.hs view
@@ -22,7 +22,6 @@ import Language.PureScript.Kinds import Language.PureScript.Values import Language.PureScript.Names-import Language.PureScript.Unknown import Language.PureScript.Declarations  import Data.Data@@ -34,6 +33,7 @@ import Control.Monad.State import Control.Monad.Error import Control.Monad.Reader+import Control.Monad.Unify import Control.Arrow ((***))  import qualified Data.Map as M@@ -227,6 +227,10 @@   -- The next type class dictionary name   --   , checkNextDictName :: Int+  -- |+  -- The current module+  --+  , checkCurrentModule :: Maybe ModuleName   }  -- |@@ -258,7 +262,7 @@ -- runCheck :: Check a -> Either String (a, Environment) runCheck c = do-  (a, s) <- flip runStateT (CheckState emptyEnvironment 0 0) $ unCheck c+  (a, s) <- flip runStateT (CheckState emptyEnvironment 0 0 Nothing) $ unCheck c   return (a, checkEnv s)  -- |@@ -284,129 +288,23 @@   return n  -- |--- A substitution maintains a mapping from unification variables to their values, ensuring that--- the type of a unification variable matches the type of its value.----newtype Substitution = Substitution { runSubstitution :: forall t. (Unifiable t) => Unknown t -> t }--instance Monoid Substitution where-  mempty = Substitution unknown-  s1 `mappend` s2 = Substitution $ \u -> apply s1 (apply s2 (unknown u))---- |--- State for the substitution monad, which contains the current substitution----data SubstState = SubstState { substSubst :: Substitution }---- |--- Configuration for the substitution monad, constaining the current module----newtype SubstContext = SubstContext { substCurrentModule :: ModuleName } deriving (Show)---- |--- The substitution monad, which provides the means to unify values to generate a substitution, in addition to--- the actions supported by the type checking monad @Check@.----newtype Subst a = Subst { unSubst :: ReaderT SubstContext (StateT SubstState Check) a }-  deriving (Functor, Monad, Applicative, MonadPlus, MonadReader SubstContext)--instance MonadState CheckState Subst where-  get = Subst . lift . lift $ get-  put = Subst . lift . lift . put--deriving instance MonadError String Subst---- | -- Lift a computation in the @Check@ monad into the substitution monad. ---liftCheck :: Check a -> Subst a-liftCheck = Subst . lift . lift---- |--- Get the current substitution monad state----getSubstState :: Subst SubstState-getSubstState = Subst . lift $ get+liftCheck :: Check a -> UnifyT Check a+liftCheck = UnifyT . lift . lift  -- | -- Run a computation in the substitution monad, generating a return value and the final substitution. ---runSubst :: SubstContext -> Subst a -> Check (a, Substitution)-runSubst context subst = do-  (a, s) <- flip runStateT (SubstState mempty) . flip runReaderT context . unSubst $ subst-  return (a, substSubst s)---- |--- Generate a substitution from a substitution function for a single type----substituteWith :: (Typeable t) => (Unknown t -> t) -> Substitution-substituteWith f = Substitution $ \u -> fromMaybe (unknown u) $ do-  u1 <- cast u-  cast (f u1)---- |--- Substitute a single unification variable----substituteOne :: (Unifiable t) => Unknown t -> t -> Substitution-substituteOne u t = substituteWith $ \u1 ->-  case u1 of-    u2 | u2 == u -> t-       | otherwise -> unknown u2---- |--- Replace a unification variable with the specified value in the current substitution----replace :: (Unifiable t) => Unknown t -> t -> Subst ()-replace u t' = do-  sub <- substSubst <$> Subst get-  let t = apply sub t'-  occursCheck u t-  let current = apply sub $ unknown u-  case isUnknown current of-    Just u1 | u1 == u -> return ()-    _ -> current ~~ t-  Subst . modify $ \s -> s { substSubst = substituteOne u t <> substSubst s }---- |--- Identifies types which support unification----class (Typeable t, Data t, Show t) => Unifiable t where-  unknown :: Unknown t -> t-  (~~) :: t -> t -> Subst ()-  isUnknown :: t -> Maybe (Unknown t)-  apply :: Substitution -> t -> t-  unknowns :: t -> [Int]--instance (Unifiable a) => Unifiable [a] where-  unknown _ = error "not supported"-  (~~) = zipWithM_ (~~)-  isUnknown _ = error "not supported"-  apply s = map (apply s)-  unknowns = concatMap unknowns---- |--- Perform the occurs check, to make sure a unification variable does not occur inside a value----occursCheck :: (Unifiable t) => Unknown s -> t -> Subst ()-occursCheck (Unknown u) t =-  case isUnknown t of-    Nothing -> guardWith "Occurs check fails" (u `notElem` unknowns t)-    _ -> return ()---- |--- Generate a fresh untyped unification variable----fresh' :: Subst Int-fresh' = do-  n <- checkNextVar <$> get-  modify $ \s -> s { checkNextVar = succ (checkNextVar s) }-  return n---- |--- Generate a fresh unification variable at a specific type----fresh :: (Unifiable t) => Subst t-fresh = unknown . Unknown <$> fresh'+liftUnify :: (Data a) => UnifyT Check a -> Check a+liftUnify unify = do+  st <- get+  e <- runUnify (defaultUnifyState { unifyNextVar = checkNextVar st }) unify+  case e of+    Left err -> throwError err+    Right (a, ust) -> do+      modify $ \st -> st { checkNextVar = unifyNextVar ust }+      return $ runSubstitution (unifyCurrentSubstitution ust) a  -- | -- Replace any unqualified names in a type wit their qualified versionss
src/Language/PureScript/TypeChecker/Types.hs view
@@ -14,7 +14,9 @@ -----------------------------------------------------------------------------  {-# OPTIONS_GHC -fno-warn-orphans #-}-{-# LANGUAGE DeriveDataTypeable, FlexibleContexts #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}  module Language.PureScript.TypeChecker.Types (     typesOf@@ -53,11 +55,11 @@ import Language.PureScript.TypeChecker.Kinds import Language.PureScript.TypeChecker.Synonyms import Language.PureScript.Pretty-import Language.PureScript.Unknown  import Control.Monad.State import Control.Monad.Error import Control.Monad.Reader+import Control.Monad.Unify  import Control.Applicative import Control.Arrow (Arrow(..))@@ -65,32 +67,16 @@ import qualified Data.Map as M import Data.Function (on) -instance Unifiable Type where+instance Unifiable Check Type where   unknown = TUnknown   isUnknown (TUnknown u) = Just u   isUnknown _ = Nothing-  (~~) = unifyTypes-  apply s (TUnknown u) = runSubstitution s u-  apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys-  apply s (ForAll idents ty) = ForAll idents $ apply s ty-  apply s (Object r) = Object (apply s r)-  apply s (Function args ret) = Function (map (apply s) args) (apply s ret)-  apply s (TypeApp t1 t2) = TypeApp (apply s t1) (apply s t2)-  apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)-  apply _ t = t-  unknowns (TUnknown (Unknown u)) = [u]-  unknowns (SaturatedTypeSynonym _ tys) = concatMap unknowns tys-  unknowns (ForAll _ ty) = unknowns ty-  unknowns (Object r) = unknowns r-  unknowns (Function args ret) = concatMap unknowns args ++ unknowns ret-  unknowns (TypeApp t1 t2) = unknowns t1 ++ unknowns t2-  unknowns (RCons _ ty r) = unknowns ty ++ unknowns r-  unknowns _ = []+  (?=) = unifyTypes  -- | -- Unify two types, updating the current substitution ---unifyTypes :: Type -> Type -> Subst ()+unifyTypes :: Type -> Type -> UnifyT Check () unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 ++ " with type " ++ prettyPrintType t2 ++ ":\n" ++ e) $ do   unifyTypes' t1 t2   where@@ -113,7 +99,7 @@   unifyTypes' String String = return ()   unifyTypes' Boolean Boolean = return ()   unifyTypes' Array Array = return ()-  unifyTypes' (Object row1) (Object row2) = row1 ~~ row2+  unifyTypes' (Object row1) (Object row2) = row1 ?= row2   unifyTypes' (Function args1 ret1) (Function args2 ret2) = do     guardWith "Function applied to incorrect number of args" $ length args1 == length args2     zipWithM_ unifyTypes args1 args2@@ -121,7 +107,7 @@   unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()   unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do     env <- getEnv-    moduleName <- substCurrentModule `fmap` ask+    Just moduleName <- checkCurrentModule <$> get     guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (typeConstructorsAreEqual env moduleName c1 c2)   unifyTypes' (TypeApp t3 t4) (TypeApp t5 t6) = do     t3 `unifyTypes` t5@@ -140,7 +126,7 @@ -- trailing row unification variable, if appropriate, otherwise leftover labels result in a unification -- error. ---unifyRows :: Type -> Type -> Subst ()+unifyRows :: Type -> Type -> UnifyT Check () unifyRows r1 r2 =   let     (s1, r1') = rowToList r1@@ -149,17 +135,17 @@     sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]     sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]   in do-    forM_ int (uncurry (~~))+    forM_ int (uncurry (?=))     unifyRows' sd1 r1' sd2 r2'   where-  unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Subst ()+  unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> UnifyT Check ()   unifyRows' [] (TUnknown u) sd r = replace u (rowFromList (sd, r))   unifyRows' sd r [] (TUnknown u) = replace u (rowFromList (sd, r))   unifyRows' ((name, ty):row) r others u@(TUnknown un) = do     occursCheck un ty     forM_ row $ \(_, t) -> occursCheck un t     u' <- fresh-    u ~~ RCons name ty u'+    u ?= RCons name ty u'     unifyRows' row r others u'   unifyRows' [] REmpty [] REmpty = return ()   unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()@@ -178,8 +164,7 @@ -- typesOf :: ModuleName -> [(Ident, Value)] -> Check [(Ident, (Value, Type))] typesOf moduleName vals = do-  tys <- fmap (\(tys, s) -> map (\(ident, (val, ty)) -> (ident, (overTypes (apply s) val, apply s ty))) tys)-         . runSubst (SubstContext moduleName) $ do+  tys <- liftUnify $ do     let es = map isTyped vals         typed = filter (isJust . snd . snd) es         untyped = filter (isNothing . snd . snd) es@@ -197,11 +182,11 @@           return (ident, (val', ty'))         (ident, (val, Nothing)) -> do           TypedValue _ val' ty <- bindNames dict $ infer val-          ty ~~ fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)+          ty ?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)           return (ident, (val', ty))       when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do         [eff, a] <- replicateM 2 fresh-        ty ~~ TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a+        ty ?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a       escapeCheck val ty       return triple   forM_ tys $ skolemEscapeCheck . snd . snd@@ -279,14 +264,14 @@ -- | -- Ensure unsolved unification variables do not escape ---escapeCheck :: Value -> Type -> Subst ()+escapeCheck :: Value -> Type -> UnifyT Check () escapeCheck value ty = do-  subst <- substSubst <$> getSubstState-  let visibleUnknowns = nub $ unknowns $ apply subst ty+  subst <- unifyCurrentSubstitution <$> UnifyT get+  let visibleUnknowns = nub $ unknowns $ runSubstitution subst ty   let allUnknowns = findAllTypes value   forM_ allUnknowns $ \t -> do-    let unsolvedUnknowns = nub . unknowns $ apply subst t-    guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns+    let unsolvedUnknowns = nub . unknowns $ runSubstitution subst t+    guardWith ("Escape check fails" ++ show ( runSubstitution subst ty, runSubstitution subst t)) $ null $ unsolvedUnknowns \\ visibleUnknowns  -- | -- Find all type annotations occuring inside a value@@ -304,7 +289,7 @@ skolemEscapeCheck ty =   case something (mkQ Nothing findSkolems) ty of     Nothing -> return ()-    Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature." ++ show ty+    Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature."   where     findSkolems (Skolem _) = return ()     findSkolems _ = mzero@@ -330,9 +315,9 @@       toName = (:) 't' . show       ty' = everywhere (mkT typeToVar) $ ty       typeToVar :: Type -> Type-      typeToVar (TUnknown (Unknown u)) = TypeVar (toName u)+      typeToVar (TUnknown (TypedUnknown (Unknown u))) = TypeVar (toName u)       typeToVar t = t-  in mkForAll (sort . map toName $ unks) ty'+  in mkForAll (sort . map (toName . runUnknown) $ unks) ty'  -- | -- Replace named type variables with types@@ -343,14 +328,14 @@ -- | -- Replace named type variables with new unification variables ---replaceAllVarsWithUnknowns :: Type -> Subst Type+replaceAllVarsWithUnknowns :: Type -> UnifyT Check Type replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns replaceAllVarsWithUnknowns ty = return ty  -- | -- Replace a single type variable with a new unification variable ---replaceVarWithUnknown :: String -> Type -> Subst Type+replaceVarWithUnknown :: String -> Type -> UnifyT Check Type replaceVarWithUnknown ident ty = do   tu <- fresh   return $ replaceTypeVars ident tu $ ty@@ -359,10 +344,10 @@ -- Replace fully applied type synonyms with the @SaturatedTypeSynonym@ data constructor, which helps generate -- better error messages during unification. ---replaceAllTypeSynonyms :: (Functor m, MonadState CheckState m, MonadReader SubstContext m, MonadError String m) => (D.Data d) => d -> m d+replaceAllTypeSynonyms :: (Functor m, MonadState CheckState m, MonadError String m) => (D.Data d) => d -> m d replaceAllTypeSynonyms d = do   env <- getEnv-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   let syns = map (\((path, name), (args, _)) -> ((path, name), length args)) . M.toList $ typeSynonyms env   either throwError return $ saturateAllTypeSynonyms env moduleName syns d @@ -378,10 +363,10 @@ -- | -- Replace a type synonym and its arguments with the aliased type ---expandTypeSynonym :: Qualified ProperName -> [Type] -> Subst Type+expandTypeSynonym :: Qualified ProperName -> [Type] -> UnifyT Check Type expandTypeSynonym name args = do   env <- getEnv-  moduleName <- substCurrentModule `fmap` ask+  Just moduleName <- checkCurrentModule <$> get   case M.lookup (canonicalizeType moduleName env name) (typeSynonyms env) of     Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body     Nothing -> error "Type synonym was not defined"@@ -395,20 +380,20 @@ -- | -- Infer a type for a value, rethrowing any error to provide a more useful error message ---infer :: Value -> Subst Value+infer :: Value -> UnifyT Check Value infer val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ infer' val  -- | -- Infer a type for a value ---infer' :: Value -> Subst Value+infer' :: Value -> UnifyT Check Value infer' v@(NumericLiteral _) = return $ TypedValue True v Number infer' v@(StringLiteral _) = return $ TypedValue True v String infer' v@(BooleanLiteral _) = return $ TypedValue True v Boolean infer' (ArrayLiteral vals) = do   ts <- mapM infer vals   els <- fresh-  forM_ ts $ \(TypedValue _ _ t) -> els ~~ TypeApp Array t+  forM_ ts $ \(TypedValue _ _ t) -> els ?= TypeApp Array t   return $ TypedValue True (ArrayLiteral ts) els infer' (Unary op val) = do   v <- infer val@@ -448,7 +433,7 @@     Just ty -> return $ TypedValue True (Accessor prop typed) ty infer' (Abs args ret) = do   ts <- replicateM (length args) fresh-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   bindLocalVariables moduleName (zip args ts) $ do     body@(TypedValue _ _ bodyTy) <- infer' ret     return $ TypedValue True (Abs args body) $ Function ts bodyTy@@ -458,7 +443,7 @@   app <- checkFunctionApplication f' ft args ret   return $ TypedValue True app ret infer' (Var var) = do-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   ty <- lookupVariable moduleName var   ty' <- replaceAllTypeSynonyms ty   case ty' of@@ -474,7 +459,7 @@   return $ TypedValue True (Block ss') ret infer' v@(Constructor c) = do   env <- getEnv-  moduleName <- substCurrentModule `fmap` ask+  Just moduleName <- checkCurrentModule <$> get   case M.lookup (qualify moduleName c) (dataConstructors env) of     Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"     Just (ty, _) -> do ty' <- replaceAllTypeSynonyms ty@@ -488,10 +473,10 @@   cond' <- check cond Boolean   v2@(TypedValue _ _ t2) <- infer th   v3@(TypedValue _ _ t3) <- infer el-  t2 ~~ t3+  t2 ?= t3   return $ TypedValue True (IfThenElse cond' v2 v3) t2 infer' (TypedValue checkType val ty) = do-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   kind <- liftCheck $ kindOf moduleName ty   guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star   ty' <- replaceAllTypeSynonyms ty@@ -502,7 +487,7 @@ -- | -- Infer the type of a property inside a record with a given type ---inferProperty :: Type -> String -> Subst (Maybe Type)+inferProperty :: Type -> String -> UnifyT Check (Maybe Type) inferProperty (Object row) prop = do   let (props, _) = rowToList row   return $ lookup prop props@@ -517,22 +502,22 @@ -- | -- Infer the type of a unary operator application ---inferUnary :: UnaryOperator -> Value -> Subst Value+inferUnary :: UnaryOperator -> Value -> UnifyT Check Value inferUnary op (TypedValue _ val valTy) =   case fromMaybe (error "Invalid operator") $ lookup op unaryOps of     (valTy', resTy) -> do-      valTy' ~~ valTy+      valTy' ?= valTy       return $ TypedValue True (Unary op val) resTy inferUnary _ _ = error "Invalid arguments to inferUnary"  -- | -- Check the type of a unary operator application ---checkUnary :: UnaryOperator -> Value -> Type -> Subst Value+checkUnary :: UnaryOperator -> Value -> Type -> UnifyT Check Value checkUnary op val res =   case fromMaybe (error "Invalid operator") $ lookup op unaryOps of     (valTy, resTy) -> do-      res ~~ resTy+      res ?= resTy       val' <- check val valTy       return $ Unary op val' @@ -548,32 +533,32 @@ -- | -- Infer the type of a binary operator application ---inferBinary :: BinaryOperator -> Value -> Value -> Subst Value+inferBinary :: BinaryOperator -> Value -> Value -> UnifyT Check Value inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) | isEqualityTest op = do-  leftTy ~~ rightTy+  leftTy ?= rightTy   return $ TypedValue True (Binary op left right) Boolean inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) =   case fromMaybe (error "Invalid operator") $ lookup op binaryOps of     (valTy, resTy) -> do-      leftTy ~~ valTy-      rightTy ~~ valTy+      leftTy ?= valTy+      rightTy ?= valTy       return $ TypedValue True (Binary op left right) resTy inferBinary _ _ _ = error "Invalid arguments to inferBinary"  -- | -- Check the type of a binary operator application ---checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst Value+checkBinary :: BinaryOperator -> Value -> Value -> Type -> UnifyT Check Value checkBinary op left right res | isEqualityTest op = do-  res ~~ Boolean+  res ?= Boolean   left'@(TypedValue _ _ t1) <- infer left   right'@(TypedValue _ _ t2) <- infer right-  t1 ~~ t2+  t1 ?= t2   return $ Binary op left' right' checkBinary op left right res =   case fromMaybe (error "Invalid operator") $ lookup op binaryOps of     (valTy, resTy) -> do-      res ~~ resTy+      res ?= resTy       left' <- check left valTy       right' <- check right valTy       return $ Binary op left' right'@@ -613,15 +598,15 @@ -- | -- Infer the types of variables brought into scope by a binder ---inferBinder :: Type -> Binder -> Subst (M.Map Ident Type)+inferBinder :: Type -> Binder -> UnifyT Check (M.Map Ident Type) inferBinder _ NullBinder = return M.empty-inferBinder val (StringBinder _) = val ~~ String >> return M.empty-inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty-inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty+inferBinder val (StringBinder _) = val ?= String >> return M.empty+inferBinder val (NumberBinder _) = val ?= Number >> return M.empty+inferBinder val (BooleanBinder _) = val ?= Boolean >> return M.empty inferBinder val (VarBinder name) = return $ M.singleton name val inferBinder val (NullaryBinder ctor) = do   env <- getEnv-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   case M.lookup (qualify moduleName ctor) (dataConstructors env) of     Just (ty, _) -> do       ty `subsumes` val@@ -629,7 +614,7 @@     _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined" inferBinder val (UnaryBinder ctor binder) = do   env <- getEnv-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   case M.lookup (qualify moduleName ctor) (dataConstructors env) of     Just (ty, _) -> do       fn <- replaceAllVarsWithUnknowns ty@@ -643,11 +628,11 @@   row <- fresh   rest <- fresh   m1 <- inferRowProperties row rest props-  val ~~ Object row+  val ?= Object row   return m1   where-  inferRowProperties :: Type -> Type -> [(String, Binder)] -> Subst (M.Map Ident Type)-  inferRowProperties nrow row [] = nrow ~~ row >> return M.empty+  inferRowProperties :: Type -> Type -> [(String, Binder)] -> UnifyT Check (M.Map Ident Type)+  inferRowProperties nrow row [] = nrow ?= row >> return M.empty   inferRowProperties nrow row ((name, binder):binders) = do     propTy <- fresh     m1 <- inferBinder propTy binder@@ -656,13 +641,13 @@ inferBinder val (ArrayBinder binders) = do   el <- fresh   m1 <- M.unions <$> mapM (inferBinder el) binders-  val ~~ TypeApp Array el+  val ?= TypeApp Array el   return m1 inferBinder val (ConsBinder headBinder tailBinder) = do   el <- fresh   m1 <- inferBinder el headBinder   m2 <- inferBinder val tailBinder-  val ~~ TypeApp Array el+  val ?= TypeApp Array el   return $ m1 `M.union` m2 inferBinder val (NamedBinder name binder) = do   m <- inferBinder val binder@@ -671,10 +656,10 @@ -- | -- Check the types of the return values in a set of binders in a case statement ---checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> Subst [([Binder], Maybe Guard, Value)]+checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> UnifyT Check [([Binder], Maybe Guard, Value)] checkBinders _ _ [] = return [] checkBinders nvals ret ((binders, grd, val):bs) = do-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   m1 <- M.unions <$> zipWithM inferBinder nvals binders   r <- bindLocalVariables moduleName (M.toList m1) $ do     val' <- check val ret@@ -689,19 +674,19 @@ -- | -- Check that a local variable name is not already used ---assignVariable :: Ident -> Subst ()+assignVariable :: Ident -> UnifyT Check () assignVariable name = do   env <- checkEnv <$> get-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   case M.lookup (moduleName, name) (names env) of-    Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."+    Just _ -> UnifyT . lift . throwError $ "Variable with name " ++ show name ++ " already exists."     _ -> return ()  -- | -- Check the type of the return values of a statement, returning whether or not the statement returns on -- all code paths ---checkStatement :: M.Map Ident Type -> Type -> Statement -> Subst (Bool, M.Map Ident Type, Statement)+checkStatement :: M.Map Ident Type -> Type -> Statement -> UnifyT Check (Bool, M.Map Ident Type, Statement) checkStatement mass _ (VariableIntroduction name val) = do   assignVariable name   val'@(TypedValue _ _ t) <- infer val@@ -710,7 +695,7 @@   val'@(TypedValue _ _ t) <- infer val   case M.lookup ident mass of     Nothing -> throwError $ "No local variable with name " ++ show ident-    Just ty -> do t ~~ ty+    Just ty -> do t ?= ty                   return (False, mass, Assignment ident val') checkStatement mass ret (While val inner) = do   val' <- check val Boolean@@ -720,7 +705,7 @@   (allCodePathsReturn, ifst') <- checkIfStatement mass ret ifst   return (allCodePathsReturn, mass, If ifst') checkStatement mass ret (For ident start end inner) = do-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   assignVariable ident   start' <- check start Number   end' <- check end Number@@ -733,7 +718,7 @@ -- | -- Check the type of an if-then-else statement ---checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> Subst (Bool, IfStatement)+checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> UnifyT Check (Bool, IfStatement) checkIfStatement mass ret (IfStatement val thens Nothing) = do   val' <- check val Boolean   (_, _, thens') <- checkBlock mass ret thens@@ -747,7 +732,7 @@ -- | -- Check the type of an else statement ---checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> Subst (Bool, ElseStatement)+checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> UnifyT Check (Bool, ElseStatement) checkElseStatement mass ret (Else elses) = do   (allCodePathsReturn, _, elses') <- checkBlock mass ret elses   return (allCodePathsReturn, Else elses')@@ -756,10 +741,10 @@ -- | -- Check the type of the return value of a block of statements ---checkBlock :: M.Map Ident Type -> Type -> [Statement] -> Subst (Bool, M.Map Ident Type, [Statement])+checkBlock :: M.Map Ident Type -> Type -> [Statement] -> UnifyT Check (Bool, M.Map Ident Type, [Statement]) checkBlock mass _ [] = return (False, mass, []) checkBlock mass ret (s:ss) = do-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   (b1, mass1, s') <- checkStatement mass ret s   bindLocalVariables moduleName (M.toList mass1) $ case (b1, ss) of     (True, []) -> return (True, mass1, [s'])@@ -771,15 +756,15 @@ -- | -- Skolemize a type variable by replacing its instances with fresh skolem constants ---skolemize :: String -> Type -> Subst Type+skolemize :: String -> Type -> UnifyT Check Type skolemize ident ty = do-  tsk <- Skolem <$> fresh'+  tsk <- Skolem . runUnknown <$> fresh'   return $ replaceTypeVars ident tsk ty  -- | -- Check the type of a value, rethrowing errors to provide a better error message ---check :: Value -> Type -> Subst Value+check :: Value -> Type -> UnifyT Check Value check val ty = rethrow errorMessage $ check' val ty   where   errorMessage msg =@@ -793,13 +778,13 @@ -- | -- Check the type of a value ---check' :: Value -> Type -> Subst Value+check' :: Value -> Type -> UnifyT Check Value check' val (ForAll idents ty) = do   sk <- skolemize idents ty   check val sk check' val (ConstrainedType constraints ty) = do   env <- getEnv-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   dictNames <- flip mapM constraints $ \(Qualified _ (ProperName className), _) -> do     n <- liftCheck freshDictionaryName     return $ Ident $ "__dict_" ++ className ++ "_" ++ show n@@ -812,7 +797,7 @@   val'@(TypedValue _ _ ty) <- infer val   -- Don't unify an unknown with an inferred polytype   ty' <- replaceAllVarsWithUnknowns ty-  ty' ~~ u+  ty' ?= u   return val' check' v@(NumericLiteral _) Number = return v check' v@(StringLiteral _) String = return v@@ -825,7 +810,7 @@   vals' <- check vals (TypeApp Array ty)   return $ Indexer index' vals' check' (Abs args ret) (Function argTys retTy) = do-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   guardWith "Incorrect number of function arguments" (length args == length argTys)   ret' <- bindLocalVariables moduleName (zip args argTys) $ check ret retTy   return $ Abs args ret'@@ -834,13 +819,13 @@   app <- checkFunctionApplication f' ft args ret   return $ app check' (Var var) ty = do-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   ty1 <- lookupVariable moduleName var   repl <- replaceAllTypeSynonyms ty1   repl `subsumes` ty   return $ Var var check' (TypedValue checkType val ty1) ty2 = do-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   kind <- liftCheck $ kindOf moduleName ty1   guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star   ty1 `subsumes` ty2@@ -879,7 +864,7 @@   return $ Block ss' check' (Constructor c) ty = do   env <- getEnv-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   case M.lookup (qualify moduleName c) (dataConstructors env) of     Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"     Just (ty1, _) -> do@@ -896,10 +881,10 @@ -- -- The @lax@ parameter controls whether or not every record member has to be provided. For object updates, this is not the case. ---checkProperties :: [(String, Value)] -> Type -> Bool -> Subst [(String, Value)]+checkProperties :: [(String, Value)] -> Type -> Bool -> UnifyT Check [(String, Value)] checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where   go [] [] REmpty = return []-  go [] [] u@(TUnknown _) = do u ~~ REmpty+  go [] [] u@(TUnknown _) = do u ?= REmpty                                return []   go [] [] (Skolem _) | lax = return []   go [] ((p, _): _) _ | lax = return []@@ -908,7 +893,7 @@   go ((p,v):ps') [] u@(TUnknown _) = do     v'@(TypedValue _ _ ty) <- infer v     rest <- fresh-    u ~~ RCons p ty rest+    u ?= RCons p ty rest     ps'' <- go ps' [] rest     return $ (p, v') : ps''   go ((p,v):ps') ts r =@@ -916,7 +901,7 @@       Nothing -> do         v'@(TypedValue _ _ ty) <- infer v         rest <- fresh-        r ~~ RCons p ty rest+        r ?= RCons p ty rest         ps'' <- go ps' ts rest         return $ (p, v') : ps''       Just ty -> do@@ -928,7 +913,7 @@ -- | -- Check the type of a function application, rethrowing errors to provide a better error message ---checkFunctionApplication :: Value -> Type -> [Value] -> Type -> Subst Value+checkFunctionApplication :: Value -> Type -> [Value] -> Type -> UnifyT Check Value checkFunctionApplication fn fnTy args ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy args ret   where   errorMessage msg = "Error applying function of type "@@ -939,7 +924,7 @@ -- | -- Check the type of a function application ---checkFunctionApplication' :: Value -> Type -> [Value] -> Type -> Subst Value+checkFunctionApplication' :: Value -> Type -> [Value] -> Type -> UnifyT Check Value checkFunctionApplication' fn (Function argTys retTy) args ret = do   guardWith "Incorrect number of function arguments" (length args == length argTys)   args' <- zipWithM check args argTys@@ -951,7 +936,7 @@ checkFunctionApplication' fn u@(TUnknown _) args ret = do   args' <- mapM (\arg -> infer arg >>= \(TypedValue _ v t) -> TypedValue True v <$> replaceAllVarsWithUnknowns t) args   let tys = map (\(TypedValue _ _ t) -> t) args'-  u ~~ Function tys ret+  u ?= Function tys ret   return $ App fn args' checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) args ret = do   ty <- expandTypeSynonym name tyArgs@@ -959,7 +944,7 @@ checkFunctionApplication' fn (ConstrainedType constraints fnTy) args ret = do   env <- getEnv   dicts <- getTypeClassDictionaries-  moduleName <- substCurrentModule <$> ask+  Just moduleName <- checkCurrentModule <$> get   checkFunctionApplication' (App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy args ret checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of type "   ++ prettyPrintType fnTy@@ -969,7 +954,7 @@ -- | -- Check whether one type subsumes another, rethrowing errors to provide a better error message ---subsumes :: Type -> Type -> Subst ()+subsumes :: Type -> Type -> UnifyT Check () subsumes ty1 ty2 = rethrow errorMessage $ subsumes' ty1 ty2   where   errorMessage msg = "Error checking that type "@@ -981,12 +966,12 @@ -- | -- Check whether one type subsumes another ---subsumes' :: Type -> Type -> Subst ()+subsumes' :: Type -> Type -> UnifyT Check () subsumes' (ForAll ident ty1) ty2 = do   replaced <- replaceVarWithUnknown ident ty1   replaced `subsumes` ty2 subsumes' (Function args1 ret1) (Function args2 ret2) = do   zipWithM_ subsumes args2 args1   ret1 `subsumes` ret2-subsumes' ty1 ty2 = ty1 ~~ ty2+subsumes' ty1 ty2 = ty1 ?= ty2
src/Language/PureScript/Types.hs view
@@ -20,8 +20,9 @@ import Data.Data import Data.Generics (mkT, mkQ, everywhereBut) +import Control.Monad.Unify+ import Language.PureScript.Names-import Language.PureScript.Unknown (Unknown(..))  -- | -- The type of types@@ -30,7 +31,7 @@   -- |   -- A unification variable of type Type   ---  = TUnknown (Unknown Type)+  = TUnknown (TypedUnknown Type)   -- |   -- Javascript numbers   --
− src/Language/PureScript/Unknown.hs 
@@ -1,28 +0,0 @@------------------------------------------------------------------------------------ Module      :  Language.PureScript.Unknown--- Copyright   :  (c) Phil Freeman 2013--- License     :  MIT------ Maintainer  :  Phil Freeman <paf31@cantab.net>--- Stability   :  experimental--- Portability :------ |--- Data type for unification variables-----------------------------------------------------------------------------------{-# LANGUAGE DeriveDataTypeable #-}--module Language.PureScript.Unknown where--import Data.Data---- |--- The type of typed unification variables----newtype Unknown t = Unknown { runUnknown :: Int } deriving (Show, Eq, Ord, Data, Typeable)---