Fix #16517 by bumping the TcLevel for method sigs
authorRichard Eisenberg <rae@richarde.dev>
Wed, 5 Jun 2019 22:02:13 +0000 (18:02 -0400)
committerBen Gamari <ben@smart-cactus.org>
Wed, 19 Jun 2019 16:39:50 +0000 (12:39 -0400)
There were actually two bugs fixed here:

1. candidateQTyVarsOfType needs to be careful that it does not
   try to zap metavariables from an outer scope as "naughty"
   quantification candidates. This commit adds a simple check
   to avoid doing so.

2. We weren't bumping the TcLevel in kcHsKindSig, which was used
   only for class method sigs. This mistake led to the acceptance
   of

     class C a where
       meth :: forall k. Proxy (a :: k) -> ()

   Note that k is *locally* quantified. This patch fixes the
   problem by using tcClassSigType, which correctly bumps the
   level. It's a bit inefficient because tcClassSigType does other
   work, too, but it would be tedious to repeat much of the code
   there with only a few changes. This version works well and is
   simple.

And, while updating comments, etc., I noticed that tcRnType was
missing a pushTcLevel, leading to #16767, which this patch also
fixes, by bumping the level. In the refactoring here, I also
use solveEqualities. This initially failed ghci/scripts/T15415,
but that was fixed by teaching solveEqualities to respect
-XPartialTypeSignatures.

This patch also cleans up some Notes around error generation that
came up in conversation.

Test case: typecheck/should_fail/T16517, ghci/scripts/T16767

(cherry picked from commit a22e51ea6f7a046c87d57ce30d143eef6abee9ff)
(cherry picked from commit 19ab32c5fb3ebd88927b94acf6b348facc1552a2)

16 files changed:
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
testsuite/tests/ghci/scripts/T16767.script [new file with mode: 0644]
testsuite/tests/ghci/scripts/T16767.stdout [new file with mode: 0644]
testsuite/tests/ghci/scripts/all.T
testsuite/tests/typecheck/should_fail/T16517.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T16517.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/all.T
testsuite/tests/typecheck/should_fail/tcfail134.stderr

index d643925..740038e 100644 (file)
@@ -2079,13 +2079,6 @@ What do we do when we have an equality
 
 where k1 and k2 differ? This Note explores this treacherous area.
 
-First off, the question above is slightly the wrong question. Flattening
-a tyvar will flatten its kind (Note [Flattening] in TcFlatten); flattening
-the kind might introduce a cast. So we might have a casted tyvar on the
-left. We thus revise our test case to
-
-  (tv |> co :: k1) ~ (rhs :: k2)
-
 We must proceed differently here depending on whether we have a Wanted
 or a Given. Consider this:
 
@@ -2109,36 +2102,33 @@ The reason for this odd behavior is much the same as
 Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the
 new `co` is a Wanted.
 
-   The solution is then not to use `co` to "rewrite" -- that is, cast
-   -- `w`, but instead to keep `w` heterogeneous and
-   irreducible. Given that we're not using `co`, there is no reason to
-   collect evidence for it, so `co` is born a Derived, with a CtOrigin
-   of KindEqOrigin.
+The solution is then not to use `co` to "rewrite" -- that is, cast -- `w`, but
+instead to keep `w` heterogeneous and irreducible. Given that we're not using
+`co`, there is no reason to collect evidence for it, so `co` is born a
+Derived, with a CtOrigin of KindEqOrigin. When the Derived is solved (by
+unification), the original wanted (`w`) will get kicked out. We thus get
 
-When the Derived is solved (by unification), the original wanted (`w`)
-will get kicked out.
+[D] _ :: k ~ Type
+[W] w :: (alpha :: k) ~ (Int :: Type)
 
-Note that, if we had [G] co1 :: k ~ Type available, then none of this code would
-trigger, because flattening would have rewritten k to Type. That is,
-`w` would look like [W] (alpha |> co1 :: Type) ~ (Int :: Type), and the tyvar
-case will trigger, correctly rewriting alpha to (Int |> sym co1).
+Note that the Wanted is unchanged and will be irreducible. This all happens
+in canEqTyVarHetero.
+
+Note that, if we had [G] co1 :: k ~ Type available, then we never get
+to canEqTyVarHetero: canEqTyVar tries flattening the kinds first. If
+we have [G] co1 :: k ~ Type, then flattening the kind of alpha would
+rewrite k to Type, and we would end up in canEqTyVarHomo.
 
 Successive canonicalizations of the same Wanted may produce
 duplicate Deriveds. Similar duplications can happen with fundeps, and there
 seems to be no easy way to avoid. I expect this case to be rare.
 
