[Git][ghc/ghc][master] Print more info about kinds in error messages

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Sat Mar 23 04:22:55 UTC 2024



Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
b72705e9 by Simon Peyton Jones at 2024-03-23T00:22:04-04:00
Print more info about kinds in error messages

This fixes #24553, where GHC unhelpfully said

  error: [GHC-83865]
    • Expected kind ‘* -> * -> *’, but ‘Foo’ has kind ‘* -> * -> *’

See Note [Showing invisible bits of types in error messages]

- - - - -


13 changed files:

- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/TyCo/Ppr.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Utils/TcType.hs
- + testsuite/tests/typecheck/should_fail/T24553.hs
- + testsuite/tests/typecheck/should_fail/T24553.stderr
- testsuite/tests/typecheck/should_fail/all.T


Changes:

=====================================
compiler/GHC/Core/Map/Type.hs
=====================================
@@ -228,7 +228,7 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) =
     andEq TEQX e = hasCast e
     andEq TEQ  e = e
 
-    -- See Note [Comparing nullary type synonyms] in GHC.Core.Type
+    -- See Note [Comparing nullary type synonyms] in GHC.Core.TyCo.Compare
     go (D _ (TyConApp tc1 [])) (D _ (TyConApp tc2 []))
       | tc1 == tc2
       = TEQ


