[commit: ghc] master: Comments adding to the fix for Trac #15859 (0ce66be)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/0ce66be953becf7c9de3cbea406953306b4db3b1/ghc

>---------------------------------------------------------------

commit 0ce66be953becf7c9de3cbea406953306b4db3b1
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Nov 6 09:10:30 2018 +0000

    Comments adding to the fix for Trac #15859


>---------------------------------------------------------------

0ce66be953becf7c9de3cbea406953306b4db3b1
 compiler/typecheck/TcExpr.hs | 28 ++++++++++++++++++++++++----
 compiler/types/TyCoRep.hs    |  5 ++++-
 2 files changed, 28 insertions(+), 5 deletions(-)

diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index a087917..9eaead5 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -1331,8 +1331,9 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
            ; case tcSplitForAllTy_maybe upsilon_ty of
                Just (tvb, inner_ty)
                  | binderArgFlag tvb == Specified ->
-                   -- It really can't be Inferred, because we've just instantiated those
-                   -- But, oddly, it might just be Required. See #15859.
+                   -- It really can't be Inferred, because we've justn
+                   -- instantiated those. But, oddly, it might just be Required.
+                   -- See Note [Required quantifiers in the type of a term]
                  do { let tv   = binderVar tvb
                           kind = tyVarKind tv
                     ; ty_arg <- tcHsTypeApp hs_ty_arg kind
@@ -1381,8 +1382,27 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
                text "Cannot apply expression of type" <+> quotes (ppr ty) $$
                text "to a visible type argument" <+> quotes (ppr arg) }
 
-{- Note [Visible type application zonk]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Required quantifiers in the type of a term]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #15859)
+
+  data A k :: k -> Type      -- A      :: forall k -> k -> Type
+  type KindOf (a :: k) = k   -- KindOf :: forall k. k -> Type
+  a = (undefind :: KindOf A) @Int
+
+With ImpredicativeTypes (thin ice, I know), we instantiate
+KindOf at type (forall k -> k -> Type), so
+  KindOf A = forall k -> k -> Type
+whose first argument is Required
+
+We want to reject this type application to Int, but in earlier
+GHCs we had an ASSERT that Required could not occur here.
+
+The ice is thin; c.f. Note [No Required TyCoBinder in terms]
+in TyCoRep.
+
+Note [Visible type application zonk]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 * Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg).
 
 * tcHsTypeApp only guarantees that
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 1c0d5f9..d6c0f33 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -711,7 +711,7 @@ See also Note [Required, Specified, and Inferred for types] in TcTyClsDecls
   Visible Type Applications paper (ESOP'16).
 
 Note [No Required TyCoBinder in terms]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We don't allow Required foralls for term variables, including pattern
 synonyms and data constructors.  Why?  Because then an application
 would need a /compulsory/ type argument (possibly without an "@"?),
@@ -719,6 +719,9 @@ thus (f Int); and we don't have concrete syntax for that.
 
 We could change this decision, but Required, Named TyCoBinders are rare
 anyway.  (Most are Anons.)
+
+However the type of a term can (just about) have a required quantifier;
+see Note [Required quantifiers in the type of a term] in TcExpr.
 -}