Allow visible type application for []

This amounts to a one-line change in `tcExpr`. I've added a Note to
explain what is going on.

This requires a separate change in the pattern-match checker to
account for the fact that typechecked `[]` expressions become
`ConLikeOut`s, not `ExplicitList`s.

Test Plan: make test TEST=T13680

Reviewers: goldfire, mpickering, austin, bgamari

Reviewed By: mpickering, bgamari

Subscribers: rwbarton, thomie, goldfire

GHC Trac Issues: #13680

Differential Revision: https://phabricator.haskell.org/D3733

3 files changed, 37 insertions, 0 deletions

diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index cf8bf0c053..0e1e8662bf 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -54,6 +54,7 @@ import NameEnv
 import NameSet
 import RdrName
 import TyCon
+import TyCoRep
 import Type
 import TcEvidence
 import VarSet
@@ -1170,6 +1171,16 @@ tcApp m_herald orig_fun orig_args res_ty
            ; sel_name  <- disambiguateSelector lbl sig_tc_ty
            ; go (L loc (HsRecFld (Unambiguous lbl sel_name))) args }
 
+    -- See Note [Visible type application for the empty list constructor]
+    go (L loc (ExplicitList _ Nothing [])) [Right ty_arg]
+      = do { ty_arg' <- tcHsTypeApp ty_arg liftedTypeKind
+           ; let list_ty = TyConApp listTyCon [ty_arg']
+           ; _ <- tcSubTypeDS (OccurrenceOf nilDataConName) GenSigCtxt
+                              list_ty res_ty
+           ; let expr :: LHsExpr GhcTcId
+                 expr = L loc $ ExplicitList ty_arg' Nothing []
+           ; return (idHsWrapper, expr, []) }
+
     go fun args
       = do {   -- Type-check the function
            ; (fun1, fun_sigma) <- tcInferFun fun
@@ -1198,6 +1209,26 @@ mk_app_msg fun = sep [ text "The function" <+> quotes (ppr fun)
 mk_op_msg :: LHsExpr GhcRn -> SDoc
 mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes"
 
+{-
+Note [Visible type application for the empty list constructor]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Getting the expression [] @Int to typecheck is slightly tricky since [] isn't
+an ordinary data constructor. By default, when tcExpr typechecks a list
+expression, it wraps the expression in a coercion, which gives it a type to the
+effect of p[a]. It isn't until later zonking that the type becomes
+forall a. [a], but that's too late for visible type application.
+
+The workaround is to check for empty list expressions that have a visible type
+argument in tcApp, and if so, directly typecheck [] @ty data constructor name.
+This avoids the intermediate coercion and produces an expression of type [ty],
+as one would intuitively expect.
+
+Unfortunately, this workaround isn't terribly robust, since more involved
+expressions such as (let in []) @Int won't work. Until a more elegant fix comes
+along, however, this at least allows direct type application on [] to work,
+which is better than before.
+-}
+
 ----------------
 tcInferFun :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType)
 -- Infer type of a function
diff --git a/testsuite/tests/typecheck/should_compile/T13680.hs b/testsuite/tests/typecheck/should_compile/T13680.hs
new file mode 100644
index 0000000000..7c1a8553a4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13680.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeApplications #-}
+module T13680 where
+
+foo :: [Int]
+foo = [] @Int
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index d6aaef53d2..8f7996c6dd 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -561,6 +561,7 @@ test('T13603', normal, compile, [''])
 test('T13333', normal, compile, [''])
 test('T13585', [extra_files(['T13585.hs', 'T13585a.hs', 'T13585b.hs'])], run_command, ['$MAKE -s --no-print-directory T13585'])
 test('T13651', normal, compile, [''])
+test('T13680', normal, compile, [''])
 test('T13785', normal, compile, [''])
 test('T13804', normal, compile, [''])
 test('T13822', normal, compile, [''])