From 484182b74e39a9eb58b09200283bfb80876f7e89 Mon Sep 17 00:00:00 2001
From: Gabriel Gonzalez <Gabriel439@gmail.com>
Date: Thu, 27 Jun 2019 13:19:16 -0700
Subject: [PATCH] Remove the `InvalidField` error constructor (#1026)

Fixes https://github.com/dhall-lang/dhall-haskell/issues/1025

There were two error constructors related to invalid field types:

* `InvalidField`: for field types whose types were invalid type-checking
  constants
* `InvalidFieldType`: for all other invalid field types

As @sjakobi noted, there are no invalid field types for the former
category, so we can remove that category of error entirely.

Note that `InvalidField` was still being used in a few places, but each
of those uses should actually have been using `InvalidFieldType`
instead, which this change also fixes.
---
 dhall/src/Dhall/TypeCheck.hs | 42 ++----------------------------------
 1 file changed, 2 insertions(+), 40 deletions(-)

diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs
index 4291704..cd1ad2d 100644
--- a/dhall/src/Dhall/TypeCheck.hs
+++ b/dhall/src/Dhall/TypeCheck.hs
@@ -496,7 +496,7 @@ typeWithA tpa = loop
                 s0 <- fmap Dhall.Core.normalize (loop ctx t0)
                 c <- case s0 of
                     Const c -> pure c
-                    _       -> Left (TypeError ctx e (InvalidField k0 v0))
+                    _       -> Left (TypeError ctx e (InvalidFieldType k0 v0))
                 let process k v = do
                         t <- loop ctx v
                         s <- fmap Dhall.Core.normalize (loop ctx t)
@@ -505,7 +505,7 @@ typeWithA tpa = loop
                                 if c == c'
                                 then return ()
                                 else Left (TypeError ctx e (FieldMismatch k v c k0 v0 c'))
-                            _ -> Left (TypeError ctx e (InvalidField k t))
+                            _ -> Left (TypeError ctx e (InvalidFieldType k t))
 
                         return t
                 kts <- Dhall.Map.traverseWithKey process kvs
@@ -881,7 +881,6 @@ data TypeMessage s a
     | InvalidPredicate (Expr s a) (Expr s a)
     | IfBranchMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
     | IfBranchMustBeTerm Bool (Expr s a) (Expr s a) (Expr s a)
-    | InvalidField Text (Expr s a)
     | InvalidFieldType Text (Expr s a)
     | FieldAnnotationMismatch Text (Expr s a) Const Text (Expr s a) Const
     | FieldMismatch Text (Expr s a) Const Text (Expr s a) Const
@@ -2293,43 +2292,6 @@ prettyTypeMessage (FieldMismatch k0 expr0 c0 k1 expr1 c1) = ErrorMessages {..}
         level Kind = "type"
         level Sort = "kind"
 
-prettyTypeMessage (InvalidField k expr0) = ErrorMessages {..}
-  where
-    short = "Invalid field"
-
-    long =
-        "Explanation: Every record literal is a set of fields assigned to values, like   \n\
-        \this:                                                                           \n\
-        \                                                                                \n\
-        \    ┌────────────────────────────────────────┐                                  \n\
-        \    │ { foo = 100, bar = True, baz = \"ABC\" } │                                \n\
-        \    └────────────────────────────────────────┘                                  \n\
-        \                                                                                \n\
-        \However, fields can only be terms and or ❰Type❱s and not ❰Kind❱s                \n\
-        \                                                                                \n\
-        \For example, the following record literal is " <> _NOT <> " valid:              \n\
-        \                                                                                \n\
-        \                                                                                \n\
-        \    ┌────────────────┐                                                          \n\
-        \    │ { foo = Type } │                                                          \n\
-        \    └────────────────┘                                                          \n\
-        \              ⇧                                                                 \n\
-        \              ❰Type❱ is a ❰Kind❱, which is not allowed                          \n\
-        \                                                                                \n\
-        \                                                                                \n\
-        \You provided a record literal with a field named:                               \n\
-        \                                                                                \n\
-        \" <> txt0 <> "\n\
-        \                                                                                \n\
-        \... whose value is:                                                             \n\
-        \                                                                                \n\
-        \" <> txt1 <> "\n\
-        \                                                                                \n\
-        \... which is not a term or ❰Type❱                                               \n"
-      where
-        txt0 = insert k
-        txt1 = insert expr0
-
 prettyTypeMessage (InvalidAlternativeType k expr0) = ErrorMessages {..}
   where
     short = "Invalid alternative type"