Overhaul -fprint-explicit-kinds to use VKA

This patch changes the behavior of `-fprint-explicit-kinds`
so that it displays kind argument using visible kind application.
In other words, the flag now:

1. Prints instantiations of specified variables with `@(...)`.
2. Prints instantiations of inferred variables with `@{...}`.

In addition, this patch removes the `Use -fprint-explicit-kinds to
see the kind arguments` error message that often arises when a type
mismatch occurs due to different kinds. Instead, whenever there is a
kind mismatch, we now enable the `-fprint-explicit-kinds` flag
locally to help cue to the programmer where the error lies.
(See `Note [Kind arguments in error messages]` in `TcErrors`.)
As a result, these funny `@{...}` things can now appear to the user
even without turning on the `-fprint-explicit-kinds` flag explicitly,
so I took the liberty of documenting them in the users' guide.

Test Plan: ./validate

Reviewers: goldfire, simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15871

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

1 files changed, 80 insertions, 15 deletions

diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 2ddb4c4604..d454f4cd32 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -100,7 +100,7 @@ module TcType (
   isImprovementPred,
 
   -- * Finding type instances
-  tcTyFamInsts, isTyFamFree,
+  tcTyFamInsts, tcTyFamInstsAndVis, tcTyConAppTyFamInstsAndVis, isTyFamFree,
 
   -- * Finding "exact" (non-dead) type variables
   exactTyCoVarsOfType, exactTyCoVarsOfTypes,
@@ -858,20 +858,85 @@ promoteSkolemsX tclvl = mapAccumL (promoteSkolemX tclvl)
 -- we don't need to take <big type> into account when asking if
 -- the calls on the RHS are smaller than the LHS
 tcTyFamInsts :: Type -> [(TyCon, [Type])]
-tcTyFamInsts ty
-  | Just exp_ty <- tcView ty    = tcTyFamInsts exp_ty
-tcTyFamInsts (TyVarTy _)        = []
-tcTyFamInsts (TyConApp tc tys)
-  | isTypeFamilyTyCon tc        = [(tc, take (tyConArity tc) tys)]
-  | otherwise                   = concat (map tcTyFamInsts tys)
-tcTyFamInsts (LitTy {})         = []
-tcTyFamInsts (ForAllTy bndr ty) = tcTyFamInsts (binderType bndr)
-                                  ++ tcTyFamInsts ty
-tcTyFamInsts (FunTy ty1 ty2)    = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
-tcTyFamInsts (AppTy ty1 ty2)    = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
-tcTyFamInsts (CastTy ty _)      = tcTyFamInsts ty
-tcTyFamInsts (CoercionTy _)     = []  -- don't count tyfams in coercions,
-                                      -- as they never get normalized, anyway
+tcTyFamInsts = map (\(_,b,c) -> (b,c)) . tcTyFamInstsAndVis
+
+-- | Like 'tcTyFamInsts', except that the output records whether the
+-- type family and its arguments occur as an /invisible/ argument in
+-- some type application. This information is useful because it helps GHC know
+-- when to turn on @-fprint-explicit-kinds@ during error reporting so that
+-- users can actually see the type family being mentioned.
+--
+-- As an example, consider:
+--
+-- @
+-- class C a
+-- data T (a :: k)
+-- type family F a :: k
+-- instance C (T @(F Int) (F Bool))
+-- @
+--
+-- There are two occurrences of the type family `F` in that `C` instance, so
+-- @'tcTyFamInstsAndVis' (C (T \@(F Int) (F Bool)))@ will return:
+--
+-- @
+-- [ ('True',  F, [Int])
+-- , ('False', F, [Bool]) ]
+-- @
+--
+-- @F Int@ is paired with 'True' since it appears as an /invisible/ argument
+-- to @C@, whereas @F Bool@ is paired with 'False' since it appears an a
+-- /visible/ argument to @C@.
+--
+-- See also @Note [Kind arguments in error messages]@ in "TcErrors".
+tcTyFamInstsAndVis :: Type -> [(Bool, TyCon, [Type])]
+tcTyFamInstsAndVis = tcTyFamInstsAndVisX False
+
+tcTyFamInstsAndVisX
+  :: Bool -- ^ Is this an invisible argument to some type application?
+  -> Type -> [(Bool, TyCon, [Type])]
+tcTyFamInstsAndVisX = go
+  where
+    go is_invis_arg ty
+      | Just exp_ty <- tcView ty       = go is_invis_arg exp_ty
+    go _ (TyVarTy _)                   = []
+    go is_invis_arg (TyConApp tc tys)
+      | isTypeFamilyTyCon tc
+      = [(is_invis_arg, tc, take (tyConArity tc) tys)]
+      | otherwise
+      = tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys
+    go _            (LitTy {})         = []
+    go is_invis_arg (ForAllTy bndr ty) = go is_invis_arg (binderType bndr)
+                                         ++ go is_invis_arg ty
+    go is_invis_arg (FunTy ty1 ty2)    = go is_invis_arg ty1
+                                         ++ go is_invis_arg ty2
+    go is_invis_arg ty@(AppTy _ _)     =
+      let (ty_head, ty_args) = splitAppTys ty
+          ty_arg_flags       = appTyArgFlags ty_head ty_args
+      in go is_invis_arg ty_head
+         ++ concat (zipWith (\flag -> go (isInvisibleArgFlag flag))
+                            ty_arg_flags ty_args)
+    go is_invis_arg (CastTy ty _)      = go is_invis_arg ty
+    go _            (CoercionTy _)     = [] -- don't count tyfams in coercions,
+                                            -- as they never get normalized,
+                                            -- anyway
+
+-- | In an application of a 'TyCon' to some arguments, find the outermost
+-- occurrences of type family applications within the arguments. This function
+-- will not consider the 'TyCon' itself when checking for type family
+-- applications.
+--
+-- See 'tcTyFamInstsAndVis' for more details on how this works (as this
+-- function is called inside of 'tcTyFamInstsAndVis').
+tcTyConAppTyFamInstsAndVis :: TyCon -> [Type] -> [(Bool, TyCon, [Type])]
+tcTyConAppTyFamInstsAndVis = tcTyConAppTyFamInstsAndVisX False
+
+tcTyConAppTyFamInstsAndVisX
+  :: Bool -- ^ Is this an invisible argument to some type application?
+  -> TyCon -> [Type] -> [(Bool, TyCon, [Type])]
+tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys =
+  let (invis_tys, vis_tys) = partitionInvisibleTypes tc tys
+  in concat $ map (tcTyFamInstsAndVisX True)         invis_tys
+           ++ map (tcTyFamInstsAndVisX is_invis_arg) vis_tys
 
 isTyFamFree :: Type -> Bool
 -- ^ Check that a type does not contain any type family applications.