Comments adding to the fix for Trac #15859

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

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.
 -}