Add detailed

src/Dhall.hs

@@ -297,6 +297,7 @@ module Dhall
     (
     -- * Input
       input
+    , detailed
 
     -- * Types
     , Type
@@ -318,11 +319,14 @@ module Dhall
 import Control.Applicative (empty, liftA2, (<|>))
 import Control.Exception (Exception)
 import Data.Monoid ((<>))
+import Data.Text.Buildable (Buildable)
 import Data.Text.Lazy (Text)
+import Data.Typeable (Typeable)
 import Data.Vector (Vector)
 import Dhall.Core (Expr(..))
+import Dhall.Import (Imported(..))
 import Dhall.Parser (Src(..))
-import Dhall.TypeCheck (X)
+import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)
 import GHC.Generics
 import Numeric.Natural (Natural)
 import Prelude hiding (maybe)
@@ -389,6 +393,121 @@ input (Type {..}) text = do
         Just x  -> return x
         Nothing -> fail "input: malformed `Type`"
 
+{-| Use this to provide more detailed error messages
+
+>> input auto "True" :: IO Integer
+> *** Exception: Error: Expression doesn't match annotation
+> 
+> True : Integer
+> 
+> (input):1:1
+
+>> detailed (input auto "True") :: IO Integer
+> *** Exception: Error: Expression doesn't match annotation
+> 
+> Explanation: You can annotate an expression with its type or kind using the
+> ❰:❱ symbol, like this:
+> 
+> 
+>     ┌───────┐
+>     │ x : t │  ❰x❱ is an expression and ❰t❱ is the annotated type or kind of ❰x❱
+>     └───────┘
+> 
+> The type checker verifies that the expression's type or kind matches the
+> provided annotation
+> 
+> For example, all of the following are valid annotations that the type checker
+> accepts:
+> 
+> 
+>     ┌─────────────┐
+>     │ 1 : Integer │  ❰1❱ is an expression that has type ❰Integer❱, so the type
+>     └─────────────┘  checker accepts the annotation
+> 
+> 
+>     ┌────────────────────────┐
+>     │ Natural/even +2 : Bool │  ❰Natural/even +2❱ has type ❰Bool❱, so the type
+>     └────────────────────────┘  checker accepts the annotation
+> 
+> 
+>     ┌────────────────────┐
+>     │ List : Type → Type │  ❰List❱ is an expression that has kind ❰Type → Type❱,
+>     └────────────────────┘  so the type checker accepts the annotation
+> 
+> 
+>     ┌──────────────────┐
+>     │ List Text : Type │  ❰List Text❱ is an expression that has kind ❰Type❱, so
+>     └──────────────────┘  the type checker accepts the annotation
+> 
+> 
+> However, the following annotations are not valid and the type checker will
+> reject them:
+> 
+> 
+>     ┌──────────┐
+>     │ 1 : Text │  The type checker rejects this because ❰1❱ does not have type
+>     └──────────┘  ❰Text❱
+> 
+> 
+>     ┌─────────────┐
+>     │ List : Type │  ❰List❱ does not have kind ❰Type❱
+>     └─────────────┘
+> 
+> 
+> You or the interpreter annotated this expression:
+> 
+> ↳ True
+> 
+> ... with this type or kind:
+> 
+> ↳ Integer
+> 
+> ... but the inferred type or kind of the expression is actually:
+> 
+> ↳ Bool
+> 
+> Some common reasons why you might get this error:
+> 
+> ● The Haskell Dhall interpreter implicitly inserts a top-level annotation
+>   matching the expected type
+> 
+>   For example, if you run the following Haskell code:
+> 
+> 
+>     ┌───────────────────────────────┐
+>     │ >>> input auto "1" :: IO Text │
+>     └───────────────────────────────┘
+> 
+> 
+>   ... then the interpreter will actually type check the following annotated
+>   expression:
+> 
+> 
+>     ┌──────────┐
+>     │ 1 : Text │
+>     └──────────┘
+> 
+> 
+>   ... and then type-checking will fail
+> 
+> ────────────────────────────────────────────────────────────────────────────────
+> 
+> True : Integer
+> 
+> (input):1:1
+
+-}
+detailed :: IO a -> IO a
+detailed =
+    Control.Exception.handle handler1 . Control.Exception.handle handler0
+  where
+    handler0 :: Imported (TypeError Src) -> IO a
+    handler0 (Imported ps e) =
+        Control.Exception.throwIO (Imported ps (DetailedTypeError e))
+
+    handler1 :: TypeError Src -> IO a
+    handler1 e = Control.Exception.throwIO (DetailedTypeError e)
+
 {-| A @(Type a)@ represents a way to marshal a value of type @\'a\'@ from Dhall
     into Haskell