Make isNormalized consistent with normalize (#1115)

To be more precise (citing the haddocks):

    Given a well-typed expression e, (isNormalized e) is equivalent to
    (e == normalize e).

    Given an ill-typed expression, isNormalized may return True or False.

An even closer correspondence between isNormalized and 'normalize' is
currently tricky to achieve as 'normalize' returns errors only for some
ill-typed expressions. Once 'normalize' is more principled in this
regard, isNormalized could be changed to return a (Maybe Bool).

This re-enables a property test checking this consistency. Since
'normalize' returns errors for some ill-typed expressions, we
catch have to catch these, which requires an NFData for Expr.

dhall/dhall.cabal

@@ -538,6 +538,7 @@ Library
         containers                  >= 0.5.0.0  && < 0.7 ,
         contravariant                              < 1.6 ,
         cryptonite                  >= 0.23     && < 1.0 ,
+        deepseq                                    < 1.5 ,
         Diff                        >= 0.2      && < 0.4 ,
         directory                   >= 1.2.2.0  && < 1.4 ,
         dotgen                      >= 0.4.2    && < 0.5 ,
@@ -686,6 +687,7 @@ Test-Suite tasty
         QuickCheck                >= 2.10     && < 2.14,
         quickcheck-instances      >= 0.3.12   && < 0.4 ,
         serialise                                      ,
+        spoon                                    < 0.4 ,
         tasty                     >= 0.11.2   && < 1.3 ,
         tasty-hunit               >= 0.9.2    && < 0.11,
         tasty-quickcheck          >= 0.9.2    && < 0.11,

dhall/src/Dhall/Core.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE BangPatterns       #-}
 {-# LANGUAGE CPP                #-}
+{-# LANGUAGE DeriveAnyClass     #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric      #-}
 {-# LANGUAGE DeriveTraversable  #-}
@@ -68,6 +69,7 @@ module Dhall.Core (
 import Control.Applicative (Applicative(..), (<$>))
 #endif
 import Control.Applicative (empty)
+import Control.DeepSeq (NFData)
 import Control.Exception (Exception)
 import Control.Monad.IO.Class (MonadIO(..))
 import Crypto.Hash (SHA256)
@@ -126,7 +128,7 @@ import qualified Text.Printf
     Dhall is not a dependently typed language
 -}
 data Const = Type | Kind | Sort
-    deriving (Show, Eq, Ord, Data, Bounded, Enum, Generic)
+    deriving (Show, Eq, Ord, Data, Bounded, Enum, Generic, NFData)
 
 instance Pretty Const where
     pretty = Pretty.unAnnotate . prettyConst
@@ -138,7 +140,7 @@ instance Pretty Const where
     @Directory { components = [ "baz", "bar", "foo" ] }@
 -}
 newtype Directory = Directory { components :: [Text] }
-    deriving (Eq, Generic, Ord, Show)
+    deriving (Eq, Generic, Ord, Show, NFData)
 
 instance Semigroup Directory where
     Directory components₀ <> Directory components₁ =
@@ -153,7 +155,7 @@ instance Pretty Directory where
 data File = File
     { directory :: Directory
     , file      :: Text
-    } deriving (Eq, Generic, Ord, Show)
+    } deriving (Eq, Generic, Ord, Show, NFData)
 
 instance Pretty File where
     pretty (File {..}) =
@@ -174,23 +176,23 @@ data FilePrefix
     -- ^ Path relative to @..@
     | Home
     -- ^ Path relative to @~@
-    deriving (Eq, Generic, Ord, Show)
+    deriving (Eq, Generic, Ord, Show, NFData)
 
 instance Pretty FilePrefix where
     pretty Absolute = ""
     pretty Here     = "."
     pretty Parent   = ".."
     pretty Home     = "~"
 
-data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show)
+data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show, NFData)
 
 data URL = URL
     { scheme    :: Scheme
     , authority :: Text
     , path      :: File
     , query     :: Maybe Text
     , headers   :: Maybe (Expr Src Import)
-    } deriving (Eq, Generic, Ord, Show)
+    } deriving (Eq, Generic, Ord, Show, NFData)
 
 instance Pretty URL where
     pretty (URL {..}) =
@@ -228,7 +230,7 @@ data ImportType
     | Env  Text
     -- ^ Environment variable
     | Missing
