Simpe custom typechecking for Embedded terms (#186)

dhall-hash/Main.hs

@@ -13,7 +13,7 @@ import Data.Version (showVersion)
 import Dhall.Core (pretty, normalize)
 import Dhall.Import (Imported(..), hashExpressionToCode, load)
 import Dhall.Parser (Src, exprFromText)
-import Dhall.TypeCheck (DetailedTypeError(..), TypeError)
+import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)
 import Options.Generic (Generic, ParseRecord, type (<?>)(..))
 import System.IO (stderr)
 import System.Exit (exitFailure, exitSuccess)
@@ -46,7 +46,7 @@ main = do
             .   Control.Exception.handle handler0
           where
             handler0 e = do
-                let _ = e :: TypeError Src
+                let _ = e :: TypeError Src X
                 System.IO.hPutStrLn stderr ""
                 if unHelpful (explain options)
                     then Control.Exception.throwIO (DetailedTypeError e)
@@ -55,7 +55,7 @@ main = do
                         Control.Exception.throwIO e
 
             handler1 (Imported ps e) = do
-                let _ = e :: TypeError Src
+                let _ = e :: TypeError Src X
                 System.IO.hPutStrLn stderr ""
                 if unHelpful (explain options)
                     then Control.Exception.throwIO (Imported ps (DetailedTypeError e))

dhall/Main.hs

@@ -13,7 +13,7 @@ import Data.Version (showVersion)
 import Dhall.Core (normalize)
 import Dhall.Import (Imported(..), load)
 import Dhall.Parser (Src, exprAndHeaderFromText)
-import Dhall.TypeCheck (DetailedTypeError(..), TypeError)
+import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X)
 import Options.Generic (Generic, ParseRecord, type (<?>)(..))
 import System.Exit (exitFailure, exitSuccess)
 import Text.Trifecta.Delta (Delta(..))
@@ -55,7 +55,7 @@ main = do
             .   Control.Exception.handle handler0
           where
             handler0 e = do
-                let _ = e :: TypeError Src
+                let _ = e :: TypeError Src X
                 System.IO.hPutStrLn System.IO.stderr ""
                 if unHelpful (explain options)
                     then Control.Exception.throwIO (DetailedTypeError e)
@@ -64,7 +64,7 @@ main = do
                         Control.Exception.throwIO e
 
             handler1 (Imported ps e) = do
-                let _ = e :: TypeError Src
+                let _ = e :: TypeError Src X
                 System.IO.hPutStrLn System.IO.stderr ""
                 if unHelpful (explain options)
                     then Control.Exception.throwIO (Imported ps (DetailedTypeError e))

src/Dhall.hs

@@ -162,7 +162,7 @@ input (Type {..}) txt = do
 --   For other use cases, use `input` from `Dhall` module. It will give you
 --   a much better user experience.
 rawInput
-    :: Alternative f 
+    :: Alternative f
     => Type a
     -- ^ The type of value to decode from Dhall to Haskell
     -> Expr s X
@@ -180,103 +180,103 @@ rawInput (Type {..}) expr = do
 
 >> 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
 
 -}
@@ -284,11 +284,11 @@ detailed :: IO a -> IO a
 detailed =
     Control.Exception.handle handler1 . Control.Exception.handle handler0
   where
-    handler0 :: Imported (TypeError Src) -> IO a
+    handler0 :: Imported (TypeError Src X) -> IO a
     handler0 (Imported ps e) =
         Control.Exception.throwIO (Imported ps (DetailedTypeError e))
 
-    handler1 :: TypeError Src -> IO a
+    handler1 :: TypeError Src X -> IO a
     handler1 e = Control.Exception.throwIO (DetailedTypeError e)
 
 {-| A @(Type a)@ represents a way to marshal a value of type @\'a\'@ from Dhall

tests/Regression.hs

@@ -16,7 +16,7 @@ import qualified Util
 
 import Dhall.Import (Imported)
 import Dhall.Parser (Src)
-import Dhall.TypeCheck (TypeError)
+import Dhall.TypeCheck (TypeError, X)
 import Test.Tasty (TestTree)
 import Test.Tasty.HUnit ((@?=))
 
@@ -80,7 +80,7 @@ issue126 = Test.Tasty.HUnit.testCase "Issue #126" (do
 issue151 :: TestTree
 issue151 = Test.Tasty.HUnit.testCase "Issue #151" (do
     let shouldNotTypeCheck text = do
-            let handler :: Imported (TypeError Src) -> IO Bool
+            let handler :: Imported (TypeError Src X) -> IO Bool
                 handler _ = return True
 
             let typeCheck = do
@@ -88,7 +88,7 @@ issue151 = Test.Tasty.HUnit.testCase "Issue #151" (do
                     return False
             b <- Control.Exception.handle handler typeCheck
             Test.Tasty.HUnit.assertBool "The expression should not type-check" b
-            
+
     -- These two examples contain the following expression that loops infinitely
     -- if you normalize the expression before type-checking the expression:
     --