From acda2b3337df36beb24bac0696b29085bf8f7f19 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 1 May 2018 20:33:17 -0400 Subject: [PATCH 1/6] Use Exception rather than Frame, reduce constraints imposed by forceThunk --- src/Nix/Builtins.hs | 109 +++++++++++++++++++++------------------- src/Nix/Convert.hs | 2 +- src/Nix/Eval.hs | 22 ++++---- src/Nix/Exec.hs | 96 +++++++++++++++++++---------------- src/Nix/Frames.hs | 30 +++-------- src/Nix/Lint.hs | 21 ++++---- src/Nix/Normal.hs | 2 +- src/Nix/Render/Frame.hs | 15 +++--- src/Nix/Thunk.hs | 14 +++--- src/Nix/Value.hs | 5 +- 10 files changed, 159 insertions(+), 157 deletions(-) diff --git a/src/Nix/Builtins.hs b/src/Nix/Builtins.hs index 97f6e537..d7d31e33 100644 --- a/src/Nix/Builtins.hs +++ b/src/Nix/Builtins.hs @@ -111,7 +111,7 @@ builtinsList = sequence [ , add0 Normal "nixPath" nixPath , add TopLevel "abort" throw_ -- for now - , add2 Normal "add" add_ + , add2 Normal "add" add_ , add2 Normal "all" all_ , add2 Normal "any" any_ , add Normal "attrNames" attrNames @@ -201,7 +201,8 @@ builtinsList = sequence [ arity1 f = Prim . pure . f arity2 f = ((Prim . pure) .) . f - mkThunk n = thunk . withFrame Info ("While calling builtin " ++ Text.unpack n ++ "\n") + mkThunk n = thunk . withFrame Info + (ErrorCall $ "While calling builtin " ++ Text.unpack n ++ "\n") add0 t n v = wrap t n <$> mkThunk n v add t n v = wrap t n <$> mkThunk n (builtin (Text.unpack n) v) @@ -228,7 +229,7 @@ foldNixPath f z = do go x rest = case Text.splitOn "=" x of [p] -> f (Text.unpack p) Nothing rest [n, p] -> f (Text.unpack p) (Just (Text.unpack n)) rest - _ -> throwError @String $ "Unexpected entry in NIX_PATH: " ++ show x + _ -> throwError $ ErrorCall $ "Unexpected entry in NIX_PATH: " ++ show x nixPath :: MonadNix e m => m (NValue m) nixPath = fmap nvList $ flip foldNixPath [] $ \p mn rest -> @@ -242,23 +243,22 @@ toString :: MonadNix e m => m (NValue m) -> m (NValue m) toString str = str >>= normalForm >>= valueText False >>= toNix @(Text, DList Text) -hasAttr :: MonadNix e m => m (NValue m) -> m (NValue m) -> m (NValue m) -hasAttr x y = x >>= \x' -> y >>= \y' -> case (x', y') of - (NVStr key _, NVSet aset _) -> - return . nvConstant . NBool $ M.member key aset - (x, y) -> throwError @String $ "Invalid types for builtin.hasAttr: " - ++ show (x, y) +hasAttr :: forall e m. MonadNix e m => m (NValue m) -> m (NValue m) -> m (NValue m) +hasAttr x y = + fromValue @Text x >>= \key -> + fromValue @(AttrSet (NThunk m), AttrSet SourcePos) y >>= \(aset, _) -> + toNix $ M.member key aset attrsetGet :: MonadNix e m => Text -> AttrSet t -> m t attrsetGet k s = case M.lookup k s of Just v -> pure v Nothing -> - throwError ("Attribute '" ++ Text.unpack k ++ "' required" :: String) + throwError $ ErrorCall $ "Attribute '" ++ Text.unpack k ++ "' required" getAttr :: MonadNix e m => m (NValue m) -> m (NValue m) -> m (NValue m) getAttr x y = x >>= \x' -> y >>= \y' -> case (x', y') of (NVStr key _, NVSet aset _) -> attrsetGet key aset >>= force' - (x, y) -> throwError @String $ "Invalid types for builtin.getAttr: " + (x, y) -> throwError $ ErrorCall $ "Invalid types for builtin.getAttr: " ++ show (x, y) unsafeGetAttrPos :: forall e m. MonadNix e m @@ -266,10 +266,10 @@ unsafeGetAttrPos :: forall e m. MonadNix e m unsafeGetAttrPos x y = x >>= \x' -> y >>= \y' -> case (x', y') of (NVStr key _, NVSet _ apos) -> case M.lookup key apos of Nothing -> - throwError @String $ "unsafeGetAttrPos: field '" ++ Text.unpack key + throwError $ ErrorCall $ "unsafeGetAttrPos: field '" ++ Text.unpack key ++ "' does not exist in attr set: " ++ show apos Just delta -> toValue delta - (x, y) -> throwError @String $ "Invalid types for builtin.unsafeGetAttrPos: " + (x, y) -> throwError $ ErrorCall $ "Invalid types for builtin.unsafeGetAttrPos: " ++ show (x, y) -- This function is a bit special in that it doesn't care about the contents @@ -340,12 +340,12 @@ foldl'_ fun z xs = head_ :: MonadNix e m => m (NValue m) -> m (NValue m) head_ = fromValue >=> \case - [] -> throwError @String "builtins.head: empty list" + [] -> throwError $ ErrorCall "builtins.head: empty list" h:_ -> force' h tail_ :: MonadNix e m => m (NValue m) -> m (NValue m) tail_ = fromValue >=> \case - [] -> throwError @String "builtins.tail: empty list" + [] -> throwError $ ErrorCall "builtins.tail: empty list" _:t -> return $ nvList t data VersionComponent @@ -470,7 +470,7 @@ thunkStr s = valueThunk (nvStr (decodeUtf8 s) mempty) substring :: MonadNix e m => Int -> Int -> Text -> Prim m Text substring start len str = Prim $ if start < 0 --NOTE: negative values of 'len' are OK - then throwError @String $ "builtins.substring: negative start position: " ++ show start + then throwError $ ErrorCall $ "builtins.substring: negative start position: " ++ show start else pure $ Text.take len $ Text.drop start str attrNames :: forall e m. MonadNix e m => m (NValue m) -> m (NValue m) @@ -483,7 +483,8 @@ attrValues = fromValue @(ValueSet m) >=> map_ :: forall e m. MonadNix e m => m (NValue m) -> m (NValue m) -> m (NValue m) map_ fun xs = fun >>= \f -> - toNix <=< traverse (thunk . withFrame @String Debug "While applying f in map:\n" + toNix <=< traverse (thunk . withFrame Debug + (ErrorCall "While applying f in map:\n") . (f `callFunc`) . force') <=< fromValue @[NThunk m] $ xs @@ -503,13 +504,13 @@ baseNameOf :: MonadNix e m => m (NValue m) -> m (NValue m) baseNameOf x = x >>= \case NVStr path ctx -> pure $ nvStr (Text.pack $ takeFileName $ Text.unpack path) ctx NVPath path -> pure $ nvPath $ takeFileName path - v -> throwError @String $ "dirOf: expected string or path, got " ++ show v + v -> throwError $ ErrorCall $ "dirOf: expected string or path, got " ++ show v dirOf :: MonadNix e m => m (NValue m) -> m (NValue m) dirOf x = x >>= \case NVStr path ctx -> pure $ nvStr (Text.pack $ takeDirectory $ Text.unpack path) ctx NVPath path -> pure $ nvPath $ takeDirectory path - v -> throwError @String $ "dirOf: expected string or path, got " ++ show v + v -> throwError $ ErrorCall $ "dirOf: expected string or path, got " ++ show v -- jww (2018-04-28): This should only be a string argument, and not coerced? unsafeDiscardStringContext :: MonadNix e m => m (NValue m) -> m (NValue m) @@ -542,7 +543,7 @@ elemAt_ :: MonadNix e m => m (NValue m) -> m (NValue m) -> m (NValue m) elemAt_ xs n = fromValue n >>= \n' -> fromValue xs >>= \xs' -> case elemAt xs' n' of Just a -> force' a - Nothing -> throwError @String $ "builtins.elem: Index " ++ show n' + Nothing -> throwError $ ErrorCall $ "builtins.elem: Index " ++ show n' ++ " too large for list of length " ++ show (length xs') genList :: MonadNix e m => m (NValue m) -> m (NValue m) -> m (NValue m) @@ -550,24 +551,22 @@ genList generator = fromValue @Integer >=> \n -> if n >= 0 then generator >>= \f -> toNix =<< forM [0 .. n - 1] (\i -> thunk $ f `callFunc` toNix i) - else throwError @String $ "builtins.genList: Expected a non-negative number, got " + else throwError $ ErrorCall $ "builtins.genList: Expected a non-negative number, got " ++ show n genericClosure :: forall e m. MonadNix e m => m (NValue m) -> m (NValue m) genericClosure = fromValue @(AttrSet (NThunk m)) >=> \s -> case (M.lookup "startSet" s, M.lookup "operator" s) of (Nothing, Nothing) -> - throwError - ("builtins.genericClosure: Attributes 'startSet' and 'operator' required" - :: String) + throwError $ ErrorCall $ + "builtins.genericClosure: " + ++ "Attributes 'startSet' and 'operator' required" (Nothing, Just _) -> - throwError - ("builtins.genericClosure: Attribute 'startSet' required" - :: String) + throwError $ ErrorCall $ + "builtins.genericClosure: Attribute 'startSet' required" (Just _, Nothing) -> - throwError - ("builtins.genericClosure: Attribute 'operator' required" - :: String) + throwError $ ErrorCall $ + "builtins.genericClosure: Attribute 'operator' required" (Just startSet, Just operator) -> fromValue @[NThunk m] startSet >>= \ss -> force operator $ \op -> @@ -580,8 +579,8 @@ genericClosure = fromValue @(AttrSet (NThunk m)) >=> \s -> force t $ \v -> fromValue @(AttrSet (NThunk m)) t >>= \s -> case M.lookup "key" s of Nothing -> - throwError - ("builtins.genericClosure: Attribute 'key' required" :: String) + throwError $ ErrorCall $ + "builtins.genericClosure: Attribute 'key' required" Just k -> force k $ \k' -> if S.member k' ks then go op ts ks @@ -598,8 +597,9 @@ replaceStrings tfrom tto ts = fromNix tto >>= \(to :: [Text]) -> fromValue ts >>= \(s :: Text) -> do when (length from /= length to) $ - throwError @String $ "'from' and 'to' arguments to 'replaceStrings'" - ++ " have different lengths" + throwError $ ErrorCall $ + "'from' and 'to' arguments to 'replaceStrings'" + ++ " have different lengths" let lookupPrefix s = do (prefix, replacement) <- find ((`Text.isPrefixOf` s) . fst) $ zip from to @@ -646,8 +646,8 @@ functionArgs fun = fun >>= \case case p of Param name -> M.singleton name False ParamSet s _ _ -> isJust <$> M.fromList s - v -> throwError @String $ "builtins.functionArgs: expected function, got " - ++ show v + v -> throwError $ ErrorCall $ + "builtins.functionArgs: expected function, got " ++ show v toPath :: MonadNix e m => m (NValue m) -> m (NValue m) toPath = fromValue @Path >=> toNix @Path @@ -656,7 +656,8 @@ pathExists_ :: MonadNix e m => m (NValue m) -> m (NValue m) pathExists_ path = path >>= \case NVPath p -> toNix =<< pathExists p NVStr s _ -> toNix =<< pathExists (Text.unpack s) - v -> throwError @String $ "builtins.pathExists: expected path, got " ++ show v + v -> throwError $ ErrorCall $ + "builtins.pathExists: expected path, got " ++ show v hasKind :: forall a e m. (MonadNix e m, FromValue a m (NValue m)) => m (NValue m) -> m (NValue m) @@ -689,7 +690,7 @@ isFunction func = func >>= \case _ -> toValue False throw_ :: MonadNix e m => m (NValue m) -> m (NValue m) -throw_ = fromValue >=> throwError . Text.unpack +throw_ = fromValue >=> throwError . ErrorCall . Text.unpack import_ :: MonadNix e m => m (NValue m) -> m (NValue m) import_ = fromValue >=> importPath M.empty . getPath @@ -723,8 +724,9 @@ sort_ comparator xs = comparator >>= \comp -> lessThan :: MonadNix e m => m (NValue m) -> m (NValue m) -> m (NValue m) lessThan ta tb = ta >>= \va -> tb >>= \vb -> do - let badType = throwError @String $ "builtins.lessThan: expected two numbers or two strings, " - ++ "got " ++ show va ++ " and " ++ show vb + let badType = throwError $ ErrorCall $ + "builtins.lessThan: expected two numbers or two strings, " + ++ "got " ++ show va ++ " and " ++ show vb nvConstant . NBool <$> case (va, vb) of (NVConstant ca, NVConstant cb) -> case (ca, cb) of (NInt a, NInt b) -> pure $ a < b @@ -746,7 +748,10 @@ listToAttrs = fromValue @[NThunk m] >=> \l -> forM l $ fromValue @(AttrSet (NThunk m)) >=> \s -> case (M.lookup "name" s, M.lookup "value" s) of (Just name, Just value) -> fromValue name <&> (, value) - _ -> throwError $ + _ -> throwError $ ErrorCall $ + -- jww (2018-05-01): Rather than include the function name + -- in the message like this, we should add it as a frame + -- in `callFunc' before calling each builtin. "builtins.listToAttrs: expected set with name and value, got" ++ show s @@ -757,7 +762,7 @@ hashString algo s = Prim $ do "sha1" -> pure SHA1.hash "sha256" -> pure SHA256.hash "sha512" -> pure SHA512.hash - _ -> throwError @String $ "builtins.hashString: " + _ -> throwError $ ErrorCall $ "builtins.hashString: " ++ "expected \"md5\", \"sha1\", \"sha256\", or \"sha512\", got " ++ show algo pure $ decodeUtf8 $ Base16.encode $ hash $ encodeUtf8 s @@ -766,10 +771,10 @@ absolutePathFromValue = \case NVStr pathText _ -> do let path = Text.unpack pathText unless (isAbsolute path) $ - throwError @String $ "string " ++ show path ++ " doesn't represent an absolute path" + throwError $ ErrorCall $ "string " ++ show path ++ " doesn't represent an absolute path" pure path NVPath path -> pure path - v -> throwError @String $ "expected a path, got " ++ show v + v -> throwError $ ErrorCall $ "expected a path, got " ++ show v readFile_ :: MonadNix e m => m (NValue m) -> m (NValue m) readFile_ path = @@ -806,7 +811,8 @@ readDir_ pathThunk = do fromJSON :: MonadNix e m => m (NValue m) -> m (NValue m) fromJSON = fromValue >=> \encoded -> case A.eitherDecodeStrict' @A.Value $ encodeUtf8 encoded of - Left jsonError -> throwError @String $ "builtins.fromJSON: " ++ jsonError + Left jsonError -> + throwError $ ErrorCall $ "builtins.fromJSON: " ++ jsonError Right v -> toValue v toXML_ :: MonadNix e m => m (NValue m) -> m (NValue m) @@ -846,19 +852,20 @@ tryEval e = catch (onSuccess <$> e) (pure . onError) fetchTarball :: forall e m. MonadNix e m => m (NValue m) -> m (NValue m) fetchTarball v = v >>= \case NVSet s _ -> case M.lookup "url" s of - Nothing -> throwError @String "builtins.fetchTarball: Missing url attribute" + Nothing -> throwError $ ErrorCall + "builtins.fetchTarball: Missing url attribute" Just url -> force url $ go (M.lookup "sha256" s) v@NVStr {} -> go Nothing v v@(NVConstant (NUri _)) -> go Nothing v - v -> throwError @String $ "builtins.fetchTarball: Expected URI or set, got " - ++ show v + v -> throwError $ ErrorCall $ + "builtins.fetchTarball: Expected URI or set, got " ++ show v where go :: Maybe (NThunk m) -> NValue m -> m (NValue m) go msha = \case NVStr uri _ -> fetch uri msha NVConstant (NUri uri) -> fetch uri msha - v -> throwError @String $ "builtins.fetchTarball: Expected URI or string, got " - ++ show v + v -> throwError $ ErrorCall $ + "builtins.fetchTarball: Expected URI or string, got " ++ show v {- jww (2018-04-11): This should be written using pipes in another module fetch :: Text -> Maybe (NThunk m) -> m (NValue m) @@ -868,7 +875,7 @@ fetchTarball v = v >>= \case ".bz2" -> undefined ".xz" -> undefined ".tar" -> undefined - ext -> throwError @String $ "builtins.fetchTarball: Unsupported extension '" + ext -> throwError $ ErrorCall $ "builtins.fetchTarball: Unsupported extension '" ++ ext ++ "'" -} diff --git a/src/Nix/Convert.hs b/src/Nix/Convert.hs index f02777ae..0938f8cf 100644 --- a/src/Nix/Convert.hs +++ b/src/Nix/Convert.hs @@ -440,7 +440,7 @@ instance Applicative m => ToValue Bool m (NExprF r) where instance Applicative m => ToValue () m (NExprF r) where toValue _ = pure . NConstant $ NNull -whileForcingThunk :: forall s e m r. (Framed e m, Frame s, Typeable m) +whileForcingThunk :: forall s e m r. (Framed e m, Exception s, Typeable m) => s -> m r -> m r whileForcingThunk frame = withFrame Debug (ForcingThunk @m) . withFrame Debug frame diff --git a/src/Nix/Eval.hs b/src/Nix/Eval.hs index 58e7b053..f2911971 100644 --- a/src/Nix/Eval.hs +++ b/src/Nix/Eval.hs @@ -81,7 +81,7 @@ class (Show v, Monad m) => MonadEval v m | v -> m where evalLet :: m v -> m v -} - evalError :: Frame s => s -> m a + evalError :: Exception s => s -> m a type MonadNixEval e v t m = (MonadEval v m, @@ -99,7 +99,7 @@ data EvalFrame m v | ForcingExpr (Scopes m v) NExprLoc deriving (Show, Typeable) -instance (Typeable m, Typeable v) => Frame (EvalFrame m v) +instance (Typeable m, Typeable v) => Exception (EvalFrame m v) eval :: forall e v t m. MonadNixEval e v t m => NExprF (m v) -> m v @@ -128,7 +128,7 @@ eval (NSelect aset attr alt) = do Right v -> v Left (s, ks) -> fromMaybe err alt where - err = evalError @v $ "Could not look up attribute " + err = evalError @v $ ErrorCall $ "Could not look up attribute " ++ intercalate "." (map Text.unpack (NE.toList ks)) ++ " in " ++ show @v s @@ -199,7 +199,7 @@ attrSetAlter :: forall e v t m. MonadNixEval e v t m -> m v -> m (AttrSet (m v)) attrSetAlter [] _ _ = - evalError @v ("invalid selector with no components" :: String) + evalError @v $ ErrorCall "invalid selector with no components" attrSetAlter (p:ps) m val = case M.lookup p m of Nothing | null ps -> go @@ -289,8 +289,8 @@ evalBinds allowDynamic recursive binds = do >>= \(s, _) -> clearScopes @t $ pushScope s $ lookupVar key case mv of - Nothing -> evalError @v $ "Inheriting unknown attribute: " - ++ show (void name) + Nothing -> evalError @v $ ErrorCall $ + "Inheriting unknown attribute: " ++ show (void name) Just v -> force v pure) buildResult :: Scopes m t @@ -356,14 +356,14 @@ evalKeyNameStatic :: forall v m. MonadEval v m evalKeyNameStatic = \case StaticKey k p -> pure (k, p) DynamicKey _ -> - evalError @v ("dynamic attribute not allowed in this context" :: String) + evalError @v $ ErrorCall "dynamic attribute not allowed in this context" evalKeyNameDynamicNotNull :: forall v m. (MonadEval v m, FromValue (Text, DList Text) m v) => NKeyName (m v) -> m (Text, Maybe SourcePos) evalKeyNameDynamicNotNull = evalKeyNameDynamicNullable >=> \case (Nothing, _) -> - evalError @v ("value is null while a string was expected" :: String) + evalError @v $ ErrorCall "value is null while a string was expected" (Just k, p) -> pure (k, p) -- | Evaluate a component of an attribute path in a context where we are @@ -421,12 +421,14 @@ buildArgument params arg = do -> m t assemble scope isVariadic k = \case That Nothing -> - const $ evalError @v $ "Missing value for parameter: " ++ show k + const $ evalError @v $ ErrorCall $ + "Missing value for parameter: " ++ show k That (Just f) -> \args -> thunk $ withScopes scope $ pushScope args f This x | isVariadic -> const (pure x) | otherwise -> - const $ evalError @v $ "Unexpected parameter: " ++ show k + const $ evalError @v $ ErrorCall $ + "Unexpected parameter: " ++ show k These x _ -> const (pure x) addSourcePositions :: (MonadReader e m, Has e SrcSpan) diff --git a/src/Nix/Exec.hs b/src/Nix/Exec.hs index e13966d6..44858173 100644 --- a/src/Nix/Exec.hs +++ b/src/Nix/Exec.hs @@ -88,9 +88,9 @@ type MonadNix e m = data ExecFrame m = Assertion SrcSpan (NValue m) deriving (Show, Typeable) -instance Typeable m => Frame (ExecFrame m) +instance Typeable m => Exception (ExecFrame m) -nverr :: forall s e m a. (MonadNix e m, Frame s) => s -> m a +nverr :: forall s e m a. (MonadNix e m, Exception s) => s -> m a nverr = evalError @(NValue m) currentPos :: forall e m. (MonadReader e m, Has e SrcSpan) => m SrcSpan @@ -109,8 +109,9 @@ instance MonadNix e m => MonadThunk (NValue m) (NThunk m) m where -- Gather the current evaluation context at the time of thunk -- creation, and record it along with the thunk. - let go (fromFrame -> Just (EvaluatingExpr scope - (Fix (Compose (Ann span e))))) = + let go (fromException -> + Just (EvaluatingExpr scope + (Fix (Compose (Ann span e))))) = let e' = Compose (Ann span (Nothing <$ e)) in [Provenance scope e'] go _ = [] @@ -120,11 +121,17 @@ instance MonadNix e m => MonadThunk (NValue m) (NThunk m) m where else fmap (NThunk [] . coerce) . buildThunk $ mv - force (NThunk ps t) f = case ps of - [] -> forceThunk t f - Provenance scope e@(Compose (Ann span _)):_ -> - withFrame Info (ForcingExpr scope (wrapExprLoc span e)) - (forceThunk t f) + -- The ThunkLoop exception is thrown as an exception with MonadThrow, + -- which does not capture the current stack frame information to provide + -- it in a NixException, so we catch and re-throw it here using + -- 'throwError' from Frames.hs. + force (NThunk ps t) f = catch go (throwError @ThunkLoop) + where + go = case ps of + [] -> forceThunk t f + Provenance scope e@(Compose (Ann span _)):_ -> + withFrame Info (ForcingExpr scope (wrapExprLoc span e)) + (forceThunk t f) value = NThunk [] . coerce . valueRef @@ -140,7 +147,7 @@ prov p v = do instance MonadNix e m => MonadEval (NValue m) m where freeVariable var = - nverr $ "Undefined variable '" ++ Text.unpack var ++ "'" + nverr $ ErrorCall $ "Undefined variable '" ++ Text.unpack var ++ "'" evalCurPos = do scope <- currentScopes @@ -164,7 +171,7 @@ instance MonadNix e m => MonadEval (NValue m) m where span <- currentPos pure $ nvStrP (Provenance scope (NStr_ span (DoubleQuoted [Plain s]))) s c - Nothing -> nverr ("Failed to assemble string" :: String) + Nothing -> nverr $ ErrorCall $ "Failed to assemble string" evalLiteralPath p = do scope <- currentScopes @@ -233,7 +240,7 @@ callFunc fun arg = case fun of s@(NVSet m _) | Just f <- M.lookup "__functor" m -> do traceM "callFunc:__functor" force f $ (`callFunc` pure s) >=> (`callFunc` arg) - x -> throwError $ "Attempt to call non-function: " ++ show x + x -> throwError $ ErrorCall $ "Attempt to call non-function: " ++ show x execUnaryOp :: (Framed e m, MonadVar m) => Scopes m (NThunk m) -> SrcSpan -> NUnaryOp -> NValue m @@ -245,9 +252,9 @@ execUnaryOp scope span op arg = do (NNeg, NInt i) -> unaryOp $ NInt (-i) (NNeg, NFloat f) -> unaryOp $ NFloat (-f) (NNot, NBool b) -> unaryOp $ NBool (not b) - _ -> throwError $ "unsupported argument type for unary operator " - ++ show op - x -> throwError $ "argument to unary operator" + _ -> throwError $ ErrorCall $ + "unsupported argument type for unary operator " ++ show op + x -> throwError $ ErrorCall $ "argument to unary operator" ++ " must evaluate to an atomic type: " ++ show x where unaryOp = pure . nvConstantP (Provenance scope (NUnary_ span op (Just arg))) @@ -291,16 +298,16 @@ execBinaryOp scope span op lval rarg = do (NGt, l, r) -> toBool $ l > r (NGte, l, r) -> toBool $ l >= r (NAnd, _, _) -> - nverr @String "should be impossible: && is handled above" + nverr $ ErrorCall "should be impossible: && is handled above" (NOr, _, _) -> - nverr @String "should be impossible: || is handled above" + nverr $ ErrorCall "should be impossible: || is handled above" (NPlus, l, r) -> numBinOp bin (+) l r (NMinus, l, r) -> numBinOp bin (-) l r (NMult, l, r) -> numBinOp bin (*) l r (NDiv, l, r) -> numBinOp' bin div (/) l r (NImpl, NBool l, NBool r) -> toBool $ not l || r - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVStr ls lc, NVStr rs rc) -> case op of NPlus -> pure $ bin nvStrP (ls `mappend` rs) (lc `mappend` rc) @@ -310,68 +317,68 @@ execBinaryOp scope span op lval rarg = do NLte -> toBool $ ls <= rs NGt -> toBool $ ls > rs NGte -> toBool $ ls >= rs - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVStr _ _, NVConstant NNull) -> case op of NEq -> toBool =<< valueEq lval (nvStr "" mempty) NNEq -> toBool . not =<< valueEq lval (nvStr "" mempty) - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVConstant NNull, NVStr _ _) -> case op of NEq -> toBool =<< valueEq (nvStr "" mempty) rval NNEq -> toBool . not =<< valueEq (nvStr "" mempty) rval - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVSet ls lp, NVSet rs rp) -> case op of NUpdate -> pure $ bin nvSetP (rs `M.union` ls) (rp `M.union` lp) NEq -> toBool =<< valueEq lval rval NNEq -> toBool . not =<< valueEq lval rval - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVSet ls lp, NVConstant NNull) -> case op of NUpdate -> pure $ bin nvSetP ls lp NEq -> toBool =<< valueEq lval (nvSet M.empty M.empty) NNEq -> toBool . not =<< valueEq lval (nvSet M.empty M.empty) - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVConstant NNull, NVSet rs rp) -> case op of NUpdate -> pure $ bin nvSetP rs rp NEq -> toBool =<< valueEq (nvSet M.empty M.empty) rval NNEq -> toBool . not =<< valueEq (nvSet M.empty M.empty) rval - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVList ls, NVList rs) -> case op of NConcat -> pure $ bin nvListP $ ls ++ rs NEq -> toBool =<< valueEq lval rval NNEq -> toBool . not =<< valueEq lval rval - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVList ls, NVConstant NNull) -> case op of NConcat -> pure $ bin nvListP ls NEq -> toBool =<< valueEq lval (nvList []) NNEq -> toBool . not =<< valueEq lval (nvList []) - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVConstant NNull, NVList rs) -> case op of NConcat -> pure $ bin nvListP rs NEq -> toBool =<< valueEq (nvList []) rval NNEq -> toBool . not =<< valueEq (nvList []) rval - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVPath p, NVStr s _) -> case op of NEq -> toBool $ p == Text.unpack s NNEq -> toBool $ p /= Text.unpack s NPlus -> bin nvPathP <$> makeAbsolutePath (p `mappend` Text.unpack s) - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval (NVPath ls, NVPath rs) -> case op of NPlus -> bin nvPathP <$> makeAbsolutePath (ls ++ rs) - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval _ -> case op of NEq -> toBool False NNEq -> toBool True - _ -> nverr $ unsupportedTypes lval rval + _ -> nverr $ ErrorCall $ unsupportedTypes lval rval where unsupportedTypes :: Show a => a -> a -> String unsupportedTypes lval rval = @@ -391,7 +398,7 @@ execBinaryOp scope span op lval rarg = do (NInt li, NFloat rf) -> toFloat $ fromInteger li `floatF` rf (NFloat lf, NInt ri) -> toFloat $ lf `floatF` fromInteger ri (NFloat lf, NFloat rf) -> toFloat $ lf `floatF` rf - _ -> nverr $ unsupportedTypes l r + _ -> nverr $ ErrorCall $ unsupportedTypes l r where toInt = pure . bin nvConstantP . NInt toFloat = pure . bin nvConstantP . NFloat @@ -416,7 +423,7 @@ coerceToString = \case NVSet s _ | Just p <- M.lookup "outPath" s -> force p coerceToString - v -> throwError $ "Expected a string, but saw: " ++ show v + v -> throwError $ ErrorCall $ "Expected a string, but saw: " ++ show v newtype Lazy m a = Lazy { runLazy :: ReaderT (Context (Lazy m) (NThunk (Lazy m))) @@ -448,8 +455,8 @@ instance MonadException m => MonadException (Lazy m) where let run' = RunIO (fmap Lazy . run . runLazy) in runLazy <$> f run' -instance (MonadFix m, MonadCatch m, MonadThrow m, MonadIO m, - Alternative m, MonadPlus m, Typeable m) +instance (MonadFix m, MonadCatch m, MonadIO m, Alternative m, + MonadPlus m, Typeable m) => MonadEffects (Lazy m) where addPath path = do (exitCode, out, _) <- @@ -458,7 +465,8 @@ instance (MonadFix m, MonadCatch m, MonadThrow m, MonadIO m, ExitSuccess -> do let dropTrailingLinefeed p = take (length p - 1) p return $ StorePath $ dropTrailingLinefeed out - _ -> throwError $ "addPath: failed: nix-store --add " ++ show path + _ -> throwError $ ErrorCall $ + "addPath: failed: nix-store --add " ++ show path makeAbsolutePath origPath = do origPathExpanded <- liftIO $ expandHomePath origPath @@ -469,7 +477,7 @@ instance (MonadFix m, MonadCatch m, MonadThrow m, MonadIO m, Nothing -> liftIO getCurrentDirectory Just v -> force v $ \case NVPath s -> return $ takeDirectory s - v -> throwError $ "when resolving relative path," + v -> throwError $ ErrorCall $ "when resolving relative path," ++ " __cur_file is in scope," ++ " but is not a path; it is: " ++ show v @@ -493,7 +501,7 @@ instance (MonadFix m, MonadCatch m, MonadThrow m, MonadIO m, return $ takeDirectory p' path traceM $ "Importing file " ++ path' - withFrame Info ("While importing file " ++ show path') $ do + withFrame Info (ErrorCall $ "While importing file " ++ show path') $ do imports <- Lazy $ ReaderT $ const get expr <- case M.lookup path' imports of Just expr -> pure expr @@ -501,8 +509,8 @@ instance (MonadFix m, MonadCatch m, MonadThrow m, MonadIO m, eres <- Lazy $ parseNixFileLoc path' case eres of Failure err -> - throwError $ text "Parse during import failed:" - P. err + throwError $ ErrorCall . show $ + text "Parse during import failed:" P. err Success expr -> do Lazy $ ReaderT $ const $ modify (M.insert origPath expr) @@ -557,11 +565,11 @@ instance (MonadFix m, MonadCatch m, MonadThrow m, MonadIO m, case exitCode of ExitSuccess -> case parseNixTextLoc (Text.pack out) of Failure err -> - throwError $ "Error parsing output of nix-instantiate: " - ++ show err + throwError $ ErrorCall $ + "Error parsing output of nix-instantiate: " ++ show err Success v -> evalExprLoc v status -> - throwError $ "nix-instantiate failed: " ++ show status + throwError $ ErrorCall $ "nix-instantiate failed: " ++ show status ++ ": " ++ err getRecursiveSize = @@ -629,7 +637,7 @@ findEnvPathM name = do foldM go Nothing l case mpath of Nothing -> - throwError $ "file '" ++ name + throwError $ ErrorCall $ "file '" ++ name ++ "' was not found in the Nix search path" ++ " (add it using $NIX_PATH or -I)" Just path -> return path @@ -646,7 +654,7 @@ findEnvPathM name = do tryPath path (Just (Text.unpack pfx)) _ -> tryPath path Nothing Nothing -> - throwError $ "__nixPath must be a list of attr sets" + throwError $ ErrorCall $ "__nixPath must be a list of attr sets" ++ " with 'path' elements, but saw: " ++ show s tryPath p (Just n) | n':ns <- splitDirectories name, n == n' = diff --git a/src/Nix/Frames.hs b/src/Nix/Frames.hs index 969ff93c..aa518760 100644 --- a/src/Nix/Frames.hs +++ b/src/Nix/Frames.hs @@ -4,8 +4,8 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} -module Nix.Frames (NixLevel(..), Frames, Framed, Frame(..), NixFrame(..), - NixException(..), SomeFrame(..), withFrame, throwError, +module Nix.Frames (NixLevel(..), Frames, Framed, NixFrame(..), + NixException(..), withFrame, throwError, module Data.Typeable, module Control.Exception) where @@ -14,29 +14,13 @@ import Control.Monad.Catch import Control.Monad.Reader import Data.Typeable hiding (typeOf) import Nix.Utils -import Text.PrettyPrint.ANSI.Leijen (Doc) data NixLevel = Fatal | Error | Warning | Info | Debug deriving (Ord, Eq, Bounded, Enum, Show) -data SomeFrame = forall e. Frame e => SomeFrame e - -instance Show SomeFrame where - show (SomeFrame f) = show f - -class (Typeable e, Show e) => Frame e where - toFrame :: e -> SomeFrame - fromFrame :: SomeFrame -> Maybe e - - toFrame = SomeFrame - fromFrame (SomeFrame e) = cast e - -instance Frame [Char] -instance Frame Doc - data NixFrame = NixFrame { frameLevel :: NixLevel - , frame :: SomeFrame + , frame :: SomeException } instance Show NixFrame where @@ -52,11 +36,11 @@ newtype NixException = NixException Frames instance Exception NixException -withFrame :: forall s e m a. (Framed e m, Frame s) => NixLevel -> s -> m a -> m a -withFrame level f = local (over hasLens (NixFrame level (toFrame f) :)) +withFrame :: forall s e m a. (Framed e m, Exception s) => NixLevel -> s -> m a -> m a +withFrame level f = local (over hasLens (NixFrame level (toException f) :)) -throwError :: forall s e m a. (Framed e m, Frame s, MonadThrow m) => s -> m a +throwError :: forall s e m a. (Framed e m, Exception s, MonadThrow m) => s -> m a throwError err = do context <- asks (view hasLens) traceM "Throwing error..." - throwM $ NixException (NixFrame Error (toFrame err):context) + throwM $ NixException (NixFrame Error (toException err):context) diff --git a/src/Nix/Lint.hs b/src/Nix/Lint.hs index c1b6f63f..90276c83 100644 --- a/src/Nix/Lint.hs +++ b/src/Nix/Lint.hs @@ -122,7 +122,7 @@ unpackSymbolic = readVar . coerce type MonadLint e m = (Scoped e (SThunk m) m, Framed e m, MonadVar m) symerr :: forall e m a. MonadLint e m => String -> m a -symerr = evalError @(Symbolic m) +symerr = evalError @(Symbolic m) . ErrorCall renderSymbolic :: MonadLint e m => Symbolic m -> m String renderSymbolic = unpackSymbolic >=> \case @@ -182,9 +182,9 @@ merge context = go then go xs ys else (TSet (Just m) :) <$> go xs ys (TClosure {}, TClosure {}) -> - throwError "Cannot unify functions" + throwError $ ErrorCall "Cannot unify functions" (TBuiltin _ _, TBuiltin _ _) -> - throwError "Cannot unify builtin functions" + throwError $ ErrorCall "Cannot unify builtin functions" _ | compareTypes x y == LT -> go xs (y:ys) | compareTypes x y == GT -> go (x:xs) ys | otherwise -> error "impossible" @@ -227,7 +227,7 @@ unify context (Symbolic x) (Symbolic y) = do then do -- x' <- renderSymbolic (Symbolic x) -- y' <- renderSymbolic (Symbolic y) - throwError "Cannot unify " + throwError $ ErrorCall "Cannot unify " -- ++ show x' ++ " with " ++ show y' -- ++ " in context: " ++ show context else do @@ -296,7 +296,7 @@ instance MonadLint e m => MonadEval (Symbolic m) m where pushWeakScope ?? body $ force s $ unpackSymbolic >=> \case NMany [TSet (Just s')] -> return s' NMany [TSet Nothing] -> error "NYI: with unknown" - _ -> throwError "scope must be a set in with statement" + _ -> throwError $ ErrorCall "scope must be a set in with statement" evalIf cond t f = do t' <- t @@ -362,7 +362,8 @@ lintApp :: forall e m. MonadLint e m => NExprF () -> Symbolic m -> m (Symbolic m) -> m (HashMap VarName (Symbolic m), Symbolic m) lintApp context fun arg = unpackSymbolic fun >>= \case - NAny -> throwError "Cannot apply something not known to be a function" + NAny -> throwError $ ErrorCall + "Cannot apply something not known to be a function" NMany xs -> do (args:_, ys) <- fmap unzip $ forM xs $ \case TClosure _params _f -> arg >>= unpackSymbolic >>= \case @@ -372,10 +373,10 @@ lintApp context fun arg = unpackSymbolic fun >>= \case NMany [TSet (Just _)] -> do error "NYI" - NMany _ -> throwError "NYI: lintApp NMany not set" - TBuiltin _ _f -> throwError "NYI: lintApp builtin" - TSet _m -> throwError "NYI: lintApp Set" - _x -> throwError "Attempt to call non-function" + NMany _ -> throwError $ ErrorCall "NYI: lintApp NMany not set" + TBuiltin _ _f -> throwError $ ErrorCall "NYI: lintApp builtin" + TSet _m -> throwError $ ErrorCall "NYI: lintApp Set" + _x -> throwError $ ErrorCall "Attempt to call non-function" y <- everyPossible (args,) <$> foldM (unify context) y ys diff --git a/src/Nix/Normal.hs b/src/Nix/Normal.hs index d6314cf0..a8e083c5 100644 --- a/src/Nix/Normal.hs +++ b/src/Nix/Normal.hs @@ -27,7 +27,7 @@ import Nix.Value newtype NormalLoop m = NormalLoop (NValue m) deriving Show -instance Typeable m => Frame (NormalLoop m) +instance Typeable m => Exception (NormalLoop m) normalFormBy :: forall e m. (Framed e m, MonadVar m, Typeable m) diff --git a/src/Nix/Render/Frame.hs b/src/Nix/Render/Frame.hs index 4e940d7e..8e4148bd 100644 --- a/src/Nix/Render/Frame.hs +++ b/src/Nix/Render/Frame.hs @@ -61,7 +61,7 @@ renderFrames (x:xs) = do framePos :: forall v (m :: * -> *). (Typeable m, Typeable v) => NixFrame -> Maybe SourcePos framePos (NixFrame _ f) - | Just (e :: EvalFrame m v) <- fromFrame f = case e of + | Just (e :: EvalFrame m v) <- fromException f = case e of EvaluatingExpr _ (Fix (Compose (Ann (SrcSpan beg _) _))) -> Just beg _ -> Nothing @@ -72,14 +72,13 @@ renderFrame :: forall v e m. MonadFile m, Typeable m, Typeable v) => NixFrame -> m [Doc] renderFrame (NixFrame level f) - | Just (e :: EvalFrame m v) <- fromFrame f = renderEvalFrame level e - | Just (e :: ThunkLoop) <- fromFrame f = renderThunkLoop level e - | Just (e :: ValueFrame m) <- fromFrame f = renderValueFrame level e - | Just (_ :: NormalLoop m) <- fromFrame f = + | Just (e :: EvalFrame m v) <- fromException f = renderEvalFrame level e + | Just (e :: ThunkLoop) <- fromException f = renderThunkLoop level e + | Just (e :: ValueFrame m) <- fromException f = renderValueFrame level e + | Just (_ :: NormalLoop m) <- fromException f = pure [text "<>"] - | Just (e :: ExecFrame m) <- fromFrame f = renderExecFrame level e - | Just (e :: String) <- fromFrame f = pure [text e] - | Just (e :: Doc) <- fromFrame f = pure [e] + | Just (e :: ExecFrame m) <- fromException f = renderExecFrame level e + | Just (e :: ErrorCall) <- fromException f = pure [text (show e)] | otherwise = error $ "Unrecognized frame: " ++ show f wrapExpr :: NExprF r -> NExpr diff --git a/src/Nix/Thunk.hs b/src/Nix/Thunk.hs index 9160f0a5..c601fe11 100644 --- a/src/Nix/Thunk.hs +++ b/src/Nix/Thunk.hs @@ -15,7 +15,9 @@ module Nix.Thunk where -import Nix.Frames +import Control.Exception +import Control.Monad.Catch +import Data.Typeable #if ENABLE_TRACING import Data.IORef @@ -49,7 +51,7 @@ data Thunk m v newtype ThunkLoop = ThunkLoop (Maybe Int) deriving (Show, Typeable) -instance Frame ThunkLoop +instance Exception ThunkLoop valueRef :: v -> Thunk m v valueRef = Value @@ -64,7 +66,7 @@ buildThunk action = #endif <$> newVar False <*> newVar (Deferred action) -forceThunk :: (Framed e m, MonadVar m) => Thunk m v -> (v -> m a) -> m a +forceThunk :: (MonadVar m, MonadThrow m) => Thunk m v -> (v -> m a) -> m a forceThunk (Value ref) k = k ref #if ENABLE_TRACING forceThunk (Thunk n active ref) k = do @@ -79,9 +81,9 @@ forceThunk (Thunk _ active ref) k = do if nowActive then #if ENABLE_TRACING - throwError $ ThunkLoop (Just n) + throwM $ ThunkLoop (Just n) #else - throwError $ ThunkLoop Nothing + throwM $ ThunkLoop Nothing #endif else do #if ENABLE_TRACING @@ -92,7 +94,7 @@ forceThunk (Thunk _ active ref) k = do _ <- atomicModifyVar active (False,) k v -forceEffects :: (Framed e m, MonadVar m) => Thunk m v -> (v -> m a) -> m a +forceEffects :: MonadVar m => Thunk m v -> (v -> m a) -> m a forceEffects (Value ref) k = k ref forceEffects (Thunk _ active ref) k = do nowActive <- atomicModifyVar active (True,) diff --git a/src/Nix/Value.hs b/src/Nix/Value.hs index 373f20b4..d2dd3c77 100644 --- a/src/Nix/Value.hs +++ b/src/Nix/Value.hs @@ -182,8 +182,7 @@ instance Ord (NValue m) where NVPath x <= NVPath y = x < y _ <= _ = False -checkComparable :: (Framed e m, MonadThrow m, Typeable m) - => NValue m -> NValue m -> m () +checkComparable :: (Framed e m, Typeable m) => NValue m -> NValue m -> m () checkComparable x y = case (x, y) of (NVConstant (NFloat _), NVConstant (NInt _)) -> pure () (NVConstant (NInt _), NVConstant (NFloat _)) -> pure () @@ -327,4 +326,4 @@ data ValueFrame m | Expectation ValueType (NValue m) deriving (Show, Typeable) -instance Typeable m => Frame (ValueFrame m) +instance Typeable m => Exception (ValueFrame m) From 18063e5acd87376ec4fd848c7b5977173aa9c2a2 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 1 May 2018 20:34:48 -0400 Subject: [PATCH 2/6] Importing Control.Monad.ST.Unsafe was not needed in Lint.hs --- src/Nix/Lint.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Nix/Lint.hs b/src/Nix/Lint.hs index 90276c83..4b9ddfc5 100644 --- a/src/Nix/Lint.hs +++ b/src/Nix/Lint.hs @@ -29,7 +29,6 @@ import Control.Monad.Catch import Control.Monad.Fix import Control.Monad.Reader (MonadReader) import Control.Monad.ST -import Control.Monad.ST.Unsafe import Control.Monad.Trans.Reader -- import qualified Data.ByteString as BS import Data.Coerce @@ -401,7 +400,7 @@ instance MonadVar (Lint s) where -- readFile x = Lint $ ReaderT $ \_ -> unsafeIOToST $ BS.readFile x instance MonadThrow (Lint s) where - throwM e = Lint $ ReaderT $ \_ -> unsafeIOToST $ throw e + throwM e = Lint $ ReaderT $ \_ -> throw e runLintM :: Options -> Lint s a -> ST s a runLintM opts = flip runReaderT (newContext opts) . runLint From 9b02ad780f7afa329b758aca9571d48feb3792b2 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 1 May 2018 20:35:01 -0400 Subject: [PATCH 3/6] Pretty print type errors a little better (but more work needed) --- main/Main.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/main/Main.hs b/main/Main.hs index 37f34809..8d73375d 100644 --- a/main/Main.hs +++ b/main/Main.hs @@ -73,7 +73,7 @@ main = do when (check opts) $ do case HM.inferTop Env.empty [("it", stripAnnotation expr)] of Left err -> - errorWithoutStackTrace $ "Type error: " ++ show err + errorWithoutStackTrace $ "Type error: " ++ PS.ppShow err Right ty -> liftIO $ putStrLn $ "Type of expression: " ++ PS.ppShow ty From ee8ba02dfd8f2c34116d519ae05af064984b7a9a Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 1 May 2018 20:35:13 -0400 Subject: [PATCH 4/6] Much more work on type inference; report multiple possible types This is needed because of a function like this: x: y: x + y This is polymorphic, but over exactly four possibilities: int -> int int -> float float -> int float -> float The "type" is really the combination of the four, since we don't yet have a mechanism like type classes, which could have rendered this as a single type: (Num a, Num b) => (x :: a): (y :: b): x + y Going this route will require that we manage an implicit type classes hierarchy, and perform unification on constraints as well as types. In the interim, I just lifted the unification algorithm into the LogicT monad, and use back-tracking search to find all the possible types an expression could be. The main problem with using LogicT, however, is that there are many types it *couldn't* be, and in the case of a unification failure, it not yet clear what the type should have been. For example: "foo" + 2 Should the string have been a float or an integer or a path? Or should the integer have been a string? So for now we report all the possibilities, since it's not obvious which part of the expression is in error: hnix: Type error: TypeInferenceErrors [ UnificationFail (TCon "integer") (TCon "string") , UnificationFail (TCon "string") (TCon "path") , UnificationFail (TCon "string") (TCon "float") , UnificationFail (TCon "string") (TCon "integer") ] This is a case where enumerating types rather than trying to make them compact using type classes might actually be an improvement, since the errors here would have been only slightly less numerous: string != Num a => a string != path integer != string Clearly a better reporting mechanism is needed to clarify these problems. I can imagine that in an IDE, there would be a squiggly under both sides of the expression, each suggesting the type that was expected for that argument under the assumption that the other argument (the one not be inspected) was the correct one. --- hnix.cabal | 3 +- main/Main.hs | 13 +- package.yaml | 1 + src/Nix/Type/Env.hs | 17 +-- src/Nix/Type/Infer.hs | 292 ++++++++++++++++++++++++++---------------- src/Nix/Type/Type.hs | 13 +- 6 files changed, 208 insertions(+), 131 deletions(-) diff --git a/hnix.cabal b/hnix.cabal index e88883fc..ae62e739 100644 --- a/hnix.cabal +++ b/hnix.cabal @@ -2,7 +2,7 @@ -- -- see: https://github.com/sol/hpack -- --- hash: 07cd6a1b7913ff6635f99b4d896cdcbd096091580710fe2b350ebd5cedc52802 +-- hash: 495fbcc0ec91c76bd2a6f9a571bca3014f7dd68489dc137eb17528a4dfde7a00 name: hnix version: 0.5.0 @@ -101,6 +101,7 @@ library , filepath , hashable , haskeline + , logict , megaparsec , monadlist , mtl diff --git a/main/Main.hs b/main/Main.hs index 8d73375d..443a3cf1 100644 --- a/main/Main.hs +++ b/main/Main.hs @@ -12,11 +12,13 @@ import qualified Control.Exception as Exc import Control.Monad import Control.Monad.Catch import Control.Monad.IO.Class -import Control.Monad.ST +-- import Control.Monad.ST import qualified Data.Aeson.Encoding as A import qualified Data.Aeson.Text as A import qualified Data.HashMap.Lazy as M +import qualified Data.Map as Map import Data.List (sortOn) +import Data.Maybe (fromJust) import qualified Data.Text as Text import qualified Data.Text.IO as Text import qualified Data.Text.Lazy.Encoding as TL @@ -24,7 +26,7 @@ import qualified Data.Text.Lazy.IO as TL import Nix import Nix.Convert import qualified Nix.Eval as Eval -import Nix.Lint +-- import Nix.Lint import qualified Nix.Type.Env as Env import qualified Nix.Type.Infer as HM import Nix.Utils @@ -75,10 +77,11 @@ main = do Left err -> errorWithoutStackTrace $ "Type error: " ++ PS.ppShow err Right ty -> - liftIO $ putStrLn $ "Type of expression: " ++ PS.ppShow ty + liftIO $ putStrLn $ "Type of expression: " + ++ PS.ppShow (fromJust (Map.lookup "it" (Env.types ty))) - liftIO $ putStrLn $ runST $ - runLintM opts . renderSymbolic =<< lint opts expr + -- liftIO $ putStrLn $ runST $ + -- runLintM opts . renderSymbolic =<< lint opts expr catch (process opts mpath expr) $ \case NixException frames -> diff --git a/package.yaml b/package.yaml index b29d5186..c0797c5b 100644 --- a/package.yaml +++ b/package.yaml @@ -74,6 +74,7 @@ library: - directory - hashable - haskeline + - logict - megaparsec - monadlist - pretty-show diff --git a/src/Nix/Type/Env.hs b/src/Nix/Type/Env.hs index d4cf918b..bb05077c 100644 --- a/src/Nix/Type/Env.hs +++ b/src/Nix/Type/Env.hs @@ -25,22 +25,23 @@ import Data.Semigroup -- Typing Environment ------------------------------------------------------------------------------- -newtype Env = TypeEnv { types :: Map.Map Name Scheme } +newtype Env = TypeEnv { types :: Map.Map Name [Scheme] } deriving (Eq, Show) empty :: Env empty = TypeEnv Map.empty -extend :: Env -> (Name, Scheme) -> Env +extend :: Env -> (Name, [Scheme]) -> Env extend env (x, s) = env { types = Map.insert x s (types env) } remove :: Env -> Name -> Env remove (TypeEnv env) var = TypeEnv (Map.delete var env) -extends :: Env -> [(Name, Scheme)] -> Env -extends env xs = env { types = Map.union (Map.fromList xs) (types env) } +extends :: Env -> [(Name, [Scheme])] -> Env +extends env xs = + env { types = Map.union (Map.fromList xs) (types env) } -lookup :: Name -> Env -> Maybe Scheme +lookup :: Name -> Env -> Maybe [Scheme] lookup key (TypeEnv tys) = Map.lookup key tys merge :: Env -> Env -> Env @@ -50,15 +51,15 @@ mergeEnvs :: [Env] -> Env mergeEnvs = foldl' merge empty singleton :: Name -> Scheme -> Env -singleton x y = TypeEnv (Map.singleton x y) +singleton x y = TypeEnv (Map.singleton x [y]) keys :: Env -> [Name] keys (TypeEnv env) = Map.keys env -fromList :: [(Name, Scheme)] -> Env +fromList :: [(Name, [Scheme])] -> Env fromList xs = TypeEnv (Map.fromList xs) -toList :: Env -> [(Name, Scheme)] +toList :: Env -> [(Name, [Scheme])] toList (TypeEnv env) = Map.toList env instance Semigroup Env where diff --git a/src/Nix/Type/Infer.hs b/src/Nix/Type/Infer.hs index e11d7e5c..3d48c640 100644 --- a/src/Nix/Type/Infer.hs +++ b/src/Nix/Type/Infer.hs @@ -5,7 +5,10 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} @@ -13,17 +16,37 @@ module Nix.Type.Infer ( Constraint(..), TypeError(..), + InferError(..), Subst(..), inferTop ) where +import Control.Applicative +import Control.Arrow +import Control.Monad.Catch +import Control.Monad.Except +import Control.Monad.Logic +import Control.Monad.Reader +import Control.Monad.ST +import Control.Monad.State +import Data.Coerce +import Data.Fix +import Data.Foldable +import qualified Data.HashMap.Lazy as M +import Data.List (delete, find, nub, intersect, (\\)) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Maybe (fromJust) +import Data.STRef +import Data.Semigroup +import qualified Data.Set as Set +import Data.Text (Text) import Nix.Atoms import Nix.Convert import Nix.Eval (MonadEval(..)) import qualified Nix.Eval as Eval import Nix.Expr.Types import Nix.Expr.Types.Annotated -import Nix.Frames (Frame) import Nix.Scope import Nix.Thunk import qualified Nix.Type.Assumption as As @@ -32,38 +55,19 @@ import qualified Nix.Type.Env as Env import Nix.Type.Type import Nix.Utils -import Control.Applicative -import Control.Arrow -import Control.Monad.Except -import Control.Monad.Reader -import Control.Monad.State - -import Data.Fix -import Data.Foldable -import Data.List (delete, find, nub, intersect, (\\)) -import Data.Map (Map) -import qualified Data.Map as Map -import Data.Maybe (fromJust) -import Data.Semigroup -import qualified Data.HashMap.Lazy as M -import qualified Data.Set as Set -import Data.Text (Text) - ------------------------------------------------------------------------------- -- Classes ------------------------------------------------------------------------------- -- | Inference monad -newtype Infer a = Infer +newtype Infer s a = Infer { getInfer :: - ReaderT (Set.Set TVar, Scopes Infer Judgment) -- Monomorphic set - (StateT InferState -- Inference state - (Except TypeError)) -- Inference errors - a -- Result + ReaderT (Set.Set TVar, Scopes (Infer s) (JThunk s)) + (StateT InferState (ExceptT InferError (ST s))) a } deriving (Functor, Applicative, Alternative, Monad, MonadPlus, MonadFix, - MonadReader (Set.Set TVar, Scopes Infer Judgment), - MonadState InferState, MonadError TypeError) + MonadReader (Set.Set TVar, Scopes (Infer s) (JThunk s)), + MonadState InferState, MonadError InferError) -- | Inference state newtype InferState = InferState { count :: Int } @@ -94,8 +98,7 @@ instance Substitutable TVar where instance Substitutable Type where apply _ (TCon a) = TCon a - apply s (TSet a) = TSet (M.map (apply s) a) - apply s (TSubSet a) = TSubSet (M.map (apply s) a) + apply s (TSet b a) = TSet b (M.map (apply s) a) apply s (TList a) = TList (map (apply s) a) apply (Subst s) t@(TVar a) = Map.findWithDefault t a s apply s (t1 `TArr` t2) = apply s t1 `TArr` apply s t2 @@ -123,8 +126,7 @@ class FreeTypeVars a where instance FreeTypeVars Type where ftv TCon{} = Set.empty ftv (TVar a) = Set.singleton a - ftv (TSet a) = Set.unions (map ftv (M.elems a)) - ftv (TSubSet a) = Set.unions (map ftv (M.elems a)) + ftv (TSet _ a) = Set.unions (map ftv (M.elems a)) ftv (TList a) = Set.unions (map ftv a) ftv (t1 `TArr` t2) = ftv t1 `Set.union` ftv t2 @@ -153,23 +155,30 @@ instance ActiveTypeVars Constraint where instance ActiveTypeVars a => ActiveTypeVars [a] where atv = foldr (Set.union . atv) Set.empty - data TypeError = UnificationFail Type Type | InfiniteType TVar Type - | UnboundVariable Text + | UnboundVariables [Text] | Ambigious [Constraint] | UnificationMismatch [Type] [Type] - | forall s. Frame s => EvaluationError s - | InferenceAborted + deriving (Eq, Show) -deriving instance Show TypeError +data InferError + = TypeInferenceErrors [TypeError] + | TypeInferenceAborted + | forall s. Exception s => EvaluationError s -instance Semigroup TypeError where +typeError :: MonadError InferError m => TypeError -> m () +typeError err = throwError $ TypeInferenceErrors [err] + +deriving instance Show InferError +instance Exception InferError + +instance Semigroup InferError where x <> _ = x -instance Monoid TypeError where - mempty = InferenceAborted +instance Monoid InferError where + mempty = TypeInferenceAborted mappend = (<>) ------------------------------------------------------------------------------- @@ -177,42 +186,57 @@ instance Monoid TypeError where ------------------------------------------------------------------------------- -- | Run the inference monad -runInfer :: Infer a -> Either TypeError a -runInfer m = - runExcept $ evalStateT (runReaderT (getInfer m) (Set.empty, emptyScopes)) initInfer +runInfer' :: Infer s a -> ST s (Either InferError a) +runInfer' = runExceptT + . (`evalStateT` initInfer) + . (`runReaderT` (Set.empty, emptyScopes)) + . getInfer -inferType :: Env -> NExpr -> Infer (Subst, Type) +runInfer :: (forall s. Infer s a) -> Either InferError a +runInfer m = runST (runInfer' m) + +inferType :: Env -> NExpr -> Infer s [(Subst, Type)] inferType env ex = do Judgment as cs t <- infer ex - let unbounds = Set.fromList (As.keys as) `Set.difference` Set.fromList (Env.keys env) - unless (Set.null unbounds) $ throwError $ UnboundVariable (Set.findMin unbounds) - let cs' = [ExpInstConst t s | (x, s) <- Env.toList env, t <- As.lookup x as] - subst <- solve (cs ++ cs') - return (subst, apply subst t) + let unbounds = Set.fromList (As.keys as) `Set.difference` + Set.fromList (Env.keys env) + unless (Set.null unbounds) $ + typeError $ UnboundVariables (nub (Set.toList unbounds)) + let cs' = [ ExpInstConst t s + | (x, ss) <- Env.toList env + , s <- ss + , t <- As.lookup x as] + inferState <- get + let eres = (`evalState` inferState) $ runSolver $ do + subst <- solve (cs ++ cs') + return (subst, subst `apply` t) + case eres of + Left errs -> throwError $ TypeInferenceErrors errs + Right xs -> pure xs -- | Solve for the toplevel type of an expression in a given environment -inferExpr :: Env -> NExpr -> Either TypeError Scheme +inferExpr :: Env -> NExpr -> Either InferError [Scheme] inferExpr env ex = case runInfer (inferType env ex) of Left err -> Left err - Right (subst, ty) -> Right $ closeOver $ apply subst ty + Right xs -> Right $ map (\(subst, ty) -> closeOver (subst `apply` ty)) xs -- | Canonicalize and return the polymorphic toplevel type. closeOver :: Type -> Scheme closeOver = normalize . generalize Set.empty -extendMSet :: TVar -> Infer a -> Infer a +extendMSet :: TVar -> Infer s a -> Infer s a extendMSet x = Infer . local (first (Set.insert x)) . getInfer letters :: [String] letters = [1..] >>= flip replicateM ['a'..'z'] -fresh :: Infer Type -fresh = Infer $ do +fresh :: MonadState InferState m => m Type +fresh = do s <- get put s{count = count s + 1} return $ TVar $ TV (letters !! count s) -instantiate :: Scheme -> Infer Type +instantiate :: MonadState InferState m => Scheme -> m Type instantiate (Forall as t) = do as' <- mapM (const fresh) as let s = Subst $ Map.fromList $ zip as as' @@ -282,12 +306,28 @@ binops u1 = \case , typeFun [typeFloat, typeInt, typeFloat] ] ] -instance MonadThunk Judgment Judgment Infer where - thunk = id - force v f = f v - value = id +instance MonadVar (Infer s) where + type Var (Infer s) = STRef s -instance MonadEval Judgment Infer where + newVar x = Infer $ lift $ lift $ lift $ newSTRef x + readVar x = Infer $ lift $ lift $ lift $ readSTRef x + writeVar x y = Infer $ lift $ lift $ lift $ writeSTRef x y + atomicModifyVar x f = Infer $ lift $ lift $ lift $ do + res <- snd . f <$> readSTRef x + _ <- modifySTRef x (fst . f) + return res + +newtype JThunk s = JThunk (Thunk (Infer s) (Judgment s)) + +instance MonadThrow (Infer s) where + throwM = throwError . EvaluationError + +instance MonadThunk (Judgment s) (JThunk s) (Infer s) where + thunk = fmap JThunk . buildThunk + force = forceThunk . coerce + value = JThunk . valueRef + +instance MonadEval (Judgment s) (Infer s) where freeVariable var = do tv <- fresh return $ Judgment (As.singleton var tv) [] tv @@ -295,7 +335,7 @@ instance MonadEval Judgment Infer where evaledSym _ = pure evalCurPos = - return $ Judgment As.empty [] $ TSet $ M.fromList + return $ Judgment As.empty [] $ TSet False $ M.fromList [ ("file", typePath) , ("line", typeInt) , ("col", typeInt) ] @@ -363,45 +403,50 @@ instance MonadEval Judgment Infer where evalError = throwError . EvaluationError -data Judgment = Judgment +data Judgment s = Judgment { assumptions :: As.Assumption , typeConstraints :: [Constraint] , inferredType :: Type } deriving Show -instance FromValue (Text, DList Text) Infer Judgment where +instance FromValue (Text, DList Text) (Infer s) (Judgment s) where fromValueMay _ = return Nothing fromValue _ = error "Unused" -instance FromValue (AttrSet Judgment, AttrSet SourcePos) Infer Judgment where +instance FromValue (AttrSet (JThunk s), AttrSet SourcePos) (Infer s) (Judgment s) where -- jww (2018-04-30): How can we do this? TSet doesn't record enough information - fromValueMay (Judgment _ _ (TSet xs)) = - pure $ Just (M.mapWithKey (\k v -> Judgment (As.singleton k v) [] v) xs, M.empty) + fromValueMay (Judgment _ _ (TSet _ xs)) = do + let sing _ = Judgment As.empty [] + pure $ Just (M.mapWithKey (\k v -> value (sing k v)) xs, M.empty) fromValueMay _ = pure Nothing fromValue = fromValueMay >=> \case Just v -> pure v Nothing -> pure (M.empty, M.empty) -instance ToValue (AttrSet Judgment, AttrSet SourcePos) Infer Judgment where - toValue (xs, _) = pure $ Judgment - (foldr (As.merge . assumptions) As.empty xs) - (concatMap typeConstraints xs) - (TSet (M.map inferredType xs)) +instance ToValue (AttrSet (JThunk s), AttrSet SourcePos) (Infer s) (Judgment s) where + toValue (xs, _) = Judgment + <$> foldrM go As.empty xs + <*> (concat <$> traverse (`force` (pure . typeConstraints)) xs) + <*> (TSet True <$> traverse (`force` (pure . inferredType)) xs) + where + go x rest = force x $ \x' -> pure $ As.merge (assumptions x') rest -instance ToValue [Judgment] Infer Judgment where - toValue xs = pure $ Judgment - (foldr (As.merge . assumptions) As.empty xs) - (concatMap typeConstraints xs) - (TList (map inferredType xs)) +instance ToValue [JThunk s] (Infer s) (Judgment s) where + toValue xs = Judgment + <$> foldrM go As.empty xs + <*> (concat <$> traverse (`force` (pure . typeConstraints)) xs) + <*> (TList <$> traverse (`force` (pure . inferredType)) xs) + where + go x rest = force x $ \x' -> pure $ As.merge (assumptions x') rest -instance ToValue Bool Infer Judgment where +instance ToValue Bool (Infer s) (Judgment s) where toValue _ = pure $ Judgment As.empty [] typeBool -infer :: NExpr -> Infer Judgment +infer :: NExpr -> Infer s (Judgment s) infer = cata Eval.eval -inferTop :: Env -> [(Text, NExpr)] -> Either TypeError Env +inferTop :: Env -> [(Text, NExpr)] -> Either InferError Env inferTop env [] = Right env inferTop env ((name, ex):xs) = case inferExpr env ex of Left err -> Left err @@ -415,14 +460,12 @@ normalize (Forall _ body) = Forall (map snd ord) (normtype body) fv (TVar a) = [a] fv (TArr a b) = fv a ++ fv b fv (TCon _) = [] - fv (TSet a) = concatMap fv (M.elems a) - fv (TSubSet a) = concatMap fv (M.elems a) + fv (TSet _ a) = concatMap fv (M.elems a) fv (TList a) = concatMap fv a normtype (TArr a b) = TArr (normtype a) (normtype b) normtype (TCon a) = TCon a - normtype (TSet a) = TSet (M.map normtype a) - normtype (TSubSet a) = TSubSet (M.map normtype a) + normtype (TSet b a) = TSet b (M.map normtype a) normtype (TList a) = TList (map normtype a) normtype (TVar a) = case Prelude.lookup a ord of @@ -433,15 +476,34 @@ normalize (Forall _ body) = Forall (map snd ord) (normtype body) -- Constraint Solver ------------------------------------------------------------------------------- +newtype Solver m a = Solver (LogicT (StateT [TypeError] m) a) + deriving (Functor, Applicative, Alternative, Monad, MonadPlus, + MonadLogic, MonadState [TypeError]) + +instance MonadTrans Solver where + lift = Solver . lift . lift + +instance Monad m => MonadError TypeError (Solver m) where + throwError err = Solver $ lift (modify (err:)) >> mzero + catchError _ _ = error "This is never used" + +runSolver :: Monad m => Solver m a -> m (Either [TypeError] [a]) +runSolver (Solver s) = do + res <- runStateT (observeAllT s) [] + pure $ case res of + (x:xs, _) -> Right (x:xs) + (_, es) -> Left (nub es) + -- | The empty substitution emptySubst :: Subst emptySubst = mempty -- | Compose substitutions compose :: Subst -> Subst -> Subst -(Subst s1) `compose` (Subst s2) = Subst $ Map.map (apply (Subst s1)) s2 `Map.union` s1 +Subst s1 `compose` Subst s2 = + Subst $ Map.map (apply (Subst s1)) s2 `Map.union` s1 -unifyMany :: [Type] -> [Type] -> Infer Subst +unifyMany :: Monad m => [Type] -> [Type] -> Solver m Subst unifyMany [] [] = return emptySubst unifyMany (t1 : ts1) (t2 : ts2) = do su1 <- unifies t1 t2 @@ -449,21 +511,34 @@ unifyMany (t1 : ts1) (t2 : ts2) = return (su2 `compose` su1) unifyMany t1 t2 = throwError $ UnificationMismatch t1 t2 -unifies :: Type -> Type -> Infer Subst +allSameType :: [Type] -> Bool +allSameType [] = True +allSameType [_] = True +allSameType (x:y:ys) = x == y && allSameType (y:ys) + +unifies :: Monad m => Type -> Type -> Solver m Subst unifies t1 t2 | t1 == t2 = return emptySubst unifies (TVar v) t = v `bind` t unifies t (TVar v) = v `bind` t -unifies (TList _) (TList _) = return emptySubst -unifies (TSet b) (TSubSet s) +unifies (TList xs) (TList ys) + | allSameType xs && allSameType ys = case (xs, ys) of + (x:_, y:_) -> unifies x y + _ -> return emptySubst + | length xs == length ys = unifyMany xs ys +-- We assume that lists of different lengths containing various types cannot +-- be unified. +unifies t1@(TList _) t2@(TList _) = throwError $ UnificationFail t1 t2 +unifies (TSet True _) (TSet True _) = return emptySubst +unifies (TSet False b) (TSet True s) | M.keys b `intersect` M.keys s == M.keys s = return emptySubst -unifies (TSubSet s) (TSet b) - | M.keys b `intersect` M.keys s == M.keys s = return emptySubst -unifies (TSet s) (TSet b) +unifies (TSet True s) (TSet False b) + | M.keys b `intersect` M.keys s == M.keys b = return emptySubst +unifies (TSet False s) (TSet False b) | null (M.keys b \\ M.keys s) = return emptySubst unifies (TArr t1 t2) (TArr t3 t4) = unifyMany [t1, t2] [t3, t4] unifies t1 t2 = throwError $ UnificationFail t1 t2 -bind :: TVar -> Type -> Infer Subst +bind :: Monad m => TVar -> Type -> Solver m Subst bind a t | t == TVar a = return emptySubst | occursCheck a t = throwError $ InfiniteType a t | otherwise = return (Subst $ Map.singleton a t) @@ -475,36 +550,33 @@ nextSolvable :: [Constraint] -> (Constraint, [Constraint]) nextSolvable xs = fromJust (find solvable (chooseOne xs)) where chooseOne xs = [(x, ys) | x <- xs, let ys = delete x xs] + solvable (EqConst{}, _) = True solvable (EqConstOneOf{}, _) = True solvable (ExpInstConst{}, _) = True solvable (ImpInstConst _t1 ms t2, cs) = Set.null ((ftv t2 `Set.difference` ms) `Set.intersection` atv cs) -solve :: [Constraint] -> Infer Subst +considering :: [a] -> Solver m a +considering xs = Solver $ LogicT $ \c n -> foldr c n xs + +solve :: MonadState InferState m => [Constraint] -> Solver m Subst solve [] = return emptySubst solve cs = solve' (nextSolvable cs) + where + solve' (EqConst t1 t2, cs) = simple t1 t2 cs -solve' :: (Constraint, [Constraint]) -> Infer Subst -solve' (EqConst t1 t2, cs) = do - su1 <- unifies t1 t2 - su2 <- solve (apply su1 cs) - return (su2 `compose` su1) + solve' (EqConstOneOf t1 t2s, cs) = + considering t2s >>- simple t1 ?? cs -solve' (EqConstOneOf t1 t2, cs) = do - -- jww (2018-04-30): Instead of picking the first that matches, collect all - -- that match into a 'TVariant [Type]' type, so that we can report that a - -- function like 'x: y: x + y' has type: forall a b. a one of integer, - -- float, string, b the same as a, or compatible, result is determined by - -- the finally decided type of the function (in this case, one of int, - -- float, string or path, based on the types of a and b). - su1 <- asum (map (unifies t1) t2) - su2 <- solve (apply su1 cs) - return (su2 `compose` su1) + solve' (ImpInstConst t1 ms t2, cs) = + solve (ExpInstConst t1 (generalize ms t2) : cs) -solve' (ImpInstConst t1 ms t2, cs) = - solve (ExpInstConst t1 (generalize ms t2) : cs) + solve' (ExpInstConst t s, cs) = do + s' <- lift $ instantiate s + solve (EqConst t s' : cs) -solve' (ExpInstConst t s, cs) = do - s' <- instantiate s - solve (EqConst t s' : cs) + simple t1 t2 cs = + unifies t1 t2 >>- \su1 -> + solve (apply su1 cs) >>- \su2 -> + return (su2 `compose` su1) diff --git a/src/Nix/Type/Type.hs b/src/Nix/Type/Type.hs index 839d48e5..1833f211 100644 --- a/src/Nix/Type/Type.hs +++ b/src/Nix/Type/Type.hs @@ -8,12 +8,11 @@ newtype TVar = TV String deriving (Show, Eq, Ord) data Type - = TVar TVar -- type variable - | TCon String -- known type - | TSet (AttrSet Type) -- heterogenous map: { a = b; } - | TSubSet (AttrSet Type) -- subset of heterogenous map: { a = b; ... } - | TList [Type] -- heterogenous list - | TArr Type Type -- type -> type + = TVar TVar -- type variable + | TCon String -- known type + | TSet Bool (AttrSet Type) -- heterogenous map, bool if variadic + | TList [Type] -- heterogenous list + | TArr Type Type -- type -> type deriving (Show, Eq, Ord) data Scheme = Forall [TVar] Type -- forall a b. a -> b @@ -21,7 +20,7 @@ data Scheme = Forall [TVar] Type -- forall a b. a -> b -- This models a set that unifies with any other set. typeSet :: Type -typeSet = TSubSet M.empty +typeSet = TSet True M.empty typeList :: Type typeList = TList [] From 49e71222c387beed075d41cc64df3e98821957ed Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 1 May 2018 21:04:10 -0400 Subject: [PATCH 5/6] Instead of EqConstOneOf, use TMany which is more fundamental This allows both multiple function types, or a function that might return one of many possible values, for example. --- src/Nix/Type/Infer.hs | 92 ++++++++++++++++++++----------------------- src/Nix/Type/Type.hs | 1 + 2 files changed, 44 insertions(+), 49 deletions(-) diff --git a/src/Nix/Type/Infer.hs b/src/Nix/Type/Infer.hs index 3d48c640..f78e2cd8 100644 --- a/src/Nix/Type/Infer.hs +++ b/src/Nix/Type/Infer.hs @@ -78,9 +78,6 @@ initInfer = InferState { count = 0 } data Constraint = EqConst Type Type - | EqConstOneOf Type [Type] - -- ^ The first type must unify with the second. For example, integer - -- could unify with integer, or a type variable. | ExpInstConst Type Scheme | ImpInstConst Type (Set.Set TVar) Type deriving (Show, Eq, Ord) @@ -102,6 +99,7 @@ instance Substitutable Type where apply s (TList a) = TList (map (apply s) a) apply (Subst s) t@(TVar a) = Map.findWithDefault t a s apply s (t1 `TArr` t2) = apply s t1 `TArr` apply s t2 + apply s (TMany ts) = TMany (map (apply s) ts) instance Substitutable Scheme where apply (Subst s) (Forall as t) = Forall as $ apply s' t @@ -109,7 +107,6 @@ instance Substitutable Scheme where instance Substitutable Constraint where apply s (EqConst t1 t2) = EqConst (apply s t1) (apply s t2) - apply s (EqConstOneOf t1 t2) = EqConstOneOf (apply s t1) (apply s t2) apply s (ExpInstConst t sc) = ExpInstConst (apply s t) (apply s sc) apply s (ImpInstConst t1 ms t2) = ImpInstConst (apply s t1) (apply s ms) (apply s t2) @@ -129,6 +126,7 @@ instance FreeTypeVars Type where ftv (TSet _ a) = Set.unions (map ftv (M.elems a)) ftv (TList a) = Set.unions (map ftv a) ftv (t1 `TArr` t2) = ftv t1 `Set.union` ftv t2 + ftv (TMany ts) = Set.unions (map ftv ts) instance FreeTypeVars TVar where ftv = Set.singleton @@ -148,7 +146,6 @@ class ActiveTypeVars a where instance ActiveTypeVars Constraint where atv (EqConst t1 t2) = ftv t1 `Set.union` ftv t2 - atv (EqConstOneOf t1 t2) = ftv t1 `Set.union` ftv t2 atv (ImpInstConst t1 ms t2) = ftv t1 `Set.union` (ftv ms `Set.intersection` ftv t2) atv (ExpInstConst t s) = ftv t `Set.union` ftv s @@ -248,9 +245,9 @@ generalize free t = Forall as t unops :: Type -> NUnaryOp -> [Constraint] unops u1 = \case - NNot -> [ EqConst u1 ( typeFun [typeBool, typeBool] ) ] - NNeg -> [ EqConstOneOf u1 [ typeFun [typeInt, typeInt] - , typeFun [typeFloat, typeFloat] ] ] + NNot -> [ EqConst u1 (typeFun [typeBool, typeBool]) ] + NNeg -> [ EqConst u1 (TMany [ typeFun [typeInt, typeInt] + , typeFun [typeFloat, typeFloat] ]) ] binops :: Type -> NBinaryOp -> [Constraint] binops u1 = \case @@ -266,45 +263,45 @@ binops u1 = \case NLt -> inequality NLte -> inequality - NAnd -> [ EqConst u1 ( typeFun [typeBool, typeBool, typeBool]) ] - NOr -> [ EqConst u1 ( typeFun [typeBool, typeBool, typeBool]) ] - NImpl -> [ EqConst u1 ( typeFun [typeBool, typeBool, typeBool]) ] + NAnd -> [ EqConst u1 (typeFun [typeBool, typeBool, typeBool]) ] + NOr -> [ EqConst u1 (typeFun [typeBool, typeBool, typeBool]) ] + NImpl -> [ EqConst u1 (typeFun [typeBool, typeBool, typeBool]) ] - NConcat -> [ EqConstOneOf u1 [ typeFun [typeList, typeList, typeList] - , typeFun [typeList, typeNull, typeList] - , typeFun [typeNull, typeList, typeList] - ] ] + NConcat -> [ EqConst u1 (TMany [ typeFun [typeList, typeList, typeList] + , typeFun [typeList, typeNull, typeList] + , typeFun [typeNull, typeList, typeList] + ]) ] - NUpdate -> [ EqConstOneOf u1 [ typeFun [typeSet, typeSet, typeSet] - , typeFun [typeSet, typeNull, typeSet] - , typeFun [typeNull, typeSet, typeSet] - ] ] + NUpdate -> [ EqConst u1 (TMany [ typeFun [typeSet, typeSet, typeSet] + , typeFun [typeSet, typeNull, typeSet] + , typeFun [typeNull, typeSet, typeSet] + ]) ] - NPlus -> [ EqConstOneOf u1 [ typeFun [typeInt, typeInt, typeInt] - , typeFun [typeFloat, typeFloat, typeFloat] - , typeFun [typeInt, typeFloat, typeFloat] - , typeFun [typeFloat, typeInt, typeFloat] - , typeFun [typeString, typeString, typeString] - , typeFun [typePath, typePath, typePath] - , typeFun [typeString, typeString, typePath] - ] ] + NPlus -> [ EqConst u1 (TMany [ typeFun [typeInt, typeInt, typeInt] + , typeFun [typeFloat, typeFloat, typeFloat] + , typeFun [typeInt, typeFloat, typeFloat] + , typeFun [typeFloat, typeInt, typeFloat] + , typeFun [typeString, typeString, typeString] + , typeFun [typePath, typePath, typePath] + , typeFun [typeString, typeString, typePath] + ]) ] NMinus -> arithmetic NMult -> arithmetic NDiv -> arithmetic where inequality = - [ EqConstOneOf u1 [ typeFun [typeInt, typeInt, typeBool] - , typeFun [typeFloat, typeFloat, typeBool] - , typeFun [typeInt, typeFloat, typeBool] - , typeFun [typeFloat, typeInt, typeBool] - ] ] + [ EqConst u1 (TMany [ typeFun [typeInt, typeInt, typeBool] + , typeFun [typeFloat, typeFloat, typeBool] + , typeFun [typeInt, typeFloat, typeBool] + , typeFun [typeFloat, typeInt, typeBool] + ]) ] arithmetic = - [ EqConstOneOf u1 [ typeFun [typeInt, typeInt, typeInt] - , typeFun [typeFloat, typeFloat, typeFloat] - , typeFun [typeInt, typeFloat, typeFloat] - , typeFun [typeFloat, typeInt, typeFloat] - ] ] + [ EqConst u1 (TMany [ typeFun [typeInt, typeInt, typeInt] + , typeFun [typeFloat, typeFloat, typeFloat] + , typeFun [typeInt, typeFloat, typeFloat] + , typeFun [typeFloat, typeInt, typeFloat] + ]) ] instance MonadVar (Infer s) where type Var (Infer s) = STRef s @@ -399,7 +396,7 @@ instance MonadEval (Judgment s) (Infer s) where (cs ++ [EqConst t' tv | t' <- As.lookup x as]) (tv `TArr` t) - evalAbs (ParamSet _x _variadic _mname) _e = undefined + evalAbs (ParamSet p variadic mname) e = undefined evalError = throwError . EvaluationError @@ -415,7 +412,6 @@ instance FromValue (Text, DList Text) (Infer s) (Judgment s) where fromValue _ = error "Unused" instance FromValue (AttrSet (JThunk s), AttrSet SourcePos) (Infer s) (Judgment s) where - -- jww (2018-04-30): How can we do this? TSet doesn't record enough information fromValueMay (Judgment _ _ (TSet _ xs)) = do let sing _ = Judgment As.empty [] pure $ Just (M.mapWithKey (\k v -> value (sing k v)) xs, M.empty) @@ -462,11 +458,13 @@ normalize (Forall _ body) = Forall (map snd ord) (normtype body) fv (TCon _) = [] fv (TSet _ a) = concatMap fv (M.elems a) fv (TList a) = concatMap fv a + fv (TMany ts) = concatMap fv ts normtype (TArr a b) = TArr (normtype a) (normtype b) normtype (TCon a) = TCon a normtype (TSet b a) = TSet b (M.map normtype a) normtype (TList a) = TList (map normtype a) + normtype (TMany ts) = TMany (map normtype ts) normtype (TVar a) = case Prelude.lookup a ord of Just x -> TVar x @@ -536,6 +534,8 @@ unifies (TSet True s) (TSet False b) unifies (TSet False s) (TSet False b) | null (M.keys b \\ M.keys s) = return emptySubst unifies (TArr t1 t2) (TArr t3 t4) = unifyMany [t1, t2] [t3, t4] +unifies (TMany t1s) t2 = considering t1s >>- unifies ?? t2 +unifies t1 (TMany t2s) = considering t2s >>- unifies t1 unifies t1 t2 = throwError $ UnificationFail t1 t2 bind :: Monad m => TVar -> Type -> Solver m Subst @@ -552,7 +552,6 @@ nextSolvable xs = fromJust (find solvable (chooseOne xs)) chooseOne xs = [(x, ys) | x <- xs, let ys = delete x xs] solvable (EqConst{}, _) = True - solvable (EqConstOneOf{}, _) = True solvable (ExpInstConst{}, _) = True solvable (ImpInstConst _t1 ms t2, cs) = Set.null ((ftv t2 `Set.difference` ms) `Set.intersection` atv cs) @@ -564,10 +563,10 @@ solve :: MonadState InferState m => [Constraint] -> Solver m Subst solve [] = return emptySubst solve cs = solve' (nextSolvable cs) where - solve' (EqConst t1 t2, cs) = simple t1 t2 cs - - solve' (EqConstOneOf t1 t2s, cs) = - considering t2s >>- simple t1 ?? cs + solve' (EqConst t1 t2, cs) = + unifies t1 t2 >>- \su1 -> + solve (apply su1 cs) >>- \su2 -> + return (su2 `compose` su1) solve' (ImpInstConst t1 ms t2, cs) = solve (ExpInstConst t1 (generalize ms t2) : cs) @@ -575,8 +574,3 @@ solve cs = solve' (nextSolvable cs) solve' (ExpInstConst t s, cs) = do s' <- lift $ instantiate s solve (EqConst t s' : cs) - - simple t1 t2 cs = - unifies t1 t2 >>- \su1 -> - solve (apply su1 cs) >>- \su2 -> - return (su2 `compose` su1) diff --git a/src/Nix/Type/Type.hs b/src/Nix/Type/Type.hs index 1833f211..a485ee2c 100644 --- a/src/Nix/Type/Type.hs +++ b/src/Nix/Type/Type.hs @@ -13,6 +13,7 @@ data Type | TSet Bool (AttrSet Type) -- heterogenous map, bool if variadic | TList [Type] -- heterogenous list | TArr Type Type -- type -> type + | TMany [Type] -- variant type deriving (Show, Eq, Ord) data Scheme = Forall [TVar] Type -- forall a b. a -> b From 853885923020ed6b4ae294b9a1257d17133edde4 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 1 May 2018 21:50:50 -0400 Subject: [PATCH 6/6] Work on type inference for functions that take attr sets --- src/Nix/Eval.hs | 9 ++------- src/Nix/Exec.hs | 3 +-- src/Nix/Lint.hs | 5 ++--- src/Nix/Type/Infer.hs | 21 ++++++++++++++++++++- src/Nix/Value.hs | 3 +-- 5 files changed, 26 insertions(+), 15 deletions(-) diff --git a/src/Nix/Eval.hs b/src/Nix/Eval.hs index f2911971..b3605c4b 100644 --- a/src/Nix/Eval.hs +++ b/src/Nix/Eval.hs @@ -36,7 +36,6 @@ import Data.Text (Text) import qualified Data.Text as Text import Data.These import Data.Traversable (for) -import Data.Void import Nix.Atoms import Nix.Convert import Nix.Expr @@ -63,7 +62,7 @@ class (Show v, Monad m) => MonadEval v m | v -> m where evalIf :: v -> m v -> m v -> m v evalAssert :: v -> m v -> m v evalApp :: v -> m v -> m v - evalAbs :: Params Void -> (m v -> m v) -> m v + evalAbs :: Params (m v) -> (m v -> m v) -> m v {- evalSelect :: v -> NonEmpty Text -> Maybe (m v) -> m v @@ -171,14 +170,10 @@ eval (NAbs params body) = do -- we defer here so the present scope is restored when the parameters and -- body are forced during application. scope <- currentScopes @_ @t - evalAbs (clearDefaults params) $ \arg -> + evalAbs params $ \arg -> withScopes @t scope $ do args <- buildArgument params arg pushScope args body - where - clearDefaults :: Params r -> Params Void - clearDefaults (Param name) = Param name - clearDefaults (ParamSet xs b mv) = ParamSet (map (Nothing <$) xs) b mv -- | If you know that the 'scope' action will result in an 'AttrSet t', then -- this implementation may be used as an implementation for 'evalWith'. diff --git a/src/Nix/Exec.hs b/src/Nix/Exec.hs index 44858173..21e3f65e 100644 --- a/src/Nix/Exec.hs +++ b/src/Nix/Exec.hs @@ -46,7 +46,6 @@ import Data.List.Split import Data.Text (Text) import qualified Data.Text as Text import Data.Typeable -import Data.Void import Nix.Atoms import Nix.Context import Nix.Convert @@ -224,7 +223,7 @@ instance MonadNix e m => MonadEval (NValue m) m where evalAbs p b = do scope <- currentScopes span <- currentPos - pure $ nvClosureP (Provenance scope (NAbs_ span (fmap absurd p) Nothing)) p b + pure $ nvClosureP (Provenance scope (NAbs_ span (Nothing <$ p) Nothing)) (void p) b evalError = throwError diff --git a/src/Nix/Lint.hs b/src/Nix/Lint.hs index 4b9ddfc5..e90b9ed8 100644 --- a/src/Nix/Lint.hs +++ b/src/Nix/Lint.hs @@ -38,7 +38,6 @@ import Data.List import Data.STRef import Data.Text (Text) import qualified Data.Text as Text -import Data.Void import Nix.Atoms import Nix.Context import Nix.Convert @@ -65,7 +64,7 @@ data NTypeF (m :: * -> *) r | TStr | TList r | TSet (Maybe (HashMap Text r)) - | TClosure (Params Void) (m (Symbolic m) -> m (Symbolic m)) + | TClosure (Params ()) (m (Symbolic m) -> m (Symbolic m)) | TPath | TBuiltin String (SThunk m -> m (Symbolic m)) deriving Functor @@ -311,7 +310,7 @@ instance MonadLint e m => MonadEval (Symbolic m) m where pure body' evalApp = (fmap snd .) . lintApp (NBinary NApp () ()) - evalAbs params body = mkSymbolic [TClosure params body] + evalAbs params body = mkSymbolic [TClosure (void params) body] evalError = throwError diff --git a/src/Nix/Type/Infer.hs b/src/Nix/Type/Infer.hs index f78e2cd8..a27b58e1 100644 --- a/src/Nix/Type/Infer.hs +++ b/src/Nix/Type/Infer.hs @@ -396,7 +396,26 @@ instance MonadEval (Judgment s) (Infer s) where (cs ++ [EqConst t' tv | t' <- As.lookup x as]) (tv `TArr` t) - evalAbs (ParamSet p variadic mname) e = undefined + evalAbs (ParamSet ps _variadic _mname) e = do + js <- fmap concat $ forM ps $ \(name, mdef) -> case mdef of + Just _ -> pure [] + Nothing -> do + tv <- fresh + pure [(name, tv)] + let (env, tys) = (\f -> foldl' f (As.empty, M.empty) js) + $ \(as1, t1) (k, t) -> + (as1 `As.merge` As.singleton k t, M.insert k t t1) + names = map fst js + Judgment as cs t <- + (\f -> foldr f (e (pure (Judgment env [] (TSet True tys)))) js) + $ \(_, TVar a) rest -> extendMSet a rest + return $ Judgment + (foldl' As.remove as names) + (cs ++ [ EqConst t' (tys M.! x) + | x <- names + , t' <- As.lookup x as]) + -- jww (2018-05-01): How do we recover the actual args used? + (t `TArr` t) evalError = throwError . EvaluationError diff --git a/src/Nix/Value.hs b/src/Nix/Value.hs index d2dd3c77..50c400e3 100644 --- a/src/Nix/Value.hs +++ b/src/Nix/Value.hs @@ -35,7 +35,6 @@ import Data.Monoid (appEndo) import Data.Text (Text) import Data.These import Data.Typeable (Typeable) -import Data.Void import GHC.Generics import Nix.Atoms import Nix.Expr.Types @@ -56,7 +55,7 @@ data NValueF m r | NVPathF FilePath | NVListF [r] | NVSetF (AttrSet r) (AttrSet SourcePos) - | NVClosureF (Params Void) (m (NValue m) -> m (NValue m)) + | NVClosureF (Params ()) (m (NValue m) -> m (NValue m)) -- ^ A function is a closed set of parameters representing the "call -- signature", used at application time to check the type of arguments -- passed to the function. Since it supports default values which may