-    deriving (Eq, Generic, Ord, Show)
+    deriving (Eq, Generic, Ord, Show, NFData)
 
 parent :: File
 parent = File { directory = Directory { components = [ ".." ] }, file = "" }
@@ -267,13 +269,13 @@ instance Pretty ImportType where
 
 -- | How to interpret the import's contents (i.e. as Dhall code or raw text)
 data ImportMode = Code | RawText | Location
-  deriving (Eq, Generic, Ord, Show)
+  deriving (Eq, Generic, Ord, Show, NFData)
 
 -- | A `ImportType` extended with an optional hash for semantic integrity checks
 data ImportHashed = ImportHashed
     { hash       :: Maybe (Crypto.Hash.Digest SHA256)
     , importType :: ImportType
-    } deriving (Eq, Generic, Ord, Show)
+    } deriving (Eq, Generic, Ord, Show, NFData)
 
 instance Semigroup ImportHashed where
     ImportHashed _ importType₀ <> ImportHashed hash importType₁ =
@@ -289,7 +291,7 @@ instance Pretty ImportHashed where
 data Import = Import
     { importHashed :: ImportHashed
     , importMode   :: ImportMode
-    } deriving (Eq, Generic, Ord, Show)
+    } deriving (Eq, Generic, Ord, Show, NFData)
 
 instance Semigroup Import where
     Import importHashed₀ _ <> Import importHashed₁ code =
@@ -337,7 +339,7 @@ instance Pretty Import where
     appear as a numeric suffix.
 -}
 data Var = V Text !Int
-    deriving (Data, Generic, Eq, Ord, Show)
+    deriving (Data, Generic, Eq, Ord, Show, NFData)
 
 instance IsString Var where
     fromString str = V (fromString str) 0
@@ -484,7 +486,9 @@ data Expr s a
     | ImportAlt (Expr s a) (Expr s a)
     -- | > Embed import                             ~  import
     | Embed a
-    deriving (Eq, Ord, Foldable, Generic, Traversable, Show, Data)
+    deriving (Eq, Ord, Foldable, Generic, Traversable, Show, Data, NFData)
+-- NB: If you add a constructor to Expr, please also update the Arbitrary
+-- instance in Dhall.Test.QuickCheck.
 
 -- This instance is hand-written due to the fact that deriving
 -- it does not give us an INLINABLE pragma. We annotate this fmap
@@ -710,7 +714,7 @@ data Binding s a = Binding
     { variable   :: Text
     , annotation :: Maybe (Expr s a)
     , value      :: Expr s a
-    } deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data)
+    } deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data, NFData)
 
 instance Bifunctor Binding where
     first k (Binding a b c) = Binding a (fmap (first k) b) (first k c)
@@ -719,7 +723,7 @@ instance Bifunctor Binding where
 
 -- | The body of an interpolated @Text@ literal
 data Chunks s a = Chunks [(Text, Expr s a)] Text
-    deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data)
+    deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data, NFData)
 
 instance Data.Semigroup.Semigroup (Chunks s a) where
     Chunks xysL zL <> Chunks         []    zR =
@@ -1754,6 +1758,11 @@ isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
 isNormalizedWith ctx e = e == normalizeWith (Just (ReifiedNormalizer ctx)) e
 
 -- | Quickly check if an expression is in normal form
+--
+-- Given a well-typed expression @e@, @'isNormalized' e@ is equivalent to
+-- @e == 'normalize' e@.
+--
+-- Given an ill-typed expression, 'isNormalized' may return 'True' or 'False'.
 isNormalized :: Eq a => Expr s a -> Bool
 isNormalized e0 = loop (denote e0)
   where
@@ -1775,6 +1784,7 @@ isNormalized e0 = loop (denote e0)
           App (App OptionalBuild _) (App (App OptionalFold _) _) -> False
 
           App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False
+          App NaturalFold (NaturalLit _) -> False
           App NaturalBuild _ -> False
           App NaturalIsZero (NaturalLit _) -> False
           App NaturalEven (NaturalLit _) -> False
@@ -1921,30 +1931,20 @@ isNormalized e0 = loop (denote e0)
                               Nothing -> True
                       _ -> True
               _ -> True