=====================================
compiler/GHC/Core/TyCo/Compare.hs
=====================================
@@ -12,8 +12,9 @@ module GHC.Core.TyCo.Compare (
     nonDetCmpTypesX, nonDetCmpTc,
     eqVarBndrs,
 
-    pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, tcEqTypeVis,
+    pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck,
     tcEqTyConApps,
+    mayLookIdentical,
 
    -- * Visiblity comparision
    eqForAllVis, cmpForAllVis
@@ -22,7 +23,8 @@ module GHC.Core.TyCo.Compare (
 
 import GHC.Prelude
 
-import GHC.Core.Type( typeKind, coreView, tcSplitAppTyNoView_maybe, splitAppTyNoView_maybe )
+import GHC.Core.Type( typeKind, coreView, tcSplitAppTyNoView_maybe, splitAppTyNoView_maybe
+                    , isLevityTy, isRuntimeRepTy, isMultiplicityTy )
 
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.FVs
@@ -129,52 +131,119 @@ Cabal.
 See #19226.
 -}
 
+mayLookIdentical :: Type -> Type -> Bool
+-- | Returns True if the /visible/ part of the types
+-- might look equal, even if they are really unequal (in the invisible bits)
+--
+-- This function is very similar to tc_eq_type but it is much more
+-- heuristic.  Notably, it is always safe to return True, even with types
+-- that might (in truth) be unequal  -- this affects error messages only
+-- (Originally there were one function with an extra flag, but the result
+--  was hard to understand.)
+mayLookIdentical orig_ty1 orig_ty2
+  = go orig_env orig_ty1 orig_ty2
+  where
+    orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
+
+    go :: RnEnv2 -> Type -> Type -> Bool
+    -- See Note [Comparing nullary type synonyms]
+    go _  (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 = True
+
+    go env t1 t2 | Just t1' <- coreView t1 = go env t1' t2
+    go env t1 t2 | Just t2' <- coreView t2 = go env t1 t2'
+
+    go env (TyVarTy tv1)   (TyVarTy tv2)   = rnOccL env tv1 == rnOccR env tv2
+    go _   (LitTy lit1)    (LitTy lit2)    = lit1 == lit2
+    go env (CastTy t1 _)   t2              = go env t1 t2
+    go env t1              (CastTy t2 _)   = go env t1 t2
+    go _   (CoercionTy {}) (CoercionTy {}) = True
+
+    go env (ForAllTy (Bndr tv1 vis1) ty1)
+           (ForAllTy (Bndr tv2 vis2) ty2)
+      =  vis1 `eqForAllVis` vis2  -- See Note [ForAllTy and type equality]
+      && go (rnBndr2 env tv1 tv2) ty1 ty2
+         -- Visible stuff only: ignore kinds of binders
+
+    -- If we have (forall (r::RunTimeRep). ty1  ~   blah) then respond
+    -- with True.  Reason: the type pretty-printer defaults RuntimeRep
+    -- foralls (see Ghc.Iface.Type.hideNonStandardTypes).  That can make,
+    -- say (forall r. TYPE r -> Type) into (Type -> Type), so it looks the
+    -- same as a very different type (#24553).  By responding True, we
+    -- tell GHC (see calls of mayLookIdentical) to display without defaulting.
+    -- See Note [Showing invisible bits of types in error messages]
+    -- in GHC.Tc.Errors.Ppr
+    go _ (ForAllTy b _) _ | isDefaultableBndr b = True
+    go _ _ (ForAllTy b _) | isDefaultableBndr b = True
+
+    go env (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2)
+      = go env arg1 arg2 && go env res1 res2 && go env w1 w2
+        -- Visible stuff only: ignore agg kinds
+
+      -- See Note [Equality on AppTys] in GHC.Core.Type
+    go env (AppTy s1 t1) ty2
+      | Just (s2, t2) <- tcSplitAppTyNoView_maybe ty2
+      = go env s1 s2 && go env t1 t2
+    go env ty1 (AppTy s2 t2)
+      | Just (s1, t1) <- tcSplitAppTyNoView_maybe ty1
+      = go env s1 s2 && go env t1 t2
+
+    go env (TyConApp tc1 ts1)   (TyConApp tc2 ts2)
+      = tc1 == tc2 && gos env (tyConBinders tc1) ts1 ts2
+
+    go _ _ _ = False
+
+    gos :: RnEnv2 -> [TyConBinder] -> [Type] -> [Type] -> Bool
+    gos _   _         []       []      = True
+    gos env bs (t1:ts1) (t2:ts2)
+      | (invisible, bs') <- case bs of
+                               []     -> (False,                    [])
+                               (b:bs) -> (isInvisibleTyConBinder b, bs)
+      = (invisible || go env t1 t2) && gos env bs' ts1 ts2
+
+    gos _ _ _ _ = False
+
+
 -- | Type equality comparing both visible and invisible arguments and expanding
 -- type synonyms.
 tcEqTypeNoSyns :: Type -> Type -> Bool
-tcEqTypeNoSyns ta tb = tc_eq_type False False ta tb
-
--- | Like 'tcEqType', but returns True if the /visible/ part of the types
--- are equal, even if they are really unequal (in the invisible bits)
-tcEqTypeVis :: Type -> Type -> Bool
-tcEqTypeVis ty1 ty2 = tc_eq_type False True ty1 ty2
+tcEqTypeNoSyns ta tb = tc_eq_type False ta tb
 
 -- | Like 'pickyEqTypeVis', but returns a Bool for convenience
 pickyEqType :: Type -> Type -> Bool
 -- Check when two types _look_ the same, _including_ synonyms.
 -- So (pickyEqType String [Char]) returns False
 -- This ignores kinds and coercions, because this is used only for printing.
-pickyEqType ty1 ty2 = tc_eq_type True False ty1 ty2
+pickyEqType ty1 ty2 = tc_eq_type True ty1 ty2
 
 -- | Real worker for 'tcEqType'. No kind check!
 tc_eq_type :: Bool          -- ^ True <=> do not expand type synonyms
-           -> Bool          -- ^ True <=> compare visible args only
            -> Type -> Type
            -> Bool
 -- Flags False, False is the usual setting for tc_eq_type
 -- See Note [Computing equality on types] in Type
-tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
+{-# INLINE tc_eq_type #-} -- See Note [Specialising tc_eq_type].
+tc_eq_type keep_syns orig_ty1 orig_ty2
   = go orig_env orig_ty1 orig_ty2
   where
+    orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
+
     go :: RnEnv2 -> Type -> Type -> Bool
-    -- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
-    go _   (TyConApp tc1 []) (TyConApp tc2 [])
-      | tc1 == tc2
-      = True
+    -- See Note [Comparing nullary type synonyms]
+    go _ (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 = True
 
     go env t1 t2 | not keep_syns, Just t1' <- coreView t1 = go env t1' t2
     go env t1 t2 | not keep_syns, Just t2' <- coreView t2 = go env t1 t2'
 
-    go env (TyVarTy tv1) (TyVarTy tv2)
-      = rnOccL env tv1 == rnOccR env tv2
-
-    go _   (LitTy lit1) (LitTy lit2)
-      = lit1 == lit2
+    go env (TyVarTy tv1)   (TyVarTy tv2)   = rnOccL env tv1 == rnOccR env tv2
+    go _   (LitTy lit1)    (LitTy lit2)    = lit1 == lit2
+    go env (CastTy t1 _)   t2              = go env t1 t2
+    go env t1              (CastTy t2 _)   = go env t1 t2
+    go _   (CoercionTy {}) (CoercionTy {}) = True
 
     go env (ForAllTy (Bndr tv1 vis1) ty1)
            (ForAllTy (Bndr tv2 vis2) ty2)
       =  vis1 `eqForAllVis` vis2  -- See Note [ForAllTy and type equality]
-      && (vis_only || go env (varType tv1) (varType tv2))
+      && go env (varType tv1) (varType tv2)
       && go (rnBndr2 env tv1 tv2) ty1 ty2
 
     -- Make sure we handle all FunTy cases since falling through to the
@@ -183,11 +252,9 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
     -- See Note [Equality on FunTys] in GHC.Core.TyCo.Rep: we must check
     -- kinds here
     go env (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2)
-      = kinds_eq && go env arg1 arg2 && go env res1 res2 && go env w1 w2
-      where
-        kinds_eq | vis_only  = True
-                 | otherwise = go env (typeKind arg1) (typeKind arg2) &&
-                               go env (typeKind res1) (typeKind res2)
+      = go env (typeKind arg1) (typeKind arg2) &&
+        go env (typeKind res1) (typeKind res2) &&
+        go env arg1 arg2 && go env res1 res2 && go env w1 w2
 
       -- See Note [Equality on AppTys] in GHC.Core.Type
     go env (AppTy s1 t1)        ty2
@@ -198,32 +265,24 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
       = go env s1 s2 && go env t1 t2
 
     go env (TyConApp tc1 ts1)   (TyConApp tc2 ts2)
-      = tc1 == tc2 && gos env (tc_vis tc1) ts1 ts2
-
-    go env (CastTy t1 _)   t2              = go env t1 t2
-    go env t1              (CastTy t2 _)   = go env t1 t2
-    go _   (CoercionTy {}) (CoercionTy {}) = True
+      = tc1 == tc2 && gos env ts1 ts2
 
     go _ _ _ = False
 
-    gos _   _         []       []      = True
-    gos env (ig:igs) (t1:ts1) (t2:ts2) = (ig || go env t1 t2)
-                                      && gos env igs ts1 ts2
-    gos _ _ _ _ = False
+    gos _   []       []       = True
+    gos env (t1:ts1) (t2:ts2) = go env t1 t2 && gos env ts1 ts2
+    gos _ _ _                 = False
 
-    tc_vis :: TyCon -> [Bool]  -- True for the fields we should ignore
-    tc_vis tc | vis_only  = inviss ++ repeat False    -- Ignore invisibles
-              | otherwise = repeat False              -- Ignore nothing
-       -- The repeat False is necessary because tycons
-       -- can legitimately be oversaturated
-      where
-        bndrs = tyConBinders tc
-        inviss  = map isInvisibleTyConBinder bndrs
-
-    orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
-
-{-# INLINE tc_eq_type #-} -- See Note [Specialising tc_eq_type].
 
+isDefaultableBndr :: ForAllTyBinder -> Bool
+-- This function should line up with the defaulting done
+--   by GHC.Iface.Type.defaultIfaceTyVarsOfKind
+-- See Note [Showing invisible bits of types in error messages]
+--   in GHC.Tc.Errors.Ppr
+isDefaultableBndr (Bndr tv vis)
+  = isInvisibleForAllTyFlag vis && is_defaultable (tyVarKind tv)
+  where
+    is_defaultable ki = isLevityTy ki || isRuntimeRepTy ki  || isMultiplicityTy ki
 
 -- | Do these denote the same level of visibility? 'Required'
 -- arguments are visible, others are not. So this function
@@ -543,7 +602,7 @@ nonDetCmpTypeX env orig_t1 orig_t2 =
     -- Returns both the resulting ordering relation between
     -- the two types and whether either contains a cast.
     go :: RnEnv2 -> Type -> Type -> TypeOrdering
-    -- See Note [Comparing nullary type synonyms].
+    -- See Note [Comparing nullary type synonyms]
     go _   (TyConApp tc1 []) (TyConApp tc2 [])
       | tc1 == tc2
       = TEQ


=====================================
compiler/GHC/Core/TyCo/Ppr.hs
=====================================
@@ -14,7 +14,7 @@ module GHC.Core.TyCo.Ppr
         pprTyVar, pprTyVars,
         pprThetaArrowTy, pprClassPred,
         pprKind, pprParendKind, pprTyLit,
-        pprDataCons, pprWithExplicitKindsWhen,
+        pprDataCons, pprWithInvisibleBitsWhen,
         pprWithTYPE, pprSourceTyCon,
 
 
@@ -330,13 +330,14 @@ pprTypeApp tc tys
     -- TODO: toIfaceTcArgs seems rather wasteful here
 
 ------------------
--- | Display all kind information (with @-fprint-explicit-kinds@) when the
--- provided 'Bool' argument is 'True'.
--- See @Note [Kind arguments in error messages]@ in "GHC.Tc.Errors".
-pprWithExplicitKindsWhen :: Bool -> SDoc -> SDoc
-pprWithExplicitKindsWhen b
+-- | Display all foralls, runtime-reps, and kind information
+-- when provided 'Bool' argument is 'True'.  See GHC.Tc.Errors.Ppr
+-- Note [Showing invisible bits of types in error messages]
+pprWithInvisibleBitsWhen :: Bool -> SDoc -> SDoc
+pprWithInvisibleBitsWhen b
   = updSDocContext $ \ctx ->
-      if b then ctx { sdocPrintExplicitKinds = True }
+      if b then ctx { sdocPrintExplicitKinds   = True
+                    , sdocPrintExplicitRuntimeReps = True }
            else ctx
 
 -- | This variant preserves any use of TYPE in a type, effectively


=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1066,7 +1066,7 @@ unify_ty :: UMEnv
 -- Respects newtypes, PredTypes
 -- See Note [Computing equality on types] in GHC.Core.Type
 unify_ty _env (TyConApp tc1 []) (TyConApp tc2 []) _kco
-  -- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
+  -- See Note [Comparing nullary type synonyms] in GHC.Core.TyCo.Compare
   | tc1 == tc2
   = return ()
 


=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -1189,7 +1189,7 @@ defaultIfaceTyVarsOfKind def_rep def_mult ty = go emptyFsEnv True ty
        -> IfaceType
     go subs True (IfaceForAllTy (Bndr (IfaceTvBndr (var, var_kind)) argf) ty)
      | isInvisibleForAllTyFlag argf  -- Don't default *visible* quantification
-                                -- or we get the mess in #13963
+                                     -- or we get the mess in #13963
      , Just substituted_ty <- check_substitution var_kind
       = let subs' = extendFsEnv subs var substituted_ty
             -- Record that we should replace it with LiftedRep/Lifted/Many,


=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -2094,10 +2094,9 @@ mkMismatchMsg item ty1 ty2 =
   case orig of
     TypeEqOrigin { uo_actual, uo_expected, uo_thing = mb_thing } ->
       (TypeEqMismatch
-        { teq_mismatch_ppr_explicit_kinds = ppr_explicit_kinds
-        , teq_mismatch_item = item
-        , teq_mismatch_ty1  = ty1
-        , teq_mismatch_ty2  = ty2
+        { teq_mismatch_item     = item
+        , teq_mismatch_ty1      = ty1
+        , teq_mismatch_ty2      = ty2
         , teq_mismatch_actual   = uo_actual
         , teq_mismatch_expected = uo_expected
         , teq_mismatch_what     = mb_thing
@@ -2121,25 +2120,6 @@ mkMismatchMsg item ty1 ty2 =
   where
     orig = errorItemOrigin item
     mb_same_occ = sameOccExtras ty2 ty1
-    ppr_explicit_kinds = shouldPprWithExplicitKinds ty1 ty2 orig
-
--- | Whether to print explicit kinds (with @-fprint-explicit-kinds@)
--- in an 'SDoc' when a type mismatch occurs to due invisible kind arguments.
---
--- This function first checks to see if the 'CtOrigin' argument is a
--- 'TypeEqOrigin'. If so, it first checks whether the equality is a visible
--- equality; if it's not, definitely print the kinds. Even if the equality is
--- a visible equality, check the expected/actual types to see if the types
--- have equal visible components. If the 'CtOrigin' is
--- not a 'TypeEqOrigin', fall back on the actual mismatched types themselves.
-shouldPprWithExplicitKinds :: Type -> Type -> CtOrigin -> Bool
-shouldPprWithExplicitKinds _ty1 _ty2 (TypeEqOrigin { uo_actual = act
-                                                   , uo_expected = exp
-                                                   , uo_visible = vis })
-  | not vis   = True                  -- See tests T15870, T16204c
-  | otherwise = tcEqTypeVis act exp   -- See tests T9171, T9144.
-shouldPprWithExplicitKinds ty1 ty2 _ct
-  = tcEqTypeVis ty1 ty2
 
 {- Note [Insoluble mis-match]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2403,29 +2383,6 @@ results in
       in the import of ‘Data.Monoid’
 -}
 
-{-
-Note [Kind arguments in error messages]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It can be terribly confusing to get an error message like (#9171)
-
-    Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
-                with actual type ‘GetParam Base (GetParam Base Int)’
-
-The reason may be that the kinds don't match up.  Typically you'll get
-more useful information, but not when it's as a result of ambiguity.
-
-To mitigate this, GHC attempts to enable the -fprint-explicit-kinds flag
-whenever any error message arises due to a kind mismatch. This means that
-the above error message would instead be displayed as:
-
-    Couldn't match expected type
-                  ‘GetParam @* @k2 @* Base (GetParam @* @* @k2 Base Int)’
-                with actual type
-                  ‘GetParam @* @k20 @* Base (GetParam @* @* @k20 Base Int)’
-
-Which makes it clearer that the culprit is the mismatch between `k2` and `k20`.
--}
-
 -----------------------
 -- relevantBindings looks at the value environment and finds values whose
 -- types mention any of the offending type variables.  It has to be


=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -54,8 +54,8 @@ import GHC.Core.ConLike
 import GHC.Core.FamInstEnv ( FamInst(..), famInstAxiom, pprFamInst )
 import GHC.Core.InstEnv
 import GHC.Core.TyCo.Rep (Type(..))
-import GHC.Core.TyCo.Ppr (pprWithExplicitKindsWhen,
-                          pprSourceTyCon, pprTyVars, pprWithTYPE, pprTyVar, pprTidiedType)
+import GHC.Core.TyCo.Ppr (pprWithInvisibleBitsWhen, pprSourceTyCon,
+                          pprTyVars, pprWithTYPE, pprTyVar, pprTidiedType)
 import GHC.Core.PatSyn ( patSynName, pprPatSynType )
 import GHC.Core.Predicate
 import GHC.Core.Type
@@ -536,7 +536,7 @@ instance Diagnostic TcRnMessage where
                                 , text "cannot be inferred from the right-hand side." ]
                      in (injectivityErrorHerald $$ body $$ text "In the type family equation:", show_kinds)
 
-         in mkSimpleDecorated $ pprWithExplicitKindsWhen show_kinds $
+         in mkSimpleDecorated $ pprWithInvisibleBitsWhen show_kinds $
               hang herald
                 2 (vcat (map (pprCoAxBranchUser fam_tc) (eqn1 : rest_eqns)))
     TcRnBangOnUnliftedType ty
@@ -1182,7 +1182,7 @@ instance Diagnostic TcRnMessage where
                 ppr con <+> dcolon <+> ppr (dataConDisplayType True con))
               IsGADT ->
                 (text "A newtype must not be a GADT",
-                ppr con <+> dcolon <+> pprWithExplicitKindsWhen sneaky_eq_spec
+                ppr con <+> dcolon <+> pprWithInvisibleBitsWhen sneaky_eq_spec
                                        (ppr $ dataConDisplayType show_linear_types con))
               HasConstructorContext ->
                 (text "A newtype constructor must not have a context in its type",
@@ -1432,7 +1432,7 @@ instance Diagnostic TcRnMessage where
             , text "Perhaps enable PolyKinds or add a kind signature" ])
     TcRnUninferrableTyVar tidied_tvs context ->
       mkSimpleDecorated $
-      pprWithExplicitKindsWhen True $
+      pprWithInvisibleBitsWhen True $
       vcat [ text "Uninferrable type variable"
               <> plural tidied_tvs
               <+> pprWithCommas pprTyVar tidied_tvs
@@ -1440,7 +1440,7 @@ instance Diagnostic TcRnMessage where
             , pprUninferrableTyVarCtx context ]
     TcRnSkolemEscape escapees tv orig_ty ->
       mkSimpleDecorated $
-      pprWithExplicitKindsWhen True $
+      pprWithInvisibleBitsWhen True $
       vcat [ sep [ text "Cannot generalise type; skolem" <> plural escapees
                 , quotes $ pprTyVars escapees
                 , text "would escape" <+> itsOrTheir escapees <+> text "scope"
@@ -1884,7 +1884,7 @@ instance Diagnostic TcRnMessage where
 
     TcRnInvalidDefaultedTyVar wanteds proposal bad_tvs ->
       mkSimpleDecorated $
-      pprWithExplicitKindsWhen True $
+      pprWithInvisibleBitsWhen True $
       vcat [ text "Invalid defaulting proposal."
            , hang (text "The following type variable" <> plural (NE.toList bad_tvs) <+> text "cannot be defaulted, as" <+> why <> colon)
                 2 (pprQuotedList (NE.toList bad_tvs))
@@ -4146,17 +4146,18 @@ pprMismatchMsg _
               | otherwise       = text "kind" <+> quotes (ppr exp)
 
 pprMismatchMsg ctxt
-  (TypeEqMismatch { teq_mismatch_ppr_explicit_kinds = ppr_explicit_kinds
-                  , teq_mismatch_item     = item
+  (TypeEqMismatch { teq_mismatch_item     = item
                   , teq_mismatch_ty1      = ty1   -- These types are the actual types
                   , teq_mismatch_ty2      = ty2   --   that don't match; may be swapped
                   , teq_mismatch_expected = exp   -- These are the context of
                   , teq_mismatch_actual   = act   --   the mis-match
                   , teq_mismatch_what     = mb_thing
                   , teq_mb_same_occ       = mb_same_occ })
-  = addArising ct_loc $ pprWithExplicitKindsWhen ppr_explicit_kinds msg
-  $$ maybe empty pprSameOccInfo mb_same_occ
+  = addArising ct_loc $
+    pprWithInvisibleBitsWhen ppr_invis_bits msg
+    $$ maybe empty pprSameOccInfo mb_same_occ
   where
+
     msg | Just (torc, rep) <- sORTKind_maybe exp
         = msg_for_exp_sort torc rep
 
@@ -4219,6 +4220,7 @@ pprMismatchMsg ctxt
     ct_loc = errorItemCtLoc item
     orig   = errorItemOrigin item
     level  = ctLocTypeOrKind_maybe ct_loc `orElse` TypeLevel
+    ppr_invis_bits = shouldPprWithInvisibleBits ty1 ty2 orig
 
     num_args_msg = case level of
       KindLevel
@@ -4310,6 +4312,60 @@ pprMismatchMsg ctxt (CouldNotDeduce useful_givens (item :| others) mb_extra)
         _        -> pprTheta wanteds
 
 
+-- | Whether to print explicit kinds (with @-fprint-explicit-kinds@)
+-- in an 'SDoc' when a type mismatch occurs to due invisible parts of the types.
+-- See Note [Showing invisible bits of types in error messages]
+--
+-- This function first checks to see if the 'CtOrigin' argument is a
+-- 'TypeEqOrigin'. If so, it first checks whether the equality is a visible
+-- equality; if it's not, definitely print the kinds. Even if the equality is
+-- a visible equality, check the expected/actual types to see if the types
+-- have equal visible components. If the 'CtOrigin' is
+-- not a 'TypeEqOrigin', fall back on the actual mismatched types themselves.
+shouldPprWithInvisibleBits :: Type -> Type -> CtOrigin -> Bool
+shouldPprWithInvisibleBits _ty1 _ty2 (TypeEqOrigin { uo_actual = act
+                                                   , uo_expected = exp
+                                                   , uo_visible = vis })
+  | not vis   = True                  -- See tests T15870, T16204c
+  | otherwise = mayLookIdentical act exp   -- See tests T9171, T9144.
+shouldPprWithInvisibleBits ty1 ty2 _ct
+  = mayLookIdentical ty1 ty2
+
+{- Note [Showing invisible bits of types in error messages]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It can be terribly confusing to get an error message like (#9171)
+
+    Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
+                with actual type ‘GetParam Base (GetParam Base Int)’
+
+The reason may be that the kinds don't match up.  Typically you'll get
+more useful information, but not when it's as a result of ambiguity.
+
+To mitigate this, when we find a type or kind mis-match:
+
+* See if normally-visible parts of the type would make the two types
+  look different.  This check is made by
+  `GHC.Core.TyCo.Compare.mayLookIdentical`
+
+* If not, display the types with their normally-visible parts made visible,
+  by setting flags in the `SDocContext":
+  Specifically:
+    - Display kind arguments: sdocPrintExplicitKinds
+    - Don't default away runtime-reps: sdocPrintExplicitRuntimeReps,
+           which controls `GHC.Iface.Type.hideNonStandardTypes`
+  (NB: foralls are always printed by pprType, it turns out.)
+
+As a result the above error message would instead be displayed as:
+
+    Couldn't match expected type
+                  ‘GetParam @* @k2 @* Base (GetParam @* @* @k2 Base Int)’
+                with actual type
+                  ‘GetParam @* @k20 @* Base (GetParam @* @* @k20 Base Int)’
+
+Which makes it clearer that the culprit is the mismatch between `k2` and `k20`.
+
+Another example of what goes wrong without this: #24553.
+-}
 
 {- *********************************************************************
 *                                                                      *
@@ -6033,7 +6089,7 @@ pprIllegalInstance = \case
   IllegalFamilyInstance reason ->
     pprIllegalFamilyInstance reason
   IllegalFamilyApplicationInInstance inst_ty invis_arg tf_tc tf_args ->
-    pprWithExplicitKindsWhen invis_arg $
+    pprWithInvisibleBitsWhen invis_arg $
       hang (text "Illegal type synonym family application"
               <+> quotes (ppr tf_ty) <+> text "in instance" <> colon)
          2 (ppr inst_ty)
@@ -6116,7 +6172,7 @@ pprNotCovered clas
   , not_covered_invis_vis_tvs = undetermined_tvs
   , not_covered_liberal       = which_cc_failed
   } =
-  pprWithExplicitKindsWhen (isEmptyVarSet $ pSnd undetermined_tvs) $
+  pprWithInvisibleBitsWhen (isEmptyVarSet $ pSnd undetermined_tvs) $
     vcat [ sep [ text "The"
                   <+> ppWhen liberal (text "liberal")
                   <+> text "coverage condition fails in class"
@@ -6378,7 +6434,7 @@ pprInvalidAssocInstance = \case
         , text "mentions none of the type or kind variables of the class" <+>
                 quotes (ppr cls <+> hsep (map ppr (classTyVars cls)))]
   AssocTyVarsDontMatch vis fam_tc exp_tys act_tys ->
-    pprWithExplicitKindsWhen (isInvisibleForAllTyFlag vis) $
+    pprWithInvisibleBitsWhen (isInvisibleForAllTyFlag vis) $
     vcat [ text "Type indexes must match class instance head"
          , text "Expected:" <+> pp exp_tys
          , text "  Actual:" <+> pp act_tys ]
@@ -6402,7 +6458,7 @@ pprInvalidAssocDefault = \case
             let (pat_tv, pat_vis) = NE.head dups
             in (pat_vis,
                 text "Illegal duplicate variable" <+> quotes (ppr pat_tv) <+> text "in:")
-    in pprWithExplicitKindsWhen (isInvisibleForAllTyFlag pat_vis) $
+    in pprWithInvisibleBitsWhen (isInvisibleForAllTyFlag pat_vis) $
          hang main_msg
             2 (vcat [ppr_eqn, suggestion])
     where


=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -5508,8 +5508,7 @@ data MismatchMsg
   --
   -- Test cases: T1470, tcfail212.
   | TypeEqMismatch
-      { teq_mismatch_ppr_explicit_kinds :: Bool
-      , teq_mismatch_item     :: ErrorItem
+      { teq_mismatch_item     :: ErrorItem
       , teq_mismatch_ty1      :: Type
       , teq_mismatch_ty2      :: Type
       , teq_mismatch_expected :: Type -- ^ The overall expected type


=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -311,7 +311,7 @@ can_eq_nc
    -> Type -> Type    -- RHS, after and before type-synonym expansion, resp
    -> TcS (StopOrContinue (Either IrredCt EqCt))
 
--- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
+-- See Note [Comparing nullary type synonyms] in GHC.Core.TyCo.Compare
 can_eq_nc _flat _rdr_env _envs ev eq_rel ty1@(TyConApp tc1 []) _ps_ty1 (TyConApp tc2 []) _ps_ty2
   | tc1 == tc2
   = canEqReflexive ev eq_rel ty1


=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -95,7 +95,7 @@ module GHC.Tc.Utils.TcType (
   -- Re-exported from GHC.Core.TyCo.Compare
   -- mainly just for back-compat reasons
   eqType, eqTypes, nonDetCmpType, nonDetCmpTypes, eqTypeX,
-  pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, tcEqTypeVis,
+  pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, mayLookIdentical,
   tcEqTyConApps, eqForAllVis, eqVarBndrs,
 
   ---------------------------------
@@ -888,7 +888,8 @@ tcTyFamInsts = map (\(_,b,c) -> (b,c)) . tcTyFamInstsAndVis
 -- to @C@, whereas @F Bool@ is paired with 'False' since it appears an a
 -- /visible/ argument to @C at .
 --
--- See also @Note [Kind arguments in error messages]@ in "GHC.Tc.Errors".
+-- See also Note [Showing invisible bits of types in error messages]
+-- in "GHC.Tc.Errors.Ppr".
 tcTyFamInstsAndVis :: Type -> [(Bool, TyCon, [Type])]
 tcTyFamInstsAndVis = tcTyFamInstsAndVisX False
 


=====================================
testsuite/tests/typecheck/should_fail/T24553.hs
=====================================
@@ -0,0 +1,8 @@
+module T24553 where
+
+import GHC.Exts
+
+type Foo :: * -> forall r. TYPE r -> *
+newtype Foo m a = MkFoo ()
+
+type Bar = Foo :: forall r. * -> TYPE r -> *


=====================================
testsuite/tests/typecheck/should_fail/T24553.stderr
=====================================
@@ -0,0 +1,6 @@
+
+T24553.hs:8:12: error: [GHC-83865]
+    • Expected kind ‘forall (r :: RuntimeRep). * -> TYPE r -> *’,
+        but ‘Foo’ has kind ‘* -> forall (r :: RuntimeRep). TYPE r -> *’
+    • In the type ‘Foo :: forall r. * -> TYPE r -> *’
+      In the type declaration for ‘Bar’


=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -724,3 +724,5 @@ test('T17594d', normal, compile_fail, [''])
 test('T17594g', normal, compile_fail, [''])
 
 test('T24470a', normal, compile_fail, [''])
+test('T24553', normal, compile_fail, [''])
+



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b72705e9b2ae5575aef92ede6ff975bbbe43004d

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b72705e9b2ae5575aef92ede6ff975bbbe43004d
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240323/3255391c/attachment-0001.html>


More information about the ghc-commits mailing list