-For Givens, this problem doesn't bite, so a heterogeneous Given gives
+For Givens, this problem (the Wanteds-rewriting-Wanteds action of
+a kind coercion) doesn't bite, so a heterogeneous Given gives
 rise to a Given kind equality. No Deriveds here. We thus homogenise
-the Given (see the "homo_co" in the Given case in canEqTyVar) and
+the Given (see the "homo_co" in the Given case in canEqTyVarHetero) and
 carry on with a homogeneous equality constraint.
 
-Separately, I (Richard E) spent some time pondering what to do in the case
-that we have [W] (tv |> co1 :: k1) ~ (tv |> co2 :: k2) where k1 and k2
-differ. Note that the tv is the same. (This case is handled as the first
-case in canEqTyVarHomo.) At one point, I thought we could solve this limited
-form of heterogeneous Wanted, but I then reconsidered and now treat this case
-just like any other heterogeneous Wanted.
-
 Note [Type synonyms and canonicalization]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We treat type synonym applications as xi types, that is, they do not
index df307f2..62d918a 100644 (file)
@@ -158,14 +158,22 @@ reportUnsolved wanted
 -- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
 -- However, do not make any evidence bindings, because we don't
 -- have any convenient place to put them.
+-- NB: Type-level holes are OK, because there are no bindings.
 -- See Note [Deferring coercion errors to runtime]
 -- Used by solveEqualities for kind equalities
---      (see Note [Fail fast on kind errors] in TcSimplify]
+--      (see Note [Fail fast on kind errors] in TcSimplify)
 -- and for simplifyDefault.
 reportAllUnsolved :: WantedConstraints -> TcM ()
 reportAllUnsolved wanted
   = do { ev_binds <- newNoTcEvBinds
-       ; report_unsolved TypeError HoleError HoleError HoleError
+
+       ; partial_sigs      <- xoptM LangExt.PartialTypeSignatures
+       ; warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
+       ; let type_holes | not partial_sigs  = HoleError
+                        | warn_partial_sigs = HoleWarn
+                        | otherwise         = HoleDefer
+
+       ; report_unsolved TypeError HoleError type_holes HoleError
                          ev_binds wanted }
 
 -- | Report all unsolved goals as warnings (but without deferring any errors to
index 5f3750f..5c268c0 100644 (file)
@@ -11,7 +11,7 @@
 
 module TcHsType (
         -- Type signatures
-        kcHsSigType, tcClassSigType,
+        kcClassSigType, tcClassSigType,
         tcHsSigType, tcHsSigWcType,
         tcHsPartialSigType,
         funsSigCtxt, addSigCtxt, pprSigCtxt,
@@ -187,24 +187,40 @@ tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
 -- already checked this, so we can simply ignore it.
 tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
 
-kcHsSigType :: [Located Name] -> LHsSigType GhcRn -> TcM ()
-kcHsSigType names (HsIB { hsib_body = hs_ty
-                                  , hsib_ext = sig_vars })
-  = addSigCtxt (funsSigCtxt names) hs_ty $
-    discardResult $
-    bindImplicitTKBndrs_Skol sig_vars $
-    tc_lhs_type typeLevelMode hs_ty liftedTypeKind
-
-kcHsSigType _ (XHsImplicitBndrs _) = panic "kcHsSigType"
+kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
+kcClassSigType skol_info names sig_ty
+  = discardResult $
+    tcClassSigType skol_info names sig_ty
+  -- tcClassSigType does a fair amount of extra work that we don't need,
+  -- such as ordering quantified variables. But we absolutely do need
+  -- to push the level when checking method types and solve local equalities,
+  -- and so it seems easier just to call tcClassSigType than selectively
+  -- extract the lines of code from tc_hs_sig_type that we really need.
+  -- If we don't push the level, we get #16517, where GHC accepts
+  --   class C a where
+  --     meth :: forall k. Proxy (a :: k) -> ()
+  -- Note that k is local to meth -- this is hogwash.
 
 tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
 -- Does not do validity checking
 tcClassSigType skol_info names sig_ty
   = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
-    tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
+    snd <$> tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
        -- Do not zonk-to-Type, nor perform a validity check
        -- We are in a knot with the class and associated types
        -- Zonking and validity checking is done by tcClassDecl
+       -- No need to fail here if the type has an error:
+       --   If we're in the kind-checking phase, the solveEqualities
+       --     in kcTyClGroup catches the error
+       --   If we're in the type-checking phase, the solveEqualities
+       --     in tcClassDecl1 gets it
+       -- Failing fast here degrades the error message in, e.g., tcfail135:
+       --   class Foo f where
+       --     baa :: f a -> f
+       -- If we fail fast, we're told that f has kind `k1` when we wanted `*`.
+       -- It should be that f has kind `k2 -> *`, but we never get a chance
+       -- to run the solver where the kind of f is touchable. This is
+       -- painfully delicate.
 
 tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
 -- Does validity checking
@@ -214,10 +230,13 @@ tcHsSigType ctxt sig_ty
     do { traceTc "tcHsSigType {" (ppr sig_ty)
 
           -- Generalise here: see Note [Kind generalisation]
-       ; ty <- tc_hs_sig_type skol_info sig_ty
-                                      (expectedKindInCtxt ctxt)
+       ; (insol, ty) <- tc_hs_sig_type skol_info sig_ty
+                                       (expectedKindInCtxt ctxt)
        ; ty <- zonkTcType ty
 
+       ; when insol failM
+       -- See Note [Fail fast if there are insoluble kind equalities] in TcSimplify
+
        ; checkValidType ctxt ty
        ; traceTc "end tcHsSigType }" (ppr ty)
        ; return ty }
@@ -225,12 +244,14 @@ tcHsSigType ctxt sig_ty
     skol_info = SigTypeSkol ctxt
 
 tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
-               -> ContextKind -> TcM Type
+               -> ContextKind -> TcM (Bool, TcType)
 -- Kind-checks/desugars an 'LHsSigType',
 --   solve equalities,
 --   and then kind-generalizes.
 -- This will never emit constraints, as it uses solveEqualities interally.
 -- No validity checking or zonking
+-- Returns also a Bool indicating whether the type induced an insoluble constraint;
+-- True <=> constraint is insoluble
 tc_hs_sig_type skol_info hs_sig_type ctxt_kind
   | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
   = do { (tc_lvl, (wanted, (spec_tkvs, ty)))
@@ -249,13 +270,9 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
        ; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs)
                                   tc_lvl wanted
 
-       -- See Note [Fail fast if there are insoluble kind equalities]
-       --     in TcSimplify
-       ; when (insolubleWC wanted) failM
-
-       ; return (mkInvForAllTys kvs ty1) }
+       ; return (insolubleWC wanted, mkInvForAllTys kvs ty1) }
 
-tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
+tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
 
 tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
 -- tcTopLHsType is used for kind-checking top-level HsType where
@@ -2060,7 +2077,8 @@ kindGeneralize :: TcType -> TcM [KindVar]
 -- Quantify the free kind variables of a kind or type
 -- In the latter case the type is closed, so it has no free
 -- type variables.  So in both cases, all the free vars are kind vars
--- Input needn't be zonked.
+-- Input needn't be zonked. All variables to be quantified must
+-- have a TcLevel higher than the ambient TcLevel.
 -- NB: You must call solveEqualities or solveLocalEqualities before
 -- kind generalization
 --
@@ -2078,7 +2096,8 @@ kindGeneralize kind_or_type
 
 -- | This variant of 'kindGeneralize' refuses to generalize over any
 -- variables free in the given WantedConstraints. Instead, it promotes
--- these variables into an outer TcLevel. See also
+-- these variables into an outer TcLevel. All variables to be quantified must
+-- have a TcLevel higher than the ambient TcLevel. See also
 -- Note [Promoting unification variables] in TcSimplify
 kindGeneralizeLocal :: WantedConstraints -> TcType -> TcM [KindVar]
 kindGeneralizeLocal wanted kind_or_type
index ffeb602..ce7c1ee 100644 (file)
@@ -759,14 +759,14 @@ writeMetaTyVar tyvar ty
 
 -- Everything from here on only happens if DEBUG is on
   | not (isTcTyVar tyvar)
-  = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
+  = ASSERT2( False, text "Writing to non-tc tyvar" <+> ppr tyvar )
     return ()
 
   | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
   = writeMetaTyVarRef tyvar ref ty
 
   | otherwise
-  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
+  = ASSERT2( False, text "Writing to non-meta tyvar" <+> ppr tyvar )
     return ()
 
 --------------------
@@ -1066,18 +1066,18 @@ we are trying to generalise this type:
   forall arg. ... (alpha[tau]:arg) ...
 
 We have a metavariable alpha whose kind mentions a skolem variable
