Improve type-inference of annotated list literals (#1366)

* Remove a redundant check of the type annotation.

* Replace dead code for processing the list elements
  with an error.

* Document the ListLit invariant.

Closes https://github.com/dhall-lang/dhall-haskell/issues/1359.

dhall/src/Dhall/Core.hs

@@ -509,8 +509,20 @@ data Expr s a
     | TextShow
     -- | > List                                     ~  List
     | List
-    -- | > ListLit (Just t ) [x, y, z]              ~  [x, y, z] : t
+    -- | > ListLit (Just t ) []                     ~  [] : t
     --   > ListLit  Nothing  [x, y, z]              ~  [x, y, z]
+    --
+    --   Invariant: A non-empty list literal is always represented as
+    --   @ListLit Nothing xs@.
+    --
+    --   When an annotated, non-empty list literal is parsed, it is represented
+    --   as
+    --
+    --   > Annot (ListLit Nothing [x, y, z]) t      ~ [x, y, z] : t
+
+    -- Eventually we should have separate constructors for empty and non-empty
+    -- list literals. For now it's easier to check the invariant in @infer@.
+    -- See https://github.com/dhall-lang/dhall-haskell/issues/1359#issuecomment-537087234.
     | ListLit (Maybe (Expr s a)) (Seq (Expr s a))
     -- | > ListAppend x y                           ~  x # y
     | ListAppend (Expr s a) (Expr s a)
@@ -1685,7 +1697,7 @@ normalizeWithM ctx e0 = loop (denote e0)
     TextShow -> pure TextShow
     List -> pure List
     ListLit t es
-        | Data.Sequence.null es -> ListLit <$> t' <*> es'
+        | Data.Sequence.null es -> ListLit <$> t' <*> pure Data.Sequence.empty
         | otherwise             -> ListLit Nothing <$> es'
       where
         t'  = traverse loop t

dhall/src/Dhall/Eval.hs

@@ -639,7 +639,7 @@ eval !env t0 =
             VPrim $ \ ~a ->
             VPrim $ \case
                 VListLit t as | null as ->
-                    VListLit t (Sequence.reverse as)
+                    VListLit t as
                 VListLit _ as ->
                     VListLit Nothing (Sequence.reverse as)
                 t ->

dhall/src/Dhall/TypeCheck.hs

@@ -595,35 +595,20 @@ infer typer = loop
                     die MissingListType
 
         ListLit (Just _T₀) ts -> do
-            _ <- loop ctx _T₀
+            if Data.Sequence.null ts
+                then do
+                    _ <- loop ctx _T₀
 
-            let _T₀' = eval values _T₀
+                    let _T₀' = eval values _T₀
 
-            let _T₀'' = quote names _T₀'
+                    let _T₀'' = quote names _T₀'
 
-            case _T₀' of
-                VList _T₁' -> do
-                    tT₁' <- loop ctx (quote names _T₁')
+                    case _T₀' of
+                        VList _ -> return _T₀'
+                        _       -> die (InvalidListType _T₀'')
 
-                    case tT₁' of
-                        VConst Type -> return ()
-                        _           -> die (InvalidListType _T₀'')
-
-                _ -> do
-                    die (InvalidListType _T₀'')
-
-            let process i t = do
-                    _T₁' <- loop ctx t
-
-                    if Eval.conv values _T₀' _T₁'
-                        then return ()
-                        else do
-                            let _T₁'' = quote names _T₁'
-                            die (InvalidListElement i _T₀'' t _T₁'')
-
-            traverseWithIndex_ process ts
-
-            return _T₀'
+                -- See https://github.com/dhall-lang/dhall-haskell/issues/1359.
+                else die ListLitInvariant
 
         ListAppend x y -> do
             tx' <- loop ctx x
@@ -1279,6 +1264,7 @@ data TypeMessage s a
     | MismatchedListElements Int (Expr s a) (Expr s a) (Expr s a)
     | InvalidListElement Int (Expr s a) (Expr s a) (Expr s a)
     | InvalidListType (Expr s a)
+    | ListLitInvariant
     | InvalidSome (Expr s a) (Expr s a) (Expr s a)
     | InvalidPredicate (Expr s a) (Expr s a)
     | IfBranchMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
@@ -2251,6 +2237,21 @@ prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) =
         txt2 = insert expr2
         txt3 = insert expr3
 
+prettyTypeMessage (ListLitInvariant) = ErrorMessages {..}
+  where
+    short = "Internal error: A non-empty list literal violated an internal invariant"
+
+    long =
+        "Explanation: Internal error: A non-empty list literal violated an internal      \n\
+        \invariant.                                                                      \n\
+        \                                                                                \n\
+        \A non-empty list literal must always be represented as                          \n\
+        \                                                                                \n\
+        \    ListLit Nothing [x, y, ...]                                                 \n\
+        \                                                                                \n\
+        \Please file a bug report at https://github.com/dhall-lang/dhall-haskell/issues, \n\
+        \ideally including the offending source code.                                    \n"
+
 prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}
   where
     short = "Invalid type for ❰List❱"
@@ -4306,6 +4307,8 @@ messageExpressions f m = case m of
         InvalidListElement <$> pure a <*> f b <*> f c <*> f d
     InvalidListType a ->
         InvalidListType <$> f a
+    ListLitInvariant ->
+        pure ListLitInvariant
     InvalidSome a b c ->
         InvalidSome <$> f a <*> f b <*> f c
     InvalidPredicate a b ->