Show some details in InvalidType error output (#824)

dhall/dhall.cabal

@@ -464,6 +464,7 @@ Test-Suite tasty
     Main-Is: Dhall/Test/Main.hs
     GHC-Options: -Wall
     Other-Modules:
+        Dhall.Test.Dhall
         Dhall.Test.Format
         Dhall.Test.Import
         Dhall.Test.Lint

dhall/src/Dhall.hs

@@ -105,6 +105,7 @@ import Data.Monoid ((<>))
 import Data.Scientific (Scientific)
 import Data.Sequence (Seq)
 import Data.Text (Text)
+import Data.Text.Prettyprint.Doc (Pretty)
 import Data.Typeable (Typeable)
 import Data.Vector (Vector)
 import Data.Word (Word8, Word16, Word32, Word64)
@@ -141,6 +142,7 @@ import qualified Dhall.Map
 import qualified Dhall.Parser
 import qualified Dhall.Pretty.Internal
 import qualified Dhall.TypeCheck
+import qualified Dhall.Util
 
 -- $setup
 -- >>> :set -XOverloadedStrings
@@ -156,19 +158,36 @@ throws (Right r) = return r
     This exception indicates that an invalid `Type` was provided to the `input`
     function
 -}
-data InvalidType = InvalidType deriving (Typeable)
+data InvalidType s a = InvalidType
+  { invalidTypeExpected :: Expr s a
+  , invalidTypeExpression :: Expr s a
+  }
+  deriving (Typeable)
 
 _ERROR :: String
 _ERROR = "\ESC[1;31mError\ESC[0m"
 
-instance Show InvalidType where
-    show InvalidType =
+instance (Pretty s, Pretty a, Typeable s, Typeable a) => Show (InvalidType s a) where
+    show InvalidType { .. } =
         _ERROR <> ": Invalid Dhall.Type                                                  \n\
         \                                                                                \n\
         \Every Type must provide an extract function that succeeds if an expression      \n\
-        \matches the expected type.  You provided a Type that disobeys this contract     \n"
+        \matches the expected type.  You provided a Type that disobeys this contract     \n\
+        \                                                                                \n\
+        \The Type provided has the expected dhall type:                                  \n\
+        \                                                                                \n\
+        \" <> show txt0 <> "\n\
+        \                                                                                \n\
+        \and it couldn't extract a value from the well-typed expression:                 \n\
+        \                                                                                \n\
+        \" <> show txt1 <> "\n\
+        \                                                                                \n"
+        where
+          txt0 = Dhall.Util.insert invalidTypeExpected
+          txt1 = Dhall.Util.insert invalidTypeExpression
+            
 
-instance Exception InvalidType
+instance (Pretty s, Pretty a, Typeable s, Typeable a) => Exception (InvalidType s a)
 
 -- | @since 1.16
 data InputSettings = InputSettings
@@ -341,9 +360,14 @@ inputWithSettings settings (Type {..}) txt = do
             _ ->
                 Annot expr' expected
     _ <- throws (Dhall.TypeCheck.typeWith (view startingContext settings) annot)