-      ToMap x t -> loop x && all loop t
-      Field r x -> loop r &&
-          case r of
-              RecordLit kvs ->
-                  case Dhall.Map.lookup x kvs of
-                      Just _  -> False
-                      Nothing -> True
-              Union kvs ->
-                  case Dhall.Map.lookup x kvs of
-                      Just _  -> False
-                      Nothing -> True
-              _ -> True
-      Project r xs -> loop r &&
-          case r of
-              RecordLit kvs ->
-                  case xs of
-                      Left  s -> not (all (flip Dhall.Map.member kvs) s) && Dhall.Set.isSorted s
-                      Right e' ->
-                          case e' of
-                              Record kts ->
-                                  loop (Project r (Left (Dhall.Set.fromSet (Dhall.Map.keysSet kts))))
-                              _ ->
-                                  False
-              _ -> not (null xs)
+      ToMap x t -> case x of
+          RecordLit _ -> False
+          _ -> loop x && all loop t
+      Field r _ -> case r of
+          RecordLit _ -> False
+          _ -> loop r
+      Project r p -> loop r &&
+          case p of
+              Left s -> case r of
+                  RecordLit _ -> False
+                  _ -> not (Dhall.Set.null s) && Dhall.Set.isSorted s
+              Right e' -> case e' of
+                  Record _ -> False
+                  _ -> loop e'
       Note _ e' -> loop e'
       ImportAlt l _r -> loop l
       Embed _ -> True

dhall/src/Dhall/Map.hs

@@ -1,5 +1,7 @@
 {-# LANGUAGE CPP                #-}
+{-# LANGUAGE DeriveAnyClass     #-}
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric      #-}
 {-# LANGUAGE DeriveTraversable  #-}
 {-# LANGUAGE RecordWildCards    #-}
 {-# LANGUAGE TypeFamilies       #-}
@@ -63,8 +65,10 @@ module Dhall.Map
     ) where
 
 import Control.Applicative ((<|>))
+import Control.DeepSeq (NFData)
 import Data.Data (Data)
 import Data.Semigroup
+import GHC.Generics (Generic)
 import Prelude hiding (filter, lookup)
 
 import qualified Data.List
@@ -81,12 +85,12 @@ import qualified Prelude
     and also to improve performance
 -}
 data Map k v = Map (Data.Map.Map k v) (Keys k)
-    deriving (Data)
+    deriving (Data, Generic, NFData)
 
 data Keys a
     = Sorted
     | Original [a]
-    deriving (Data)
+    deriving (Data, Generic, NFData)
 
 instance (Ord k, Eq v) => Eq (Map k v) where
   m1 == m2 =

dhall/src/Dhall/Set.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
 
 -- | This module only exports ways of constructing a Set,
@@ -18,9 +19,11 @@ module Dhall.Set (
     , difference
     , sort
     , isSorted
+    , null
     ) where
 
-import Prelude
+import Prelude hiding (null)
+import Control.DeepSeq (NFData)
 import Data.List (foldl')
 import Data.Sequence (Seq, (|>))
 import Data.Data (Data)
@@ -31,7 +34,7 @@ import qualified Data.Sequence
 import qualified Data.Foldable
 
 data Set a = Set (Data.Set.Set a) (Seq a)
-    deriving (Eq, Generic, Ord, Show, Data)
+    deriving (Eq, Generic, Ord, Show, Data, NFData)
 
 instance Foldable Set where
     foldMap f = foldMap f . toSeq
@@ -85,3 +88,12 @@ True
 -}
 isSorted :: Ord a => Set a -> Bool
 isSorted s = toList s == Data.Set.toList (toSet s)
+
+{-|
+>>> null (fromList [1])
+False
+>>> null (fromList [])
+True
+-}
+null :: Set a -> Bool
+null (Set s _) = Data.Set.null s

dhall/src/Dhall/Src.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE DeriveAnyClass     #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric      #-}
 {-# LANGUAGE OverloadedStrings  #-}
@@ -9,6 +10,7 @@ module Dhall.Src
       Src(..)
     ) where
 
+import Control.DeepSeq (NFData)
 import Data.Data (Data)
 import Data.Monoid ((<>))
 import Data.Text (Text)
@@ -25,7 +27,7 @@ import qualified Text.Printf     as Printf
 -- | Source code extract
 data Src = Src !SourcePos !SourcePos Text
   -- Text field is intentionally lazy
-  deriving (Data, Eq, Generic, Ord, Show)
+  deriving (Data, Eq, Generic, Ord, Show, NFData)
 
 instance Pretty Src where
     pretty (Src begin _ text) =