-boudn inside the very type we are generalising.
+bound inside the very type we are generalising.
 This can arise while type-checking a user-written type signature
 (see the test case for the full code).
 
 We cannot generalise over alpha!  That would produce a type like
   forall {a :: arg}. forall arg. ...blah...
 The fact that alpha's kind mentions arg renders it completely
-ineligible for generaliation.
+ineligible for generalisation.
 
 However, we are not going to learn any new constraints on alpha,
-because its kind isn't even in scope in the outer context.  So alpha
-is entirely unconstrained.
+because its kind isn't even in scope in the outer context (but see Wrinkle).
+So alpha is entirely unconstrained.
 
 What then should we do with alpha?  During generalization, every
 metavariable is either (A) promoted, (B) generalized, or (C) zapped
@@ -1098,6 +1098,17 @@ We do this eager zapping in candidateQTyVars, which always precedes
 generalisation, because at that moment we have a clear picture of
 what skolems are in scope.
 
+Wrinkle:
+
+We must make absolutely sure that alpha indeed is not
+from an outer context. (Otherwise, we might indeed learn more information
+about it.) This can be done easily: we just check alpha's TcLevel.
+That level must be strictly greater than the ambient TcLevel in order
+to treat it as naughty. We say "strictly greater than" because the call to
+candidateQTyVars is made outside the bumped TcLevel, as stated in the
+comment to candidateQTyVarsOfType. The level check is done in go_tv
+in collect_cant_qtvs. Skipping this check caused #16517.
+
 -}
 
 data CandidatesQTvs
@@ -1145,13 +1156,17 @@ candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
 -- | Gathers free variables to use as quantification candidates (in
 -- 'quantifyTyVars'). This might output the same var
 -- in both sets, if it's used in both a type and a kind.
+-- The variables to quantify must have a TcLevel strictly greater than
+-- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
 -- See Note [CandidatesQTvs determinism and order]
 -- See Note [Dependent type variables]
 candidateQTyVarsOfType :: TcType       -- not necessarily zonked
                        -> TcM CandidatesQTvs
 candidateQTyVarsOfType ty = collect_cand_qtvs False emptyVarSet mempty ty
 
--- | Like 'splitDepVarsOfType', but over a list of types
+-- | Like 'candidateQTyVarsOfType', but over a list of types
+-- The variables to quantify must have a TcLevel strictly greater than
+-- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
 candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs
 candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempty tys
 
@@ -1175,7 +1190,7 @@ delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
 
 collect_cand_qtvs
   :: Bool            -- True <=> consider every fv in Type to be dependent
-  -> VarSet          -- Bound variables (both locally bound and globally bound)
+  -> VarSet          -- Bound variables (locals only)
   -> CandidatesQTvs  -- Accumulating parameter
   -> Type            -- Not necessarily zonked
   -> TcM CandidatesQTvs
@@ -1220,16 +1235,26 @@ collect_cand_qtvs is_dep bound dvs ty
 
     -----------------
     go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
-      | tv `elemDVarSet` kvs = return dv  -- We have met this tyvar aleady
+      | tv `elemDVarSet` kvs
+      = return dv  -- We have met this tyvar aleady
+
       | not is_dep