-    case extract (Dhall.Core.normalizeWith (Dhall.Core.getReifiedNormalizer (view normalizer settings)) expr') of
+    let normExpr = Dhall.Core.normalizeWith
+                     (Dhall.Core.getReifiedNormalizer
+                       (view normalizer settings))
+                     expr'
+    case extract normExpr  of
         Just x  -> return x
-        Nothing -> Control.Exception.throwIO InvalidType
+        Nothing -> Control.Exception.throwIO
+                     (InvalidType expected expr')
 
 {-| Type-check and evaluate a Dhall program that is read from the
     file-system.

dhall/src/Dhall/TypeCheck.hs

@@ -947,8 +947,7 @@ _NOT :: Doc ann
 _NOT = "\ESC[1mnot\ESC[0m"
 
 insert :: Pretty a => a -> Doc Ann
-insert expression =
-    "↳ " <> Pretty.align (Dhall.Util.snipDoc (Pretty.pretty expression))
+insert = Dhall.Util.insert
 
 prettyDiff :: (Eq a, Pretty a) => Expr s a -> Expr s a -> Doc Ann
 prettyDiff exprL exprR = Dhall.Diff.diffNormalized exprL exprR

dhall/src/Dhall/Util.hs

@@ -5,11 +5,12 @@
 module Dhall.Util
     ( snip
     , snipDoc
+    , insert
     ) where
 
 import Data.Monoid ((<>))
 import Data.Text (Text)
-import Data.Text.Prettyprint.Doc (Doc)
+import Data.Text.Prettyprint.Doc (Doc, Pretty)
 import Dhall.Pretty (Ann)
 
 import qualified Data.Text
@@ -67,3 +68,8 @@ takeEnd n l = go (drop n l) l
   where
     go (_:xs) (_:ys) = go xs ys
     go _ r = r
+
+-- | Function to insert an aligned pretty expression
+insert :: Pretty a => a -> Doc Ann
+insert expression =
+    "↳ " <> Pretty.align (snipDoc (Pretty.pretty expression))

dhall/tests/Dhall/Test/Dhall.hs

@@ -0,0 +1,59 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Dhall.Test.Dhall where
+
+import Control.Exception (SomeException, try)
+import Numeric.Natural (Natural)
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import qualified Dhall
+import qualified Dhall.Core
+import qualified Dhall.Map
+
+tests :: TestTree
+tests =
+    testGroup "Input"
+     [ shouldShowDetailedTypeError ]
+
+data MyType = MyType { foo :: String , bar :: Natural }
+
+wrongDhallType :: Dhall.Type MyType 
+wrongDhallType = Dhall.Type { .. }
+  where expected =
+          Dhall.Core.Record
+            ( Dhall.Map.fromList
+              [ ( "bar", Dhall.Core.Natural)
+              , ( "foo", Dhall.Core.Text )
+              ]
+            )
+        extract _ = Nothing
+
+shouldShowDetailedTypeError :: TestTree
+shouldShowDetailedTypeError = testCase "detailed TypeError" $ do
+  inputEx :: Either SomeException MyType <-
+        try ( Dhall.input wrongDhallType "{  bar = 0, foo = \"foo\" }") 
+
+  let expectedMsg =
+        "\ESC[1;31mError\ESC[0m: Invalid Dhall.Type                                                  \n\
+        \                                                                                \n\
+        \Every Type must provide an extract function that succeeds if an expression      \n\
+        \matches the expected type.  You provided a Type that disobeys this contract     \n\
+        \                                                                                \n\
+        \The Type provided has the expected dhall type:                                  \n\
+        \                                                                                \n\
+        \↳ { bar : Natural, foo : Text }\n\
+        \                                                                                \n\
+        \and it couldn't extract a value from the well-typed expression:                 \n\
+        \                                                                                \n\
+        \↳ { bar = 0, foo = \"foo\" }\n\
+        \                                                                                \n"
+
+  let assertMsg = "The exception message did not match the expected output"
+  
+  case inputEx of
+    Left ex -> assertEqual assertMsg expectedMsg (show ex)
+    Right _ -> fail "The extraction using a wrong type succeded"
+ 
+        

dhall/tests/Dhall/Test/Main.hs

@@ -2,6 +2,7 @@ module Main where
 
 import Test.Tasty (TestTree)
 
+import qualified Dhall.Test.Dhall
 import qualified Dhall.Test.Format
 import qualified Dhall.Test.Import
 import qualified Dhall.Test.Lint
@@ -31,6 +32,7 @@ allTests =
         , Dhall.Test.Import.tests
         , Dhall.Test.QuickCheck.tests
         , Dhall.Test.Lint.tests
+        , Dhall.Test.Dhall.tests
         ]
 
 main :: IO ()