Reject custom contexts that are ill-formed

src/Dhall/Context.hs

@@ -9,6 +9,7 @@ module Dhall.Context (
       Context
     , empty
     , insert
+    , match
     , lookup
     , toList
     ) where
@@ -41,6 +42,17 @@ insert :: Text -> a -> Context a -> Context a
 insert k v (Context kvs) = Context ((k, v) : kvs)
 {-# INLINABLE insert #-}
 
+{-| \"Pattern match\" on a `Context`
+
+> match (insert k v ctx) = Just (k, v, ctx)
+> match  empty           = Nothing
+-}
+match :: Context a -> Maybe (Text, a, Context a)
+match (Context ((k, v) : kvs)) = Just (k, v, Context kvs)
+match (Context           []  ) = Nothing
+
+{-# INLINABLE match #-}
+
 {-| Look up a key by name and index
 
 > lookup _ _         empty  = Nothing

src/Dhall/TypeCheck.hs

@@ -11,6 +11,7 @@ module Dhall.TypeCheck (
       typeWith
     , typeOf
     , typeWithA
+    , checkContext
 
     -- * Types
     , Typer
@@ -131,7 +132,9 @@ propEqual eL0 eR0 =
     returned type then you may want to `Dhall.Core.normalize` it afterwards.
 -}
 typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s X) (Expr s X)
-typeWith = typeWithA absurd
+typeWith ctx expr = do
+    checkContext ctx
+    typeWithA absurd ctx expr
 
 type Typer a = forall s. a -> Expr s a
 
@@ -3254,3 +3257,20 @@ instance (Buildable a, Buildable s) => Buildable (DetailedTypeError s a) where
         source = case expr of
             Note s _ -> build s
             _        -> mempty
+
+{-| This function verifies that a custom context is well-formed so that
+    type-checking will not loop
+
+    Note that `typeWith` already calls `checkContext` for you on the `Context`
+    that you supply
+-}
+checkContext :: Context (Expr s X) -> Either (TypeError s X) ()
+checkContext context =
+    case Dhall.Context.match context of
+        Nothing -> do
+            return ()
+        Just (x, v, context') -> do
+            let shiftedV       =       Dhall.Core.shift (-1) (V x 0)  v
+            let shiftedContext = fmap (Dhall.Core.shift (-1) (V x 0)) context'
+            _ <- typeWith shiftedContext shiftedV
+            return ()

tests/Regression.hs

@@ -11,8 +11,10 @@ import qualified Data.Text.Lazy.IO
 import qualified Data.Text.Prettyprint.Doc
 import qualified Data.Text.Prettyprint.Doc.Render.Text
 import qualified Dhall
+import qualified Dhall.Context
 import qualified Dhall.Core
 import qualified Dhall.Parser
+import qualified Dhall.TypeCheck
 import qualified System.Timeout
 import qualified Test.Tasty
 import qualified Test.Tasty.HUnit
@@ -35,6 +37,7 @@ regressionTests =
         , issue201
         , issue209
         , issue216
+        , issue253
         , parsing0
         , typeChecking0
         , typeChecking1
@@ -157,6 +160,17 @@ issue216 = Test.Tasty.HUnit.testCase "Issue #216" (do
 
     Test.Tasty.HUnit.assertEqual "Pretty-printing should preserve string interpolation" text1 text0 )
 
+issue253 :: TestTree
+issue253 = Test.Tasty.HUnit.testCase "Issue #253" (do
+    -- Verify that type-checking rejects ill-formed custom contexts
+    let context = Dhall.Context.insert "x" "x" Dhall.Context.empty
+    let result = Dhall.TypeCheck.typeWith context "x"
+
+    -- If the context is not validated correctly then type-checking will
+    -- infinitely loop
+    Just _ <- System.Timeout.timeout 1000000 (Control.Exception.evaluate $! result)
+    return () )
+
 parsing0 :: TestTree
 parsing0 = Test.Tasty.HUnit.testCase "Parsing regression #0" (do
     -- Verify that parsing should not fail