-      , tv `elemDVarSet` tvs = return dv  -- We have met this tyvar aleady
+      , tv `elemDVarSet` tvs
+      = return dv  -- We have met this tyvar aleady
+
       | otherwise
       = do { tv_kind <- zonkTcType (tyVarKind tv)
                  -- This zonk is annoying, but it is necessary, both to
                  -- ensure that the collected candidates have zonked kinds
                  -- (Trac #15795) and to make the naughty check
                  -- (which comes next) works correctly
-           ; if intersectsVarSet bound (tyCoVarsOfType tv_kind)
+
+           ; cur_lvl <- getTcLevel
+           ; if tcTyVarLevel tv `strictlyDeeperThan` cur_lvl &&
+                   -- this tyvar is from an outer context: see Wrinkle
+                   -- in Note [Naughty quantification candidates]
+
+                intersectsVarSet bound (tyCoVarsOfType tv_kind)
 
              then -- See Note [Naughty quantification candidates]
                   do { traceTc "Zapping naughty quantifier" (pprTyVar tv)
index 36ec8dc..0388f0c 100644 (file)
@@ -2427,12 +2427,13 @@ tcRnType hsc_env normalise rdr_type
         -- It can have any rank or kind
         -- First bring into scope any wildcards
        ; traceTc "tcRnType" (vcat [ppr wcs, ppr rn_type])
-       ; ((ty, kind), lie)  <-
-                       captureConstraints $
+       ; (ty, kind) <- pushTcLevelM_         $
+                        -- must push level to satisfy level precondition of
+                        -- kindGeneralize, below
+                       solveEqualities       $
                        tcWildCardBinders wcs $ \ wcs' ->
                        do { emitWildCardHoleConstraints wcs'
                           ; tcLHsTypeUnsaturated rn_type }
-       ; _ <- checkNoErrs (simplifyInteractive lie)
 
        -- Do kind generalisation; see Note [Kind-generalise in tcRnType]
        ; kind <- zonkTcType kind
index 7c9d70e..ccf2d0d 100644 (file)
@@ -2095,6 +2095,16 @@ see dropDerivedWC.  For example
    [D] Int ~ Bool, and we don't want to report that because it's
    incomprehensible. That is why we don't rewrite wanteds with wanteds!
 
+ * We might float out some Wanteds from an implication, leaving behind
+   their insoluble Deriveds. For example:
+
+   forall a[2]. [W] alpha[1] ~ Int
+                [W] alpha[1] ~ Bool
+                [D] Int ~ Bool
+
+   The Derived is insoluble, but we very much want to drop it when floating
+   out.
+
 But (tiresomely) we do keep *some* Derived constraints:
 
  * Type holes are derived constraints, because they have no evidence
@@ -2103,8 +2113,7 @@ But (tiresomely) we do keep *some* Derived constraints:
  * Insoluble kind equalities (e.g. [D] * ~ (* -> *)), with
    KindEqOrigin, may arise from a type equality a ~ Int#, say.  See
    Note [Equalities with incompatible kinds] in TcCanonical.
-   These need to be kept because the kind equalities might have different
-   source locations and hence different error messages.
+   Keeping these around produces better error messages, in practice.
    E.g., test case dependent/should_fail/T11471
 
  * We keep most derived equalities arising from functional dependencies
index 9e23eca..838fb78 100644 (file)
@@ -154,9 +154,10 @@ solveLocalEqualities callsite thing_inside
        ; emitConstraints wanted
 
        -- See Note [Fail fast if there are insoluble kind equalities]
-       ; if insolubleWC wanted
-         then failM
-         else return res }
+       ; when (insolubleWC wanted) $
+           failM
+
+       ; return res }
 
 {- Note [Fail fast if there are insoluble kind equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
index 7bf5e20..edb91b8 100644 (file)
@@ -1038,9 +1038,11 @@ kcTyClDecl (ClassDecl { tcdLName = (dL->L _ name)
     do  { _ <- tcHsContext ctxt
         ; mapM_ (wrapLocM_ kc_sig) sigs }
   where
-    kc_sig (ClassOpSig _ _ nms op_ty) = kcHsSigType nms op_ty
+    kc_sig (ClassOpSig _ _ nms op_ty) = kcClassSigType skol_info nms op_ty
     kc_sig _                          = return ()
 
+    skol_info = TyConSkol ClassFlavour name
+
 kcTyClDecl (FamDecl _ (FamilyDecl { fdLName  = (dL->L _ fam_tc_name)
                                   , fdInfo   = fd_info }))
 -- closed type families look at their equations, but other families don't
index b2c9b32..c4cc25e 100644 (file)
@@ -516,6 +516,17 @@ superSkolemTv   = SkolemTv topTcLevel True   -- Treat this as a completely disti
                   -- The choice of level number here is a bit dodgy, but
                   -- topTcLevel works in the places that vanillaSkolemTv is used
 
+instance Outputable TcTyVarDetails where
+  ppr = pprTcTyVarDetails
+
+pprTcTyVarDetails :: TcTyVarDetails -> SDoc
+-- For debugging
+pprTcTyVarDetails (RuntimeUnk {})      = text "rt"
+pprTcTyVarDetails (SkolemTv lvl True)  = text "ssk" <> colon <> ppr lvl
+pprTcTyVarDetails (SkolemTv lvl False) = text "sk"  <> colon <> ppr lvl
+pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
+  = ppr info <> colon <> ppr tclvl
+
 -----------------------------
 data MetaDetails
   = Flexi  -- Flexi type variables unify to become Indirects
@@ -544,20 +555,11 @@ instance Outputable MetaDetails where
   ppr Flexi         = text "Flexi"
   ppr (Indirect ty) = text "Indirect" <+> ppr ty
 
-pprTcTyVarDetails :: TcTyVarDetails -> SDoc
--- For debugging
-pprTcTyVarDetails (RuntimeUnk {})      = text "rt"
-pprTcTyVarDetails (SkolemTv lvl True)  = text "ssk" <> colon <> ppr lvl
-pprTcTyVarDetails (SkolemTv lvl False) = text "sk"  <> colon <> ppr lvl
-pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
-  = pp_info <> colon <> ppr tclvl
-  where
-    pp_info = case info of
-                TauTv      -> text "tau"
-                TyVarTv    -> text "tyv"
-                FlatMetaTv -> text "fmv"
-                FlatSkolTv -> text "fsk"
-
+instance Outputable MetaInfo where
+  ppr TauTv         = text "tau"
+  ppr TyVarTv       = text "tyv"
+  ppr FlatMetaTv    = text "fmv"
+  ppr FlatSkolTv    = text "fsk"
 
 {- *********************************************************************
 *                                                                      *
@@ -795,10 +797,10 @@ checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
 checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
   = ctxt_tclvl >= tv_tclvl
 
+-- Returns topTcLevel for non-TcTyVars
 tcTyVarLevel :: TcTyVar -> TcLevel
 tcTyVarLevel tv
-  = ASSERT2( tcIsTcTyVar tv, ppr tv )
-    case tcTyVarDetails tv of
+  = case tcTyVarDetails tv of
           MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
           SkolemTv tv_lvl _             -> tv_lvl
           RuntimeUnk                    -> topTcLevel
diff --git a/testsuite/tests/ghci/scripts/T16767.script b/testsuite/tests/ghci/scripts/T16767.script
new file mode 100644 (file)
index 0000000..40d4812
--- /dev/null
@@ -0,0 +1,3 @@
+:set -fprint-explicit-foralls -fprint-explicit-kinds -XTypeApplications -XDataKinds
+import Data.Proxy
+:kind! 'Proxy @_
diff --git a/testsuite/tests/ghci/scripts/T16767.stdout b/testsuite/tests/ghci/scripts/T16767.stdout
new file mode 100644 (file)
index 0000000..340ed6e
--- /dev/null
@@ -0,0 +1,2 @@
+'Proxy @_ :: forall {k} {_ :: k}. Proxy @{k} _
+= 'Proxy @{k} @_
index 9ece912..de8716d 100755 (executable)
@@ -296,3 +296,4 @@ test('T16030', normal, ghci_script, ['T16030.script'])
 test('T11606', normal, ghci_script, ['T11606.script'])
 test('T16089', normal, ghci_script, ['T16089.script'])
 test('T16527', normal, ghci_script, ['T16527.script'])
+test('T16767', normal, ghci_script, ['T16767.script'])
diff --git a/testsuite/tests/typecheck/should_fail/T16517.hs b/testsuite/tests/typecheck/should_fail/T16517.hs
new file mode 100644 (file)
index 0000000..2664a18
--- /dev/null
@@ -0,0 +1,5 @@
+{-# LANGUAGE PolyKinds #-}
+module T16517 where
+
+import Data.Proxy
+class C a where m :: Proxy (a :: k)
diff --git a/testsuite/tests/typecheck/should_fail/T16517.stderr b/testsuite/tests/typecheck/should_fail/T16517.stderr
new file mode 100644 (file)
index 0000000..8d20665
--- /dev/null
@@ -0,0 +1,6 @@
+
+T16517.hs:5:29: error:
+    • Expected kind ‘k’, but ‘a’ has kind ‘k0’
+    • In the first argument of ‘Proxy’, namely ‘(a :: k)’
+      In the type signature: m :: Proxy (a :: k)
+      In the class declaration for ‘C’
index 2c09afa..30a079c 100644 (file)
@@ -511,3 +511,4 @@ test('T16059e', [extra_files(['T16059b.hs'])], multimod_compile_fail,
     ['T16059e', '-v0'])
 test('T16255', normal, compile_fail, [''])
 test('T16204c', normal, compile_fail, [''])
+test('T16517', normal, compile_fail, [''])
index 8e1170c..46ddc33 100644 (file)
@@ -2,6 +2,5 @@
 tcfail134.hs:5:33: error:
     • Expecting one more argument to ‘XML’
       Expected a type, but ‘XML’ has kind ‘* -> Constraint’
-    • In the type signature:
-        toXML :: a -> XML
+    • In the type signature: toXML :: a -> XML
       In the class declaration for ‘XML’