Track type variable scope more carefully.
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Mon, 4 Sep 2017 21:27:17 +0000 (22:27 +0100)
committerRichard Eisenberg <rae@cs.brynmawr.edu>
Sun, 1 Apr 2018 03:16:46 +0000 (23:16 -0400)
The main job of this commit is to track more accurately the scope
of tyvars introduced by user-written foralls. For example, it would
be to have something like this:

  forall a. Int -> (forall k (b :: k). Proxy '[a, b]) -> Bool

In that type, a's kind must be k, but k isn't in scope. We had a
terrible way of doing this before (not worth repeating or describing
here, but see the old tcImplicitTKBndrs and friends), but now
we have a principled approach: make an Implication when kind-checking
a forall. Doing so then hooks into the existing machinery for
preventing skolem-escape, performing floating, etc. This also means
that we bump the TcLevel whenever going into a forall.

The new behavior is done in TcHsType.scopeTyVars, but see also
TcHsType.tc{Im,Ex}plicitTKBndrs, which have undergone significant
rewriting. There are several Notes near there to guide you. Of
particular interest there is that Implication constraints can now
have skolems that are out of order; this situation is reported in
TcErrors.

A major consequence of this is a slightly tweaked process for type-
checking type declarations. The new Note [Use SigTvs in kind-checking
pass] in TcTyClsDecls lays it out.

The error message for dependent/should_fail/TypeSkolEscape has become
noticeably worse. However, this is because the code in TcErrors goes to
some length to preserve pre-8.0 error messages for kind errors. It's time
to rip off that plaster and get rid of much of the kind-error-specific
error messages. I tried this, and doing so led to a lovely error message
for TypeSkolEscape. So: I'm accepting the error message quality regression
for now, but will open up a new ticket to fix it, along with a larger
error-message improvement I've been pondering. This applies also to
dependent/should_fail/{BadTelescope2,T14066,T14066e}, polykinds/T11142.

Other minor changes:
 - isUnliftedTypeKind didn't look for tuples and sums. It does now.

 - check_type used check_arg_type on both sides of an AppTy. But the left
   side of an AppTy isn't an arg, and this was causing a bad error message.
   I've changed it to use check_type on the left-hand side.

 - Some refactoring around when we print (TYPE blah) in error messages.
   The changes decrease the times when we do so, to good effect.
   Of course, this is still all controlled by
   -fprint-explicit-runtime-reps

Fixes #14066 #14749

Test cases: dependent/should_compile/{T14066a,T14749},
            dependent/should_fail/T14066{,c,d,e,f,g,h}

121 files changed:
compiler/basicTypes/DataCon.hs
compiler/basicTypes/Var.hs
compiler/deSugar/DsExpr.hs
compiler/hsSyn/HsDecls.hs
compiler/hsSyn/HsTypes.hs
compiler/iface/IfaceType.hs
compiler/iface/ToIface.hs
compiler/nativeGen/RegAlloc/Liveness.hs
compiler/prelude/PrelNames.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcClassDcl.hs
compiler/typecheck/TcDeriv.hs
compiler/typecheck/TcEnv.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnMonad.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSigs.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
compiler/typecheck/TcValidity.hs
compiler/types/Coercion.hs
compiler/types/TyCoRep.hs
compiler/types/TyCoRep.hs-boot
compiler/types/TyCon.hs
compiler/types/Type.hs
compiler/utils/Bag.hs
compiler/utils/Outputable.hs
docs/users_guide/glasgow_exts.rst
testsuite/tests/codeGen/should_fail/T13233.stderr
testsuite/tests/dependent/should_compile/InferDependency.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/T11635.hs
testsuite/tests/dependent/should_compile/T14066a.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/T14066a.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_compile/T14749.hs [moved from testsuite/tests/typecheck/should_compile/T14749.hs with 100% similarity]
testsuite/tests/dependent/should_compile/all.T
testsuite/tests/dependent/should_fail/BadTelescope.stderr
testsuite/tests/dependent/should_fail/BadTelescope2.stderr
testsuite/tests/dependent/should_fail/BadTelescope3.stderr
testsuite/tests/dependent/should_fail/BadTelescope4.stderr
testsuite/tests/dependent/should_fail/InferDependency.stderr
testsuite/tests/dependent/should_fail/T13601.stderr
testsuite/tests/dependent/should_fail/T13780c.stderr
testsuite/tests/dependent/should_fail/T14066.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066c.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066c.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066d.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066d.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066e.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066e.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066f.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066f.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066g.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066g.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066h.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066h.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
testsuite/tests/dependent/should_fail/all.T
testsuite/tests/deriving/should_compile/T11732c.hs
testsuite/tests/gadt/T12468.stderr
testsuite/tests/ghci/scripts/T10248.stderr
testsuite/tests/ghci/scripts/T10249.stderr
testsuite/tests/ghci/scripts/T8353.stderr
testsuite/tests/indexed-types/should_fail/T7938.stderr
testsuite/tests/indexed-types/should_fail/T8129.stdout
testsuite/tests/module/mod71.stderr
testsuite/tests/partial-sigs/should_compile/T12531.stderr
testsuite/tests/partial-sigs/should_fail/T10615.stderr
testsuite/tests/partial-sigs/should_fail/T11976.stderr
testsuite/tests/partial-sigs/should_fail/T14040a.stderr
testsuite/tests/perf/haddock/all.T
testsuite/tests/polykinds/SigTvKinds3.hs [new file with mode: 0644]
testsuite/tests/polykinds/SigTvKinds3.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T11142.stderr
testsuite/tests/polykinds/T12593.stderr
testsuite/tests/polykinds/T13985.stderr
testsuite/tests/polykinds/T14563.hs
testsuite/tests/polykinds/T14846.stderr
testsuite/tests/polykinds/T7230.stderr
testsuite/tests/polykinds/T8566.stderr
testsuite/tests/polykinds/T9222.stderr
testsuite/tests/polykinds/all.T
testsuite/tests/th/T10267.stderr
testsuite/tests/typecheck/should_compile/T13050.stderr
testsuite/tests/typecheck/should_compile/T13343.hs
testsuite/tests/typecheck/should_compile/T14590.stderr
testsuite/tests/typecheck/should_compile/T2494.stderr
testsuite/tests/typecheck/should_compile/T9497a.stderr
testsuite/tests/typecheck/should_compile/abstract_refinement_substitutions.stderr
testsuite/tests/typecheck/should_compile/all.T
testsuite/tests/typecheck/should_compile/hole_constraints.stderr
testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr
testsuite/tests/typecheck/should_compile/holes.stderr
testsuite/tests/typecheck/should_compile/holes3.stderr
testsuite/tests/typecheck/should_compile/refinement_substitutions.stderr
testsuite/tests/typecheck/should_compile/valid_substitutions.stderr
testsuite/tests/typecheck/should_compile/valid_substitutions_interactions.stderr
testsuite/tests/typecheck/should_fail/T11355.stderr
testsuite/tests/typecheck/should_fail/T12177.stderr
testsuite/tests/typecheck/should_fail/T14350.stderr
testsuite/tests/typecheck/should_fail/T14607.hs
testsuite/tests/typecheck/should_fail/T14607.stderr
testsuite/tests/typecheck/should_fail/T9497d.stderr
testsuite/tests/typecheck/should_fail/all.T
testsuite/tests/typecheck/should_run/T9497a-run.stderr
testsuite/tests/typecheck/should_run/T9497b-run.stderr
testsuite/tests/typecheck/should_run/T9497c-run.stderr

index 4351e38..6f0cf41 100644 (file)
@@ -894,7 +894,11 @@ mkDataCon name declared_infix prom_info
       == Set.fromList (binderVars user_tvbs)
     user_tvbs' =
       ASSERT2( user_tvbs_invariant
-             , ppr univ_tvs $$ ppr ex_tvs $$ ppr user_tvbs )
+             , (vcat [ ppr name
+                     , ppr univ_tvs
+                     , ppr ex_tvs
+                     , ppr eq_spec
+                     , ppr user_tvbs ]) )
       user_tvbs
     con = MkData {dcName = name, dcUnique = nameUnique name,
                   dcVanilla = is_vanilla, dcInfix = declared_infix,
index 1bf60ca..afefa6e 100644 (file)
@@ -35,7 +35,7 @@
 module Var (
         -- * The main data type and synonyms
         Var, CoVar, Id, NcId, DictId, DFunId, EvVar, EqVar, EvId, IpId, JoinId,
-        TyVar, TypeVar, KindVar, TKVar, TyCoVar,
+        TyVar, TcTyVar, TypeVar, KindVar, TKVar, TyCoVar,
 
         -- * In and Out variants
         InVar,  InCoVar,  InId,  InTyVar,
@@ -128,6 +128,9 @@ type TyVar   = Var     -- Type *or* kind variable (historical)
 -- | Type or Kind Variable
 type TKVar   = Var     -- Type *or* kind variable (historical)
 
+-- | Type variable that might be a metavariable
+type TcTyVar = Var
+
 -- | Type Variable
 type TypeVar = Var     -- Definitely a type variable
 
@@ -378,8 +381,9 @@ updateVarTypeM f id = do { ty' <- f (varType id)
 -- permitted by request ('Specified') (visible type application), or
 -- prohibited entirely from appearing in source Haskell ('Inferred')?
 -- See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility] in TyCoRep
-data ArgFlag = Required | Specified | Inferred
-  deriving (Eq, Data)
+data ArgFlag = Inferred | Specified | Required
+  deriving (Eq, Ord, Data)
+  -- (<) on ArgFlag meant "is less visible than"
 
 -- | Does this 'ArgFlag' classify an argument that is written in Haskell?
 isVisibleArgFlag :: ArgFlag -> Bool
index 17cbcab..392bacc 100644 (file)
@@ -1167,6 +1167,6 @@ badUseOfLevPolyPrimop id ty
 levPolyPrimopErr :: Id -> Type -> [Type] -> DsM ()
 levPolyPrimopErr primop ty bad_tys
   = errDs $ vcat [ hang (text "Cannot use primitive with levity-polymorphic arguments:")
-                      2 (ppr primop <+> dcolon <+> ppr ty)
+                      2 (ppr primop <+> dcolon <+> pprWithTYPE ty)
                  , hang (text "Levity-polymorphic arguments:")
-                      2 (vcat (map (\t -> ppr t <+> dcolon <+> ppr (typeKind t)) bad_tys)) ]
+                      2 (vcat (map (\t -> pprWithTYPE t <+> dcolon <+> pprWithTYPE (typeKind t)) bad_tys)) ]
index a3fe5a7..6f1d5be 100644 (file)
@@ -19,7 +19,7 @@
 module HsDecls (
   -- * Toplevel declarations
   HsDecl(..), LHsDecl, HsDataDefn(..), HsDeriving,
-  HsDerivingClause(..), LHsDerivingClause,
+  HsDerivingClause(..), LHsDerivingClause, NewOrData(..), newOrDataToFlavour,
 
   -- ** Class or type declarations
   TyClDecl(..), LTyClDecl,
@@ -35,7 +35,7 @@ module HsDecls (
   FamilyDecl(..), LFamilyDecl,
 
   -- ** Instance declarations
-  InstDecl(..), LInstDecl, NewOrData(..), FamilyInfo(..),
+  InstDecl(..), LInstDecl, FamilyInfo(..),
   TyFamInstDecl(..), LTyFamInstDecl, instDeclDataFamInsts,
   DataFamInstDecl(..), LDataFamInstDecl, pprDataFamInstFlavour, pprFamInstLHS,
   FamInstEqn, LFamInstEqn, FamEqn(..),
@@ -958,7 +958,7 @@ famDeclHasCusk _ (FamilyDecl { fdInfo      = ClosedTypeFamily _
                              , fdResultSig = L _ resultSig })
   = hsTvbAllKinded tyvars && hasReturnKindSignature resultSig
 famDeclHasCusk mb_class_cusk _ = mb_class_cusk `orElse` True
-        -- all un-associated open families have CUSKs!
+        -- all un-associated open families have CUSKs
 
 -- | Does this family declaration have user-supplied return kind signature?
 hasReturnKindSignature :: FamilyResultSig a -> Bool
@@ -1114,6 +1114,11 @@ data NewOrData
   | DataType                    -- ^ @data Blah ...@
   deriving( Eq, Data )                -- Needed because Demand derives Eq
 
+-- | Convert a 'NewOrData' to a 'TyConFlavour'
+newOrDataToFlavour :: NewOrData -> TyConFlavour
+newOrDataToFlavour NewType  = NewtypeFlavour
+newOrDataToFlavour DataType = DataTypeFlavour
+
 -- | Located data Constructor Declaration
 type LConDecl pass = Located (ConDecl pass)
       -- ^ May have 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnSemi' when
index 6503670..15c570f 100644 (file)
@@ -1036,13 +1036,13 @@ splitLHsSigmaTy ty
   = (tvs, ctxt, ty2)
 
 splitLHsForAllTy :: LHsType pass -> ([LHsTyVarBndr pass], LHsType pass)
+splitLHsForAllTy (L _ (HsParTy ty)) = splitLHsForAllTy ty
 splitLHsForAllTy (L _ (HsForAllTy { hst_bndrs = tvs, hst_body = body })) = (tvs, body)
-splitLHsForAllTy (L _ (HsParTy t)) = splitLHsForAllTy t
 splitLHsForAllTy body              = ([], body)
 
 splitLHsQualTy :: LHsType pass -> (LHsContext pass, LHsType pass)
+splitLHsQualTy (L _ (HsParTy ty)) = splitLHsQualTy ty
 splitLHsQualTy (L _ (HsQualTy { hst_ctxt = ctxt, hst_body = body })) = (ctxt,     body)
-splitLHsQualTy (L _ (HsParTy t)) = splitLHsQualTy t
 splitLHsQualTy body              = (noLoc [], body)
 
 splitLHsInstDeclTy :: LHsSigType GhcRn
index d0adce9..4523093 100644 (file)
@@ -53,6 +53,7 @@ module IfaceType (
 import GhcPrelude
 
 import {-# SOURCE #-} TysWiredIn ( liftedRepDataConTyCon )
+import {-# SOURCE #-} TyCoRep    ( isRuntimeRepTy )
 
 import DynFlags
 import TyCon hiding ( pprPromotionQuote )
@@ -671,7 +672,7 @@ overhead.
 
 For this reason it was decided that we would hide RuntimeRep variables for now
 (see #11549). We do this by defaulting all type variables of kind RuntimeRep to
-PtrLiftedRep. This is done in a pass right before pretty-printing
+LiftedRep. This is done in a pass right before pretty-printing
 (defaultRuntimeRepVars, controlled by -fprint-explicit-runtime-reps)
 -}
 
@@ -690,8 +691,8 @@ PtrLiftedRep. This is done in a pass right before pretty-printing
 -- syntactic overhead in otherwise simple type signatures (e.g. ($)). See
 -- Note [Defaulting RuntimeRep variables] and #11549 for further discussion.
 --
-defaultRuntimeRepVars :: IfaceType -> IfaceType
-defaultRuntimeRepVars = go emptyFsEnv
+defaultRuntimeRepVars :: PprStyle -> IfaceType -> IfaceType
+defaultRuntimeRepVars sty = go emptyFsEnv
   where
     go :: FastStringEnv () -> IfaceType -> IfaceType
     go subs (IfaceForAllTy bndr ty)
@@ -707,12 +708,27 @@ defaultRuntimeRepVars = go emptyFsEnv
         var :: IfLclName
         (var, var_kind) = binderVar bndr
 
-    go subs (IfaceTyVar tv)
+    go subs ty@(IfaceTyVar tv)
       | tv `elemFsEnv` subs
       = IfaceTyConApp liftedRep ITC_Nil
+      | otherwise
+      = ty
+
+    go _ ty@(IfaceFreeTyVar tv)
+      | userStyle sty && TyCoRep.isRuntimeRepTy (tyVarKind tv)
+         -- don't require -fprint-explicit-runtime-reps for good debugging output
+      = IfaceTyConApp liftedRep ITC_Nil
+      | otherwise
+      = ty
 
-    go subs (IfaceFunTy kind ty)
-      = IfaceFunTy (go subs kind) (go subs ty)
+    go subs (IfaceTyConApp tc tc_args)
+      = IfaceTyConApp tc (go_args subs tc_args)
+
+    go subs (IfaceTupleTy sort is_prom tc_args)
+      = IfaceTupleTy sort is_prom (go_args subs tc_args)
+
+    go subs (IfaceFunTy arg res)
+      = IfaceFunTy (go subs arg) (go subs res)
 
     go subs (IfaceAppTy x y)
       = IfaceAppTy (go subs x) (go subs y)
@@ -723,7 +739,13 @@ defaultRuntimeRepVars = go emptyFsEnv
     go subs (IfaceCastTy x co)
       = IfaceCastTy (go subs x) co
 
-    go _ other = other
+    go _ ty@(IfaceLitTy {}) = ty
+    go _ ty@(IfaceCoercionTy {}) = ty
+
+    go_args :: FastStringEnv () -> IfaceTcArgs -> IfaceTcArgs
+    go_args _ ITC_Nil = ITC_Nil
+    go_args subs (ITC_Vis ty args)   = ITC_Vis   (go subs ty) (go_args subs args)
+    go_args subs (ITC_Invis ty args) = ITC_Invis (go subs ty) (go_args subs args)
 
     liftedRep :: IfaceTyCon
     liftedRep =
@@ -739,7 +761,7 @@ eliminateRuntimeRep :: (IfaceType -> SDoc) -> IfaceType -> SDoc
 eliminateRuntimeRep f ty = sdocWithDynFlags $ \dflags ->
     if gopt Opt_PrintExplicitRuntimeReps dflags
       then f ty
-      else f (defaultRuntimeRepVars ty)
+      else getPprStyle $ \sty -> f (defaultRuntimeRepVars sty ty)
 
 instance Outputable IfaceTcArgs where
   ppr tca = pprIfaceTcArgs tca
index da24d38..b74368d 100644 (file)
@@ -74,9 +74,13 @@ import Data.Maybe ( catMaybes )
 
 ----------------
 toIfaceTvBndr :: TyVar -> IfaceTvBndr
-toIfaceTvBndr tyvar   = ( occNameFS (getOccName tyvar)
-                        , toIfaceKind (tyVarKind tyvar)
-                        )
+toIfaceTvBndr = toIfaceTvBndrX emptyVarSet
+
+toIfaceTvBndrX :: VarSet -> TyVar -> IfaceTvBndr
+toIfaceTvBndrX fr tyvar = ( occNameFS (getOccName tyvar)
+                          , toIfaceTypeX fr (tyVarKind tyvar)
+                          )
+
 
 toIfaceIdBndr :: Id -> (IfLclName, IfaceType)
 toIfaceIdBndr id      = (occNameFS (getOccName id),    toIfaceType (idType id))
@@ -120,7 +124,7 @@ toIfaceTypeX fr (TyVarTy tv)   -- See Note [TcTyVars in IfaceType] in IfaceType
   | otherwise                  = IfaceTyVar (toIfaceTyVar tv)
 toIfaceTypeX fr (AppTy t1 t2)  = IfaceAppTy (toIfaceTypeX fr t1) (toIfaceTypeX fr t2)
 toIfaceTypeX _  (LitTy n)      = IfaceLitTy (toIfaceTyLit n)
-toIfaceTypeX fr (ForAllTy b t) = IfaceForAllTy (toIfaceForAllBndr b)
+toIfaceTypeX fr (ForAllTy b t) = IfaceForAllTy (toIfaceForAllBndrX fr b)
                                                (toIfaceTypeX (fr `delVarSet` binderVar b) t)
 toIfaceTypeX fr (FunTy t1 t2)
   | isPredTy t1                 = IfaceDFunTy (toIfaceTypeX fr t1) (toIfaceTypeX fr t2)
@@ -160,7 +164,10 @@ toIfaceCoVar :: CoVar -> FastString
 toIfaceCoVar = occNameFS . getOccName
 
 toIfaceForAllBndr :: TyVarBinder -> IfaceForAllBndr
-toIfaceForAllBndr (TvBndr v vis) = TvBndr (toIfaceTvBndr v) vis
+toIfaceForAllBndr = toIfaceForAllBndrX emptyVarSet
+
+toIfaceForAllBndrX :: VarSet -> TyVarBinder -> IfaceForAllBndr
+toIfaceForAllBndrX fr (TvBndr v vis) = TvBndr (toIfaceTvBndrX fr v) vis
 
 ----------------
 toIfaceTyCon :: TyCon -> IfaceTyCon
index d4fecf2..2a2990f 100644 (file)
@@ -1008,5 +1008,3 @@ liveness1 platform liveregs blockmap (LiveInstr instr _)
             r_dying_br  = nonDetEltsUniqSet (mkUniqSet r_dying `unionUniqSets`
                                              live_branch_only)
                           -- See Note [Unique Determinism and code generation]
-
-
index 280f1ef..3f419eb 100644 (file)
@@ -2025,12 +2025,16 @@ tupleRepDataConKey                      = mkPreludeDataConUnique 72
 sumRepDataConKey                        = mkPreludeDataConUnique 73
 
 -- See Note [Wiring in RuntimeRep] in TysWiredIn
-runtimeRepSimpleDataConKeys :: [Unique]
+runtimeRepSimpleDataConKeys, unliftedSimpleRepDataConKeys, unliftedRepDataConKeys :: [Unique]
 liftedRepDataConKey :: Unique
-runtimeRepSimpleDataConKeys@(
-  liftedRepDataConKey : _)
+runtimeRepSimpleDataConKeys@(liftedRepDataConKey : unliftedSimpleRepDataConKeys)
   = map mkPreludeDataConUnique [74..82]
 
+unliftedRepDataConKeys = vecRepDataConKey :
+                         tupleRepDataConKey :
+                         sumRepDataConKey :
+                         unliftedSimpleRepDataConKeys
+
 -- See Note [Wiring in RuntimeRep] in TysWiredIn
 -- VecCount
 vecCountDataConKeys :: [Unique]
index 60ed962..1b02a34 100644 (file)
@@ -40,7 +40,7 @@ import FamInstEnv( normaliseType )
 import FamInst( tcGetFamInstEnvs )
 import TyCon
 import TcType
-import Type( mkStrLitTy, tidyOpenType, splitTyConApp_maybe)
+import Type( mkStrLitTy, tidyOpenType, splitTyConApp_maybe, mkCastTy)
 import TysPrim
 import TysWiredIn( mkBoxedTupleTy )
 import Id
@@ -987,14 +987,14 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
       | otherwise -- Can't happen; by now we know it's a partial sig
       = pprPanic "report_sig_tv_err" (ppr sig)
 
-    choose_psig_context :: VarSet -> TcThetaType -> Maybe TcTyVar
+    choose_psig_context :: VarSet -> TcThetaType -> Maybe TcType
                         -> TcM (VarSet, TcThetaType)
     choose_psig_context _ annotated_theta Nothing
       = do { let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
                                             `unionVarSet` tau_tvs)
            ; return (free_tvs, annotated_theta) }
 
-    choose_psig_context psig_qtvs annotated_theta (Just wc_var)
+    choose_psig_context psig_qtvs annotated_theta (Just wc_var_ty)
       = do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta seed_tvs)
                             -- growThetaVars just like the no-type-sig case
                             -- Omitting this caused #12844
@@ -1012,7 +1012,13 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
                                  | pred <- my_theta
                                  , all (not . (`eqType` pred)) annotated_theta ]
            ; ctuple <- mk_ctuple inferred_diff
-           ; writeMetaTyVar wc_var ctuple
+
+           ; case tcGetCastedTyVar_maybe wc_var_ty of
+               -- We know that wc_co must have type kind(wc_var) ~ Constraint, as it
+               -- comes from the checkExpectedKind in TcHsType.tcWildCardOcc. So, to
+               -- make the kinds work out, we reverse the cast here.
+               Just (wc_var, wc_co) -> writeMetaTyVar wc_var (ctuple `mkCastTy` mkTcSymCo wc_co)
+               Nothing              -> pprPanic "chooseInferredQuantifiers 1" (ppr wc_var_ty)
 
            ; traceTc "completeTheta" $
                 vcat [ ppr sig
@@ -1517,6 +1523,7 @@ tcExtendTyVarEnvForRhs (Just sig) thing_inside
 tcExtendTyVarEnvFromSig :: TcIdSigInst -> TcM a -> TcM a
 tcExtendTyVarEnvFromSig sig_inst thing_inside
   | TISI { sig_inst_skols = skol_prs, sig_inst_wcs = wcs } <- sig_inst
+     -- Note [Use tcExtendTyVar not scopeTyVars in tcRhs]
   = tcExtendTyVarEnv2 wcs $
     tcExtendTyVarEnv2 skol_prs $
     thing_inside
@@ -1656,6 +1663,30 @@ Example for (E2), we generate
 The beta is untoucable, but floats out of the constraint and can
 be solved absolutely fine.
 
+Note [Use tcExtendTyVar not scopeTyVars in tcRhs]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Normally, any place that corresponds to Λ or ∀ in Core should be flagged
+with a call to scopeTyVars, which arranges for an implication constraint
+to be made, bumps the TcLevel, and (crucially) prevents a unification
+variable created outside the scope of a local skolem to unify with that
+skolem.
+
+We do not need to do this here, however.
+
+- Note that this happens only in the case of a partial signature.
+  Complete signatures go via tcPolyCheck, not tcPolyInfer.
+
+- The TcLevel is incremented in tcPolyInfer, right outside the call
+  to tcMonoBinds. We thus don't have to worry about outer metatvs unifying
+  with local skolems.
+
+- The other potential concern is that we need SkolemInfo associated with
+  the skolems. This, too, is OK, though: the constraints pass through
+  simplifyInfer (which doesn't report errors), at the end of which
+  the skolems will get quantified and put into an implication constraint.
+  Thus, by the time any errors are reported, the SkolemInfo will be
+  in place.
+
 ************************************************************************
 *                                                                      *
                 Generalisation
index 2503197..dcc85af 100644 (file)
@@ -144,11 +144,15 @@ tcClassSigs clas sigs def_methods
     dm_bind_names :: [Name] -- These ones have a value binding in the class decl
     dm_bind_names = [op | L _ (FunBind {fun_id = L _ op}) <- bagToList def_methods]
 
+    skol_info = TyConSkol ClassFlavour clas
+
     tc_sig :: NameEnv (SrcSpan, Type) -> ([Located Name], LHsSigType GhcRn)
            -> TcM [TcMethInfo]
     tc_sig gen_dm_env (op_names, op_hs_ty)
       = do { traceTc "ClsSig 1" (ppr op_names)
-           ; op_ty <- tcClassSigType op_names op_hs_ty   -- Class tyvars already in scope
+           ; op_ty <- tcClassSigType skol_info op_names op_hs_ty
+                   -- Class tyvars already in scope
+
            ; traceTc "ClsSig 2" (ppr op_names)
            ; return [ (op_name, op_ty, f op_name) | L _ op_name <- op_names ] }
            where
@@ -157,7 +161,7 @@ tcClassSigs clas sigs def_methods
                   | otherwise                               = Nothing
 
     tc_gen_sig (op_names, gen_hs_ty)
-      = do { gen_op_ty <- tcClassSigType op_names gen_hs_ty
+      = do { gen_op_ty <- tcClassSigType skol_info op_names gen_hs_ty
            ; return [ (op_name, (loc, gen_op_ty)) | L loc op_name <- op_names ] }
 
 {-
@@ -194,6 +198,9 @@ tcClassDecl2 (L _ (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
 
         ; let tc_item = tcDefMeth clas clas_tyvars this_dict
                                   default_binds sig_fn prag_fn
+                   -- tcExtendTyVarEnv here (instead of scopeTyVars) is OK:
+                   -- the tcDefMeth calls checkConstraints to bump the TcLevel
+                   -- and make the implication constraint
         ; dm_binds <- tcExtendTyVarEnv clas_tyvars $
                       mapM tc_item op_items
 
@@ -276,7 +283,7 @@ tcDefMeth clas tyvars this_dict binds_in hs_sig_fn prag_fn
                                         , sig_loc   = getLoc (hsSigType hs_ty) }
 
        ; (ev_binds, (tc_bind, _))
-               <- checkConstraints (ClsSkol clas) tyvars [this_dict] $
+               <- checkConstraints (TyConSkol ClassFlavour (getName clas)) tyvars [this_dict] $
                   tcPolyCheck no_prag_fn local_dm_sig
                               (L bind_loc lm_bind)
 
index 0e7268b..3144564 100644 (file)
@@ -717,6 +717,9 @@ deriveTyData tvs tc tc_args deriv_strat deriv_pred
   = setSrcSpan (getLoc (hsSigType deriv_pred)) $
     -- Use loc of the 'deriving' item
     do  { (deriv_tvs, cls, cls_tys, cls_arg_kinds)
+                   -- Why not scopeTyVars? Because these are *TyVar*s, not TcTyVars.
+                   -- Their kinds are fully settled. No need to worry about skolem
+                   -- escape.
                 <- tcExtendTyVarEnv tvs $
                    tcHsDeriv deriv_pred
                 -- Deriving preds may (now) mention
index 28130b7..5d59a83 100644 (file)
@@ -401,10 +401,18 @@ tcExtendKindEnv extra_env thing_inside
 
 -----------------------
 -- Scoped type and kind variables
+-- Before using this function, consider using TcHsType.scopeTyVars, which
+-- bumps the TcLevel and thus prevents any of these TyVars from appearing
+-- in kinds of tyvars in an outer scope.
+-- Indeed, you should always use scopeTyVars unless some other code nearby
+-- bumps the TcLevel.
 tcExtendTyVarEnv :: [TyVar] -> TcM r -> TcM r
 tcExtendTyVarEnv tvs thing_inside
   = tcExtendTyVarEnv2 (mkTyVarNamePairs tvs) thing_inside
 
+-- Before using this function, consider using TcHsType.scopeTyVars2, which
+-- bumps the TcLevel and thus prevents any of these TyVars from appearing
+-- in kinds of tyvars in an outer scope.
 tcExtendTyVarEnv2 :: [(Name,TcTyVar)] -> TcM r -> TcM r
 tcExtendTyVarEnv2 binds thing_inside
   -- this should be used only for explicitly mentioned scoped variables.
index 0700d02..27148af 100644 (file)
@@ -38,7 +38,7 @@ import Name
 import RdrName ( lookupGlobalRdrEnv, lookupGRE_Name, GlobalRdrEnv
                , mkRdrUnqual, isLocalGRE, greSrcSpan, pprNameProvenance
                , GlobalRdrElt (..), globalRdrEnvElts )
-import PrelNames ( typeableClassName, hasKey, liftedRepDataConKey )
+import PrelNames ( typeableClassName, hasKey, liftedRepDataConKey, tYPETyConKey )
 import Id
 import Var
 import VarSet
@@ -130,7 +130,7 @@ reportUnsolved wanted
        ; defer_errors <- goptM Opt_DeferTypeErrors
        ; warn_errors <- woptM Opt_WarnDeferredTypeErrors -- implement #10283
        ; let type_errors | not defer_errors = TypeError
-                         | warn_errors      = TypeWarn
+                         | warn_errors      = TypeWarn (Reason Opt_WarnDeferredTypeErrors)
                          | otherwise        = TypeDefer
 
        ; defer_holes <- goptM Opt_DeferTypedHoles
@@ -151,7 +151,7 @@ reportUnsolved wanted
                                 | warn_out_of_scope      = HoleWarn
                                 | otherwise              = HoleDefer
 
-       ; report_unsolved binds_var False type_errors expr_holes
+       ; report_unsolved binds_var type_errors expr_holes
           type_holes out_of_scope_holes wanted
 
        ; ev_binds <- getTcEvBindsMap binds_var
@@ -166,8 +166,8 @@ reportUnsolved wanted
 -- and for simplifyDefault.
 reportAllUnsolved :: WantedConstraints -> TcM ()
 reportAllUnsolved wanted
-  = do { ev_binds <- newTcEvBinds
-       ; report_unsolved ev_binds False TypeError
+  = do { ev_binds <- newNoTcEvBinds
+       ; report_unsolved ev_binds TypeError
                          HoleError HoleError HoleError wanted }
 
 -- | Report all unsolved goals as warnings (but without deferring any errors to
@@ -176,23 +176,27 @@ reportAllUnsolved wanted
 warnAllUnsolved :: WantedConstraints -> TcM ()
 warnAllUnsolved wanted
   = do { ev_binds <- newTcEvBinds
-       ; report_unsolved ev_binds True TypeWarn
+       ; report_unsolved ev_binds (TypeWarn NoReason)
                          HoleWarn HoleWarn HoleWarn wanted }
 
 -- | Report unsolved goals as errors or warnings.
 report_unsolved :: EvBindsVar        -- cec_binds
-                -> Bool              -- Errors as warnings
                 -> TypeErrorChoice   -- Deferred type errors
                 -> HoleChoice        -- Expression holes
                 -> HoleChoice        -- Type holes
                 -> HoleChoice        -- Out of scope holes
                 -> WantedConstraints -> TcM ()
-report_unsolved mb_binds_var err_as_warn type_errors expr_holes
+report_unsolved mb_binds_var type_errors expr_holes
     type_holes out_of_scope_holes wanted
   | isEmptyWC wanted
   = return ()
   | otherwise
-  = do { traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted)
+  = do { traceTc "reportUnsolved warning/error settings:" $
+           vcat [ text "type errors:" <+> ppr type_errors
+                , text "expr holes:" <+> ppr expr_holes
+                , text "type holes:" <+> ppr type_holes
+                , text "scope holes:" <+> ppr out_of_scope_holes ]
+       ; traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted)
 
        ; wanted <- zonkWC wanted   -- Zonk to reveal all information
        ; env0 <- tcInitTidyEnv
@@ -210,7 +214,6 @@ report_unsolved mb_binds_var err_as_warn type_errors expr_holes
        ; let err_ctxt = CEC { cec_encl  = []
                             , cec_tidy  = tidy_env
                             , cec_defer_type_errors = type_errors
-                            , cec_errors_as_warns = err_as_warn
                             , cec_expr_holes = expr_holes
                             , cec_type_holes = type_holes
                             , cec_out_of_scope_holes = out_of_scope_holes
@@ -275,7 +278,11 @@ valid_substitutions docs = mempty { report_valid_substitutions = [docs] }
 
 data TypeErrorChoice   -- What to do for type errors found by the type checker
   = TypeError     -- A type error aborts compilation with an error message
-  | TypeWarn      -- A type error is deferred to runtime, plus a compile-time warning
+  | TypeWarn WarnReason
+                  -- A type error is deferred to runtime, plus a compile-time warning
+                  -- The WarnReason should usually be (Reason Opt_WarnDeferredTypeErrors)
+                  -- but it isn't for the Safe Haskell Overlapping Instances warnings
+                  -- see warnAllUnsolved
   | TypeDefer     -- A type error is deferred to runtime; no error or warning at compile time
 
 data HoleChoice
@@ -289,9 +296,9 @@ instance Outputable HoleChoice where
   ppr HoleDefer = text "HoleDefer"
 
 instance Outputable TypeErrorChoice  where
-  ppr TypeError = text "TypeError"
-  ppr TypeWarn  = text "TypeWarn"
-  ppr TypeDefer = text "TypeDefer"
+  ppr TypeError         = text "TypeError"
+  ppr (TypeWarn reason) = text "TypeWarn" <+> ppr reason
+  ppr TypeDefer         = text "TypeDefer"
 
 data ReportErrCtxt
     = CEC { cec_encl :: [Implication]  -- Enclosing implications
@@ -303,10 +310,6 @@ data ReportErrCtxt
                                        -- into warnings, and emit evidence bindings
                                        -- into 'cec_binds' for unsolved constraints
 
-          , cec_errors_as_warns :: Bool   -- Turn all errors into warnings
-                                          -- (except for Holes, which are
-                                          -- controlled by cec_type_holes and
-                                          -- cec_expr_holes)
           , cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime
 
           -- cec_expr_holes is a union of:
@@ -327,7 +330,6 @@ data ReportErrCtxt
 
 instance Outputable ReportErrCtxt where
   ppr (CEC { cec_binds              = bvar
-           , cec_errors_as_warns    = ew
            , cec_defer_type_errors  = dte
            , cec_expr_holes         = eh
            , cec_type_holes         = th
@@ -336,7 +338,6 @@ instance Outputable ReportErrCtxt where
            , cec_suppress           = sup })
     = text "CEC" <+> braces (vcat
          [ text "cec_binds"              <+> equals <+> ppr bvar
-         , text "cec_errors_as_warns"    <+> equals <+> ppr ew
          , text "cec_defer_type_errors"  <+> equals <+> ppr dte
          , text "cec_expr_holes"         <+> equals <+> ppr eh
          , text "cec_type_holes"         <+> equals <+> ppr th
@@ -344,6 +345,21 @@ instance Outputable ReportErrCtxt where
          , text "cec_warn_redundant"     <+> equals <+> ppr wr
          , text "cec_suppress"           <+> equals <+> ppr sup ])
 
+-- | Returns True <=> the ReportErrCtxt indicates that something is deferred
+deferringAnyBindings :: ReportErrCtxt -> Bool
+  -- Don't check cec_type_holes, as these don't cause bindings to be deferred
+deferringAnyBindings (CEC { cec_defer_type_errors  = TypeError
+                          , cec_expr_holes         = HoleError
+                          , cec_out_of_scope_holes = HoleError }) = False
+deferringAnyBindings _                                            = True
+
+-- | Transforms a 'ReportErrCtxt' into one that does not defer any bindings
+-- at all.
+noDeferredBindings :: ReportErrCtxt -> ReportErrCtxt
+noDeferredBindings ctxt = ctxt { cec_defer_type_errors  = TypeError
+                               , cec_expr_holes         = HoleError
+                               , cec_out_of_scope_holes = HoleError }
+
 {-
 Note [Suppressing error messages]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -359,7 +375,8 @@ Specifically (see reportWanteds)
 -}
 
 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
-reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
+reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope
+                                 , ic_given = given
                                  , ic_wanted = wanted, ic_binds = evb
                                  , ic_status = status, ic_info = info
                                  , ic_env = tcl_env, ic_tclvl = tc_lvl })
@@ -374,7 +391,8 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
   = do { traceTc "reportImplic" (ppr implic')
        ; reportWanteds ctxt' tc_lvl wanted
        ; when (cec_warn_redundant ctxt) $
-         warnRedundantConstraints ctxt' tcl_env info' dead_givens }
+         warnRedundantConstraints ctxt' tcl_env info' dead_givens
+       ; when bad_telescope $ reportBadTelescope ctxt tcl_env m_telescope tvs }
   where
     insoluble    = isInsolubleStatus status
     (env1, tvs') = mapAccumL tidyTyCoVarBndr (cec_tidy ctxt) tvs
@@ -382,8 +400,9 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
     implic' = implic { ic_skols = tvs'
                      , ic_given = map (tidyEvVar env1) given
                      , ic_info  = info' }
-    ctxt1 | termEvidenceAllowed info = ctxt
-          | otherwise                = ctxt { cec_defer_type_errors = TypeError }
+    ctxt1 | NoEvBindsVar{} <- evb    = noDeferredBindings ctxt
+          | termEvidenceAllowed info = ctxt
+          | otherwise                = noDeferredBindings ctxt
           -- If we go inside an implication that has no term
           -- evidence (i.e. unifying under a forall), we can't defer
           -- type errors.  You could imagine using the /enclosing/
@@ -406,6 +425,10 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
                     IC_Solved { ics_dead = dead } -> dead
                     _                             -> []
 
+    bad_telescope = case status of
+              IC_BadTelescope -> True
+              _               -> False
+
 warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [EvVar] -> TcM ()
 -- See Note [Tracking redundant constraints] in TcSimplify
 warnRedundantConstraints ctxt env info ev_vars
@@ -436,6 +459,20 @@ warnRedundantConstraints ctxt env info ev_vars
    improving ev_var = any isImprovementPred $
                       transSuperClasses (idType ev_var)
 
+reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> Maybe SDoc -> [TcTyVar] -> TcM ()
+reportBadTelescope ctxt env (Just telescope) skols
+  = do { msg <- mkErrorReport ctxt env (important doc)
+       ; reportError msg }
+  where
+    doc = hang (text "These kind and type variables:" <+> telescope $$
+                text "are out of dependency order. Perhaps try this ordering:")
+             2 (pprTyVars sorted_tvs)
+
+    sorted_tvs = toposortTyVars skols
+
+reportBadTelescope _ _ Nothing skols
+  = pprPanic "reportBadTelescope" (ppr skols)
+
 {- Note [Redundant constraints in instance decls]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 For instance declarations, we don't report unused givens if
@@ -792,19 +829,17 @@ maybeReportError ctxt err
   | cec_suppress ctxt    -- Some worse error has occurred;
   = return ()            -- so suppress this error/warning
 
-  | cec_errors_as_warns ctxt
-  = reportWarning NoReason err
-
   | otherwise
   = case cec_defer_type_errors ctxt of
-      TypeDefer -> return ()
-      TypeWarn  -> reportWarning (Reason Opt_WarnDeferredTypeErrors) err
-      TypeError -> reportError err
+      TypeDefer       -> return ()
+      TypeWarn reason -> reportWarning reason err
+      TypeError       -> reportError err
 
 addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
 -- See Note [Deferring coercion errors to runtime]
 addDeferredBinding ctxt err ct
-  | CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
+  | deferringAnyBindings ctxt
+  , CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
     -- Only add deferred bindings for Wanted constraints
   = do { dflags <- getDynFlags
        ; let err_msg = pprLocErrMsg err
@@ -1229,7 +1264,7 @@ validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
                   (vcat (map (pprHoleFit showProvenance) sortedRSubs)
                     $$ ppWhen rDiscards refSubsDiscardMsg) }
        else return empty
-     ; traceTc "}" empty
+     ; traceTc "findingValidSubstitutionsFor }" empty
      ; return (vMsg $$ refMsg)}
   where
     hole_loc = ctEvLoc $ ctEvidence ct
@@ -1334,7 +1369,13 @@ validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
     getHoleCloningSubst :: TcType -> TcM TCvSubst
     getHoleCloningSubst hole_ty = mkTvSubstPrs <$> getClonedVars
       where cloneFV :: TyVar -> TcM (TyVar, Type)
-            cloneFV fv = ((,) fv) <$> newFlexiTyVarTy (varType fv)
+            cloneFV fv = ((,) fv) <$> pushTcLevelM_ (newFlexiTyVarTy (varType fv))
+             -- The subsumption check pushes the level, so as to be sure that
+             -- its invocation of the solver doesn't unify type variables floating
+             -- about that are unrelated to the subsumption check. However, these
+             -- cloned variables in the hole type *should* be unified, so we make
+             -- sure to bump the level before creating them
+
             getClonedVars :: TcM [(TyVar, Type)]
             getClonedVars = mapM cloneFV (fvVarList $ tyCoFVsOfType hole_ty)
 
@@ -2314,13 +2355,22 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
                , maybe (text "found something with kind")
                        (\thing -> quotes thing <+> text "has kind")
                        maybe_thing
-               , quotes (ppr act) ]
+               , quotes (pprWithTYPE act) ]
 
     msg5 th = hang (text "Expected" <+> kind_desc <> comma)
                  2 (text "but" <+> quotes th <+> text "has kind" <+>
                     quotes (ppr act))
       where
         kind_desc | isConstraintKind exp = text "a constraint"
+
+                    -- TYPE t0
+                  | Just (tc, [arg]) <- tcSplitTyConApp_maybe exp
+                  , tc `hasKey` tYPETyConKey
+                  , tcIsTyVarTy arg      = sdocWithDynFlags $ \dflags ->
+                                           if gopt Opt_PrintExplicitRuntimeReps dflags
+                                           then text "kind" <+> quotes (ppr exp)
+                                           else text "a type"
+
                   | otherwise            = text "kind" <+> quotes (ppr exp)
 
     num_args_msg = case level of
index 0930d7a..628bb7a 100644 (file)
@@ -401,6 +401,14 @@ data EvBindsVar
       -- See Note [Tracking redundant constraints] in TcSimplify
     }
 
+  | NoEvBindsVar {  -- used when we're solving only for equalities,
+                    -- which don't have bindings
+
+        -- see above for comments
+      ebv_uniq :: Unique,
+      ebv_tcvs :: IORef CoVarSet
+    }
+
 instance Data.Data TcEvBinds where
   -- Placeholder; we can't travers into TcEvBinds
   toConstr _   = abstractConstr "TcEvBinds"
@@ -873,9 +881,11 @@ instance Outputable TcEvBinds where
 instance Outputable EvBindsVar where
   ppr (EvBindsVar { ebv_uniq = u })
      = text "EvBindsVar" <> angleBrackets (ppr u)
+  ppr (NoEvBindsVar { ebv_uniq = u })
+     = text "NoEvBindsVar" <> angleBrackets (ppr u)
 
 instance Uniquable EvBindsVar where
-  getUnique (EvBindsVar { ebv_uniq = u }) = u
+  getUnique = ebv_uniq
 
 instance Outputable EvBind where
   ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
index 43ff221..00b9be5 100644 (file)
@@ -1518,6 +1518,7 @@ zonkEvBindsVar :: ZonkEnv -> EvBindsVar -> TcM (ZonkEnv, Bag EvBind)
 zonkEvBindsVar env (EvBindsVar { ebv_binds = ref })
   = do { bs <- readMutVar ref
        ; zonkEvBinds env (evBindMapBinds bs) }
+zonkEvBindsVar env (NoEvBindsVar {}) = return (env, emptyBag)
 
 zonkEvBinds :: ZonkEnv -> Bag EvBind -> TcM (ZonkEnv, Bag EvBind)
 zonkEvBinds env binds
index 2b324ca..3125927 100644 (file)
@@ -18,12 +18,17 @@ module TcHsType (
         tcHsDeriv, tcHsVectInst,
         tcHsTypeApp,
         UserTypeCtxt(..),
-        tcImplicitTKBndrs, tcImplicitTKBndrsType, tcExplicitTKBndrs,
+        tcImplicitTKBndrs, tcImplicitTKBndrsX, tcImplicitTKBndrsSig,
+        tcExplicitTKBndrs, tcExplicitTKBndrsX, tcExplicitTKBndrsSig,
+        kcExplicitTKBndrs, kcImplicitTKBndrs,
 
                 -- Type checking type and class decls
         kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
         tcDataKindSig,
 
+          -- tyvars
+        scopeTyVars, scopeTyVars2,
+
         -- Kind-checking types
         -- No kind generalisation, no checkValidType
         kcLHsQTyVars, kcLHsTyVarBndrs,
@@ -42,6 +47,9 @@ module TcHsType (
         -- Sort-checking kinds
         tcLHsKindSig, badKindSig,
 
+        -- Zonking and promoting
+        zonkPromoteType,
+
         -- Pattern type signatures
         tcHsPatSigType, tcPatSig, funAppCtxt
    ) where
@@ -58,12 +66,13 @@ import TcMType
 import TcValidity
 import TcUnify
 import TcIface
-import TcSimplify ( solveEqualities )
+import TcSimplify
 import TcType
 import TcHsSyn( zonkSigType )
 import Inst   ( tcInstBinders, tcInstBinder )
 import TyCoRep( TyBinder(..) )  -- Used in tcDataKindSig
 import Type
+import Coercion
 import Kind
 import RdrName( lookupLocalRdrOcc )
 import Var
@@ -183,23 +192,24 @@ 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_vars = sig_vars })
+kcHsSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
+kcHsSigType skol_info names (HsIB { hsib_body = hs_ty
+                                  , hsib_vars = sig_vars })
   = addSigCtxt (funsSigCtxt names) hs_ty $
     discardResult $
-    tcImplicitTKBndrsType sig_vars $
+    tcImplicitTKBndrs skol_info sig_vars $
     tc_lhs_type typeLevelMode hs_ty liftedTypeKind
 
-tcClassSigType :: [Located Name] -> LHsSigType GhcRn -> TcM Type
+tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
 -- Does not do validity checking; this must be done outside
 -- the recursive class declaration "knot"
-tcClassSigType names sig_ty
+tcClassSigType skol_info names sig_ty
   = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
-    tc_hs_sig_type_and_gen sig_ty liftedTypeKind
+    tc_hs_sig_type_and_gen skol_info sig_ty liftedTypeKind
 
 tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
 -- Does validity checking
+-- See Note [Recipe for checking a signature]
 tcHsSigType ctxt sig_ty
   = addSigCtxt ctxt (hsSigType sig_ty) $
     do { kind <- case expectedKindInCtxt ctxt of
@@ -212,36 +222,48 @@ tcHsSigType ctxt sig_ty
           -- Generalise here: see Note [Kind generalisation]
        ; do_kind_gen <- decideKindGeneralisationPlan sig_ty
        ; ty <- if do_kind_gen
-               then tc_hs_sig_type_and_gen sig_ty kind
-               else tc_hs_sig_type         sig_ty kind >>= zonkTcType
+               then tc_hs_sig_type_and_gen skol_info sig_ty kind
+               else tc_hs_sig_type         skol_info sig_ty kind
 
        ; checkValidType ctxt ty
        ; return ty }
+  where
+    skol_info = SigTypeSkol ctxt
 
-tc_hs_sig_type_and_gen :: LHsSigType GhcRn -> Kind -> TcM Type
+tc_hs_sig_type_and_gen :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
 -- Kind-checks/desugars an 'LHsSigType',
 --   solve equalities,
 --   and then kind-generalizes.
 -- This will never emit constraints, as it uses solveEqualities interally.
 -- No validity checking, but it does zonk en route to generalization
-tc_hs_sig_type_and_gen hs_ty kind
-  = do { ty <- solveEqualities $
-               tc_hs_sig_type hs_ty kind
+tc_hs_sig_type_and_gen skol_info (HsIB { hsib_vars = sig_vars
+                                       , hsib_body = hs_ty }) kind
+  = do { (tkvs, ty) <- solveEqualities $
+                       tcImplicitTKBndrs skol_info sig_vars $
+                       tc_lhs_type typeLevelMode hs_ty kind
          -- NB the call to solveEqualities, which unifies all those
          --    kind variables floating about, immediately prior to
          --    kind generalisation
-       ; kindGeneralizeType ty }
 
-tc_hs_sig_type :: LHsSigType GhcRn -> Kind -> TcM Type
+         -- We use "InKnot", because this is called on class method sigs
+         -- in the knot
+       ; ty1 <- zonkPromoteTypeInKnot $ mkSpecForAllTys tkvs ty
+       ; kvs <- kindGeneralize ty1
+       ; zonkSigType (mkInvForAllTys kvs ty1) }
+
+tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
 -- Kind-check/desugar a 'LHsSigType', but does not solve
 -- the equalities that arise from doing so; instead it may
 -- emit kind-equality constraints into the monad
--- No zonking or validity checking
-tc_hs_sig_type (HsIB { hsib_vars = sig_vars
-                     , hsib_body = hs_ty }) kind
-  = do { (tkvs, ty) <- tcImplicitTKBndrsType sig_vars $
+-- Zonking, but no validity checking
+tc_hs_sig_type skol_info (HsIB { hsib_vars = sig_vars
+                               , hsib_body = hs_ty }) kind
+  = do { (tkvs, ty) <- tcImplicitTKBndrs skol_info sig_vars $
                        tc_lhs_type typeLevelMode hs_ty kind
-       ; return (mkSpecForAllTys tkvs ty) }
+
+          -- need to promote any remaining metavariables; test case:
+          -- dependent/should_fail/T14066e.
+       ; zonkPromoteType (mkSpecForAllTys tkvs ty) }
 
 -----------------
 tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
@@ -256,7 +278,7 @@ tcHsDeriv hs_ty
                     -- can be no covars in an outer scope
        ; ty <- checkNoErrs $
                  -- avoid redundant error report with "illegal deriving", below
-               tc_hs_sig_type_and_gen hs_ty cls_kind
+               tc_hs_sig_type_and_gen (SigTypeSkol DerivClauseCtxt) hs_ty cls_kind
        ; cls_kind <- zonkTcType cls_kind
        ; let (tvs, pred) = splitForAllTys ty
        ; let (args, _) = splitFunTys cls_kind
@@ -270,7 +292,7 @@ tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
 -- Like tcHsSigType, but for a class instance declaration
 tcHsClsInstType user_ctxt hs_inst_ty
   = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
-    do { inst_ty <- tc_hs_sig_type_and_gen hs_inst_ty constraintKind
+    do { inst_ty <- tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind
        ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
 
 -- Used for 'VECTORISE [SCALAR] instance' declarations
@@ -292,11 +314,12 @@ tcHsVectInst ty
 ----------------------------------------------
 -- | Type-check a visible type application
 tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
+-- See Note [Recipe for checking a signature] in TcHsType
 tcHsTypeApp wc_ty kind
   | HsWC { hswc_wcs = sig_wcs, hswc_body = hs_ty } <- wc_ty
-  = do { ty <- tcWildCardBindersX newWildTyVar sig_wcs $ \ _ ->
+  = do { ty <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ _ ->
                tcCheckLHsType hs_ty kind
-       ; ty <- zonkTcType ty
+       ; ty <- zonkPromoteType ty
        ; checkValidType TypeAppCtxt ty
        ; return ty }
         -- NB: we don't call emitWildcardHoleConstraints here, because
@@ -611,15 +634,13 @@ tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind
   = tc_fun_type mode ty1 ty2 exp_kind
 
 --------- Foralls
-tc_hs_type mode (HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
-  = fmap fst $
-    tcExplicitTKBndrs hs_tvs $ \ tvs' ->
+tc_hs_type mode forall@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
+  = do { (tvs', ty') <- tcExplicitTKBndrs (ForAllSkol (ppr forall)) hs_tvs $
+                        tc_lhs_type mode ty exp_kind
     -- Do not kind-generalise here!  See Note [Kind generalisation]
     -- Why exp_kind?  See Note [Body kind of HsForAllTy]
-    do { ty' <- tc_lhs_type mode ty exp_kind
-       ; let bound_vars = allBoundVariables ty'
-             bndrs      = mkTyVarBinders Specified tvs'
-       ; return (mkForAllTys bndrs ty', bound_vars) }
+       ; let bndrs      = mkTyVarBinders Specified tvs'
+       ; return (mkForAllTys bndrs ty') }
 
 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
   | null (unLoc ctxt)
@@ -759,9 +780,8 @@ tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
 tc_hs_type mode ty@(HsCoreTy {})  ek = tc_infer_hs_type_ek mode ty ek
 
 tc_hs_type _ (HsWildCardTy wc) exp_kind
-  = do { wc_tv <- tcWildCardOcc wc exp_kind
-       ; return (mkNakedCastTy (mkTyVarTy wc_tv)
-                               (mkTcNomReflCo exp_kind))
+  = do { wc_ty <- tcWildCardOcc wc exp_kind
+       ; return (mkNakedCastTy wc_ty (mkTcNomReflCo exp_kind))
          -- Take care here! Even though the coercion is Refl,
          -- we still need it to establish Note [The tcType invariant]
        }
@@ -770,13 +790,12 @@ tc_hs_type _ (HsWildCardTy wc) exp_kind
 tc_hs_type _ ty@(HsAppsTy {}) _
   = pprPanic "tc_hs_tyep HsAppsTy" (ppr ty)
 
-tcWildCardOcc :: HsWildCardInfo GhcRn -> Kind -> TcM TcTyVar
+tcWildCardOcc :: HsWildCardInfo GhcRn -> Kind -> TcM TcType
 tcWildCardOcc wc_info exp_kind
   = do { wc_tv <- tcLookupTyVar (wildCardName wc_info)
           -- The wildcard's kind should be an un-filled-in meta tyvar
-       ; let Just wc_kind_var = tcGetTyVar_maybe (tyVarKind wc_tv)
-       ; writeMetaTyVar wc_kind_var exp_kind
-       ; return wc_tv }
+       ; checkExpectedKind (HsWildCardTy wc_info) (mkTyVarTy wc_tv)
+                           (tyVarKind wc_tv) exp_kind }
 
 ---------------------------
 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
@@ -947,10 +966,10 @@ tcTyApps mode orig_hs_ty fun_ty fun_ki args
 --------------------------
 -- Like checkExpectedKindX, but returns only the final type; convenient wrapper
 -- Obeys Note [The tcType invariant]
-checkExpectedKind :: HsType GhcRn
-                  -> TcType
-                  -> TcKind
-                  -> TcKind
+checkExpectedKind :: HsType GhcRn   -- type we're checking (for printing)
+                  -> TcType         -- type we're checking (might be knot-tied)
+                  -> TcKind         -- the known kind of that type
+                  -> TcKind         -- the expected kind
                   -> TcM TcType
 checkExpectedKind hs_ty ty act exp
   = fstOf3 <$> checkExpectedKindX Nothing (ppr hs_ty) ty act exp
@@ -1356,24 +1375,6 @@ addTypeCtxt (L _ ty) thing
 %*                                                                      *
 %************************************************************************
 
-Note [Scope-check inferred kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-
-  data SameKind :: k -> k -> *
-  foo :: forall a (b :: Proxy a) (c :: Proxy d). SameKind b c
-
-d has no binding site. So it gets bound implicitly, at the top. The
-problem is that d's kind mentions `a`. So it's all ill-scoped.
-
-The way we check for this is to gather all variables *bound* in a
-type variable's scope. The type variable's kind should not mention
-any of these variables. That is, d's kind can't mention a, b, or c.
-We can't just check to make sure that d's kind is in scope, because
-we might be about to kindGeneralize.
-
-A little messy, but it works.
-
 Note [Dependent LHsQTyVars]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We track (in the renamer) which explicitly bound variables in a
@@ -1407,8 +1408,8 @@ Earlier, thought it would work simply to do a free-variable check
 during kcLHsQTyVars, but this is bogus, because there may be
 unsolved equalities about. And we don't want to eagerly solve the
 equalities, because we may get further information after
-kcLHsQTyVars is called.  (Recall that kcLHsQTyVars is usually
-called from getInitialKind.  The only other case is in kcConDecl.)
+kcLHsQTyVars is called.  (Recall that kcLHsQTyVars is called
+only from getInitialKind.)
 This is what implements the rule that all variables intended to be
 dependent must be manifestly so.
 
@@ -1450,25 +1451,98 @@ There are some wrinkles
   We sort this out using findDupSigTvs, in TcTyClTyVars; very much
   as we do with partial type signatures in mk_psig_qtvs in
   TcBinds.chooseInferredQuantifiers
+
+Note [Keeping scoped variables in order: Explicit]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When the user writes `forall a b c. blah`, we bring a, b, and c into
+scope and then check blah. In the process of checking blah, we might
+learn the kinds of a, b, and c, and these kinds might indicate that
+b depends on c, and thus that we should reject the user-written type.
+
+One approach to doing this would be to bring each of a, b, and c into
+scope, one at a time, creating an implication constraint and
+bumping the TcLevel for each one. This would work, because the kind
+of, say, b would be untouchable when c is in scope (and the constraint
+couldn't float out because c blocks it). However, it leads to terrible
+error messages, complaining about skolem escape. While it is indeed
+a problem of skolem escape, we can do better.
+
+Instead, our approach is to bring the block of variables into scope
+all at once, creating one implication constraint for the lot. The
+user-written variables are skolems in the implication constraint. In
+TcSimplify.setImplicationStatus, we check to make sure that the ordering
+is correct, choosing ImplicationStatus IC_BadTelescope if they aren't.
+Then, in TcErrors, we report if there is a bad telescope. This way,
+we can report a suggested ordering to the user if there is a problem.
+
+Note [Keeping scoped variables in order: Implicit]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When the user implicitly quantifies over variables (say, in a type
+signature), we need to come up with some ordering on these variables.
+This is done by bumping the TcLevel, bringing the tyvars into scope,
+and then type-checking the thing_inside. The constraints are all
+wrapped in an implication, which is then solved. Finally, we can
+zonk all the binders and then order them with toposortTyVars.
+
+It's critical to solve before zonking and ordering in order to uncover
+any unifications. You might worry that this eager solving could cause
+trouble elsewhere. I don't think it will. Because it will solve only
+in an increased TcLevel, it can't unify anything that was mentioned
+elsewhere. Additionally, we require that the order of implicitly
+quantified variables is manifest by the scope of these variables, so
+we're not going to learn more information later that will help order
+these variables.
+
+Note [Recipe for checking a signature]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Checking a user-written signature requires several steps:
+
+ 1. Generate constraints.
+ 2. Solve constraints.
+ 3. Zonk and promote tyvars.
+ 4. (Optional) Kind-generalize.
+ 5. Check validity.
+
+There may be some surprises in here:
+
+Step 2 is necessary for two reasons: most signatures also bring
+implicitly quantified variables into scope, and solving is necessary
+to get these in the right order (see Note [Keeping scoped variables in
+order: Implicit]). Additionally, solving is necessary in order to
+kind-generalize correctly.
+
+Step 3 requires *promoting* type variables. If there are any foralls
+in a type, the TcLevel will be bumped within the forall. This might
+lead to the generation of matavars with a high level. If we don't promote,
+we violate MetaTvInv of Note [TcLevel and untouchable type variables]
+in TcType.
+
 -}
 
-tcWildCardBinders :: [Name]
+tcWildCardBinders :: SkolemInfo
+                  -> [Name]
                   -> ([(Name, TcTyVar)] -> TcM a)
                   -> TcM a
-tcWildCardBinders = tcWildCardBindersX new_tv
+tcWildCardBinders info = tcWildCardBindersX new_tv (Just info)
   where
     new_tv name = do { kind <- newMetaKindVar
                      ; newSkolemTyVar name kind }
 
 tcWildCardBindersX :: (Name -> TcM TcTyVar)
+                   -> Maybe SkolemInfo -- Just <=> we're bringing fresh vars
+                                       -- into scope; use scopeTyVars
                    -> [Name]
                    -> ([(Name, TcTyVar)] -> TcM a)
                    -> TcM a
-tcWildCardBindersX new_wc wc_names thing_inside
+tcWildCardBindersX new_wc maybe_skol_info wc_names thing_inside
   = do { wcs <- mapM new_wc wc_names
        ; let wc_prs = wc_names `zip` wcs
-       ; tcExtendTyVarEnv2 wc_prs $
+       ; scope_tvs wc_prs $
          thing_inside wc_prs }
+  where
+    scope_tvs
+      | Just info <- maybe_skol_info = scopeTyVars2 info
+      | otherwise                    = tcExtendTyVarEnv2
 
 -- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
 -- user-supplied kind signature (CUSK), generalise the result.
@@ -1478,25 +1552,26 @@ tcWildCardBindersX new_wc wc_names thing_inside
 -- HsDecls.
 --
 -- This function does not do telescope checking.
-kcLHsQTyVars :: Name    -- ^ of the thing being checked
-             -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
-             -> Bool    -- ^ True <=> the decl being checked has a CUSK
-             -> Bool    -- ^ True <=> all the hsq_implicit are *kind* vars
-                        -- (will give these kind * if -XNoTypeInType)
+kcLHsQTyVars :: Name              -- ^ of the thing being checked
+             -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
+             -> Bool              -- ^ True <=> the decl being checked has a CUSK
              -> LHsQTyVars GhcRn
              -> TcM (Kind, r)     -- ^ The result kind, possibly with other info
              -> TcM (TcTyCon, r)  -- ^ A suitably-kinded TcTyCon
-kcLHsQTyVars name flav cusk all_kind_vars
-  (HsQTvs { hsq_implicit = kv_ns, hsq_explicit = hs_tvs
-          , hsq_dependent = dep_names }) thing_inside
+kcLHsQTyVars name flav cusk
+  user_tyvars@(HsQTvs { hsq_implicit = kv_ns, hsq_explicit = hs_tvs
+                      , hsq_dependent = dep_names }) thing_inside
   | cusk
-  = do { kv_kinds <- mk_kv_kinds
-       ; lvl <- getTcLevel
-       ; let scoped_kvs    = zipWith (mk_skolem_tv lvl) kv_ns kv_kinds
-       ; tcExtendTyVarEnv scoped_kvs $
-    do { (tc_tvs, (res_kind, stuff))
-              <- solveEqualities $
-                 kcLHsTyVarBndrs open_fam hs_tvs thing_inside
+  = do { typeintype <- xoptM LangExt.TypeInType
+       ; let m_kind
+               | typeintype = Nothing
+               | otherwise  = Just liftedTypeKind
+                 -- without -XTypeInType, default all kind variables to have kind *
+
+       ; (scoped_kvs, (tc_tvs, (res_kind, stuff)))
+           <- solveEqualities $
+              tcImplicitTKBndrsX newSkolemTyVar m_kind skol_info kv_ns $
+              kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
 
            -- Now, because we're in a CUSK, quantify over the mentioned
            -- kind vars, in dependency order.
@@ -1510,7 +1585,17 @@ kcLHsQTyVars name flav cusk all_kind_vars
           -- If there are any meta-tvs left, the user has
           -- lied about having a CUSK. Error.
        ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
-       ; when (not (null meta_tvs)) $
+          -- skip this check for associated types. Why?
+          -- Any variables mentioned in the definition will get defaulted,
+          -- except those that appear in the class head. Defaulted vars do
+          -- not concern us here (they are fully determined). Variables from
+          -- the class head will be fully determined whenever the class has
+          -- a CUSK, and an associated family has a CUSK only when the enclosing
+          -- class has one. So skipping is safe. But why is it necessary?
+          -- It's possible that a class variable has too low a TcLevel to have
+          -- fully settled down by this point, and so this check will get
+          -- a false positive.
+       ; when (not_associated && not (null meta_tvs)) $
          report_non_cusk_tvs (qkvs ++ tc_tvs)
 
           -- If any of the scoped_kvs aren't actually mentioned in a binder's
@@ -1526,7 +1611,7 @@ kcLHsQTyVars name flav cusk all_kind_vars
 
        ; let final_binders = map (mkNamedTyConBinder Specified) good_tvs
                             ++ tc_binders
-             tycon = mkTcTyCon name final_binders res_kind
+             tycon = mkTcTyCon name (ppr user_tyvars) final_binders res_kind
                                (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
                                flav
                            -- the tvs contain the binders already
@@ -1539,19 +1624,26 @@ kcLHsQTyVars name flav cusk all_kind_vars
               , ppr tc_tvs, ppr (mkTyConKind final_binders res_kind)
               , ppr qkvs, ppr meta_tvs, ppr good_tvs, ppr final_binders ]
 
-       ; return (tycon, stuff) }}
+       ; return (tycon, stuff) }
 
   | otherwise
-  = do { kv_kinds <- mk_kv_kinds
-       ; scoped_kvs <- zipWithM newSigTyVar kv_ns kv_kinds
+  = do { typeintype <- xoptM LangExt.TypeInType
+
+             -- if -XNoTypeInType and we know all the implicits are kind vars,
+             -- just give the kind *. This prevents test
+             -- dependent/should_fail/KindLevelsB from compiling, as it should
+       ; let default_kind
+               | typeintype = Nothing
+               | otherwise  = Just liftedTypeKind
            -- Why newSigTyVar?  See Note [Kind generalisation and sigTvs]
-       ; (tc_tvs, (res_kind, stuff))
-           <- tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
-              kcLHsTyVarBndrs open_fam hs_tvs thing_inside
+       ; (scoped_kvs, (tc_tvs, (res_kind, stuff)))
+           <- kcImplicitTKBndrs kv_ns default_kind $
+              kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
+
        ; let   -- NB: Don't add scoped_kvs to tyConTyVars, because they
                -- must remain lined up with the binders
              tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
-             tycon = mkTcTyCon name tc_binders res_kind
+             tycon = mkTcTyCon name (ppr user_tyvars) tc_binders res_kind
                                (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
                                flav
 
@@ -1561,6 +1653,12 @@ kcLHsQTyVars name flav cusk all_kind_vars
        ; return (tycon, stuff) }
   where
     open_fam = tcFlavourIsOpen flav
+    not_associated = case flav of
+      DataFamilyFlavour assoc     -> not assoc
+      OpenTypeFamilyFlavour assoc -> not assoc
+      _                           -> True
+
+    skol_info = TyConSkol flav name
 
     mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
     -- See Note [Dependent LHsQTyVars]
@@ -1570,16 +1668,6 @@ kcLHsQTyVars name flav cusk all_kind_vars
        | otherwise
        = mkAnonTyConBinder tv
 
-
-      -- if -XNoTypeInType and we know all the implicits are kind vars,
-      -- just give the kind *. This prevents test
-      -- dependent/should_fail/KindLevelsB from compiling, as it should
-    mk_kv_kinds :: TcM [Kind]
-    mk_kv_kinds = do { typeintype <- xoptM LangExt.TypeInType
-                     ; if not typeintype && all_kind_vars
-                       then return (map (const liftedTypeKind) kv_ns)
-                       else mapM (const newMetaKindVar) kv_ns }
-
     report_non_cusk_tvs all_tvs
       = do { all_tvs <- mapM zonkTyCoVarKind all_tvs
            ; let (_, tidy_tvs)         = tidyOpenTyCoVars emptyTidyEnv all_tvs
@@ -1597,37 +1685,43 @@ kcLHsQTyVars name flav cusk all_kind_vars
         pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
 
 
-kcLHsTyVarBndrs :: Bool   -- True <=> Default un-annotated tyvar
+kcLHsTyVarBndrs :: Bool   -- True <=> bump the TcLevel when bringing vars into scope
+                -> Bool   -- True <=> Default un-annotated tyvar
                           --          binders to kind *
+                -> SkolemInfo
                 -> [LHsTyVarBndr GhcRn]
                 -> TcM r
                 -> TcM ([TyVar], r)
 -- There may be dependency between the explicit "ty" vars.
 -- So, we have to handle them one at a time.
-kcLHsTyVarBndrs _ [] thing
+kcLHsTyVarBndrs _ _ _ [] thing
   = do { stuff <- thing; return ([], stuff) }
 
-kcLHsTyVarBndrs open_fam (L _ hs_tv : hs_tvs) thing
+kcLHsTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing
   = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
                -- NB: Bring all tvs into scope, even non-dependent ones,
                -- as they're needed in type synonyms, data constructors, etc.
 
        ; (tvs, stuff) <- bind_unless_scoped tv_pair $
-                         kcLHsTyVarBndrs open_fam hs_tvs $
+                         kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs $
                          thing
 
        ; return ( tv : tvs, stuff ) }
   where
-
     -- | Bind the tyvar in the env't unless the bool is True
     bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a
     bind_unless_scoped (_, True)   thing_inside = thing_inside
     bind_unless_scoped (tv, False) thing_inside
-      = tcExtendTyVarEnv [tv] thing_inside
+      | cusk      = scopeTyVars skol_info [tv] thing_inside
+      | otherwise = tcExtendTyVarEnv      [tv] thing_inside
+         -- These variables haven't settled down yet, so we don't want to bump
+         -- the TcLevel. If we do, then we'll have metavars of too high a level
+         -- floating about. Changing this causes many, many failures in the
+         -- `dependent` testsuite directory.
 
     kc_hs_tv :: HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
     kc_hs_tv (UserTyVar lname@(L _ name))
-      = do { tv_pair@(tv, in_scope) <- tcHsTyVarName Nothing name
+      = do { tv_pair@(tv, in_scope) <- tcHsTyVarName newSkolemTyVar Nothing name
 
              -- Open type/data families default their variables to kind *.
              -- But don't default in-scope class tyvars, of course
@@ -1638,104 +1732,177 @@ kcLHsTyVarBndrs open_fam (L _ hs_tv : hs_tvs) thing
            ; return tv_pair }
 
     kc_hs_tv (KindedTyVar (L _ name) lhs_kind)
-      = do { kind <- tcLHsKindSig lhs_kind
-           ; tcHsTyVarName (Just kind) name }
+      = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt name) lhs_kind
+           ; tcHsTyVarName newSkolemTyVar (Just kind) name }
 
-
-tcImplicitTKBndrs :: [Name]
-                  -> TcM (a, TyVarSet)   -- vars are bound somewhere in the scope
-                                         -- see Note [Scope-check inferred kinds]
+tcImplicitTKBndrs :: SkolemInfo
+                  -> [Name]
+                  -> TcM a
                   -> TcM ([TcTyVar], a)
-tcImplicitTKBndrs = tcImplicitTKBndrsX (tcHsTyVarName Nothing)
-
--- | Convenient specialization
-tcImplicitTKBndrsType :: [Name]
-                      -> TcM Type
-                      -> TcM ([TcTyVar], Type)
-tcImplicitTKBndrsType var_ns thing_inside
-  = tcImplicitTKBndrs var_ns $
-    do { res_ty <- thing_inside
-       ; return (res_ty, allBoundVariables res_ty) }
-
--- this more general variant is needed in tcHsPatSigType.
--- See Note [Pattern signature binders]
-tcImplicitTKBndrsX :: (Name -> TcM (TcTyVar, Bool))  -- new_tv function
+tcImplicitTKBndrs = tcImplicitTKBndrsX newSkolemTyVar Nothing
+
+-- | Like 'tcImplicitTKBndrs', but uses 'newSigTyVar' to create tyvars
+tcImplicitTKBndrsSig :: SkolemInfo
+                     -> [Name]
+                     -> TcM a
+                     -> TcM ([TcTyVar], a)
+tcImplicitTKBndrsSig = tcImplicitTKBndrsX newSigTyVar Nothing
+
+tcImplicitTKBndrsX :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
+                   -> Maybe Kind           -- Just k <=> assign all names this kind
+                   -> SkolemInfo
                    -> [Name]
-                   -> TcM (a, TyVarSet)
-                   -> TcM ([TcTyVar], a)
--- Returned TcTyVars have the supplied Names,
+                   -> TcM a
+                   -> TcM ([TcTyVar], a)   -- these tyvars are dependency-ordered
+-- Returned TcTyVars have the supplied HsTyVarBndrs,
 -- but may be in different order to the original [Name]
 --   (because of sorting to respect dependency)
 -- Returned TcTyVars have zonked kinds
-tcImplicitTKBndrsX new_tv var_ns thing_inside
-  = do { tkvs_pairs <- mapM new_tv var_ns
-       ; let must_scope_tkvs = [ tkv | (tkv, False) <- tkvs_pairs ]
-             tkvs            = map fst tkvs_pairs
-       ; (result, bound_tvs) <- tcExtendTyVarEnv must_scope_tkvs $
-                                thing_inside
-
-         -- Check that the implicitly-bound kind variable
-         -- really can go at the beginning.
-         -- e.g.   forall (a :: k) (b :: *). ...(forces k :: b)...
-       ; tkvs <- mapM zonkTyCoVarKind tkvs
-                 -- NB: /not/ zonkTcTyVarToTyVar. tcImplicitTKBndrsX
-                 -- guarantees to return TcTyVars with the same Names
-                 -- as the var_ns.  See [Pattern signature binders]
-
-       ; let extra = text "NB: Implicitly-bound variables always come" <+>
-                     text "before other ones."
-       ; checkValidInferredKinds tkvs bound_tvs extra
-
-       ; let final_tvs = toposortTyVars tkvs
-       ; traceTc "tcImplicitTKBndrs" (ppr var_ns $$ ppr final_tvs)
-
+-- See Note [Keeping scoped variables in order: Implicit]
+tcImplicitTKBndrsX new_tv m_kind skol_info tv_names thing_inside
+  = do { (skol_tvs, result)
+           <- solveLocalEqualities $
+              do { (inner_tclvl, wanted, (skol_tvs, result))
+                     <- pushLevelAndCaptureConstraints $
+                     do { tv_pairs <- mapM (tcHsTyVarName new_tv m_kind) tv_names
+                        ; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ]
+                        ; result <- tcExtendTyVarEnv must_scope_tvs $
+                                    thing_inside
+                        ; return (map fst tv_pairs, result) }
+
+                 ; emitTvImplication inner_tclvl skol_tvs Nothing wanted skol_info
+                 ; return (skol_tvs, result) }
+
+       ; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
+          -- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv
+
+       ; let final_tvs = toposortTyVars skol_tvs
+       ; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs)
        ; return (final_tvs, result) }
 
-tcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
-                  -> ([TyVar] -> TcM (a, TyVarSet))
-                        -- ^ Thing inside returns the set of variables bound
-                        -- in the scope. See Note [Scope-check inferred kinds]
-                  -> TcM (a, TyVarSet)  -- ^ returns augmented bound vars
+-- | Bring implicitly quantified type/kind variables into scope during
+-- kind checking. Uses SigTvs, as per Note [Use SigTvs in kind-checking pass]
+-- in TcTyClsDecls.
+kcImplicitTKBndrs :: [Name]     -- of the vars
+                  -> Maybe Kind -- Just k <=> use k as the kind for all vars
+                                -- Nothing <=> use a meta-tyvar
+                  -> TcM a
+                  -> TcM ([TcTyVar], a)  -- returns the tyvars created
+                                         -- these are *not* dependency ordered
+kcImplicitTKBndrs var_ns m_kind thing_inside
+  = do { tkvs_pairs <- mapM (tcHsTyVarName newSigTyVar m_kind) var_ns
+       ; let must_scope_tkvs = [ tkv | (tkv, False) <- tkvs_pairs ]
+       ; result <- tcExtendTyVarEnv must_scope_tkvs $
+                   thing_inside
+       ; return (map fst tkvs_pairs, result) }
+
+tcExplicitTKBndrs :: SkolemInfo
+                  -> [LHsTyVarBndr GhcRn]
+                  -> TcM a
+                  -> TcM ([TcTyVar], a)
 -- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
-tcExplicitTKBndrs orig_hs_tvs thing_inside
-  = tcExplicitTKBndrsX newSkolemTyVar orig_hs_tvs thing_inside
+tcExplicitTKBndrs = tcExplicitTKBndrsX newSkolemTyVar
+
+-- | This brings a bunch of tyvars into scope as SigTvs, where they can unify
+-- with other type *variables* only.
+tcExplicitTKBndrsSig :: SkolemInfo
+                     -> [LHsTyVarBndr GhcRn]
+                     -> TcM a
+                     -> TcM ([TcTyVar], a)
+tcExplicitTKBndrsSig = tcExplicitTKBndrsX newSigTyVar
 
 tcExplicitTKBndrsX :: (Name -> Kind -> TcM TyVar)
+                   -> SkolemInfo
                    -> [LHsTyVarBndr GhcRn]
-                   -> ([TyVar] -> TcM (a, TyVarSet))
-                        -- ^ Thing inside returns the set of variables bound
-                        -- in the scope. See Note [Scope-check inferred kinds]
-                   -> TcM (a, TyVarSet)  -- ^ returns augmented bound vars
+                   -> TcM a
+                   -> TcM ([TcTyVar], a)
 -- See also Note [Associated type tyvar names] in Class
-tcExplicitTKBndrsX new_tv orig_hs_tvs thing_inside
-  = go orig_hs_tvs $ \ tvs ->
-    do { (result, bound_tvs) <- thing_inside tvs
-
-         -- Issue an error if the ordering is bogus.
-         -- See Note [Bad telescopes] in TcValidity.
-       ; tvs <- checkZonkValidTelescope (interppSP orig_hs_tvs) tvs empty
-       ; checkValidInferredKinds tvs bound_tvs empty
+tcExplicitTKBndrsX new_tv skol_info hs_tvs thing_inside
+-- This function brings into scope a telescope of binders as written by
+-- the user. At first blush, it would then seem that we should bring
+-- them into scope one at a time, bumping the TcLevel each time.
+-- (Recall that we bump the level to prevent skolem escape from happening.)
+-- However, this leads to terrible error messages, because we end up
+-- failing to unify with some `k0`. Better would be to allow type inference
+-- to work, potentially creating a skolem-escape problem, and then to
+-- notice that the telescope is out of order. That's what we do here,
+-- following the logic of tcImplicitTKBndrsX.
+-- See also Note [Keeping scoped variables in order: Explicit]
+  = do { (inner_tclvl, wanted, (skol_tvs, result))
+           <- pushLevelAndCaptureConstraints $
+              bind_tvbs hs_tvs
+
+       ; emitTvImplication inner_tclvl skol_tvs (Just doc) wanted skol_info
 
        ; traceTc "tcExplicitTKBndrs" $
-           vcat [ text "Hs vars:" <+> ppr orig_hs_tvs
-                , text "tvs:" <+> sep (map pprTyVar tvs) ]
+           vcat [ text "Hs vars:" <+> ppr hs_tvs
+                , text "tvs:" <+> pprTyVars skol_tvs ]
 
-       ; return (result, bound_tvs `unionVarSet` mkVarSet tvs)
-       }
-  where
-    go []                   thing = thing []
-    go (L _ hs_tv : hs_tvs) thing = do { tv <- tc_hs_tv hs_tv
-                                       ; tcExtendTyVarEnv [tv] $
-                                         go hs_tvs $ \ tvs ->
-                                         thing (tv : tvs) }
+       ; return (skol_tvs, result) }
 
-    tc_hs_tv (UserTyVar (L _ name))
-      = do { kind <- newMetaKindVar
-           ; new_tv name kind }
-
-    tc_hs_tv  (KindedTyVar (L _ name) kind)
-      = do { kind <- tcLHsKindSig kind
-           ; new_tv name kind }
+  where
+    bind_tvbs [] = do { result <- thing_inside
+                      ; return ([], result) }
+    bind_tvbs (L _ tvb : tvbs)
+      = do { (tv, in_scope) <- tcHsTyVarBndr new_tv tvb
+           ; (if in_scope then id else tcExtendTyVarEnv [tv]) $
+           do { (tvs, result) <- bind_tvbs tvbs
+              ; return (tv : tvs, result) }}
+
+    doc = sep (map ppr hs_tvs)
+
+-- | Used during the "kind-checking" pass in TcTyClsDecls only.
+-- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
+kcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
+                  -> TcM a
+                  -> TcM a
+kcExplicitTKBndrs [] thing_inside = thing_inside
+kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
+  = do { (tv, _) <- tcHsTyVarBndr newSigTyVar hs_tv
+       ; tcExtendTyVarEnv [tv] $
+         kcExplicitTKBndrs hs_tvs thing_inside }
+
+-- | Build and emit an Implication appropriate for type-checking a type.
+-- This assumes all constraints will be equality constraints, and
+-- so does not create an EvBindsVar
+emitTvImplication :: TcLevel    -- of the constraints
+                   -> [TcTyVar]  -- skolems
+                   -> Maybe SDoc  -- user-written telescope, if present
+                   -> WantedConstraints
+                   -> SkolemInfo
+                   -> TcM ()
+emitTvImplication inner_tclvl skol_tvs m_telescope wanted skol_info
+  = do { tc_lcl_env <- getLclEnv
+       ; ev_binds   <- newNoTcEvBinds
+       ; let implic = newImplication { ic_tclvl  = inner_tclvl
+                                     , ic_skols  = skol_tvs
+                                     , ic_telescope = m_telescope
+                                     , ic_no_eqs = True
+                                     , ic_wanted = wanted
+                                     , ic_binds  = ev_binds
+                                     , ic_info   = skol_info
+                                     , ic_env    = tc_lcl_env }
+       ; emitImplication implic }
+
+tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
+              -> HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
+-- Return a TcTyVar, built using the provided function
+-- Typically the Kind inside the HsTyVarBndr will be a tyvar
+-- with a mutable kind in it.
+--
+-- These variables might be in scope already (with associated types, for example).
+-- This function then checks that the kind annotation (if any) matches the
+-- kind of the in-scope type variable.
+--
+-- Returned TcTyVar has the same name; no cloning
+--
+-- See also Note [Associated type tyvar names] in Class
+--
+-- Returns True iff the tyvar was already in scope
+tcHsTyVarBndr new_tv (UserTyVar (L _ tv_nm)) = tcHsTyVarName new_tv Nothing tv_nm
+tcHsTyVarBndr new_tv (KindedTyVar (L _ tv_nm) lhs_kind)
+  = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
+       ; tcHsTyVarName new_tv (Just kind) tv_nm }
 
 newWildTyVar :: Name -> TcM TcTyVar
 -- ^ New unification variable for a wildcard
@@ -1744,7 +1911,9 @@ newWildTyVar _name
        ; uniq <- newUnique
        ; details <- newMetaDetails TauTv
        ; let name = mkSysTvName uniq (fsLit "w")
-       ; return (mkTcTyVar name kind details) }
+             tyvar = (mkTcTyVar name kind details)
+       ; traceTc "newWildTyVar" (ppr tyvar)
+       ; return tyvar }
 
 -- | Produce a tyvar of the given name (with the kind provided, or
 -- otherwise a meta-var kind). If
@@ -1752,8 +1921,11 @@ newWildTyVar _name
 -- to make sure the known kind matches any kind provided. The
 -- second return value says whether the variable is in scope (True)
 -- or not (False). (Use this for associated types, for example.)
-tcHsTyVarName :: Maybe Kind -> Name -> TcM (TcTyVar, Bool)
-tcHsTyVarName m_kind name
+tcHsTyVarName :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
+              -> Maybe Kind  -- Just k <=> use k as the variable's kind
+                             -- Nothing <=> use a meta-tyvar
+              -> Name -> TcM (TcTyVar, Bool)
+tcHsTyVarName new_tv m_kind name
   = do { mb_tv <- tcLookupLcl_maybe name
        ; case mb_tv of
            Just (ATyVar _ tv)
@@ -1764,32 +1936,46 @@ tcHsTyVarName m_kind name
            _ -> do { kind <- case m_kind of
                                Just kind -> return kind
                                Nothing   -> newMetaKindVar
-                   ; tv <- newSkolemTyVar name kind
+                   ; tv <- new_tv name kind
                    ; return (tv, False) }}
 
--- makes a new skolem tv
-newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
-newSkolemTyVar name kind = do { lvl <- getTcLevel
-                              ; return (mk_skolem_tv lvl name kind) }
+--------------------------
+-- Bringing tyvars into scope
+--------------------------
 
-mk_skolem_tv :: TcLevel -> Name -> Kind -> TcTyVar
-mk_skolem_tv lvl n k = mkTcTyVar n k (SkolemTv lvl False)
+-- | Bring tyvars into scope, wrapping the thing_inside in an implication
+-- constraint. The implication constraint is necessary to provide SkolemInfo
+-- for the tyvars and to ensure that no unification variables made outside
+-- the scope of these tyvars (i.e. lower TcLevel) unify with the locally-scoped
+-- tyvars (i.e. higher TcLevel).
+--
+-- INVARIANT: The thing_inside must check only types, never terms.
+--
+-- Use this (not tcExtendTyVarEnv) wherever you expect a Λ or ∀ in Core.
+-- Use tcExtendTyVarEnv otherwise.
+scopeTyVars :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a
+scopeTyVars skol_info tvs = scopeTyVars2 skol_info [(tyVarName tv, tv) | tv <- tvs]
+
+-- | Like 'scopeTyVars', but allows you to specify different scoped names
+-- than the Names stored within the tyvars.
+scopeTyVars2 :: SkolemInfo -> [(Name, TcTyVar)] -> TcM a -> TcM a
+scopeTyVars2 skol_info prs thing_inside
+  = fmap snd $ -- discard the TcEvBinds, which will always be empty
+    checkConstraints skol_info (map snd prs) [{- no EvVars -}] $
+    tcExtendTyVarEnv2 prs $
+    thing_inside
 
 ------------------
-kindGeneralizeType :: Type -> TcM Type
--- Result is zonked
-kindGeneralizeType ty
-  = do { kvs <- kindGeneralize ty
-       ; ty <- zonkSigType (mkInvForAllTys kvs ty)
-       ; return ty  }
-
 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 must be zonked.
+-- NB: You must call solveEqualities or solveLocalEqualities before
+-- kind generalization
 kindGeneralize kind_or_type
-  = do { kvs <- zonkTcTypeAndFV kind_or_type
-       ; let dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet }
+  = do { let kvs = tyCoVarsOfTypeDSet kind_or_type
+             dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet }
        ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
        ; quantifyTyVars gbl_tvs dvs }
 
@@ -1931,6 +2117,7 @@ kcLookupTcTyCon nm
 -- Never emits constraints, though the thing_inside might.
 kcTyClTyVars :: Name -> TcM a -> TcM a
 kcTyClTyVars tycon_name thing_inside
+  -- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
   = do { tycon <- kcLookupTcTyCon tycon_name
        ; tcExtendTyVarEnv2 (tcTyConScopedTyVars tycon) $ thing_inside }
 
@@ -1957,20 +2144,20 @@ tcTyClTyVars tycon_name thing_inside
 
        -- Do checks on scoped tyvars
        -- See Note [Free-floating kind vars]
-       ; let scoped_prs = tcTyConScopedTyVars tycon
+       ; let flav = tyConFlavour tycon
+             scoped_prs = tcTyConScopedTyVars tycon
              scoped_tvs = map snd scoped_prs
              still_sig_tvs = filter isSigTyVar scoped_tvs
 
        ; mapM_ report_sig_tv_err (findDupSigTvs scoped_prs)
 
-       ; checkNoErrs $ reportFloatingKvs tycon_name (tyConFlavour tycon)
+       ; checkNoErrs $ reportFloatingKvs tycon_name flav
                                          scoped_tvs still_sig_tvs
 
        ; let res_kind   = tyConResKind tycon
              binders    = correct_binders (tyConBinders tycon) res_kind
        ; traceTc "tcTyClTyVars" (ppr tycon_name <+> ppr binders)
-
-       ; tcExtendTyVarEnv2 scoped_prs $
+       ; scopeTyVars2 (TyConSkol flav tycon_name) scoped_prs $
          thing_inside binders res_kind }
   where
     report_sig_tv_err (n1, n2)
@@ -2122,61 +2309,70 @@ tcHsPartialSigType
   :: UserTypeCtxt
   -> LHsSigWcType GhcRn       -- The type signature
   -> TcM ( [(Name, TcTyVar)]  -- Wildcards
-         , Maybe TcTyVar      -- Extra-constraints wildcard
-         , [TcTyVar]          -- Implicitly and explicitly bound type variables
+         , Maybe TcType       -- Extra-constraints wildcard
+         , [Name]             -- Original tyvar names, in correspondence with ...
+         , [TcTyVar]          -- ... Implicitly and explicitly bound type variables
          , TcThetaType        -- Theta part
          , TcType )           -- Tau part
+-- See Note [Recipe for checking a signature]
 tcHsPartialSigType ctxt sig_ty
   | HsWC { hswc_wcs  = sig_wcs,         hswc_body = ib_ty } <- sig_ty
   , HsIB { hsib_vars = implicit_hs_tvs, hsib_body = hs_ty } <- ib_ty
   , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
   = addSigCtxt ctxt hs_ty $
-    do { (implicit_tvs, (wcs, wcx, explicit_tvs, theta, tau))
-            <- tcWildCardBindersX newWildTyVar sig_wcs        $ \ wcs ->
-               tcImplicitTKBndrsX new_implicit_tv implicit_hs_tvs $
-               tcExplicitTKBndrs explicit_hs_tvs $ \ explicit_tvs ->
-             do {   -- Instantiate the type-class context; but if there
-                    -- is an extra-constraints wildcard, just discard it here
+    do { (implicit_tvs, (explicit_tvs, (wcs, wcx, theta, tau)))
+            <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ wcs ->
+               tcImplicitTKBndrsSig skol_info implicit_hs_tvs      $
+               tcExplicitTKBndrs    skol_info explicit_hs_tvs      $
+               do {   -- Instantiate the type-class context; but if there
+                      -- is an extra-constraints wildcard, just discard it here
                     (theta, wcx) <- tcPartialContext hs_ctxt
 
                   ; tau <- tcHsOpenType hs_tau
 
-                  ; let bound_tvs = unionVarSets [ allBoundVariables tau
-                                                 , mkVarSet explicit_tvs
-                                                 , mkVarSet (map snd wcs) ]
-
-                  ; return ( (wcs, wcx, explicit_tvs, theta, tau)
-                           , bound_tvs) }
-
-        -- Spit out the wildcards (including the extra-constraints one)
-        -- as "hole" constraints, so that they'll be reported if necessary
-        -- See Note [Extra-constraint holes in partial type signatures]
-        ; emitWildCardHoleConstraints wcs
-
-        ; explicit_tvs <- mapM zonkTyCoVarKind explicit_tvs
-        ; let all_tvs = implicit_tvs ++ explicit_tvs
-                        -- The implicit_tvs already have zonked kinds
-
-        ; theta   <- mapM zonkTcType theta
-        ; tau     <- zonkTcType tau
-
-        ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
-
-        ; traceTc "tcHsPartialSigType" (ppr all_tvs)
-        ; return (wcs, wcx, all_tvs, theta, tau) }
+                  ; return (wcs, wcx, theta, tau) }
+
+         -- We must return these separately, because all the zonking below
+         -- might change the name of a SigTv. This, in turn, causes trouble
+         -- in partial type signatures that bind scoped type variables, as
+         -- we bring the wrong name into scope in the function body.
+         -- Test case: partial-sigs/should_compile/LocalDefinitionBug
+       ; let tv_names = map tyVarName (implicit_tvs ++ explicit_tvs)
+
+       -- Spit out the wildcards (including the extra-constraints one)
+       -- as "hole" constraints, so that they'll be reported if necessary
+       -- See Note [Extra-constraint holes in partial type signatures]
+       ; emitWildCardHoleConstraints wcs
+
+         -- The SigTvs created above will sometimes have too high a TcLevel
+         -- (note that they are generated *after* bumping the level in
+         -- the tc{Im,Ex}plicitTKBndrsSig functions. Bumping the level
+         -- is still important here, because the kinds of these variables
+         -- do indeed need to have the higher level, so they can unify
+         -- with other local type variables. But, now that we've type-checked
+         -- everything (and solved equalities in the tcImplicit call)
+         -- we need to promote the SigTvs so we don't violate the TcLevel
+         -- invariant
+       ; all_tvs <- mapM zonkPromoteTyCoVarBndr (implicit_tvs ++ explicit_tvs)
+            -- zonkPromoteTyCoVarBndr deals well with SigTvs
+
+       ; theta   <- mapM zonkPromoteType theta
+       ; tau     <- zonkPromoteType tau
+
+       ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
+
+       ; traceTc "tcHsPartialSigType" (ppr all_tvs)
+       ; return (wcs, wcx, tv_names, all_tvs, theta, tau) }
   where
-    new_implicit_tv name
-      = do { kind <- newMetaKindVar
-           ; tv <- newSkolemTyVar name kind
-           ; return (tv, False) }
+    skol_info   = SigTypeSkol ctxt
 
-tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcTyVar)
+tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
 tcPartialContext hs_theta
   | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
   , L _ (HsWildCardTy wc) <- ignoreParens hs_ctxt_last
-  = do { wc_tv <- tcWildCardOcc wc constraintKind
+  = do { wc_tv_ty <- tcWildCardOcc wc constraintKind
        ; theta <- mapM tcLHsPredType hs_theta1
-       ; return (theta, Just wc_tv) }
+       ; return (theta, Just wc_tv_ty) }
   | otherwise
   = do { theta <- mapM tcLHsPredType hs_theta
        ; return (theta, Nothing) }
@@ -2239,31 +2435,33 @@ tcHsPatSigType :: UserTypeCtxt
 -- (b) RULE forall bndrs  e.g. forall (x::Int). f x = x
 --
 -- This may emit constraints
-
+-- See Note [Recipe for checking a signature]
 tcHsPatSigType ctxt sig_ty
   | HsWC { hswc_wcs = sig_wcs,   hswc_body = ib_ty } <- sig_ty
   , HsIB { hsib_vars = sig_vars, hsib_body = hs_ty } <- ib_ty
   = addSigCtxt ctxt hs_ty $
-    do { (implicit_tvs, (wcs, sig_ty))
-            <- tcWildCardBindersX newWildTyVar    sig_wcs  $ \ wcs ->
-               tcImplicitTKBndrsX new_implicit_tv sig_vars $
+    do { sig_tkvs <- mapM new_implicit_tv sig_vars
+       ; (wcs, sig_ty)
+            <- tcWildCardBindersX newWildTyVar    Nothing sig_wcs  $ \ wcs ->
+               tcExtendTyVarEnv sig_tkvs                           $
                do { sig_ty <- tcHsOpenType hs_ty
-                  ; return ((wcs, sig_ty), allBoundVariables sig_ty) }
+                  ; return (wcs, sig_ty) }
 
         ; emitWildCardHoleConstraints wcs
 
-        ; sig_ty <- zonkTcType sig_ty
+          -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
+          -- contains a forall). Promote these.
+        ; sig_ty <- zonkPromoteType sig_ty
         ; checkValidType ctxt sig_ty
 
-        ; tv_pairs <- mapM mk_tv_pair implicit_tvs
+        ; tv_pairs <- mapM mk_tv_pair sig_tkvs
 
         ; traceTc "tcHsPatSigType" (ppr sig_vars)
         ; return (wcs, tv_pairs, sig_ty) }
   where
     new_implicit_tv name = do { kind <- newMetaKindVar
-                              ; tv <- new_tv name kind
-                              ; return (tv, False) }
-       -- "False" means that these tyvars aren't yet in scope
+                              ; new_tv name kind }
+
     new_tv = case ctxt of
                RuleSigCtxt {} -> newSkolemTyVar
                _              -> newSigTyVar
@@ -2418,6 +2616,89 @@ unifyKinds rn_tys act_kinds
 {-
 ************************************************************************
 *                                                                      *
+    Promotion
+*                                                                      *
+************************************************************************
+-}
+
+-- | Whenever a type is about to be added to the environment, it's necessary
+-- to make sure that any free meta-tyvars in the type are promoted to the
+-- current TcLevel. (They might be at a higher level due to the level-bumping
+-- in tcExplicitTKBndrs, for example.) This function both zonks *and*
+-- promotes.
+zonkPromoteType :: TcType -> TcM TcType
+zonkPromoteType = mapType zonkPromoteMapper ()
+
+-- cf. TcMType.zonkTcTypeMapper
+zonkPromoteMapper :: TyCoMapper () TcM
+zonkPromoteMapper = TyCoMapper { tcm_smart    = True
+                               , tcm_tyvar    = const zonkPromoteTcTyVar
+                               , tcm_covar    = const covar
+                               , tcm_hole     = const hole
+                               , tcm_tybinder = const tybinder }
+  where
+    covar cv
+      = mkCoVarCo <$> zonkPromoteTyCoVarKind cv
+
+    hole :: CoercionHole -> TcM Coercion
+    hole h
+      = do { contents <- unpackCoercionHole_maybe h
+           ; case contents of
+               Just co -> do { co <- zonkPromoteCoercion co
+                             ; checkCoercionHole cv co }
+               Nothing -> do { cv' <- zonkPromoteTyCoVarKind cv
+                             ; return $ mkHoleCo (setCoHoleCoVar h cv') } }
+      where
+        cv = coHoleCoVar h
+
+    tybinder :: TyVar -> ArgFlag -> TcM ((), TyVar)
+    tybinder tv _flag = ((), ) <$> zonkPromoteTyCoVarKind tv
+
+zonkPromoteTcTyVar :: TyCoVar -> TcM TcType
+zonkPromoteTcTyVar tv
+  | isMetaTyVar tv
+  = do { let ref = metaTyVarRef tv
+       ; contents <- readTcRef ref
+       ; case contents of
+           Flexi -> do { promoted <- promoteTyVar tv
+                       ; if promoted
+                         then zonkPromoteTcTyVar tv   -- read it again
+                         else mkTyVarTy <$> zonkPromoteTyCoVarKind tv }
+           Indirect ty -> zonkPromoteType ty }
+
+  | isTcTyVar tv && isSkolemTyVar tv  -- NB: isSkolemTyVar says "True" to pure TyVars
+  = do { tc_lvl <- getTcLevel
+       ; mkTyVarTy <$> zonkPromoteTyCoVarKind (promoteSkolem tc_lvl tv) }
+
+  | otherwise
+  = mkTyVarTy <$> zonkPromoteTyCoVarKind tv
+
+zonkPromoteTyCoVarKind :: TyCoVar -> TcM TyCoVar
+zonkPromoteTyCoVarKind = updateTyVarKindM zonkPromoteType
+
+zonkPromoteTyCoVarBndr :: TyCoVar -> TcM TyCoVar
+zonkPromoteTyCoVarBndr tv
+  | isSigTyVar tv
+  = tcGetTyVar "zonkPromoteTyCoVarBndr SigTv" <$> zonkPromoteTcTyVar tv
+
+  | isTcTyVar tv && isSkolemTyVar tv
+  = do { tc_lvl <- getTcLevel
+       ; zonkPromoteTyCoVarKind (promoteSkolem tc_lvl tv) }
+
+  | otherwise
+  = zonkPromoteTyCoVarKind tv
+
+zonkPromoteCoercion :: Coercion -> TcM Coercion
+zonkPromoteCoercion = mapCoercion zonkPromoteMapper ()
+
+zonkPromoteTypeInKnot :: TcType -> TcM TcType
+zonkPromoteTypeInKnot = mapType (zonkPromoteMapper { tcm_smart = False }) ()
+  -- NB: Just changing smart to False will still use the smart zonker (not suitable
+  -- for in-the-knot) for kinds. But that's OK, because kinds aren't knot-tied.
+
+{-
+************************************************************************
+*                                                                      *
         Sort checking kinds
 *                                                                      *
 ************************************************************************
@@ -2426,10 +2707,12 @@ tcLHsKindSig converts a user-written kind to an internal, sort-checked kind.
 It does sort checking and desugaring at the same time, in one single pass.
 -}
 
-tcLHsKindSig :: LHsKind GhcRn -> TcM Kind
-tcLHsKindSig hs_kind
-  = do { kind <- tc_lhs_kind kindLevelMode hs_kind
-       ; zonkTcType kind }
+tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
+tcLHsKindSig ctxt hs_kind
+-- See  Note [Recipe for checking a signature] in TcHsType
+  = do { kind <- solveLocalEqualities $
+                 tc_lhs_kind kindLevelMode hs_kind
+       ; kind <- zonkPromoteType kind
          -- This zonk is very important in the case of higher rank kinds
          -- E.g. Trac #13879    f :: forall (p :: forall z (y::z). <blah>).
          --                          <more blah>
@@ -2437,6 +2720,9 @@ tcLHsKindSig hs_kind
          --      it's crucial that the kind we instantiate is fully zonked,
          --      else we may fail to substitute properly
 
+       ; checkValidType ctxt kind
+       ; return kind }
+
 tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind
 tc_lhs_kind mode k
   = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $
index 7e44c4a..e5043ea 100644 (file)
@@ -479,9 +479,9 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
 
         -- Next, process any associated types.
         ; traceTc "tcLocalInstDecl" (ppr poly_ty)
-        ; tyfam_insts0  <- tcExtendTyVarEnv tyvars $
+        ; tyfam_insts0  <- scopeTyVars InstSkol tyvars $
                            mapAndRecoverM (tcTyFamInstDecl mb_info) ats
-        ; datafam_stuff <- tcExtendTyVarEnv tyvars $
+        ; datafam_stuff <- scopeTyVars InstSkol tyvars $
                            mapAndRecoverM (tcDataFamInstDecl mb_info) adts
         ; let (datafam_insts, m_deriv_infos) = unzip datafam_stuff
               deriv_infos                    = catMaybes m_deriv_infos
@@ -1282,6 +1282,8 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                                 , ib_pragmas    = sigs
                                 , ib_extensions = exts
                                 , ib_derived    = is_derived })
+      -- tcExtendTyVarEnv (not scopeTyVars) is OK because the TcLevel is pushed
+      -- in checkInstConstraints
   = tcExtendTyVarEnv2 (lexical_tvs `zip` tyvars) $
        -- The lexical_tvs scope over the 'where' part
     do { traceTc "tcInstMeth" (ppr sigs $$ ppr binds)
index c724333..377b2d6 100644 (file)
@@ -393,9 +393,11 @@ runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
 runSolverPipeline pipeline workItem
   = do { wl <- getWorkList
        ; inerts <- getTcSInerts
+       ; tclevel <- getTcLevel
        ; traceTcS "----------------------------- " empty
        ; traceTcS "Start solver pipeline {" $
-                  vcat [ text "work item =" <+> ppr workItem
+                  vcat [ text "tclevel =" <+> ppr tclevel
+                       , text "work item =" <+> ppr workItem
                        , text "inerts =" <+> ppr inerts
                        , text "rest of worklist =" <+> ppr wl ]
 
@@ -673,6 +675,18 @@ that this chain of events won't happen, but that's very fragile.)
                    interactIrred
 *                                                                               *
 *********************************************************************************
+
+Note [Multiple matching irreds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+You might think that it's impossible to have multiple irreds all match the
+work item; after all, interactIrred looks for matches and solves one from the
+other. However, note that interacting insoluble, non-droppable irreds does not
+do this matching. We thus might end up with several insoluble, non-droppable,
+matching irreds in the inert set. When another irred comes along that we have
+not yet labeled insoluble, we can find multiple matches. These multiple matches
+cause no harm, but it would be wrong to ASSERT that they aren't there (as we
+once had done). This problem can be tickled by typecheck/should_compile/holes.
+
 -}
 
 -- Two pieces of irreducible evidence: if their types are *exactly identical*
@@ -690,10 +704,10 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
   = continueWith workItem
 
   | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
-  , ((ct_i, swap) : rest) <- bagToList matching_irreds
+  , ((ct_i, swap) : _rest) <- bagToList matching_irreds
+        -- See Note [Multiple matching irreds]
   , let ev_i = ctEvidence ct_i
-  = ASSERT( null rest )
-    do { what_next <- solveOneFromTheOther ev_i ev_w
+  = do { what_next <- solveOneFromTheOther ev_i ev_w
        ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i)
        ; case what_next of
             KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
index 8f74f55..b1bc1d0 100644 (file)
@@ -45,7 +45,7 @@ module TcMType (
   newEvVar, newEvVars, newDict,
   newWanted, newWanteds, cloneWanted, cloneWC,
   emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
-  newTcEvBinds, addTcEvBind,
+  newTcEvBinds, newNoTcEvBinds, addTcEvBind,
 
   newCoercionHole, fillCoercionHole, isFilledCoercionHole,
   unpackCoercionHole, unpackCoercionHole_maybe,
@@ -55,13 +55,13 @@ module TcMType (
   -- Instantiation
   newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
   newMetaSigTyVars, newMetaSigTyVarX,
-  newSigTyVar, newWildCardX,
+  newSigTyVar, newSkolemTyVar, newWildCardX,
   tcInstType,
   tcInstSkolTyVars,tcInstSkolTyVarsX,
   tcInstSuperSkolTyVarsX,
   tcSkolDFunType, tcSuperSkolTyVars,
 
-  instSkolTyCoVars, freshenTyVarBndrs, freshenCoVarBndrsX,
+  instSkolTyCoVarsX, freshenTyVarBndrs, freshenCoVarBndrsX,
 
   --------------------------------
   -- Zonking and tidying
@@ -78,6 +78,7 @@ module TcMType (
   zonkTcTyCoVarBndr, zonkTcTyVarBinder,
   zonkTcType, zonkTcTypes, zonkCo,
   zonkTyCoVarKind, zonkTcTypeMapper,
+  zonkTcTypeInKnot,
 
   zonkEvVar, zonkWC, zonkSimples,
   zonkId, zonkCoVar,
@@ -147,6 +148,7 @@ newMetaKindVar :: TcM TcKind
 newMetaKindVar = do { uniq <- newUnique
                     ; details <- newMetaDetails TauTv
                     ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
+                    ; traceTc "newMetaKindVar" (ppr kv)
                     ; return (mkTyVarTy kv) }
 
 newMetaKindVars :: Int -> TcM [TcKind]
@@ -607,7 +609,14 @@ instead of the buggous
 newSigTyVar :: Name -> Kind -> TcM TcTyVar
 newSigTyVar name kind
   = do { details <- newMetaDetails SigTv
-       ; return (mkTcTyVar name kind details) }
+       ; let tyvar = mkTcTyVar name kind details
+       ; traceTc "newSigTyVar" (ppr tyvar)
+       ; return tyvar }
+
+-- makes a new skolem tv
+newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
+newSkolemTyVar name kind = do { lvl <- getTcLevel
+                              ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
 
 newFmvTyVar :: TcType -> TcM TcTyVar
 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
@@ -638,7 +647,9 @@ cloneMetaTyVar tv
               details' = case tcTyVarDetails tv of
                            details@(MetaTv {}) -> details { mtv_ref = ref }
                            _ -> pprPanic "cloneMetaTyVar" (ppr tv)
-        ; return (mkTcTyVar name' (tyVarKind tv) details') }
+              tyvar = mkTcTyVar name' (tyVarKind tv) details'
+        ; traceTc "cloneMetaTyVar" (ppr tyvar)
+        ; return tyvar }
 
 -- Works for both type and kind variables
 readMetaTyVar :: TyVar -> TcM MetaDetails
@@ -700,9 +711,7 @@ writeMetaTyVarRef tyvar ref ty
        ; zonked_ty      <- zonkTcType ty
        ; let zonked_ty_kind = typeKind zonked_ty  -- need to zonk even before typeKind;
                                                   -- otherwise, we can panic in piResultTy
-             kind_check_ok = isPredTy tv_kind  -- Don't check kinds for updates
-                                               -- to coercion variables. TODO (RAE): Why not?
-                          || isConstraintKind zonked_tv_kind
+             kind_check_ok = isConstraintKind zonked_tv_kind
                           || tcEqKind zonked_ty_kind zonked_tv_kind
              -- Hack alert! isConstraintKind: see TcHsType
              -- Note [Extra-constraint holes in partial type signatures]
@@ -802,7 +811,9 @@ newAnonMetaTyVar meta_info kind
                         FlatSkolTv  -> fsLit "fsk"
                         SigTv       -> fsLit "a"
         ; details <- newMetaDetails meta_info
-        ; return (mkTcTyVar name kind details) }
+        ; let tyvar = mkTcTyVar name kind details
+        ; traceTc "newAnonMetaTyVar" (ppr tyvar)
+        ; return tyvar }
 
 cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
 -- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
@@ -811,7 +822,9 @@ cloneAnonMetaTyVar info tv kind
         ; details <- newMetaDetails info
         ; let name = mkSystemName uniq (getOccName tv)
                        -- See Note [Name of an instantiated type variable]
-        ; return (mkTcTyVar name kind details) }
+              tyvar = mkTcTyVar name kind details
+        ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
+        ; return tyvar }
 
 {- Note [Name of an instantiated type variable]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -922,7 +935,7 @@ also free in the type.  Eg
      Typeable k (a::k)
 has free vars {k,a}.  But the type (see Trac #7916)
     (f::k->*) (a::k)
-has free vars {f,a}, but we must add 'k' as well! Hence step (3).
+has free vars {f,a}, but we must add 'k' as well! Hence step (2).
 
 * This function distinguishes between dependent and non-dependent
   variables only to keep correct defaulting behavior with -XNoPolyKinds.
@@ -1007,6 +1020,10 @@ quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
     --    * Kind variables, with -XNoPolyKinds: don't quantify over these
     --    * RuntimeRep variables: we never quantify over these
     zonk_quant default_kind tkv
+      | not (isTyVar tkv)
+      = return Nothing   -- this can happen for a covar that's associated with
+                         -- a coercion hole. Test case: typecheck/should_compile/T2494
+
       | not (isTcTyVar tkv)
       = return (Just tkv)  -- For associated types, we have the class variables
                            -- in scope, and they are TyVars not TcTyVars
@@ -1526,11 +1543,17 @@ zonkCo :: Coercion -> TcM Coercion
 zonkCo = mapCoercion zonkTcTypeMapper ()
 
 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
--- A tyvar binder is never a unification variable (MetaTv),
--- rather it is always a skolems.  BUT it may have a kind
+-- A tyvar binder is never a unification variable (TauTv),
+-- rather it is always a skolem. It *might* be a SigTv.
+-- (Because non-CUSK type declarations use SigTvs.)
+-- Regardless, it may have a kind
 -- that has not yet been zonked, and may include kind
 -- unification variables.
 zonkTcTyCoVarBndr tyvar
+  | isSigTyVar tyvar
+  = tcGetTyVar "zonkTcTyCoVarBndr SigTv" <$> zonkTcTyVar tyvar
+
+  | otherwise
     -- can't use isCoVar, because it looks at a TyCon. Argh.
   = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTyVar tyvar )
     updateTyVarKindM zonkTcType tyvar
@@ -1724,8 +1747,8 @@ formatLevPolyErr :: Type  -- levity-polymorphic type
                  -> SDoc
 formatLevPolyErr ty
   = hang (text "A levity-polymorphic type is not allowed here:")
-       2 (vcat [ text "Type:" <+> ppr tidy_ty
-               , text "Kind:" <+> ppr tidy_ki ])
+       2 (vcat [ text "Type:" <+> pprWithTYPE tidy_ty
+               , text "Kind:" <+> pprWithTYPE tidy_ki ])
   where
     (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
     tidy_ki             = tidyType tidy_env (typeKind ty)
index c5e367e..e768fec 100644 (file)
@@ -408,6 +408,10 @@ tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside
 tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside
   = do  { (inner_ty, tv_binds, wcs, wrap) <- tcPatSig (inPatBind penv)
                                                             sig_ty pat_ty
+                -- Using tcExtendTyVarEnv2 is appropriate here (not scopeTyVars2)
+                -- because we're not really bringing fresh tyvars into scope.
+                -- We're *naming* existing tyvars. Note that it is OK for a tyvar
+                -- from an outer scope to mention one of these tyvars in its kind.
         ; (pat', res) <- tcExtendTyVarEnv2 wcs      $
                          tcExtendTyVarEnv2 tv_binds $
                          tc_lpat pat (mkCheckExpType inner_ty) penv thing_inside
index 9c8880e..ee4a05e 100644 (file)
@@ -263,7 +263,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
             2 (text "mentions existential type variable" <> plural bad_tvs
                <+> pprQuotedList bad_tvs)
 
-         -- See Note [The pattern-synonym signature splitting rule]
+         -- See Note [The pattern-synonym signature splitting rule] in TcSigs
        ; let univ_fvs = closeOverKinds $
                         (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` explicit_univ_tvs)
              (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . binderVar) implicit_tvs
index aa3ce2e..eebac1e 100644 (file)
@@ -2299,10 +2299,11 @@ tcRnType hsc_env normalise rdr_type
         -- First bring into scope any wildcards
        ; traceTc "tcRnType" (vcat [ppr wcs, ppr rn_type])
        ; (ty, kind) <- solveEqualities $
-                       tcWildCardBinders wcs  $ \ _ ->
+                       tcWildCardBinders (SigTypeSkol GhciCtxt) wcs $ \ _ ->
                        tcLHsTypeUnsaturated rn_type
 
        -- Do kind generalisation; see Note [Kind-generalise in tcRnType]
+       ; kind <- zonkTcType kind
        ; kvs <- kindGeneralize kind
        ; ty  <- zonkTcTypeToType emptyZonkEnv ty
 
index 20185ae..e93a2a5 100644 (file)
@@ -88,7 +88,7 @@ module TcRnMonad(
   mkErrInfo,
 
   -- * Type constraints
-  newTcEvBinds,
+  newTcEvBinds, newNoTcEvBinds,
   addTcEvBind,
   getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
   chooseUniqueOccTc,
@@ -97,7 +97,7 @@ module TcRnMonad(
   emitImplication, emitImplications, emitInsoluble,
   discardConstraints, captureConstraints, tryCaptureConstraints,
   pushLevelAndCaptureConstraints,
-  pushTcLevelM_, pushTcLevelM,
+  pushTcLevelM_, pushTcLevelM, pushTcLevelsM,
   getTcLevel, setTcLevel, isTouchableTcM,
   getLclTypeEnv, setLclTypeEnv,
   traceTcConstraints, emitWildCardHoleConstraints,
@@ -1370,17 +1370,35 @@ newTcEvBinds = do { binds_ref <- newTcRef emptyEvBindMap
                                        , ebv_tcvs = tcvs_ref
                                        , ebv_uniq = uniq }) }
 
+-- | Creates an EvBindsVar incapable of holding any bindings. It still
+-- tracks covar usages (see comments on ebv_tcvs in TcEvidence), thus
+-- must be made monadically
+newNoTcEvBinds :: TcM EvBindsVar
+newNoTcEvBinds
+  = do { tcvs_ref  <- newTcRef emptyVarSet
+       ; uniq <- newUnique
+       ; traceTc "newNoTcEvBinds" (text "unique =" <+> ppr uniq)
+       ; return (NoEvBindsVar { ebv_tcvs = tcvs_ref
+                              , ebv_uniq = uniq }) }
+
 getTcEvTyCoVars :: EvBindsVar -> TcM TyCoVarSet
-getTcEvTyCoVars (EvBindsVar { ebv_tcvs = ev_ref })
-  = readTcRef ev_ref
+getTcEvTyCoVars ev_binds_var
+  = readTcRef (ebv_tcvs ev_binds_var)
 
 getTcEvBindsMap :: EvBindsVar -> TcM EvBindMap
 getTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref })
   = readTcRef ev_ref
+getTcEvBindsMap (NoEvBindsVar {})
+  = return emptyEvBindMap
 
 setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcM ()
 setTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref }) binds
   = writeTcRef ev_ref binds
+setTcEvBindsMap v@(NoEvBindsVar {}) ev_binds
+  | isEmptyEvBindMap ev_binds
+  = return ()
+  | otherwise
+  = pprPanic "setTcEvBindsMap" (ppr v $$ ppr ev_binds)
 
 addTcEvBind :: EvBindsVar -> EvBind -> TcM ()
 -- Add a binding to the TcEvBinds by side effect
@@ -1389,6 +1407,8 @@ addTcEvBind (EvBindsVar { ebv_binds = ev_ref, ebv_uniq = u }) ev_bind
                                  ppr ev_bind
        ; bnds <- readTcRef ev_ref
        ; writeTcRef ev_ref (extendEvBinds bnds ev_bind) }
+addTcEvBind (NoEvBindsVar { ebv_uniq = u }) ev_bind
+  = pprPanic "addTcEvBind NoEvBindsVar" (ppr ev_bind $$ ppr u)
 
 chooseUniqueOccTc :: (OccSet -> OccName) -> TcM OccName
 chooseUniqueOccTc fn =
@@ -1485,6 +1505,7 @@ captureConstraints thing_inside
            Left _    -> do { emitConstraints lie; failM }
            Right res -> return (res, lie) }
 
+-- | The name says it all. The returned TcLevel is the *inner* TcLevel.
 pushLevelAndCaptureConstraints :: TcM a -> TcM (TcLevel, WantedConstraints, a)
 pushLevelAndCaptureConstraints thing_inside
   = do { env <- getLclEnv
@@ -1505,6 +1526,15 @@ pushTcLevelM thing_inside
                           thing_inside
        ; return (res, tclvl') }
 
+-- Returns pushed TcLevel
+pushTcLevelsM :: Int -> TcM a -> TcM (a, TcLevel)
+pushTcLevelsM num_levels thing_inside
+  = do { env <- getLclEnv
+       ; let tclvl' = nTimes num_levels pushTcLevel (tcl_tclvl env)
+       ; res <- setLclEnv (env { tcl_tclvl = tclvl' }) $
+                thing_inside
+       ; return (res, tclvl') }
+
 getTcLevel :: TcM TcLevel
 getTcLevel = do { env <- getLclEnv
                 ; return (tcl_tclvl env) }
index f66077d..f0439a6 100644 (file)
@@ -151,7 +151,7 @@ import HscTypes
 import TcEvidence
 import Type
 import Class    ( Class )
-import TyCon    ( TyCon, tyConKind )
+import TyCon    ( TyCon, TyConFlavour, tyConKind )
 import TyCoRep  ( CoercionHole(..), coHoleCoVar )
 import Coercion ( Coercion, mkHoleCo )
 import ConLike  ( ConLike(..) )
@@ -1516,8 +1516,11 @@ data TcIdSigInst
                -- wildcards scope over the binding, and hence their
                -- Names may appear in type signatures in the binding
 
-         , sig_inst_wcx   :: Maybe TcTyVar
+         , sig_inst_wcx   :: Maybe TcType
                -- Extra-constraints wildcard to fill in, if any
+               -- If this exists, it is surely of the form (meta_tv |> co)
+               -- (where the co might be reflexive). This is filled in
+               -- only from the return value of TcHsType.tcWildCardOcc
          }
 
 {- Note [sig_inst_tau may be polymorphic]
@@ -1554,7 +1557,7 @@ data TcPatSynInfo
         patsig_name           :: Name,
         patsig_implicit_bndrs :: [TyVarBinder], -- Implicitly-bound kind vars (Inferred) and
                                                 -- implicitly-bound type vars (Specified)
-          -- See Note [The pattern-synonym signature splitting rule] in TcPatSyn
+          -- See Note [The pattern-synonym signature splitting rule] in TcSigs
         patsig_univ_bndrs     :: [TyVar],       -- Bound by explicit user forall
         patsig_req            :: TcThetaType,
         patsig_ex_bndrs       :: [TyVar],       -- Bound by explicit user forall
@@ -2329,8 +2332,9 @@ isSolvedStatus (IC_Solved {}) = True
 isSolvedStatus _              = False
 
 isInsolubleStatus :: ImplicStatus -> Bool
-isInsolubleStatus IC_Insoluble = True
-isInsolubleStatus _            = False
+isInsolubleStatus IC_Insoluble    = True
+isInsolubleStatus IC_BadTelescope = True
+isInsolubleStatus _               = False
 
 insolubleImplic :: Implication -> Bool
 insolubleImplic ic = isInsolubleStatus (ic_status ic)
@@ -2432,6 +2436,11 @@ data Implication
       ic_skols :: [TcTyVar],     -- Introduced skolems
       ic_info  :: SkolemInfo,    -- See Note [Skolems in an implication]
                                  -- See Note [Shadowing in a constraint]
+      ic_telescope :: Maybe SDoc,  -- User-written telescope, if there is one
+                                   -- The list of skolems is order-checked
+                                   -- if and only if this is a Just.
+                                   -- See Note [Keeping scoped variables in order: Explicit]
+                                   -- in TcHsType
 
       ic_given  :: [EvVar],      -- Given evidence variables
                                  --   (order does not matter)
@@ -2472,6 +2481,7 @@ newImplication
 
              -- The rest have sensible default values
            , ic_skols      = []
+           , ic_telescope  = Nothing
            , ic_given      = []
            , ic_wanted     = emptyWC
            , ic_no_eqs     = False
@@ -2486,6 +2496,9 @@ data ImplicStatus
 
   | IC_Insoluble  -- At least one insoluble constraint in the tree
 
+  | IC_BadTelescope  -- solved, but the skolems in the telescope are out of
+                     -- dependency order
+
   | IC_Unsolved   -- Neither of the above; might go either way
 
 instance Outputable Implication where
@@ -2507,8 +2520,9 @@ instance Outputable Implication where
                , pprSkolInfo info ] <+> rbrace)
 
 instance Outputable ImplicStatus where
-  ppr IC_Insoluble   = text "Insoluble"
-  ppr IC_Unsolved    = text "Unsolved"
+  ppr IC_Insoluble    = text "Insoluble"
+  ppr IC_BadTelescope = text "Bad telescope"
+  ppr IC_Unsolved     = text "Unsolved"
   ppr (IC_Solved { ics_dead = dead })
     = text "Solved" <+> (braces (text "Dead givens =" <+> ppr dead))
 
@@ -3154,7 +3168,11 @@ data SkolemInfo
        [(Name,TcTyVar)]    -- Maps the original name of the skolemised tyvar
                            -- to its instantiated version
 
-  | ClsSkol Class       -- Bound at a class decl
+  | SigTypeSkol UserTypeCtxt
+                 -- like SigSkol, but when we're kind-checking the *type*
+                 -- hence, we have less info
+
+  | ForAllSkol SDoc     -- Bound by a user-written "forall".
 
   | DerivSkol Type      -- Bound by a 'deriving' clause;
                         -- the type is the instance we are trying to derive
@@ -3166,7 +3184,6 @@ data SkolemInfo
                         --    then TypeSize = sizeTypes [ty1, .., tyn]
                         -- See Note [Solving superclass constraints] in TcInstDcls
 
-  | DataSkol            -- Bound at a data type declaration
   | FamInstSkol         -- Bound at a family instance decl
   | PatSkol             -- An existential type variable bound by a pattern for
       ConLike           -- a data constructor with an existential type.
@@ -3192,6 +3209,13 @@ data SkolemInfo
   | UnifyForAllSkol     -- We are unifying two for-all types
        TcType           -- The instantiated type *inside* the forall
 
+  | TyConSkol TyConFlavour Name  -- bound in a type declaration of the given flavour
+
+  | DataConSkol Name    -- bound as an existential in a Haskell98 datacon decl or
+                        -- as any variable in a GADT datacon decl
+
+  | ReifySkol           -- Bound during Template Haskell reification
+
   | UnkSkol             -- Unhelpful info (until I improve it)
 
 instance Outputable SkolemInfo where
@@ -3208,13 +3232,13 @@ termEvidenceAllowed _                    = True
 pprSkolInfo :: SkolemInfo -> SDoc
 -- Complete the sentence "is a rigid type variable bound by..."
 pprSkolInfo (SigSkol cx ty _) = pprSigSkolInfo cx ty
+pprSkolInfo (SigTypeSkol cx)  = pprUserTypeCtxt cx
+pprSkolInfo (ForAllSkol doc)  = quotes doc
 pprSkolInfo (IPSkol ips)      = text "the implicit-parameter binding" <> plural ips <+> text "for"
                                  <+> pprWithCommas ppr ips
-pprSkolInfo (ClsSkol cls)     = text "the class declaration for" <+> quotes (ppr cls)
 pprSkolInfo (DerivSkol pred)  = text "the deriving clause for" <+> quotes (ppr pred)
 pprSkolInfo InstSkol          = text "the instance declaration"
 pprSkolInfo (InstSC n)        = text "the instance declaration" <> whenPprDebug (parens (ppr n))
-pprSkolInfo DataSkol          = text "a data type declaration"
 pprSkolInfo FamInstSkol       = text "a family instance declaration"
 pprSkolInfo BracketSkol       = text "a Template Haskell bracket"
 pprSkolInfo (RuleSkol name)   = text "the RULE" <+> pprRuleName name
@@ -3225,6 +3249,9 @@ pprSkolInfo (InferSkol ids)   = hang (text "the inferred type" <> plural ids <+>
                                    2 (vcat [ ppr name <+> dcolon <+> ppr ty
                                                    | (name,ty) <- ids ])
 pprSkolInfo (UnifyForAllSkol ty) = text "the type" <+> ppr ty
+pprSkolInfo (TyConSkol flav name) = text "the" <+> ppr flav <+> text "declaration for" <+> quotes (ppr name)
+pprSkolInfo (DataConSkol name)= text "the data constructor" <+> quotes (ppr name)
+pprSkolInfo ReifySkol         = text "the type being reified"
 
 -- UnkSkol
 -- For type variables the others are dealt with by pprSkolTvBinding.
index c89a197..81e29db 100644 (file)
@@ -28,7 +28,7 @@ module TcSMonad (
     -- Evidence creation and transformation
     MaybeNew(..), freshGoals, isFresh, getEvExpr,
 
-    newTcEvBinds,
+    newTcEvBinds, newNoTcEvBinds,
     newWantedEq, emitNewWantedEq,
     newWanted, newWantedEvVar, newWantedNC, newWantedEvVarNC, newDerivedNC,
     newBoundEvVarId,
@@ -95,11 +95,12 @@ module TcSMonad (
     cloneMetaTyVar, demoteUnfilledFmv,
     tcInstType, tcInstSkolTyVarsX,
 
-    TcLevel, isTouchableMetaTyVarTcS,
+    TcLevel,
     isFilledMetaTyVar_maybe, isFilledMetaTyVar,
     zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
     zonkTyCoVarsAndFVList,
     zonkSimples, zonkWC,
+    zonkTcTyCoVarBndr,
 
     -- References
     newTcRef, readTcRef, updTcRef,
@@ -2566,7 +2567,7 @@ runTcSDeriveds tcs
 -- | This can deal only with equality constraints.
 runTcSEqualities :: TcS a -> TcM a
 runTcSEqualities thing_inside
-  = do { ev_binds_var <- TcM.newTcEvBinds
+  = do { ev_binds_var <- TcM.newNoTcEvBinds
        ; runTcSWithEvBinds ev_binds_var thing_inside }
 
 runTcSWithEvBinds :: EvBindsVar
@@ -2893,11 +2894,6 @@ checkWellStagedDFun pred dfun_id loc
 pprEq :: TcType -> TcType -> SDoc
 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
 
-isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
-isTouchableMetaTyVarTcS tv
-  = do { tclvl <- getTcLevel
-       ; return $ isTouchableMetaTyVar tclvl tv }
-
 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
 isFilledMetaTyVar_maybe tv
  = case tcTyVarDetails tv of
@@ -2935,6 +2931,8 @@ zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
 zonkWC :: WantedConstraints -> TcS WantedConstraints
 zonkWC wc = wrapTcS (TcM.zonkWC wc)
 
+zonkTcTyCoVarBndr :: TcTyCoVar -> TcS TcTyCoVar
+zonkTcTyCoVarBndr tv = wrapTcS (TcM.zonkTcTyCoVarBndr tv)
 
 {- *********************************************************************
 *                                                                      *
@@ -3085,6 +3083,7 @@ instFlexiHelper subst tv
        ; let name = setNameUnique (tyVarName tv) uniq
              kind = substTyUnchecked subst (tyVarKind tv)
              ty'  = mkTyVarTy (mkTcTyVar name kind details)
+       ; TcM.traceTc "instFlexi" (ppr ty')
        ; return (extendTvSubst subst tv ty') }
 
 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
@@ -3121,7 +3120,8 @@ setEvBind ev_bind
 -- | Mark variables as used filling a coercion hole
 useVars :: CoVarSet -> TcS ()
 useVars vars
-  = do { EvBindsVar { ebv_tcvs = ref } <- getTcEvBindsVar
+  = do { ev_binds_var <- getTcEvBindsVar
+       ; let ref = ebv_tcvs ev_binds_var
        ; wrapTcS $
          do { tcvs <- TcM.readTcRef ref
             ; let tcvs' = tcvs `unionVarSet` vars
@@ -3160,6 +3160,9 @@ setEvBindIfWanted ev tm
 newTcEvBinds :: TcS EvBindsVar
 newTcEvBinds = wrapTcS TcM.newTcEvBinds
 
+newNoTcEvBinds :: TcS EvBindsVar
+newNoTcEvBinds = wrapTcS TcM.newNoTcEvBinds
+
 newEvVar :: TcPredType -> TcS EvVar
 newEvVar pred = wrapTcS (TcM.newEvVar pred)
 
index 62fa832..e07ff7c 100644 (file)
@@ -41,7 +41,9 @@ import TcEvidence( HsWrapper, (<.>) )
 import Type( mkTyVarBinders )
 
 import DynFlags
-import Var      ( TyVar, tyVarName, tyVarKind )
+import Var      ( TyVar, tyVarKind )
+import VarSet
+import VarEnv   ( mkInScopeSet )
 import Id       ( Id, idName, idType, idInlinePragma, setInlinePragma, mkLocalId )
 import PrelNames( mkUnboundName )
 import BasicTypes
@@ -49,7 +51,6 @@ import Bag( foldrBag )
 import Module( getModule )
 import Name
 import NameEnv
-import VarSet
 import Outputable
 import SrcLoc
 import Util( singleton )
@@ -70,7 +71,7 @@ especially on value bindings.  Here's an overview.
     f = ...g...
     g = ...f...
 
-* HsSyn: a signature in a binding starts of as a TypeSig, in
+* HsSyn: a signature in a binding starts off as a TypeSig, in
   type HsBinds.Sig
 
 * When starting a mutually recursive group, like f/g above, we
@@ -299,38 +300,34 @@ Once we get to type checking, we decompose it into its parts, in tcPatSynSig.
 
 tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
 -- See Note [Pattern synonym signatures]
+-- See Note [Recipe for checking a signature] in TcHsType
 tcPatSynSig name sig_ty
   | HsIB { hsib_vars = implicit_hs_tvs
          , hsib_body = hs_ty }  <- sig_ty
   , (univ_hs_tvs, hs_req,  hs_ty1)     <- splitLHsSigmaTy hs_ty
   , (ex_hs_tvs,   hs_prov, hs_body_ty) <- splitLHsSigmaTy hs_ty1
-  = do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, body_ty))
-           <- solveEqualities $
-              tcImplicitTKBndrs implicit_hs_tvs $
-              tcExplicitTKBndrs univ_hs_tvs  $ \ univ_tvs ->
-              tcExplicitTKBndrs ex_hs_tvs    $ \ ex_tvs   ->
+  = do { (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty))))
+           <-  -- NB: tcImplicitTKBndrs calls solveEqualities
+              tcImplicitTKBndrs skol_info implicit_hs_tvs $
+              tcExplicitTKBndrs skol_info univ_hs_tvs     $
+              tcExplicitTKBndrs skol_info ex_hs_tvs       $
               do { req     <- tcHsContext hs_req
                  ; prov    <- tcHsContext hs_prov
                  ; body_ty <- tcHsOpenType hs_body_ty
                      -- A (literal) pattern can be unlifted;
                      -- e.g. pattern Zero <- 0#   (Trac #12094)
-                 ; let bound_tvs
-                         = unionVarSets [ allBoundVariabless req
-                                        , allBoundVariabless prov
-                                        , allBoundVariables body_ty
-                                        ]
-                 ; return ( (univ_tvs, req, ex_tvs, prov, body_ty)
-                          , bound_tvs) }
+                 ; return (req, prov, body_ty) }
+
+       ; ungen_patsyn_ty <- zonkPromoteType $
+                            build_patsyn_type [] implicit_tvs univ_tvs req
+                                              ex_tvs prov body_ty
 
        -- Kind generalisation
-       ; kvs <- kindGeneralize $
-                build_patsyn_type [] implicit_tvs univ_tvs req
-                                  ex_tvs prov body_ty
+       ; kvs <- kindGeneralize ungen_patsyn_ty
 
        -- These are /signatures/ so we zonk to squeeze out any kind
-       -- unification variables.  Do this after quantifyTyVars which may
+       -- unification variables.  Do this after kindGeneralize which may
        -- default kind variables to *.
-       ; traceTc "about zonk" empty
        ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs
        ; univ_tvs     <- mapM zonkTcTyCoVarBndr univ_tvs
        ; ex_tvs       <- mapM zonkTcTyCoVarBndr ex_tvs
@@ -338,33 +335,46 @@ tcPatSynSig name sig_ty
        ; prov         <- zonkTcTypes prov
        ; body_ty      <- zonkTcType  body_ty
 
+       -- Skolems have TcLevels too, though they're used only for debugging.
+       -- If you don't do this, the debugging checks fail in TcPatSyn.
+       -- Test case: patsyn/should_compile/T13441
+       ; tclvl <- getTcLevel
+       ; let env0                  = mkEmptyTCvSubst $ mkInScopeSet $ mkVarSet kvs
+             (env1, implicit_tvs') = promoteSkolemsX tclvl env0 implicit_tvs
+             (env2, univ_tvs')     = promoteSkolemsX tclvl env1 univ_tvs
+             (env3, ex_tvs')       = promoteSkolemsX tclvl env2 ex_tvs
+             req'                  = substTys env3 req
+             prov'                 = substTys env3 prov
+             body_ty'              = substTy  env3 body_ty
+
        -- Now do validity checking
        ; checkValidType ctxt $
-         build_patsyn_type kvs implicit_tvs univ_tvs req ex_tvs prov body_ty
+         build_patsyn_type kvs implicit_tvs' univ_tvs' req' ex_tvs' prov' body_ty'
 
        -- arguments become the types of binders. We thus cannot allow
        -- levity polymorphism here
-       ; let (arg_tys, _) = tcSplitFunTys body_ty
+       ; let (arg_tys, _) = tcSplitFunTys body_ty'
        ; mapM_ (checkForLevPoly empty) arg_tys
 
        ; traceTc "tcTySig }" $
-         vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs
+         vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs'
               , text "kvs" <+> ppr_tvs kvs
-              , text "univ_tvs" <+> ppr_tvs univ_tvs
-              , text "req" <+> ppr req
-              , text "ex_tvs" <+> ppr_tvs ex_tvs
-              , text "prov" <+> ppr prov
-              , text "body_ty" <+> ppr body_ty ]
+              , text "univ_tvs" <+> ppr_tvs univ_tvs'
+              , text "req" <+> ppr req'
+              , text "ex_tvs" <+> ppr_tvs ex_tvs'
+              , text "prov" <+> ppr prov'
+              , text "body_ty" <+> ppr body_ty' ]
        ; return (TPSI { patsig_name = name
-                      , patsig_implicit_bndrs = mkTyVarBinders Inferred kvs ++
-                                                mkTyVarBinders Specified implicit_tvs
-                      , patsig_univ_bndrs     = univ_tvs
-                      , patsig_req            = req
-                      , patsig_ex_bndrs       = ex_tvs
-                      , patsig_prov           = prov
-                      , patsig_body_ty        = body_ty }) }
+                      , patsig_implicit_bndrs = mkTyVarBinders Inferred  kvs ++
+                                                mkTyVarBinders Specified implicit_tvs'
+                      , patsig_univ_bndrs     = univ_tvs'
+                      , patsig_req            = req'
+                      , patsig_ex_bndrs       = ex_tvs'
+                      , patsig_prov           = prov'
+                      , patsig_body_ty        = body_ty' }) }
   where
     ctxt = PatSynCtxt name
+    skol_info = SigTypeSkol ctxt
 
     build_patsyn_type kvs imp univ req ex prov body
       = mkInvForAllTys kvs $
@@ -404,7 +414,7 @@ tcInstSig sig@(PartialSig { psig_hs_ty = hs_ty
                           , sig_ctxt = ctxt
                           , sig_loc = loc })
   = setSrcSpan loc $  -- Set the binding site of the tyvars
-    do { (wcs, wcx, tvs, theta, tau) <- tcHsPartialSigType ctxt hs_ty
+    do { (wcs, wcx, tv_names, tvs, theta, tau) <- tcHsPartialSigType ctxt hs_ty
 
         -- Clone the quantified tyvars
         -- Reason: we might have    f, g :: forall a. a -> _ -> a
@@ -413,8 +423,17 @@ tcInstSig sig@(PartialSig { psig_hs_ty = hs_ty
         --         the easiest way to do so, and is very similar to
         --         the tcInstType in the CompleteSig case
         -- See Trac #14643
-        ; (subst, tvs') <- instSkolTyCoVars mk_sig_tv tvs
-        ; let tv_prs = map tyVarName tvs `zip` tvs'
+       ; let in_scope = mkInScopeSet $ closeOverKinds $ unionVarSets
+                          [ mkVarSet (map snd wcs)
+                          , maybe emptyVarSet tyCoVarsOfType wcx
+                          , mkVarSet tvs
+                          , tyCoVarsOfTypes theta
+                          , tyCoVarsOfType tau ]
+               -- the in_scope is a bit bigger than nec'y, but too big is always
+               -- safe
+             empty_subst = mkEmptyTCvSubst in_scope
+       ; (subst, tvs') <- instSkolTyCoVarsX mk_sig_tv empty_subst tvs
+       ; let tv_prs = tv_names `zip` tvs'
 
        ; return (TISI { sig_inst_sig   = sig
                       , sig_inst_skols = tv_prs
index 53be792..7307f74 100644 (file)
@@ -6,12 +6,16 @@ module TcSimplify(
        simplifyAmbiguityCheck,
        simplifyDefault,
        simplifyTop, simplifyTopImplic, captureTopConstraints,
-       simplifyInteractive, solveEqualities,
+       simplifyInteractive,
+       solveEqualities, solveLocalEqualities,
        simplifyWantedsTcM,
        tcCheckSatisfiability,
        tcSubsumes,
        tcCheckHoleFit,
 
+       promoteTyVar,
+       promoteTyVarSet,
+
        -- For Rules we need these
        solveWanteds, solveWantedsAndDrop,
        approximateWC, runTcSDeriveds
@@ -58,6 +62,7 @@ import Control.Monad
 import Data.Foldable      ( toList )
 import Data.List          ( partition )
 import Data.List.NonEmpty ( NonEmpty(..) )
+import Maybes             ( isJust )
 
 {-
 *********************************************************************************
@@ -134,14 +139,33 @@ simplifyTop wanteds
 
        ; return (evBindMapBinds binds1 `unionBags` binds2) }
 
+-- | Type-check a thing that emits only equality constraints, solving any
+-- constraints we can and re-emitting constraints that we can't. The thing_inside
+-- should generally bump the TcLevel to make sure that this run of the solver
+-- doesn't affect anything lying around.
+solveLocalEqualities :: TcM a -> TcM a
+solveLocalEqualities thing_inside
+  = do { traceTc "solveLocalEqualities {" empty
+
+       ; (result, wanted) <- captureConstraints thing_inside
+
+       ; traceTc "solveLocalEqualities: running solver {" (ppr wanted)
+       ; reduced_wanted <- runTcSEqualities (solveWanteds wanted)
+       ; traceTc "solveLocalEqualities: running solver }" (ppr reduced_wanted)
+
+       ; emitConstraints reduced_wanted
+       ; return result }
+
 -- | Type-check a thing that emits only equality constraints, then
 -- solve those constraints. Fails outright if there is trouble.
+-- Use this if you're not going to get another crack at solving
+-- (because, e.g., you're checking a datatype declaration)
 solveEqualities :: TcM a -> TcM a
 solveEqualities thing_inside
   = checkNoErrs $  -- See Note [Fail fast on kind errors]
     do { (result, wanted) <- captureConstraints thing_inside
        ; traceTc "solveEqualities {" $ text "wanted = " <+> ppr wanted
-       ; final_wc <- runTcSEqualities $ simpl_top wanted
+       ; final_wc <- runTcSEqualities $ solveWanteds wanted
        ; traceTc "End solveEqualities }" empty
 
        ; traceTc "reportAllUnsolved {" empty
@@ -498,10 +522,10 @@ tcSubsumes = tcCheckHoleFit emptyBag
 tcCheckHoleFit :: Cts -> TcSigmaType -> TcSigmaType -> TcM Bool
 tcCheckHoleFit _ hole_ty ty | hole_ty `eqType` ty = return True
 tcCheckHoleFit relevantCts hole_ty ty = discardErrs $
- do { (_, wanted, _) <- pushLevelAndCaptureConstraints $
-                           tcSubType_NC ExprSigCtxt ty hole_ty
-    ; rem <- runTcSDeriveds $
-               simpl_top $ addSimples wanted relevantCts
+ do { (tclevel, wanted, _) <- pushLevelAndCaptureConstraints $
+                              tcSubType_NC ExprSigCtxt ty hole_ty
+    ; rem <- setTcLevel tclevel $ runTcSDeriveds $
+                                  simpl_top $ addSimples wanted relevantCts
     -- We don't want any insoluble or simple constraints left,
     -- but solved implications are ok (and neccessary for e.g. undefined)
     ; return (isEmptyBag (wc_simple rem)
@@ -721,8 +745,7 @@ emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
        ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
              is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars
 
-        ; tc_lvl <- TcM.getTcLevel
-        ; mapM_ (promoteTyVar tc_lvl) (tyCoVarsOfCtsList outer_simple)
+        ; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple)
 
         ; unless (isEmptyCts outer_simple) $
           do { traceTc "emitResidualConstrants:simple" (ppr outer_simple)
@@ -872,15 +895,15 @@ decideQuantification
 -- See Note [Deciding quantification]
 decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
   = do { -- Step 1: find the mono_tvs
-       ; (mono_tvs, candidates) <- decideMonoTyVars infer_mode
-                                        name_taus psigs candidates
+       ; (mono_tvs, candidates, co_vars) <- decideMonoTyVars infer_mode
+                                              name_taus psigs candidates
 
        -- Step 2: default any non-mono tyvars, and re-simplify
        -- This step may do some unification, but result candidates is zonked
        ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
 
        -- Step 3: decide which kind/type variables to quantify over
-       ; (qtvs, co_vars) <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
+       ; qtvs <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
 
        -- Step 4: choose which of the remaining candidate
        --         predicates to actually quantify over
@@ -912,12 +935,13 @@ decideMonoTyVars :: InferMode
                  -> [(Name,TcType)]
                  -> [TcIdSigInst]
                  -> [PredType]
-                 -> TcM (TcTyCoVarSet, [PredType])
+                 -> TcM (TcTyCoVarSet, [PredType], CoVarSet)
 -- Decide which tyvars and covars cannot be generalised:
 --   (a) Free in the environment
 --   (b) Mentioned in a constraint we can't generalise
 --   (c) Connected by an equality to (a) or (b)
--- Also return the reduced set of constraint we can generalise
+-- Also return CoVars that appear free in the final quatified types
+--   we can't quantify over these, and we must make sure they are in scope
 decideMonoTyVars infer_mode name_taus psigs candidates
   = do { (no_quant, maybe_quant) <- pick infer_mode candidates
 
@@ -926,13 +950,30 @@ decideMonoTyVars infer_mode name_taus psigs candidates
        ; psig_qtvs <- mapM zonkTcTyVarToTyVar $
                       concatMap (map snd . sig_inst_skols) psigs
 
+       ; psig_theta <- mapM TcM.zonkTcType $
+                       concatMap sig_inst_theta psigs
+
+       ; taus <- mapM (TcM.zonkTcType . snd) name_taus
+
        ; mono_tvs0 <- tcGetGlobalTyCoVars
-       ; let eq_constraints = filter isEqPred candidates
-             mono_tvs1     = growThetaTyVars eq_constraints mono_tvs0
+       ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
+
+             co_vars = coVarsOfTypes (psig_tys ++ taus)
+             co_var_tvs = closeOverKinds co_vars
+               -- The co_var_tvs are tvs mentioned in the types of covars or
+               -- coercion holes. We can't quantify over these covars, so we
+               -- must include the variable in their types in the mono_tvs.
+               -- E.g.  If we can't quantify over co :: k~Type, then we can't
+               --       quantify over k either!  Hence closeOverKinds
+
+             mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
+
+             eq_constraints = filter isEqPred candidates
+             mono_tvs2      = growThetaTyVars eq_constraints mono_tvs1
 
              constrained_tvs = (growThetaTyVars eq_constraints
                                                (tyCoVarsOfTypes no_quant)
-                                `minusVarSet` mono_tvs1)
+                                `minusVarSet` mono_tvs2)
                                `delVarSetList` psig_qtvs
              -- constrained_tvs: the tyvars that we are not going to
              -- quantify solely because of the moonomorphism restriction
@@ -948,15 +989,14 @@ decideMonoTyVars infer_mode name_taus psigs candidates
              --   be quantified (Trac #14479); see
              --   Note [Quantification and partial signatures], Wrinkle 3, 4
 
-             mono_tvs = mono_tvs1 `unionVarSet` constrained_tvs
+             mono_tvs = mono_tvs2 `unionVarSet` constrained_tvs
 
            -- Warn about the monomorphism restriction
        ; warn_mono <- woptM Opt_WarnMonomorphism
        ; when (case infer_mode of { ApplyMR -> warn_mono; _ -> False}) $
-         do { taus <- mapM (TcM.zonkTcType . snd) name_taus
-            ; warnTc (Reason Opt_WarnMonomorphism)
+         warnTc (Reason Opt_WarnMonomorphism)
                 (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
-                mr_msg }
+                mr_msg
 
        ; traceTc "decideMonoTyVars" $ vcat
            [ text "mono_tvs0 =" <+> ppr mono_tvs0
@@ -964,9 +1004,10 @@ decideMonoTyVars infer_mode name_taus psigs candidates
            , text "no_quant =" <+> ppr no_quant
            , text "maybe_quant =" <+> ppr maybe_quant
            , text "eq_constraints =" <+> ppr eq_constraints
-           , text "mono_tvs =" <+> ppr mono_tvs ]
+           , text "mono_tvs =" <+> ppr mono_tvs
+           , text "co_vars =" <+> ppr co_vars ]
 
-       ; return (mono_tvs, maybe_quant) }
+       ; return (mono_tvs, maybe_quant, co_vars) }
   where
     pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
     -- Split the candidates into ones we definitely
@@ -1003,12 +1044,8 @@ defaultTyVarsAndSimplify :: TcLevel
 defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
   = do {  -- Promote any tyvars that we cannot generalise
           -- See Note [Promote momomorphic tyvars]
-       ; outer_tclvl <- TcM.getTcLevel
-       ; let prom_tvs = nonDetEltsUniqSet mono_tvs
-                        -- It's OK to use nonDetEltsUniqSet here
-                        -- because promoteTyVar is commutative
-       ; traceTc "decideMonoTyVars: promotion:" (ppr prom_tvs)
-       ; proms <- mapM (promoteTyVar outer_tclvl) prom_tvs
+       ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs)
+       ; prom <- promoteTyVarSet mono_tvs
 
        -- Default any kind/levity vars
        ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
@@ -1022,7 +1059,7 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
 
        ; case () of
            _ | some_default -> simplify_cand candidates
-             | or proms     -> mapM TcM.zonkTcType candidates
+             | prom         -> mapM TcM.zonkTcType candidates
              | otherwise    -> return candidates
        }
   where
@@ -1052,10 +1089,8 @@ decideQuantifiedTyVars
    -> [(Name,TcType)]   -- Annotated theta and (name,tau) pairs
    -> [TcIdSigInst]     -- Partial signatures
    -> [PredType]        -- Candidates, zonked
-   -> TcM ([TyVar], CoVarSet)
+   -> TcM [TyVar]
 -- Fix what tyvars we are going to quantify over, and quantify them
--- Also return CoVars that appear free in the final quatified types
---   we can't quantify over these, and we must make sure they are in scope
 decideQuantifiedTyVars mono_tvs name_taus psigs candidates
   = do {     -- Why psig_tys? We try to quantify over everything free in here
              -- See Note [Quantification and partial signatures]
@@ -1074,15 +1109,6 @@ decideQuantifiedTyVars mono_tvs name_taus psigs candidates
              -- Now "grow" those seeds to find ones reachable via 'candidates'
              grown_tcvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
 
-       -- We cannot quantify a type over a coercion (term-level) variable
-       -- So, if any CoVars appear in grow_tcvs (they might for example
-       -- appear in a cast in a type) we must remove them from the quantified
-       -- variables, along with any type variables free in their kinds
-       -- E.g.  If we can't quantify over co :: k~Type, then we can't
-       --       quantify over k either!  Hence closeOverKinds
-       ; let co_vars    = filterVarSet isCoVar grown_tcvs
-             proto_qtvs = grown_tcvs `minusVarSet` closeOverKinds co_vars
-
        -- Now we have to classify them into kind variables and type variables
        -- (sigh) just for the benefit of -XNoPolyKinds; see quantifyTyVars
        --
@@ -1092,23 +1118,15 @@ decideQuantifiedTyVars mono_tvs name_taus psigs candidates
        ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
                       = candidateQTyVarsOfTypes $
                         psig_tys ++ candidates ++ tau_tys
-             pick     = (`dVarSetIntersectVarSet` proto_qtvs)
+             pick     = (`dVarSetIntersectVarSet` grown_tcvs)
              dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
 
        ; traceTc "decideQuantifiedTyVars" (vcat
            [ text "seed_tys =" <+> ppr seed_tys
            , text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys)
-           , text "grown_tcvs =" <+> ppr grown_tcvs
-           , text "co_vars =" <+> ppr co_vars
-           , text "proto_qtvs =" <+> ppr proto_qtvs])
-
-       ; qtvs <- quantifyTyVars mono_tvs dvs_plus
-       ; return (qtvs, co_vars) }
-         -- Return all the CoVars that (transitively) might be mentioned
-         -- in the tau_tys etc.  We don't need to do a closeOverKinds on
-         -- co_vars to get the transitive ones, because the grown_tvs
-         -- are already closed over kinds, and hence contain all such
-         -- co_vars
+           , text "grown_tcvs =" <+> ppr grown_tcvs])
+
+       ; quantifyTyVars mono_tvs dvs_plus }
 
 ------------------
 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
@@ -1129,6 +1147,7 @@ growThetaTyVars theta tcvs
        where
          pred_tcvs = tyCoVarsOfType pred
 
+
 {- Note [Promote momomorphic tyvars]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Promote any type variables that are free in the environment.  Eg
@@ -1579,10 +1598,12 @@ setImplicationStatus :: Implication -> TcS (Maybe Implication)
 --    * Trim the ic_wanted field to remove Derived constraints
 -- Precondition: the ic_status field is not already IC_Solved
 -- Return Nothing if we can discard the implication altogether
-setImplicationStatus implic@(Implic { ic_status = status
-                                    , ic_info   = info
-                                    , ic_wanted = wc
-                                    , ic_given  = givens })
+setImplicationStatus implic@(Implic { ic_status    = status
+                                    , ic_info      = info
+                                    , ic_skols     = skols
+                                    , ic_telescope = m_telescope
+                                    , ic_wanted    = wc
+                                    , ic_given     = givens })
  | ASSERT2( not (isSolvedStatus status ), ppr info )
    -- Precondition: we only set the status if it is not already solved
    not all_solved
@@ -1606,17 +1627,23 @@ setImplicationStatus implic@(Implic { ic_status = status
  = do { traceTcS "setImplicationStatus(all-solved) {" (ppr implic)
 
       ; implic <- neededEvVars implic
+      ; skols <- mapM TcS.zonkTcTyCoVarBndr skols
 
       ; let dead_givens | warnRedundantGivens info
                         = filterOut (`elemVarSet` ic_need_inner implic) givens
                         | otherwise = []   -- None to report
 
+            bad_telescope = check_telescope skols
+
             discard_entire_implication  -- Can we discard the entire implication?
               =  null dead_givens           -- No warning from this implication
+              && not bad_telescope
               && isEmptyBag pruned_implics  -- No live children
               && isEmptyVarSet (ic_need_outer implic) -- No needed vars to pass up to parent
 
-            final_status = IC_Solved { ics_dead = dead_givens }
+            final_status
+              | bad_telescope = IC_BadTelescope
+              | otherwise     = IC_Solved { ics_dead = dead_givens }
             final_implic = implic { ic_status = final_status
                                   , ic_wanted = pruned_wc }
 
@@ -1649,6 +1676,19 @@ setImplicationStatus implic@(Implic { ic_status = status
      | otherwise
      = True        -- Otherwise, keep it
 
+   -- See Note [Keeping scoped variables in order: Explicit] in TcHsType
+   check_telescope sks = isJust m_telescope && go emptyVarSet (reverse sks)
+     where
+       go :: TyVarSet   -- skolems that appear *later* than the current ones
+          -> [TcTyVar]  -- ordered skolems, in reverse order
+          -> Bool       -- True <=> there is an out-of-order skolem
+       go _ [] = False
+       go later_skols (one_skol : earlier_skols)
+         | tyCoVarsOfType (tyVarKind one_skol) `intersectsVarSet` later_skols
+         = True
+         | otherwise
+         = go (later_skols `extendVarSet` one_skol) earlier_skols
+
 warnRedundantGivens :: SkolemInfo -> Bool
 warnRedundantGivens (SigSkol ctxt _ _)
   = case ctxt of
@@ -1898,33 +1938,38 @@ we'll get more Givens (a unification is like adding a Given) to
 allow the implication to make progress.
 -}
 
-promoteTyVar :: TcLevel -> TcTyVar  -> TcM Bool
+promoteTyVar :: TcTyVar -> TcM Bool
 -- When we float a constraint out of an implication we must restore
 -- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
 -- Return True <=> we did some promotion
 -- See Note [Promoting unification variables]
-promoteTyVar tclvl tv
-  | isFloatedTouchableMetaTyVar tclvl tv
-  = do { cloned_tv <- TcM.cloneMetaTyVar tv
-       ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
-       ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
-       ; return True }
-  | otherwise
-  = return False
-
-promoteTyVarTcS :: TcLevel -> TcTyVar  -> TcS ()
+promoteTyVar tv
+  = do { tclvl <- TcM.getTcLevel
+       ; if (isFloatedTouchableMetaTyVar tclvl tv)
+         then do { cloned_tv <- TcM.cloneMetaTyVar tv
+                 ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
+                 ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
+                 ; return True }
+         else return False }
+
+-- Returns whether or not *any* tyvar is defaulted
+promoteTyVarSet :: TcTyVarSet -> TcM Bool
+promoteTyVarSet tvs
+  = or <$> mapM promoteTyVar (nonDetEltsUniqSet tvs)
+    -- non-determinism is OK because order of promotion doesn't matter
+
+promoteTyVarTcS :: TcTyVar  -> TcS ()
 -- When we float a constraint out of an implication we must restore
 -- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
 -- See Note [Promoting unification variables]
 -- We don't just call promoteTyVar because we want to use unifyTyVar,
 -- not writeMetaTyVar
-promoteTyVarTcS tclvl tv
-  | isFloatedTouchableMetaTyVar tclvl tv
-  = do { cloned_tv <- TcS.cloneMetaTyVar tv
-       ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
-       ; unifyTyVar tv (mkTyVarTy rhs_tv) }
-  | otherwise
-  = return ()
+promoteTyVarTcS tv
+  = do { tclvl <- TcS.getTcLevel
+       ; when (isFloatedTouchableMetaTyVar tclvl tv) $
+         do { cloned_tv <- TcS.cloneMetaTyVar tv
+            ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
+            ; unifyTyVar tv (mkTyVarTy rhs_tv) } }
 
 -- | Like 'defaultTyVar', but in the TcS monad.
 defaultTyVarTcS :: TcTyVar -> TcS Bool
@@ -2212,9 +2257,7 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
 
        -- Promote any unification variables mentioned in the floated equalities
        -- See Note [Promoting unification variables]
-       ; outer_tclvl <- TcS.getTcLevel
-       ; mapM_ (promoteTyVarTcS outer_tclvl)
-               (tyCoVarsOfCtsList flt_eqs)
+       ; mapM_ promoteTyVarTcS (tyCoVarsOfCtsList flt_eqs)
 
        ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
                                           , text "Extended skols =" <+> ppr extended_skols
index f518a42..c4a6edc 100644 (file)
@@ -1173,7 +1173,7 @@ reifyInstances th_nm th_tys
                   ; return ((tv_names, rn_ty), fvs) }
         ; (_tvs, ty)
             <- solveEqualities $
-               tcImplicitTKBndrsType tv_names $
+               tcImplicitTKBndrs ReifySkol tv_names $
                fst <$> tcLHsType rn_ty
         ; ty <- zonkTcTypeToType emptyZonkEnv ty
                 -- Substitute out the meta type variables
index 39697d6..6598942 100644 (file)
@@ -301,11 +301,10 @@ instances of families altogether in the following. However, we need to include
 the kinds of *associated* families into the construction of the initial kind
 environment. (This is handled by `allDecls').
 
-
 See also Note [Kind checking recursive type and class declarations]
 
 Note [How TcTyCons work]
-o~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~
 TcTyCons are used for two distinct purposes
 
 1.  When recovering from a type error in a type declaration,
@@ -350,6 +349,37 @@ TcTyCons are used for two distinct purposes
     into scope in kcTyClTyVars and tcTyClTyVars, both in TcHsType.
 
     In a TcTyCon, everything is zonked after the kind-checking pass (S2).
+
+Note [Check telescope again during generalisation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The telescope check before kind generalisation is useful to catch something
+like this:
+
+  data T a k = MkT (Proxy (a :: k))
+
+Clearly, the k has to come first. Checking for this problem must come before
+kind generalisation, as described in Note [Bad telescopes] in
+TcValidity.
+
+However, we have to check again *after* kind generalisation, to catch something
+like this:
+
+  data SameKind :: k -> k -> Type  -- to force unification
+  data S a (b :: a) (d :: SameKind c b)
+
+Note that c has no explicit binding site. As such, it's quantified by kind
+generalisation. (Note that kcHsTyVarBndrs does not return such variables
+as binders in its returned TcTyCon.) The user-written part of this telescope
+is well-ordered; no earlier variables depend on later ones. However, after
+kind generalisation, we put c up front, like so:
+
+  data S {c :: a} a (b :: a) (d :: SameKind c b)
+
+We now have a problem. We could detect this problem just by looking at the
+free vars of the kinds of the generalised variables (the kvs), but we get
+such a nice error message out of checkValidTelescope that it seems like the
+right thing to do.
+
 -}
 
 
@@ -403,7 +433,7 @@ kcTyClGroup decls
         -- Step 3: generalisation
         -- Kind checking done for this group
         -- Now we have to kind generalize the flexis
-        ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
+        ; res <- concat <$> mapAndReportM (generaliseTCD (tcl_env lcl_env)) decls
 
         ; traceTc "---- kcTyClGroup end ---- }" (vcat (map pp_res res))
         ; return res }
@@ -412,14 +442,19 @@ kcTyClGroup decls
     generalise :: TcTypeEnv -> Name -> TcM TcTyCon
     -- For polymorphic things this is a no-op
     generalise kind_env name
-      = do { let tc = case lookupNameEnv kind_env name of
-                        Just (ATcTyCon tc) -> tc
-                        _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
-                 tc_binders  = tyConBinders tc
-                 tc_res_kind = tyConResKind tc
-                 tc_tyvars   = tyConTyVars tc
-                 scoped_tvs  = tcTyConScopedTyVars tc
-
+      | Just (ATcTyCon tc) <- lookupNameEnv kind_env name
+      = setSrcSpan (getSrcSpan tc) $
+        addTyConCtxt tc $
+        do { tc_binders  <- mapM zonkTcTyVarBinder (tyConBinders tc)
+           ; tc_res_kind <- zonkTcType (tyConResKind tc)
+           ; let scoped_tvs  = tcTyConScopedTyVars tc
+                 user_tyvars = tcTyConUserTyVars tc
+
+              -- See Note [checkValidDependency]
+           ; checkValidDependency tc_binders tc_res_kind
+
+               -- See Note [Bad telescopes] in TcValidity
+           ; checkValidTelescope tc_binders user_tyvars empty
            ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)
 
            ; let all_binders = mkNamedTyConBinders Inferred kvs ++ tc_binders
@@ -428,17 +463,24 @@ kcTyClGroup decls
            ; tc_res_kind'        <- zonkTcTypeToType env tc_res_kind
            ; scoped_tvs'         <- zonkSigTyVarPairs scoped_tvs
 
+             -- See Note [Check telescope again during generalisation]
+           ; let extra = text "NB: Implicitly declared variables come before others."
+           ; checkValidTelescope all_binders user_tyvars extra
+
                       -- Make sure tc_kind' has the final, zonked kind variables
            ; traceTc "Generalise kind" $
              vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind)
                   , ppr kvs, ppr all_binders, ppr tc_res_kind
                   , ppr all_binders', ppr tc_res_kind'
-                  , ppr tc_tyvars, ppr (tcTyConScopedTyVars tc)]
+                  , ppr scoped_tvs ]
 
-           ; return (mkTcTyCon name all_binders' tc_res_kind'
+           ; return (mkTcTyCon name user_tyvars all_binders' tc_res_kind'
                                scoped_tvs'
                                (tyConFlavour tc)) }
 
+      | otherwise
+      = pprPanic "kcTyClGroup.generalise" (ppr name)
+
     generaliseTCD :: TcTypeEnv
                   -> LTyClDecl GhcRn -> TcM [TcTyCon]
     generaliseTCD kind_env (L _ decl)
@@ -536,7 +578,7 @@ getInitialKind :: TyClDecl GhcRn
 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
   = do { let cusk = hsDeclHasCusk decl
        ; (tycon, inner_prs) <-
-           kcLHsQTyVars name ClassFlavour cusk True ktvs $
+           kcLHsQTyVars name ClassFlavour cusk ktvs $
            do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats
               ; return (constraintKind, inner_prs) }
        ; return (extendEnvWithTcTyCon inner_prs tycon) }
@@ -546,16 +588,12 @@ getInitialKind decl@(DataDecl { tcdLName = L _ name
                               , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                          , dd_ND = new_or_data } })
   = do  { (tycon, _) <-
-           kcLHsQTyVars name flav (hsDeclHasCusk decl) True ktvs $
+           kcLHsQTyVars name (newOrDataToFlavour new_or_data) (hsDeclHasCusk decl) ktvs $
            do { res_k <- case m_sig of
-                           Just ksig -> tcLHsKindSig ksig
+                           Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig
                            Nothing   -> return liftedTypeKind
               ; return (res_k, ()) }
         ; return (mkTcTyConEnv tycon) }
-  where
-    flav = case new_or_data of
-             NewType  -> NewtypeFlavour
-             DataType -> DataTypeFlavour
 
 getInitialKind (FamDecl { tcdFam = decl })
   = getFamDeclInitialKind Nothing decl
@@ -564,11 +602,10 @@ getInitialKind decl@(SynDecl { tcdLName = L _ name
                              , tcdTyVars = ktvs
                              , tcdRhs = rhs })
   = do  { (tycon, _) <- kcLHsQTyVars name TypeSynonymFlavour
-                            (hsDeclHasCusk decl)
-                            True ktvs $
+                            (hsDeclHasCusk decl) ktvs $
             do  { res_k <- case kind_annotation rhs of
                             Nothing -> newMetaKindVar
-                            Just ksig -> tcLHsKindSig ksig
+                            Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
                 ; return (res_k, ()) }
         ; return (mkTcTyConEnv tycon) }
   where
@@ -594,10 +631,10 @@ getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
                                                , fdResultSig = L _ resultSig
                                                , fdInfo      = info })
   = do { (tycon, _) <-
-           kcLHsQTyVars name flav cusk True ktvs $
+           kcLHsQTyVars name flav cusk ktvs $
            do { res_k <- case resultSig of
-                      KindSig ki                        -> tcLHsKindSig ki
-                      TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKindSig ki
+                      KindSig ki                        -> tcLHsKindSig ctxt ki
+                      TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKindSig ctxt ki
                       _ -- open type families have * return kind by default
                         | tcFlavourIsOpen flav     -> return liftedTypeKind
                         -- closed type families have their return kind inferred
@@ -608,19 +645,25 @@ getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
   where
     cusk  = famDeclHasCusk mb_cusk decl
     flav  = case info of
-      DataFamily         -> DataFamilyFlavour
-      OpenTypeFamily     -> OpenTypeFamilyFlavour
+      DataFamily         -> DataFamilyFlavour (isJust mb_cusk)
+      OpenTypeFamily     -> OpenTypeFamilyFlavour (isJust mb_cusk)
       ClosedTypeFamily _ -> ClosedTypeFamilyFlavour
+    ctxt  = TyFamResKindCtxt name
 
 ------------------------------------------------------------------------
 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
   -- See Note [Kind checking for type and class decls]
 kcLTyClDecl (L loc decl)
+  | hsDeclHasCusk decl
+  = traceTc "kcTyClDecl skipped due to cusk" (ppr tc_name)
+  | otherwise
   = setSrcSpan loc $
     tcAddDeclCtxt decl $
-    do { traceTc "kcTyClDecl {" (ppr (tyClDeclLName decl))
+    do { traceTc "kcTyClDecl {" (ppr tc_name)
        ; kcTyClDecl decl
-       ; traceTc "kcTyClDecl done }" (ppr (tyClDeclLName decl)) }
+       ; traceTc "kcTyClDecl done }" (ppr tc_name) }
+  where
+    tc_name = tyClDeclLName decl
 
 kcTyClDecl :: TyClDecl GhcRn -> TcM ()
 -- This function is used solely for its side effect on kind variables
@@ -629,10 +672,10 @@ kcTyClDecl :: TyClDecl GhcRn -> TcM ()
 --    by getInitialKind, so we can ignore them here.
 
 kcTyClDecl (DataDecl { tcdLName = L _ name, tcdDataDefn = defn })
-  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
+  | HsDataDefn { dd_cons = cons@(L _ (ConDeclGADT {}) : _), dd_ctxt = L _ [] } <- defn
   = mapM_ (wrapLocM kcConDecl) cons
     -- hs_tvs and dd_kindSig already dealt with in getInitialKind
-    -- If dd_kindSig is Just, this must be a GADT-style decl,
+    -- This must be a GADT-style decl,
     --        (see invariants of DataDefn declaration)
     -- so (a) we don't need to bring the hs_tvs into scope, because the
     --        ConDecls bind all their own variables
@@ -656,7 +699,7 @@ kcTyClDecl (ClassDecl { tcdLName = 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) = kcHsSigType (TyConSkol ClassFlavour name) nms op_ty
     kc_sig _                        = return ()
 
 kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
@@ -674,11 +717,12 @@ kcConDecl :: ConDecl GhcRn -> TcM ()
 kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
                       , con_mb_cxt = ex_ctxt, con_args = args })
   = addErrCtxt (dataConCtxtName [name]) $
-    do { _ <- tcExplicitTKBndrs ex_tvs $ \ _ ->
-              do { _ <- tcHsMbContext ex_ctxt
-                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
-                 ; return (panic "kcConDecl", emptyVarSet) }
-       ; return () }
+      -- See Note [Use SigTvs in kind-checking pass]
+    kcExplicitTKBndrs ex_tvs $
+    do { _ <- tcHsMbContext ex_ctxt
+       ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args) }
+              -- We don't need to check the telescope here, because that's
+              -- done in tcConDecl
 
 kcConDecl (ConDeclGADT { con_names = names
                        , con_qvars = qtvs, con_mb_cxt = cxt
@@ -693,13 +737,13 @@ kcConDecl (ConDeclGADT { con_names = names
     -- If we don't look at MkT we won't get the correct kind
     -- for the type constructor T
     addErrCtxt (dataConCtxtName names) $
-    do { _ <- tcImplicitTKBndrs implicit_tkv_nms $
-              tcExplicitTKBndrs explicit_tkv_nms $ \ _ ->
-              do { _ <- tcHsMbContext cxt
-                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
-                 ; _ <- tcHsOpenType res_ty
-                 ; return (panic "kcConDecl", emptyVarSet) }
-         ; return () }
+    discardResult $
+    kcImplicitTKBndrs implicit_tkv_nms Nothing $
+    kcExplicitTKBndrs explicit_tkv_nms $
+    do { _ <- tcHsMbContext cxt
+       ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
+       ; _ <- tcHsOpenType res_ty
+       ; return () }
 
 {-
 Note [Recursion and promoting data constructors]
@@ -718,6 +762,54 @@ mappings:
 APromotionErr is only used for DataCons, and only used during type checking
 in tcTyClGroup.
 
+Note [Use SigTvs in kind-checking pass]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  data Proxy a where
+    MkProxy1 :: forall k (b :: k). Proxy b
+    MkProxy2 :: forall j (c :: j). Proxy c
+
+It seems reasonable that this should be accepted. But something very strange
+is going on here: when we're kind-checking this declaration, we need to unify
+the kind of `a` with k and j -- even though k and j's scopes are local to the type of
+MkProxy{1,2}. The best approach we've come up with is to use SigTvs during
+the kind-checking pass. First off, note that it's OK if the kind-checking pass
+is too permissive: we'll snag the problems in the type-checking pass later.
+(This extra permissiveness might happen with something like
+
+  data SameKind :: k -> k -> Type
+  data Bad a where
+    MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)
+
+which would be accepted if k1 and k2 were SigTvs. This is correctly rejected
+in the second pass, though. Test case: polykinds/SigTvKinds3)
+Recall that the kind-checking pass exists solely to collect constraints
+on the kinds and to power unification.
+
+To achieve the use of SigTvs, we must be careful to use specialized functions
+that produce SigTvs, not ordinary skolems. This is why we need
+kcExplicitTKBndrs and kcImplicitTKBndrs in TcHsType, separate from their
+tc... variants.
+
+The drawback of this approach is sometimes it will accept a definition that
+a (hypothetical) declarative specification would likely reject. As a general
+rule, we don't want to allow polymorphic recursion without a CUSK. Indeed,
+the whole point of CUSKs is to allow polymorphic recursion. Yet, the SigTvs
+approach allows a limited form of polymorphic recursion *without* a CUSK.
+
+To wit:
+  data T a = forall k (b :: k). MkT (T b) Int
+  (test case: dependent/should_compile/T14066a)
+
+Note that this is polymorphically recursive, with the recursive occurrence
+of T used at a kind other than a's kind. The approach outlined here accepts
+this definition, because this kind is still a kind variable (and so the
+SigTvs unify). Stepping back, I (Richard) have a hard time envisioning a
+way to describe exactly what declarations will be accepted and which will
+be rejected (without a CUSK). However, the accepted definitions are indeed
+well-kinded and any rejected definitions would be accepted with a CUSK,
+and so this wrinkle need not cause anyone to lose sleep.
 
 ************************************************************************
 *                                                                      *
@@ -828,7 +920,8 @@ tcTyClDecl1 _parent roles_info
 
   -- "data/newtype" declaration
 tcTyClDecl1 _parent roles_info
-            (DataDecl { tcdLName = L _ tc_name, tcdDataDefn = defn })
+            (DataDecl { tcdLName = L _ tc_name
+                      , tcdDataDefn = defn })
   = ASSERT( isNothing _parent )
     tcTyClTyVars tc_name $ \ tycon_binders res_kind ->
     tcDataDefn roles_info tc_name tycon_binders res_kind defn
@@ -875,7 +968,7 @@ tcTyClDecl1 _parent roles_info
 
 tcFamDecl1 :: Maybe Class -> FamilyDecl GhcRn -> TcM TyCon
 tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_name)
-                              , fdResultSig = L _ sig
+                              , fdResultSig = L _ sig, fdTyVars = user_tyvars
                               , fdInjectivityAnn = inj })
   | DataFamily <- fam_info
   = tcTyClTyVars tc_name $ \ binders res_kind -> do
@@ -933,10 +1026,10 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
            Just eqns -> do {
 
          -- Process the equations, creating CoAxBranches
-       ; let tc_fam_tc = mkTcTyCon tc_name binders res_kind
+       ; let tc_fam_tc = mkTcTyCon tc_name (ppr user_tyvars) binders res_kind
                                    [] ClosedTypeFamilyFlavour
 
-       ; branches <- mapM (tcTyFamInstEqn tc_fam_tc Nothing) eqns
+       ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc Nothing) eqns
          -- Do not attempt to drop equations dominated by earlier
          -- ones here; in the case of mutual recursion with a data
          -- type, we get a knot-tying failure.  Instead we check
@@ -1243,16 +1336,18 @@ kcTyFamInstEqn tc_fam_tc
            , text "feqn_pats =" <+> ppr pats ])
        ; checkTc (fam_name == eqn_tc_name)
                  (wrongTyFamName fam_name eqn_tc_name)
-       ; discardResult $
-         tc_fam_ty_pats tc_fam_tc Nothing -- not an associated type
-                        tv_names pats (kcTyFamEqnRhs Nothing hs_ty) }
+          -- this check reports an arity error instead of a kind error; easier for user
+       ; checkTc (pats `lengthIs` vis_arity) $
+                  wrongNumberOfParmsErr vis_arity
+       ; kcFamTyPats tc_fam_tc tv_names pats $ \ rhs_kind ->
+         discardResult $ kcTyFamEqnRhs Nothing hs_ty rhs_kind }
   where
     fam_name = tyConName tc_fam_tc
+    vis_arity = length (tyConVisibleTyVars tc_fam_tc)
 
 -- Infer the kind of the type on the RHS of a type family eqn. Then use
 -- this kind to check the kind of the LHS of the equation. This is useful
--- as the callback to tc_fam_ty_pats and the kind-checker to
--- tcFamTyPats.
+-- as the callback to tcFamTyPats.
 kcTyFamEqnRhs :: Maybe ClsInstInfo
               -> LHsType GhcRn        -- ^ Eqn RHS
               -> TcKind               -- ^ Inferred kind of left-hand side
@@ -1324,7 +1419,7 @@ kcDataDefn mb_kind_env
           -- See Note [Failing early in kcDataDefn]
         ; exp_res_kind <- case mb_kind of
             Nothing -> return liftedTypeKind
-            Just k  -> tcLHsKindSig k
+            Just k  -> tcLHsKindSig (DataKindCtxt (unLoc fam_name)) k
 
           -- The expected type might have a forall at the type. Normally, we
           -- can't skolemise in kinds because we don't have type-level lambda.
@@ -1370,24 +1465,6 @@ Kind check type patterns and kind annotate the embedded type variables.
    not check whether there is a pattern for each type index; the latter
    check is only required for type synonym instances.
 
-Note [tc_fam_ty_pats vs tcFamTyPats]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-tc_fam_ty_pats does the type checking of the patterns, but it doesn't
-zonk or generate any desugaring. It is used when kind-checking closed
-type families.
-
-tcFamTyPats type checks the patterns, zonks, and then calls thing_inside
-to generate a desugaring. It is used during type-checking (not kind-checking).
-
-Note [Type-checking type patterns]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When typechecking the patterns of a family instance declaration, we can't
-rely on using the family TyCon itself, because this is sometimes called
-from within a type-checking knot. (Specifically for closed type families.)
-The TcTyCon gives just enough information to do the job.
-
-See also Note [tc_fam_ty_pats vs tcFamTyPats]
-
 Note [Instantiating a family tycon]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It's possible that kind-checking the result of a family tycon applied to
@@ -1424,15 +1501,38 @@ two bad things could happen:
 -}
 
 -----------------
-tc_fam_ty_pats :: TcTyCon    -- The family TcTyCon
-                             -- See Note [Type-checking type patterns]
-               -> Maybe ClsInstInfo
-               -> [Name]              -- Bound kind/type variable names
-               -> HsTyPats GhcRn      -- Type patterns
-               -> (TcKind -> TcM r)   -- Kind checker for RHS
-               -> TcM ( [TcTyVar]     -- Returns the type-checked patterns,
-                      , [TcType]      -- the type variables that scope over
-                      , r )           -- them, and the thing inside
+kcFamTyPats :: TcTyCon
+            -> [Name]
+            -> HsTyPats GhcRn
+            -> (TcKind -> TcM ())
+            -> TcM ()
+kcFamTyPats tc_fam_tc tv_names arg_pats kind_checker
+  = discardResult $
+    kcImplicitTKBndrs tv_names Nothing $
+    do { let loc     = nameSrcSpan name
+             lhs_fun = L loc (HsTyVar NotPromoted (L loc name))
+               -- lhs_fun is for error messages only
+             no_fun  = pprPanic "kcFamTyPats" (ppr name)
+             fun_kind = tyConKind tc_fam_tc
+
+       ; (_, _, res_kind_out) <- tcInferApps typeLevelMode Nothing lhs_fun no_fun
+                                             fun_kind arg_pats
+       ; kind_checker res_kind_out }
+  where
+    name = tyConName tc_fam_tc
+
+tcFamTyPats :: TyCon
+            -> Maybe ClsInstInfo
+            -> [Name]          -- Implicitly bound kind/type variable names
+            -> HsTyPats GhcRn  -- Type patterns
+            -> (TcKind -> TcM ([TcType], TcKind))
+                -- kind-checker for RHS
+                -- See Note [Instantiating a family tycon]
+            -> (   [TcTyVar]         -- Kind and type variables
+                -> [TcType]          -- Kind and type arguments
+                -> TcKind
+                -> TcM a)            -- NB: You can use solveEqualities here.
+            -> TcM a
 -- Check the type patterns of a type or data family instance
 --     type instance F <pat1> <pat2> = <type>
 -- The 'tyvars' are the free type variables of pats
@@ -1443,65 +1543,37 @@ tc_fam_ty_pats :: TcTyCon    -- The family TcTyCon
 --          type F [a] = ...
 -- In that case, the type variable 'a' will *already be in scope*
 -- (and, if C is poly-kinded, so will its kind parameter).
-
-tc_fam_ty_pats tc_fam_tc mb_clsinfo tv_names arg_pats
-               kind_checker
+tcFamTyPats fam_tc mb_clsinfo
+            tv_names arg_pats kind_checker thing_inside
   = do { -- First, check the arity.
          -- If we wait until validity checking, we'll get kind
          -- errors below when an arity error will be much easier to
          -- understand.
          let should_check_arity
-               | DataFamilyFlavour <- flav = False
+               | DataFamilyFlavour <- flav = False
                   -- why not check data families? See [Arity of data families] in FamInstEnv
-               | otherwise                 = True
+               | otherwise                   = True
 
        ; when should_check_arity $
          checkTc (arg_pats `lengthIs` vis_arity) $
          wrongNumberOfParmsErr vis_arity
                       -- report only explicit arguments
 
-         -- Kind-check and quantify
-         -- See Note [Quantifying over family patterns]
-       ; (arg_tvs, (args, stuff)) <- tcImplicitTKBndrs tv_names $
-         do { let loc          = nameSrcSpan name
-                  lhs_fun      = L loc (HsTyVar NotPromoted (L loc name))
-                  fun_ty       = mkTyConApp tc_fam_tc []
-                  fun_kind     = tyConKind tc_fam_tc
-                  mb_kind_env  = thdOf3 <$> mb_clsinfo
-
-            ; (_, args, res_kind_out)
-                <- tcInferApps typeLevelMode mb_kind_env
-                               lhs_fun fun_ty fun_kind arg_pats
-
-            ; stuff <- kind_checker res_kind_out
+       ; (fam_used_tvs, (typats, (more_typats, res_kind)))
+            <- solveEqualities $  -- See Note [Constraints in patterns]
+               tcImplicitTKBndrs FamInstSkol tv_names $
+               do { let loc = nameSrcSpan fam_name
+                        lhs_fun = L loc (HsTyVar NotPromoted (L loc fam_name))
+                        fun_ty = mkTyConApp fam_tc []
+                        fun_kind = tyConKind fam_tc
+                        mb_kind_env = thdOf3 <$> mb_clsinfo
 
-            ; return ((args, stuff), emptyVarSet) }
+                  ; (_, args, res_kind_out)
+                      <- tcInferApps typeLevelMode mb_kind_env
+                                     lhs_fun fun_ty fun_kind arg_pats
 
-       ; return (arg_tvs, args, stuff) }
-  where
-    name      = tyConName tc_fam_tc
-    vis_arity = length (tyConVisibleTyVars tc_fam_tc)
-    flav      = tyConFlavour tc_fam_tc
-
--- See Note [tc_fam_ty_pats vs tcFamTyPats]
-tcFamTyPats :: TcTyCon
-            -> Maybe ClsInstInfo
-            -> [Name]          -- Implicitly bound kind/type variable names
-            -> HsTyPats GhcRn  -- Type patterns
-            -> (TcKind -> TcM ([TcType], TcKind))
-                -- kind-checker for RHS
-                -- See Note [Instantiating a family tycon]
-            -> (   [TcTyVar]         -- Kind and type variables
-                -> [TcType]          -- Kind and type arguments
-                -> TcKind
-                -> TcM a)            -- NB: You can use solveEqualities here.
-            -> TcM a
-tcFamTyPats tc_fam_tc mb_clsinfo
-            tv_names arg_pats kind_checker thing_inside
-  = do { (fam_used_tvs, typats, (more_typats, res_kind))
-            <- solveEqualities $  -- See Note [Constraints in patterns]
-               tc_fam_ty_pats tc_fam_tc mb_clsinfo
-                              tv_names arg_pats kind_checker
+                  ; stuff <- kind_checker res_kind_out
+                  ; return (args, stuff) }
 
           {- TODO (RAE): This should be cleverer. Consider this:
 
@@ -1528,18 +1600,19 @@ tcFamTyPats tc_fam_tc mb_clsinfo
        ; vars  <- zonkTcTypesAndSplitDepVars all_pats
        ; qtkvs <- quantifyTyVars emptyVarSet vars
 
-       ; MASSERT( isEmptyVarSet $ coVarsOfTypes typats )
+       ; when debugIsOn $
+         do { all_pats <- mapM zonkTcTypeInKnot all_pats
+            ; MASSERT2( isEmptyVarSet $ coVarsOfTypes all_pats, ppr all_pats ) }
            -- This should be the case, because otherwise the solveEqualities
            -- above would fail. TODO (RAE): Update once the solveEqualities
            -- bit is cleverer.
 
-       ; traceTc "tcFamTyPats" (ppr (getName tc_fam_tc)
+       ; traceTc "tcFamTyPats" (ppr (getName fam_tc)
                                 $$ ppr all_pats $$ ppr qtkvs)
            -- Don't print out too much, as we might be in the knot
 
            -- See Note [Free-floating kind vars] in TcHsType
-       ; let tc_flav = tyConFlavour tc_fam_tc
-             all_mentioned_tvs = mkVarSet qtkvs
+       ; let all_mentioned_tvs = mkVarSet qtkvs
                                    -- qtkvs has all the tyvars bound by LHS
                                    -- type patterns
              unmentioned_tvs   = filterOut (`elemVarSet` all_mentioned_tvs)
@@ -1547,14 +1620,19 @@ tcFamTyPats tc_fam_tc mb_clsinfo
                                    -- If there are tyvars left over, we can
                                    -- assume they're free-floating, since they
                                    -- aren't bound by a type pattern
-       ; checkNoErrs $ reportFloatingKvs (getName tc_fam_tc) tc_flav
+       ; checkNoErrs $ reportFloatingKvs fam_name flav
                                          qtkvs unmentioned_tvs
 
-       ; tcExtendTyVarEnv qtkvs $
+       ; scopeTyVars FamInstSkol qtkvs $
             -- Extend envt with TcTyVars not TyVars, because the
             -- kind checking etc done by thing_inside does not expect
             -- to encounter TyVars; it expects TcTyVars
          thing_inside qtkvs all_pats res_kind }
+  where
+    fam_name  = tyConName fam_tc
+    flav      = tyConFlavour fam_tc
+    vis_arity = length (tyConVisibleTyVars fam_tc)
+
 
 {-
 Note [Constraints in patterns]
@@ -1710,33 +1788,32 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
                       , con_args = hs_args })
   = addErrCtxt (dataConCtxtName [name]) $
     do { -- Get hold of the existential type variables
-         -- e.g. data T a = forall (b::k) f. MkT a (f b)
+         -- e.g. data T a = forall (b::k) f. MkT a (f b)
          -- Here tmpl_bndrs = {a}
          --      hs_qvars = HsQTvs { hsq_implicit = {k}
          --                        , hsq_explicit = {f,b} }
 
        ; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ])
 
-       ; ((exp_tvs, ctxt, arg_tys, field_lbls, stricts), _bound_vars)
+       ; (exp_tvs, (ctxt, arg_tys, field_lbls, stricts))
            <- solveEqualities $
-              tcExplicitTKBndrs explicit_tkv_nms $ \ exp_tvs ->
+              tcExplicitTKBndrs skol_info explicit_tkv_nms $
               do { ctxt <- tcHsMbContext hs_ctxt
                  ; btys <- tcConArgs hs_args
                  ; field_lbls <- lookupConstructorFields (unLoc name)
                  ; let (arg_tys, stricts) = unzip btys
-                       bound_vars  = emptyVarSet  -- Not used
-                 ; return ((exp_tvs, ctxt, arg_tys, field_lbls, stricts), bound_vars)
+                 ; return (ctxt, arg_tys, field_lbls, stricts)
                  }
 
          -- exp_tvs have explicit, user-written binding sites
          -- the kvs below are those kind variables entirely unmentioned by the user
          --   and discovered only by generalization
 
-             -- Kind generalisation
-       ; vars <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys exp_tvs $
-                                            mkFunTys ctxt $
-                                            mkFunTys arg_tys $
-                                            unitTy)
+       ; kvs <- quantifyConDecl (mkVarSet (binderVars tmpl_bndrs))
+                                (mkSpecForAllTys exp_tvs $
+                                 mkFunTys ctxt $
+                                 mkFunTys arg_tys $
+                                 unitTy)
                  -- That type is a lie, of course. (It shouldn't end in ()!)
                  -- And we could construct a proper result type from the info
                  -- at hand. But the result would mention only the tmpl_tvs,
@@ -1744,8 +1821,6 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
                  -- we're doing this to get the right behavior around removing
                  -- any vars bound in exp_binders.
 
-       ; kvs <- quantifyTyVars (mkVarSet (binderVars tmpl_bndrs)) vars
-
              -- Zonk to Types
        ; (ze, qkvs)      <- zonkTyBndrsX emptyZonkEnv kvs
        ; (ze, user_qtvs) <- zonkTyBndrsX ze exp_tvs
@@ -1782,6 +1857,8 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
        ; traceTc "tcConDecl 2" (ppr name)
        ; mapM buildOneDataCon [name]
        }
+  where
+    skol_info = SigTypeSkol (ConArgCtxt (unLoc name))
 
 tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
           (ConDeclGADT { con_names = names
@@ -1793,28 +1870,25 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
   = addErrCtxt (dataConCtxtName names) $
     do { traceTc "tcConDecl 1" (ppr names)
        ; let (L _ name : _) = names
+             skol_info      = DataConSkol name
 
-       ; (imp_tvs, (exp_tvs, ctxt, arg_tys, res_ty, field_lbls, stricts))
+       ; (imp_tvs, (exp_tvs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
            <- solveEqualities $
-              tcImplicitTKBndrs implicit_tkv_nms $
-              tcExplicitTKBndrs explicit_tkv_nms $ \ exp_tvs ->
+              tcImplicitTKBndrs skol_info implicit_tkv_nms $
+              tcExplicitTKBndrs skol_info explicit_tkv_nms $
               do { ctxt <- tcHsMbContext cxt
                  ; btys <- tcConArgs hs_args
                  ; res_ty' <- tcHsLiftedType res_ty
                  ; field_lbls <- lookupConstructorFields name
                  ; let (arg_tys, stricts) = unzip btys
-                       bound_vars = allBoundVariabless ctxt `unionVarSet`
-                                    allBoundVariabless arg_tys
-
-                 ; return ((exp_tvs, ctxt, arg_tys, res_ty', field_lbls, stricts), bound_vars)
+                 ; return (ctxt, arg_tys, res_ty', field_lbls, stricts)
                  }
        ; let user_tvs = imp_tvs ++ exp_tvs
 
-       ; vars <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys user_tvs $
-                                            mkFunTys ctxt $
-                                            mkFunTys arg_tys $
-                                            res_ty)
-       ; tkvs <- quantifyTyVars emptyVarSet vars
+       ; tkvs <- quantifyConDecl emptyVarSet (mkSpecForAllTys user_tvs $
+                                              mkFunTys ctxt $
+                                              mkFunTys arg_tys $
+                                              res_ty)
 
              -- Zonk to Types
        ; (ze, tkvs)     <- zonkTyBndrsX emptyZonkEnv tkvs
@@ -1863,6 +1937,15 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
        ; mapM buildOneDataCon names
        }
 
+-- | Produce the telescope of kind variables that this datacon is
+-- implicitly quantified over. Incoming type need not be zonked.
+quantifyConDecl :: TcTyCoVarSet  -- outer tvs, not to be quantified over; zonked
+                -> TcType -> TcM [TcTyVar]
+quantifyConDecl gbl_tvs ty
+  = do { ty <- zonkTcTypeInKnot ty
+       ; let fvs = candidateQTyVarsOfType ty
+       ; quantifyTyVars gbl_tvs fvs }
+
 tcConIsInfixH98 :: Name
              -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn])
              -> TcM Bool
@@ -2321,7 +2404,7 @@ checkValidTyCl tc
     recovery_code -- See Note [Recover from validity error]
       = do { traceTc "Aborted validity for tycon" (ppr tc)
            ; return fake_tc }
-    fake_tc | isFamilyTyCon tc || isTypeSynonymTyCon tc
+    fake_tc | not (isClassTyCon tc)
             = makeRecoveryTyCon tc
             | otherwise
             = tc
@@ -2370,7 +2453,6 @@ checkValidTyCon tc
 
   | otherwise
   = do { traceTc "checkValidTyCon" (ppr tc $$ ppr (tyConClass_maybe tc))
-       ; checkValidTyConTyVars tc
        ; if | Just cl <- tyConClass_maybe tc
               -> checkValidClass cl
 
@@ -2486,56 +2568,6 @@ checkFieldCompat fld con1 con2 res1 res2 fty1 fty2
     mb_subst2 = tcMatchTyX (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
 
 -------------------------------
--- | Check for ill-scoped telescopes in a tycon.
--- For example:
---
--- > data SameKind :: k -> k -> *   -- this is OK
--- > data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
---
--- The problem is that @b@ should be bound (implicitly) at the beginning,
--- but its kind mentions @a@, which is not yet in scope. Kind generalization
--- makes a mess of this, and ends up including @a@ twice in the final
--- tyvars. So this function checks for duplicates and, if there are any,
--- produces the appropriate error message.
-checkValidTyConTyVars :: TyCon -> TcM ()
-checkValidTyConTyVars tc
-  = do { -- strip off the duplicates and look for ill-scoped things
-         -- but keep the *last* occurrence of each variable, as it's
-         -- most likely the one the user wrote
-         let stripped_tvs | duplicate_vars
-                          = reverse $ nub $ reverse tvs
-                          | otherwise
-                          = tvs
-             vis_tvs      = tyConVisibleTyVars tc
-             extra | not (vis_tvs `equalLength` stripped_tvs)
-                   = text "NB: Implicitly declared kind variables are put first."
-                   | otherwise
-                   = empty
-       ; traceTc "checkValidTyConTyVars" (ppr tc <+> ppr tvs)
-       ; checkValidTelescope (pprTyVars vis_tvs) stripped_tvs extra
-         `and_if_that_doesn't_error`
-           -- This triggers on test case dependent/should_fail/InferDependency
-           -- It reports errors around Note [Dependent LHsQTyVars] in TcHsType
-         when duplicate_vars (
-          addErr (vcat [ text "Invalid declaration for" <+>
-                         quotes (ppr tc) <> semi <+> text "you must explicitly"
-                       , text "declare which variables are dependent on which others."
-                       , hang (text "Inferred variable kinds:")
-                         2 (vcat (map pp_tv stripped_tvs)) ])) }
-  where
-    tvs = tyConTyVars tc
-    duplicate_vars = tvs `lengthExceeds` sizeVarSet (mkVarSet tvs)
-
-    pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
-
-     -- only run try_second if the first reports no errors
-    and_if_that_doesn't_error :: TcM () -> TcM () -> TcM ()
-    try_first `and_if_that_doesn't_error` try_second
-      = recoverM (return ()) $
-        do { checkNoErrs try_first
-           ; try_second }
-
--------------------------------
 checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
 checkValidDataCon dflags existential_ok tc con
   = setSrcSpan (getSrcSpan con)  $
@@ -3058,7 +3090,75 @@ For example:
 
   data T a = A { m1 :: a, _m2 :: a } | B { m1 :: a }
 
+Note [checkValidDependency]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  data Proxy k (a :: k)
+  data Proxy2 k a = P (Proxy k a)
+
+(This is test dependent/should_fail/InferDependency.) While it seems GHC can
+figure out the dependency between the arguments to Proxy2, this case errors.
+The problem is that when we build the initial kind (getInitialKind) for
+a tycon, we need to decide whether an argument is dependent or not. At first,
+I thought we could just assume that *all* arguments are dependent, and then
+patch it up later. However, this causes problems in error messages (where
+tycon's have mysterious kinds "forall (a :: k) -> blah") and in unification
+(where we try to unify kappa ~ forall (a :: k) -> blah, failing because the
+RHS is not a tau-type). Perhaps a cleverer algorithm could sort this out
+(say, by storing the dependency flag in a mutable cell and by avoiding
+these fancy kinds in error messages depending on the extension in effect)
+but it doesn't seem worth it.
+
+So: we choose the dependency for each argument variable once and for all
+in getInitialKind. This means that any dependency must be lexically manifest.
+
+checkValidDependency checks to make sure that no lexically non-dependent
+argument actually appears in a kind. Note the example above, where the k
+in Proxy2 is a dependent argument, but this fact is not lexically
+manifest. checkValidDependency will reject. This function must be called
+*before* kind generalization, because kind generalization works with
+the result of mkTyConKind, which will think that Proxy2's kind is
+Type -> k -> Type, where k is unbound. (It won't use a forall for a
+"non-dependent" argument k.)
+-}
+
+-- | See Note [checkValidDependency]
+checkValidDependency :: [TyConBinder]  -- zonked
+                     -> TcKind         -- zonked (result kind)
+                     -> TcM ()
+checkValidDependency binders res_kind
+  = go (tyCoVarsOfType res_kind) (reverse binders)
+  where
+    go :: TyCoVarSet     -- fvs from scope
+       -> [TyConBinder]  -- binders, in reverse order
+       -> TcM ()
+    go _   []           = return ()  -- all set
+    go fvs (tcb : tcbs)
+      | not (isNamedTyConBinder tcb) && tcb_var `elemVarSet` fvs
+      = do { setSrcSpan (getSrcSpan tcb_var) $
+             addErrTc (vcat [ text "Type constructor argument" <+> quotes (ppr tcb_var) <+>
+                              text "is used dependently."
+                            , text "Any dependent arguments must be obviously so, not inferred"
+                            , text "by the type-checker."
+                            , hang (text "Inferred argument kinds:")
+                                 2 (vcat (map pp_binder binders))
+                            , text "Suggestion: use" <+> quotes (ppr tcb_var) <+>
+                              text "in a kind to make the dependency clearer." ])
+           ; go new_fvs tcbs }
+
+      | otherwise
+      = go new_fvs tcbs
+      where
+        new_fvs = fvs `delVarSet` tcb_var
+                      `unionVarSet` tyCoVarsOfType tcb_kind
+
+        tcb_var  = binderVar tcb
+        tcb_kind = tyVarKind tcb_var
 
+        pp_binder binder = ppr (binderVar binder) <+> dcolon <+> ppr (binderKind binder)
+
+{-
 ************************************************************************
 *                                                                      *
                 Checking role validity
index f15f704..3a8b9b3 100644 (file)
@@ -32,7 +32,7 @@ module TcType (
   TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
   strictlyDeeperThan, sameDepthAs, fmvTcLevel,
   tcTypeLevel, tcTyVarLevel, maxTcLevel,
-
+  promoteSkolem, promoteSkolemX, promoteSkolemsX,
   --------------------------------
   -- MetaDetails
   UserTypeCtxt(..), pprUserTypeCtxt, isSigMaybe,
@@ -108,9 +108,6 @@ module TcType (
   candidateQTyVarsOfType, candidateQTyVarsOfTypes, CandidatesQTvs(..),
   anyRewritableTyVar,
 
-  -- * Extracting bound variables
-  allBoundVariables, allBoundVariabless,
-
   ---------------------------------
   -- Foreign import and export
   isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
@@ -151,7 +148,7 @@ module TcType (
 
   -- Type substitutions
   TCvSubst(..),         -- Representation visible to a few friends
-  TvSubstEnv, emptyTCvSubst,
+  TvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
   zipTvSubst,
   mkTvSubstPrs, notElemTCvSubst, unionTCvSubst,
   getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
@@ -231,9 +228,9 @@ import ListSetOps ( getNth, findDupsEq )
 import Outputable
 import FastString
 import ErrUtils( Validity(..), MsgDoc, isValid )
-import FV
 import qualified GHC.LanguageExtensions as LangExt
 
+import Data.List  ( mapAccumL )
 import Data.IORef
 import Data.List.NonEmpty( NonEmpty(..) )
 import Data.Functor.Identity
@@ -329,7 +326,6 @@ GHC Trac #12785.
 -}
 
 -- See Note [TcTyVars in the typechecker]
-type TcTyVar = TyVar    -- Used only during type inference
 type TcCoVar = CoVar    -- Used only during type inference
 type TcType = Type      -- A TcType can have mutable type variables
 type TcTyCoVar = Var    -- Either a TcTyVar or a CoVar
@@ -618,6 +614,10 @@ data UserTypeCtxt
   | DataTyCtxt Name     -- The "stupid theta" part of a data decl
                         --      data <S> => T a = MkT a
   | DerivClauseCtxt     -- A 'deriving' clause
+  | TyVarBndrKindCtxt Name  -- The kind of a type variable being bound
+  | DataKindCtxt Name   -- The kind of a data/newtype (instance)
+  | TySynKindCtxt Name  -- The kind of the RHS of a type synonym
+  | TyFamResKindCtxt Name   -- The result kind of a type family
 
 {-
 -- Notes re TySynCtxt
@@ -654,6 +654,10 @@ pprUserTypeCtxt SigmaCtxt         = text "the context of a polymorphic type"
 pprUserTypeCtxt (DataTyCtxt tc)   = text "the context of the data type declaration for" <+> quotes (ppr tc)
 pprUserTypeCtxt (PatSynCtxt n)    = text "the signature for pattern synonym" <+> quotes (ppr n)
 pprUserTypeCtxt (DerivClauseCtxt) = text "a `deriving' clause"
+pprUserTypeCtxt (TyVarBndrKindCtxt n) = text "the kind annotation on the type variable" <+> quotes (ppr n)
+pprUserTypeCtxt (DataKindCtxt n)  = text "the kind annotation on the declaration for" <+> quotes (ppr n)
+pprUserTypeCtxt (TySynKindCtxt n) = text "the kind annotation on the declaration for" <+> quotes (ppr n)
+pprUserTypeCtxt (TyFamResKindCtxt n) = text "the result kind for" <+> quotes (ppr n)
 
 isSigMaybe :: UserTypeCtxt -> Maybe Name
 isSigMaybe (FunSigCtxt n _) = Just n
@@ -795,6 +799,7 @@ tcTyVarLevel tv
           SkolemTv tv_lvl _             -> tv_lvl
           RuntimeUnk                    -> topTcLevel
 
+
 tcTypeLevel :: TcType -> TcLevel
 -- Max level of any free var of the type
 tcTypeLevel ty
@@ -802,11 +807,37 @@ tcTypeLevel ty
   where
     add v lvl
       | isTcTyVar v = lvl `maxTcLevel` tcTyVarLevel v
-      | otherwise   = lvl
+      | otherwise = lvl
 
 instance Outputable TcLevel where
   ppr (TcLevel us) = ppr us
 
+promoteSkolem :: TcLevel -> TcTyVar -> TcTyVar
+promoteSkolem tclvl skol
+  | tclvl < tcTyVarLevel skol
+  = ASSERT( isTcTyVar skol && isSkolemTyVar skol )
+    setTcTyVarDetails skol (SkolemTv tclvl (isOverlappableTyVar skol))
+
+  | otherwise
+  = skol
+
+-- | Change the TcLevel in a skolem, extending a substitution
+promoteSkolemX :: TcLevel -> TCvSubst -> TcTyVar -> (TCvSubst, TcTyVar)
+promoteSkolemX tclvl subst skol
+  = ASSERT( isTcTyVar skol && isSkolemTyVar skol )
+    (new_subst, new_skol)
+  where
+    new_skol
+      | tclvl < tcTyVarLevel skol
+      = setTcTyVarDetails (updateTyVarKind (substTy subst) skol)
+                          (SkolemTv tclvl (isOverlappableTyVar skol))
+      | otherwise
+      = updateTyVarKind (substTy subst) skol
+    new_subst = extendTvSubstWithClone subst skol new_skol
+
+promoteSkolemsX :: TcLevel -> TCvSubst -> [TcTyVar] -> (TCvSubst, [TcTyVar])
+promoteSkolemsX tclvl = mapAccumL (promoteSkolemX tclvl)
+
 {- *********************************************************************
 *                                                                      *
     Finding type family instances
@@ -988,33 +1019,6 @@ out the other (Trac #14363).
 
 {- *********************************************************************
 *                                                                      *
-          Bound variables in a type
-*                                                                      *
-********************************************************************* -}
-
--- | Find all variables bound anywhere in a type.
--- See also Note [Scope-check inferred kinds] in TcHsType
-allBoundVariables :: Type -> TyVarSet
-allBoundVariables ty = fvVarSet $ go ty
-  where
-    go :: Type -> FV
-    go (TyVarTy tv)     = go (tyVarKind tv)
-    go (TyConApp _ tys) = mapUnionFV go tys
-    go (AppTy t1 t2)    = go t1 `unionFV` go t2
-    go (FunTy t1 t2)    = go t1 `unionFV` go t2
-    go (ForAllTy (TvBndr tv _) t2) = FV.unitFV tv `unionFV`
-                                    go (tyVarKind tv) `unionFV` go t2
-    go (LitTy {})       = emptyFV
-    go (CastTy ty _)    = go ty
-    go (CoercionTy {})  = emptyFV
-      -- any types mentioned in a coercion should also be mentioned in
-      -- a type.
-
-allBoundVariabless :: [Type] -> TyVarSet
-allBoundVariabless = mapUnionVarSet allBoundVariables
-
-{- *********************************************************************
-*                                                                      *
           Type and kind variables in a type
 *                                                                      *
 ********************************************************************* -}
index b7031df..f7c5e9a 100644 (file)
@@ -892,7 +892,7 @@ fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
       = do { let ty_lvl = tcTypeLevel ty
            ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
                        ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
-                       ppr ty <+> ppr (typeKind ty) $$ ppr orig_ty )
+                       ppr ty <+> dcolon <+> ppr (typeKind ty) $$ ppr orig_ty )
            ; cts <- readTcRef ref
            ; case cts of
                Just already_there -> pprPanic "writeExpType"
@@ -1183,7 +1183,11 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
   = return (emptyBag, emptyTcEvBinds)
 
   | otherwise
-  = ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
+  = ASSERT2( all (isSkolemTyVar <||> isSigTyVar) skol_tvs, ppr skol_tvs )
+      -- Why allow SigTvs? Because implicitly declared kind variables in
+      -- non-CUSK type declarations are SigTvs, and we need to bring them
+      -- into scope as a skolem in an implication. This is OK, though,
+      -- because SigTvs will always remain tyvars, even after unification.
     do { ev_binds_var <- newTcEvBinds
        ; env <- getLclEnv
        ; let implic = newImplication { ic_tclvl  = tclvl
@@ -1315,6 +1319,14 @@ uType t_or_k origin orig_ty1 orig_ty2
       | tc1 == tc2
       = return $ mkReflCo Nominal ty1
 
+    go (CastTy t1 co1) t2
+      = do { co_tys <- go t1 t2
+           ; return (mkCoherenceLeftCo co_tys co1) }
+
+    go t1 (CastTy t2 co2)
+      = do { co_tys <- go t1 t2
+           ; return (mkCoherenceRightCo co_tys co2) }
+
         -- See Note [Expanding synonyms during unification]
         --
         -- Also NB that we recurse to 'go' so that we don't push a
@@ -1327,14 +1339,6 @@ uType t_or_k origin orig_ty1 orig_ty2
       | Just ty1' <- tcView ty1 = go ty1' ty2
       | Just ty2' <- tcView ty2 = go ty1  ty2'
 
-    go (CastTy t1 co1) t2
-      = do { co_tys <- go t1 t2
-           ; return (mkCoherenceLeftCo co_tys co1) }
-
-    go t1 (CastTy t2 co2)
-      = do { co_tys <- go t1 t2
-           ; return (mkCoherenceRightCo co_tys co2) }
-
         -- Functions (or predicate functions) just check the two parts
     go (FunTy fun1 arg1) (FunTy fun2 arg2)
       = do { co_l <- uType t_or_k origin fun1 fun2
@@ -1449,6 +1453,9 @@ We expand synonyms during unification, but:
    more likely that the inferred types will mention type synonyms
    understandable to the user
 
+ * Similarly, we expand *after* the CastTy case, just in case the
+   CastTy wraps a variable.
+
  * We expand *before* the TyConApp case.  For example, if we have
       type Phantom a = Int
    and are unifying
index d2d32c6..08b7dff 100644 (file)
@@ -14,7 +14,7 @@ module TcValidity (
   ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch,
   checkValidTyFamEqn,
   arityErr, badATErr,
-  checkValidTelescope, checkZonkValidTelescope, checkValidInferredKinds,
+  checkValidTelescope,
   allDistinctTyVars
   ) where
 
@@ -29,7 +29,6 @@ import TcUnify    ( tcSubType_NC )
 import TcSimplify ( simplifyAmbiguityCheck )
 import TyCoRep
 import TcType hiding ( sizeType, sizeTypes )
-import TcMType
 import PrelNames
 import Type
 import Coercion
@@ -50,7 +49,6 @@ import FamInst     ( makeInjectivityErrors )
 import Name
 import VarEnv
 import VarSet
-import UniqSet
 import Var         ( TyVarBndr(..), mkTyVar )
 import ErrUtils
 import DynFlags
@@ -354,6 +352,12 @@ checkValidType ctxt ty
                  SpecInstCtxt   -> rank1
                  ThBrackCtxt    -> rank1
                  GhciCtxt       -> ArbitraryRank
+
+                 TyVarBndrKindCtxt _ -> rank0
+                 DataKindCtxt _      -> rank1
+                 TySynKindCtxt _     -> rank1
+                 TyFamResKindCtxt _  -> rank1
+
                  _              -> panic "checkValidType"
                                           -- Can't happen; not used for *user* sigs
 
@@ -457,7 +461,7 @@ check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
 -- Rank 0 means no for-alls anywhere
 
 check_type env ctxt rank ty
-  | not (null tvs && null theta)
+  | not (null tvbs && null theta)
   = do  { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
         ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
                 -- Reject e.g. (Maybe (?x::Int => Int)),
@@ -468,14 +472,18 @@ check_type env ctxt rank ty
                 -- but not   type T = ?x::Int
 
         ; check_type env' ctxt rank tau      -- Allow foralls to right of arrow
+
         ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
                    (forAllEscapeErr env' ty tau_kind)
         }
   where
-    (tvs, theta, tau) = tcSplitSigmaTy ty
-    tau_kind          = typeKind tau
-    (env', _)         = tidyTyCoVarBndrs env tvs
+    (tvbs, phi)  = tcSplitForAllTyVarBndrs ty
+    (theta, tau) = tcSplitPhiTy phi
 
+    tvs          = binderVars tvbs
+    (env', _)    = tidyTyCoVarBndrs env tvs
+
+    tau_kind              = typeKind tau
     phi_kind | null theta = tau_kind
              | otherwise  = liftedTypeKind
         -- If there are any constraints, the kind is *. (#11405)
@@ -489,7 +497,7 @@ check_type env ctxt rank (FunTy arg_ty res_ty)
     (arg_rank, res_rank) = funArgResRank rank
 
 check_type env ctxt rank (AppTy ty1 ty2)
-  = do  { check_arg_type env ctxt rank ty1
+  = do  { check_type env ctxt rank ty1
         ; check_arg_type env ctxt rank ty2 }
 
 check_type env ctxt rank ty@(TyConApp tc tys)
@@ -915,13 +923,16 @@ okIPCtxt (DataTyCtxt {})        = True
 okIPCtxt (PatSynCtxt {})        = True
 okIPCtxt (TySynCtxt {})         = True   -- e.g.   type Blah = ?x::Int
                                          -- Trac #11466
-
-okIPCtxt (ClassSCCtxt {})  = False
-okIPCtxt (InstDeclCtxt {}) = False
-okIPCtxt (SpecInstCtxt {}) = False
-okIPCtxt (RuleSigCtxt {})  = False
-okIPCtxt DefaultDeclCtxt   = False
-okIPCtxt DerivClauseCtxt   = False
+okIPCtxt (ClassSCCtxt {})       = False
+okIPCtxt (InstDeclCtxt {})      = False
+okIPCtxt (SpecInstCtxt {})      = False
+okIPCtxt (RuleSigCtxt {})       = False
+okIPCtxt DefaultDeclCtxt        = False
+okIPCtxt DerivClauseCtxt        = False
+okIPCtxt (TyVarBndrKindCtxt {}) = False
+okIPCtxt (DataKindCtxt {})      = False
+okIPCtxt (TySynKindCtxt {})     = False
+okIPCtxt (TyFamResKindCtxt {})  = False
 
 {-
 Note [Kind polymorphic type classes]
@@ -1840,23 +1851,16 @@ this is bogus. (We could probably figure out to put b between a and c.
 But I think this is doing users a disservice, in the long run.)
 (Testcase: dependent/should_fail/BadTelescope4)
 
-3. t3 :: forall a. (forall k (b :: k). SameKind a b) -> ()
+To catch these errors, we call checkValidTelescope during kind-checking
+datatype declarations. This must be done *before* kind-generalization,
+because kind-generalization might observe, say, T1, see that k is free
+in a's kind, and generalize over it, producing nonsense. It also must
+be done *after* kind-generalization, in order to catch the T2 case, which
+becomes apparent only after generalizing.
 
-This is a straightforward skolem escape. Note that a and b need to have
-the same kind.
-(Testcase: polykinds/T11142)
+Note [Keeping scoped variables in order: Explicit] discusses how this
+check works for `forall x y z.` written in a type.
 
-How do we deal with all of this? For TyCons, we have checkValidTyConTyVars.
-That function looks to see if any of the tyConTyVars are repeated, but
-it's really a telescope check. It works because all tycons are kind-generalized.
-If there is a bad telescope, the kind-generalization will end up generalizing
-over a variable bound later in the telescope.
-
-For non-tycons, we do scope checking when we bring tyvars into scope,
-in tcImplicitTKBndrs and tcExplicitTKBndrs. Note that we also have to
-sort implicit binders into a well-scoped order whenever we have implicit
-binders to worry about. This is done in quantifyTyVars and in
-tcImplicitTKBndrs.
 -}
 
 -- | Check a list of binders to see if they make a valid telescope.
@@ -1868,29 +1872,21 @@ tcImplicitTKBndrs.
 -- general validity checking, because once we kind-generalise, this sort
 -- of problem is harder to spot (as we'll generalise over the unbound
 -- k in a's type.) See also Note [Bad telescopes].
-checkValidTelescope :: SDoc        -- the original user-written telescope
-                    -> [TyVar]     -- explicit vars (not necessarily zonked)
-                    -> SDoc        -- note to put at bottom of message
+checkValidTelescope :: [TyConBinder]   -- explicit vars (zonked)
+                    -> SDoc            -- original, user-written telescope
+                    -> SDoc            -- extra text to print
                     -> TcM ()
-checkValidTelescope hs_tvs orig_tvs extra
-  = discardResult $ checkZonkValidTelescope hs_tvs orig_tvs extra
-
--- | Like 'checkZonkValidTelescope', but returns the zonked tyvars
-checkZonkValidTelescope :: SDoc
-                        -> [TyVar]
-                        -> SDoc
-                        -> TcM [TyVar]
-checkZonkValidTelescope hs_tvs orig_tvs extra
-  = do { orig_tvs <- mapM zonkTyCoVarKind orig_tvs
-       ; let (_, sorted_tidied_tvs) = tidyTyCoVarBndrs emptyTidyEnv $
-                                      toposortTyVars orig_tvs
-       ; unless (go [] emptyVarSet orig_tvs) $
+checkValidTelescope tvbs user_tyvars extra
+  = do { let tvs      = binderVars tvbs
+
+             (_, sorted_tidied_tvs) = tidyTyCoVarBndrs emptyTidyEnv $
+                                      toposortTyVars tvs
+       ; unless (go [] emptyVarSet (binderVars tvbs)) $
          addErr $
-         vcat [ hang (text "These kind and type variables:" <+> hs_tvs $$
+         vcat [ hang (text "These kind and type variables:" <+> user_tyvars $$
                       text "are out of dependency order. Perhaps try this ordering:")
-                   2 (sep (map pprTyVar sorted_tidied_tvs))
-              , extra ]
-       ; return orig_tvs }
+                   2 (pprTyVars sorted_tidied_tvs)
+              , extra ] }
 
   where
     go :: [TyVar]  -- misplaced variables
@@ -1905,37 +1901,6 @@ checkZonkValidTelescope hs_tvs orig_tvs extra
                       tyCoVarsOfTypeList (tyVarKind tv)
         in go (bad_tvs ++ errs) (in_scope `extendVarSet` tv) tvs
 
--- | After inferring kinds of type variables, check to make sure that the
--- inferred kinds any of the type variables bound in a smaller scope.
--- This is a skolem escape check. See also Note [Bad telescopes].
-checkValidInferredKinds :: [TyVar]     -- ^ vars to check (zonked)
-                        -> TyVarSet    -- ^ vars out of scope
-                        -> SDoc        -- ^ suffix to error message
-                        -> TcM ()
-checkValidInferredKinds orig_kvs out_of_scope extra
-  = do { let bad_pairs = [ (tv, kv)
-                         | kv <- orig_kvs
-                         , Just tv <- map (lookupVarSet out_of_scope)
-                                          (tyCoVarsOfTypeList (tyVarKind kv)) ]
-             report (tidyTyVarOcc env -> tv, tidyTyVarOcc env -> kv)
-               = addErr $
-                 text "The kind of variable" <+>
-                 quotes (ppr kv) <> text ", namely" <+>
-                 quotes (ppr (tyVarKind kv)) <> comma $$
-                 text "depends on variable" <+>
-                 quotes (ppr tv) <+> text "from an inner scope" $$
-                 text "Perhaps bind" <+> quotes (ppr kv) <+>
-                 text "sometime after binding" <+>
-                 quotes (ppr tv) $$
-                 extra
-       ; mapM_ report bad_pairs }
-
-  where
-    (env1, _) = tidyTyCoVarBndrs emptyTidyEnv orig_kvs
-    (env, _)  = tidyTyCoVarBndrs env1         (nonDetEltsUniqSet out_of_scope)
-      -- It's OK to use nonDetEltsUniqSet here because it's only used for
-      -- generating the error message
-
 {-
 ************************************************************************
 *                                                                      *
index c8105d0..3e69b71 100644 (file)
@@ -11,7 +11,8 @@
 module Coercion (
         -- * Main data type
         Coercion, CoercionN, CoercionR, CoercionP,
-        UnivCoProvenance, CoercionHole, LeftOrRight(..),
+        UnivCoProvenance, CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
+        LeftOrRight(..),
         Var, CoVar, TyCoVar,
         Role(..), ltRole,
 
index 9028460..94314d1 100644 (file)
@@ -32,7 +32,7 @@ module TyCoRep (
         -- * Coercions
         Coercion(..),
         UnivCoProvenance(..),
-        CoercionHole(..), coHoleCoVar,
+        CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
         CoercionN, CoercionR, CoercionP, KindCoercion,
 
         -- * Functions over types
@@ -811,7 +811,7 @@ isLiftedTypeKind = isTYPE is_lifted
 isUnliftedTypeKind :: Kind -> Bool
 isUnliftedTypeKind = isTYPE is_unlifted
   where
-    is_unlifted (TyConApp rr _args) = not (rr `hasKey` liftedRepDataConKey)
+    is_unlifted (TyConApp rr _args) = elem (getUnique rr) unliftedRepDataConKeys
     is_unlifted _                   = False
 
 -- | Is this the type 'RuntimeRep'?
@@ -1302,6 +1302,9 @@ data CoercionHole
 coHoleCoVar :: CoercionHole -> CoVar
 coHoleCoVar = ch_co_var
 
+setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
+setCoHoleCoVar h cv = h { ch_co_var = cv }
+
 instance Data.Data CoercionHole where
   -- don't traverse?
   toConstr _   = abstractConstr "CoercionHole"
@@ -2241,6 +2244,7 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) =
 -- Note [The substitution invariant].
 checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a
 checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
+-- TODO (RAE): Change back to ASSERT
   = WARN( not (isValidTCvSubst subst),
              text "in_scope" <+> ppr in_scope $$
              text "tenv" <+> ppr tenv $$
index 8dcbd10..3753e70 100644 (file)
@@ -1,5 +1,7 @@
 module TyCoRep where
 
+import GhcPrelude
+
 import Outputable ( SDoc )
 import Data.Data  ( Data )
 
@@ -18,6 +20,7 @@ type ThetaType = [PredType]
 pprKind :: Kind -> SDoc
 pprType :: Type -> SDoc
 
+isRuntimeRepTy :: Type -> Bool
+
 instance Data Type
   -- To support Data instances in CoAxiom
-
index f30c59e..072e397 100644 (file)
@@ -19,7 +19,7 @@ module TyCon(
         TyConBinder, TyConBndrVis(..),
         mkNamedTyConBinder, mkNamedTyConBinders,
         mkAnonTyConBinder, mkAnonTyConBinders,
-        tyConBinderArgFlag, isNamedTyConBinder,
+        tyConBinderArgFlag, tyConBndrVisArgFlag, isNamedTyConBinder,
         isVisibleTyConBinder, isInvisibleTyConBinder,
 
         -- ** Field labels
@@ -96,7 +96,7 @@ module TyCon(
         algTcFields,
         tyConRuntimeRepInfo,
         tyConBinders, tyConResKind, tyConTyVarBinders,
-        tcTyConScopedTyVars,
+        tcTyConScopedTyVars, tcTyConUserTyVars,
         mkTyConTagMap,
 
         -- ** Manipulating TyCons
@@ -396,6 +396,10 @@ data TyConBndrVis
   = NamedTCB ArgFlag
   | AnonTCB
 
+instance Outputable TyConBndrVis where
+  ppr (NamedTCB flag) = text "NamedTCB" <+> ppr flag
+  ppr AnonTCB         = text "AnonTCB"
+
 mkAnonTyConBinder :: TyVar -> TyConBinder
 mkAnonTyConBinder tv = TvBndr tv AnonTCB
 
@@ -411,8 +415,11 @@ mkNamedTyConBinders :: ArgFlag -> [TyVar] -> [TyConBinder]
 mkNamedTyConBinders vis tvs = map (mkNamedTyConBinder vis) tvs
 
 tyConBinderArgFlag :: TyConBinder -> ArgFlag
-tyConBinderArgFlag (TvBndr _ (NamedTCB vis)) = vis
-tyConBinderArgFlag (TvBndr _ AnonTCB)        = Required
+tyConBinderArgFlag (TvBndr _ vis) = tyConBndrVisArgFlag vis
+
+tyConBndrVisArgFlag :: TyConBndrVis -> ArgFlag
+tyConBndrVisArgFlag (NamedTCB vis) = vis
+tyConBndrVisArgFlag AnonTCB        = Required
 
 isNamedTyConBinder :: TyConBinder -> Bool
 -- Identifies kind variables
@@ -819,6 +826,8 @@ data TyCon
         tcTyConScopedTyVars :: [(Name,TyVar)],
                            -- ^ Scoped tyvars over the tycon's body
                            -- See Note [How TcTyCons work] in TcTyClsDecls
+                           -- Order does *not* matter.
+        tcTyConUserTyVars :: SDoc, -- ^ Original, user-written tycon tyvars
 
         tcTyConFlavour :: TyConFlavour
                            -- ^ What sort of 'TyCon' this represents.
@@ -1159,7 +1168,6 @@ so the coercion tycon CoT must have
         kind:    T ~ []
  and    arity:   0
 
-
 ************************************************************************
 *                                                                      *
                  TyConRepName
@@ -1524,13 +1532,14 @@ mkSumTyCon name binders res_kind arity tyvars cons parent
 -- See also Note [Kind checking recursive type and class declarations]
 -- in TcTyClsDecls.
 mkTcTyCon :: Name
+          -> SDoc                -- ^ user-written tycon tyvars
           -> [TyConBinder]
           -> Kind                -- ^ /result/ kind only
-          -> [(Name,TyVar)]      -- ^ Scoped type variables;
+          -> [(Name,TcTyVar)]    -- ^ Scoped type variables;
                                  -- see Note [How TcTyCons work] in TcTyClsDecls
           -> TyConFlavour        -- ^ What sort of 'TyCon' this represents
           -> TyCon
-mkTcTyCon name binders res_kind scoped_tvs flav
+mkTcTyCon name tyvars binders res_kind scoped_tvs flav
   = TcTyCon { tyConUnique  = getUnique name
             , tyConName    = name
             , tyConTyVars  = binderVars binders
@@ -1539,7 +1548,8 @@ mkTcTyCon name binders res_kind scoped_tvs flav
             , tyConKind    = mkTyConKind binders res_kind
             , tyConArity   = length binders
             , tcTyConScopedTyVars = scoped_tvs
-            , tcTyConFlavour      = flav }
+            , tcTyConFlavour      = flav
+            , tcTyConUserTyVars   = tyvars }
 
 -- | Create an unlifted primitive 'TyCon', such as @Int#@.
 mkPrimTyCon :: Name -> [TyConBinder]
@@ -1656,7 +1666,7 @@ isAbstractTyCon _ = False
 -- Used when recovering from errors
 makeRecoveryTyCon :: TyCon -> TyCon
 makeRecoveryTyCon tc
-  = mkTcTyCon (tyConName tc)
+  = mkTcTyCon (tyConName tc) empty
               (tyConBinders tc) (tyConResKind tc)
               [{- no scoped vars -}]
               (tyConFlavour tc)
@@ -2383,8 +2393,8 @@ data TyConFlavour
   | DataTypeFlavour
   | NewtypeFlavour
   | AbstractTypeFlavour
-  | DataFamilyFlavour
-  | OpenTypeFamilyFlavour
+  | DataFamilyFlavour Bool     -- True <=> associated
+  | OpenTypeFamilyFlavour Bool -- True <=> associated
   | ClosedTypeFamilyFlavour
   | TypeSynonymFlavour
   | BuiltInTypeFlavour -- ^ e.g., the @(->)@ 'TyCon'.
@@ -2401,8 +2411,10 @@ instance Outputable TyConFlavour where
       go DataTypeFlavour         = "data type"
       go NewtypeFlavour          = "newtype"
       go AbstractTypeFlavour     = "abstract type"
-      go DataFamilyFlavour       = "data family"
-      go OpenTypeFamilyFlavour   = "type family"
+      go (DataFamilyFlavour True)      = "associated data family"
+      go (DataFamilyFlavour False)     = "data family"
+      go (OpenTypeFamilyFlavour True)  = "associated type family"
+      go (OpenTypeFamilyFlavour False) = "type family"
       go ClosedTypeFamilyFlavour = "type family"
       go TypeSynonymFlavour      = "type synonym"
       go BuiltInTypeFlavour      = "built-in type"
@@ -2418,10 +2430,10 @@ tyConFlavour (AlgTyCon { algTcParent = parent, algTcRhs = rhs })
                   DataTyCon {}       -> DataTypeFlavour
                   NewTyCon {}        -> NewtypeFlavour
                   AbstractTyCon {}   -> AbstractTypeFlavour
-tyConFlavour (FamilyTyCon { famTcFlav = flav })
+tyConFlavour (FamilyTyCon { famTcFlav = flav, famTcParent = parent })
   = case flav of
-      DataFamilyTyCon{}            -> DataFamilyFlavour
-      OpenSynFamilyTyCon           -> OpenTypeFamilyFlavour
+      DataFamilyTyCon{}            -> DataFamilyFlavour (isJust parent)
+      OpenSynFamilyTyCon           -> OpenTypeFamilyFlavour (isJust parent)
       ClosedSynFamilyTyCon{}       -> ClosedTypeFamilyFlavour
       AbstractClosedSynFamilyTyCon -> ClosedTypeFamilyFlavour
       BuiltInSynFamTyCon{}         -> ClosedTypeFamilyFlavour
@@ -2436,20 +2448,20 @@ tcFlavourCanBeUnsaturated :: TyConFlavour -> Bool
 tcFlavourCanBeUnsaturated ClassFlavour            = True
 tcFlavourCanBeUnsaturated DataTypeFlavour         = True
 tcFlavourCanBeUnsaturated NewtypeFlavour          = True
-tcFlavourCanBeUnsaturated DataFamilyFlavour       = True
+tcFlavourCanBeUnsaturated DataFamilyFlavour{}     = True
 tcFlavourCanBeUnsaturated TupleFlavour{}          = True
 tcFlavourCanBeUnsaturated SumFlavour              = True
 tcFlavourCanBeUnsaturated AbstractTypeFlavour     = True
 tcFlavourCanBeUnsaturated BuiltInTypeFlavour      = True
 tcFlavourCanBeUnsaturated PromotedDataConFlavour  = True
 tcFlavourCanBeUnsaturated TypeSynonymFlavour      = False
-tcFlavourCanBeUnsaturated OpenTypeFamilyFlavour   = False
+tcFlavourCanBeUnsaturated OpenTypeFamilyFlavour{} = False
 tcFlavourCanBeUnsaturated ClosedTypeFamilyFlavour = False
 
 -- | Is this flavour of 'TyCon' an open type family or a data family?
 tcFlavourIsOpen :: TyConFlavour -> Bool
-tcFlavourIsOpen DataFamilyFlavour       = True
-tcFlavourIsOpen OpenTypeFamilyFlavour   = True
+tcFlavourIsOpen DataFamilyFlavour{}     = True
+tcFlavourIsOpen OpenTypeFamilyFlavour{} = True
 tcFlavourIsOpen ClosedTypeFamilyFlavour = False
 tcFlavourIsOpen ClassFlavour            = False
 tcFlavourIsOpen DataTypeFlavour         = False
index c274116..1607d95 100644 (file)
@@ -189,6 +189,7 @@ module Type (
         pprKind, pprParendKind, pprSourceTyCon,
         TyPrec(..), maybeParen,
         pprTyVar, pprTyVars,
+        pprWithTYPE,
 
         -- * Tidying type related things up for printing
         tidyType,      tidyTypes,
@@ -234,6 +235,7 @@ import Util
 import Outputable
 import FastString
 import Pair
+import DynFlags  ( gopt_set, GeneralFlag(Opt_PrintExplicitRuntimeReps) )
 import ListSetOps
 import Digraph
 import Unique ( nonDetCmpUnique )
@@ -2458,3 +2460,20 @@ setJoinResTy :: Int  -- Number of binders to skip
 -- INVARIANT: Same as for modifyJoinResTy
 setJoinResTy ar new_res_ty ty
   = modifyJoinResTy ar (const new_res_ty) ty
+
+{-
+%************************************************************************
+%*                                                                      *
+         Pretty-printing
+%*                                                                      *
+%************************************************************************
+
+Most pretty-printing is either in TyCoRep or IfaceType.
+
+-}
+
+-- | This variant preserves any use of TYPE in a type, effectively
+-- locally setting -fprint-explicit-runtime-reps.
+pprWithTYPE :: Type -> SDoc
+pprWithTYPE ty = updSDocDynFlags (flip gopt_set Opt_PrintExplicitRuntimeReps) $
+                 ppr ty
index af5caad..727d1c5 100644 (file)
@@ -18,7 +18,7 @@ module Bag (
         concatBag, catBagMaybes, foldBag, foldrBag, foldlBag,
         isEmptyBag, isSingletonBag, consBag, snocBag, anyBag, allBag,
         listToBag, bagToList, mapAccumBagL,
-        concatMapBag, mapMaybeBag,
+        concatMapBag, concatMapBagPair, mapMaybeBag,
         foldrBagM, foldlBagM, mapBagM, mapBagM_,
         flatMapBagM, flatMapBagPairM,
         mapAndUnzipBagM, mapAccumBagLM,
@@ -232,6 +232,19 @@ concatMapBag f (UnitBag x)     = f x
 concatMapBag f (TwoBags b1 b2) = unionBags (concatMapBag f b1) (concatMapBag f b2)
 concatMapBag f (ListBag xs)    = foldr (unionBags . f) emptyBag xs
 
+concatMapBagPair :: (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c)
+concatMapBagPair _ EmptyBag        = (EmptyBag, EmptyBag)
+concatMapBagPair f (UnitBag x)     = f x
+concatMapBagPair f (TwoBags b1 b2) = (unionBags r1 r2, unionBags s1 s2)
+  where
+    (r1, s1) = concatMapBagPair f b1
+    (r2, s2) = concatMapBagPair f b2
+concatMapBagPair f (ListBag xs)    = foldr go (emptyBag, emptyBag) xs
+  where
+    go a (s1, s2) = (unionBags r1 s1, unionBags r2 s2)
+      where
+        (r1, r2) = f a
+
 mapMaybeBag :: (a -> Maybe b) -> Bag a -> Bag b
 mapMaybeBag _ EmptyBag        = EmptyBag
 mapMaybeBag f (UnitBag x)     = case f x of
index 2b03555..e435734 100644 (file)
@@ -69,6 +69,7 @@ module Outputable (
         alwaysQualifyPackages, neverQualifyPackages,
         QualifyName(..), queryQual,
         sdocWithDynFlags, sdocWithPlatform,
+        updSDocDynFlags,
         getPprStyle, withPprStyle, withPprStyleDoc, setStyleColoured,
         pprDeeper, pprDeeperList, pprSetDepth,
         codeStyle, userStyle, debugStyle, dumpStyle, asmStyle,
@@ -387,6 +388,10 @@ sdocWithDynFlags f = SDoc $ \ctx -> runSDoc (f (sdocDynFlags ctx)) ctx
 sdocWithPlatform :: (Platform -> SDoc) -> SDoc
 sdocWithPlatform f = sdocWithDynFlags (f . targetPlatform)
 
+updSDocDynFlags :: (DynFlags -> DynFlags) -> SDoc -> SDoc
+updSDocDynFlags upd doc
+  = SDoc $ \ctx -> runSDoc doc (ctx { sdocDynFlags = upd (sdocDynFlags ctx) })
+
 qualName :: PprStyle -> QueryQualifyName
 qualName (PprUser q _ _) mod occ = queryQualifyName q mod occ
 qualName (PprDump q)     mod occ = queryQualifyName q mod occ
index 0cb8a6a..6442818 100644 (file)
@@ -8641,7 +8641,8 @@ Principles of kind inference
 
 Generally speaking, when :extension:`PolyKinds` is on, GHC tries to infer the
 most general kind for a declaration.
-In this case the definition has a right-hand side to inform kind
+In many cases (for example, in a datatype declaration)
+the definition has a right-hand side to inform kind
 inference. But that is not always the case. Consider ::
 
     type family F a
@@ -9076,6 +9077,30 @@ system does not have principal types) or merely practical (inferring this
 dependency is hard, given GHC's implementation). So, GHC takes the easy
 way out and requires a little help from the user.
 
+Inferring dependency in user-written ``forall``\s
+-------------------------------------------------
+
+A programmer may use ``forall`` in a type to introduce new quantified type
+variables. These variables may depend on each other, even in the same
+``forall``. However, GHC requires that the dependency be inferrable from
+the body of the ``forall``. Here are some examples::
+
+  data Proxy k (a :: k) = MkProxy   -- just to use below
+  
+  f :: forall k a. Proxy k a        -- This is just fine. We see that (a :: k).
+  f = undefined
+
+  g :: Proxy k a -> ()              -- This is to use below.
+  g = undefined
+
+  data Sing a
+  h :: forall k a. Sing k -> Sing a -> ()  -- No obvious relationship between k and a
+  h _ _ = g (MkProxy :: Proxy k a)  -- This fails. We didn't know that a should have kind k.
+
+Note that in the last example, it's impossible to learn that ``a`` depends on ``k`` in the
+body of the ``forall`` (that is, the ``Sing k -> Sing a -> ()``). And so GHC rejects
+the program.
+
 Kind defaulting without :extension:`PolyKinds`
 -----------------------------------------------
 
index c1cbb97..c368313 100644 (file)
@@ -8,7 +8,9 @@ T13233.hs:14:11: error:
 
 T13233.hs:22:16: error:
     Cannot use primitive with levity-polymorphic arguments:
-      GHC.Prim.(#,#) :: forall (a :: TYPE rep1) (b :: TYPE rep2).
+      GHC.Prim.(#,#) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep) (a :: TYPE
+                                                                                 rep1) (b :: TYPE
+                                                                                               rep2).
                         a -> b -> (# a, b #)
     Levity-polymorphic arguments:
       a :: TYPE rep1
diff --git a/testsuite/tests/dependent/should_compile/InferDependency.hs b/testsuite/tests/dependent/should_compile/InferDependency.hs
new file mode 100644 (file)
index 0000000..47957d4
--- /dev/null
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeInType #-}
+
+module InferDependency where
+
+data Proxy k (a :: k)
+data Proxy2 k a = P (Proxy k a)
index 1cbdbaf..2292def 100644 (file)
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll #-}
+{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll, RankNTypes #-}
 
 module T11635 where
 
diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs
new file mode 100644 (file)
index 0000000..e1a6255
--- /dev/null
@@ -0,0 +1,82 @@
+{-# LANGUAGE TypeFamilies, TypeInType, ExplicitForAll, GADTs,
+             UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+
+module T14066a where
+
+import Data.Proxy
+import Data.Kind
+import Data.Type.Bool
+
+
+type family Bar x y where
+  Bar (x :: a) (y :: b) = Int
+  Bar (x :: c) (y :: d) = Bool   -- a,b,c,d should be SigTvs and unify appropriately
+
+
+  -- the two k's, even though they have different scopes, should unify in the
+  -- kind-check and then work in the type-check because Prox3 has been generalized
+
+data Prox3 a where
+  MkProx3a :: Prox3 (a :: k1)
+  MkProx3b :: Prox3 (a :: k2)
+
+  -- This probably should be rejected, as it's polymorphic recursion without a CUSK.
+  -- But GHC accepts it because the polymorphic occurrence is at a type variable.
+data T0 a = forall k (b :: k). MkT0 (T0 b) Int
+
+  -- k and j should unify
+type family G x a where
+  G Int (b :: k) = Int
+  G Bool (c :: j) = Bool
+
+-- this last example just checks that GADT pattern-matching on kinds still works.
+-- nothing new here.
+data T (a :: k) where
+  MkT :: T (a :: Type -> Type)
+
+data S (a :: Type -> Type) where
+  MkS :: S a
+
+f :: forall k (a :: k). Proxy a -> T a -> ()
+f _ MkT = let y :: S a
+              y = MkS
+          in ()
+
+-- This is questionable. Should we use the RHS to determine dependency? It works
+-- now, but if it stops working in the future, that's not a deal-breaker.
+type P k a = Proxy (a :: k)
+
+
+-- This is a challenge. It should be accepted, but only because c's kind is learned
+-- to be Proxy True, allowing b to be assigned kind `a`. If we don't know c's kind,
+-- then GHC would need to be convinced that If (c's kind) b d always has kind `a`.
+-- Naively, we don't know about c's kind early enough.
+
+data SameKind :: forall k. k -> k -> Type
+type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
+   IfK (_ :: Proxy True)  f _ = f
+   IfK (_ :: Proxy False) _ g = g
+x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True))
+x _ = Proxy
+
+
+f2 :: forall b. b -> Proxy Maybe
+f2 x = fstOf3 y :: Proxy Maybe
+  where
+    y :: (Proxy a, Proxy c, b)
+    y = (Proxy, Proxy, x)
+
+fstOf3 (x, _, _) = x
+
+f3 :: forall b. b -> Proxy Maybe
+f3 x = fst y :: Proxy Maybe
+  where
+    y :: (Proxy a, b)
+    y = (Proxy, x)
+
+-- cf. dependent/should_fail/T14066h. Here, y's type does *not* capture any variables,
+-- so it is generalized, even with MonoLocalBinds.
+f4 x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+  where
+    y :: (Proxy a, Int)
+    y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr
new file mode 100644 (file)
index 0000000..906695f
--- /dev/null
@@ -0,0 +1,5 @@
+
+T14066a.hs:13:3: warning:
+    Type family instance equation is overlapped:
+      forall c d (x :: c) (y :: d).
+        Bar x y = Bool -- Defined at T14066a.hs:13:3
index da25b22..070e120 100644 (file)
@@ -32,3 +32,5 @@ test('T13938', [extra_files(['T13938a.hs'])], run_command,
      ['$MAKE -s --no-print-directory T13938'])
 test('T14556', normal, compile, [''])
 test('T14720', normal, compile, [''])
+test('T14066a', normal, compile, [''])
+test('T14749', normal, compile, [''])
index 2fbc35a..5fa8efd 100644 (file)
@@ -1,9 +1,6 @@
 
 BadTelescope.hs:9:1: error:
-    • These kind and type variables: (a :: k)
-                                     k
-                                     (b :: k)
-                                     (c :: SameKind a b)
+    • These kind and type variables: a k (b :: k) (c :: SameKind a b)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k) (c :: SameKind a b)
     • In the data type declaration for ‘X’
index 2a9dc76..55a4849 100644 (file)
@@ -3,14 +3,11 @@ BadTelescope2.hs:10:8: error:
     • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
-    • In the type signature:
-        foo :: forall a k (b :: k). SameKind a b
+    • In the type signature: foo :: forall a k (b :: k). SameKind a b
 
-BadTelescope2.hs:13:8: error:
-    • The kind of variable ‘b’, namely ‘Proxy a’,
-      depends on variable ‘a’ from an inner scope
-      Perhaps bind ‘b’ sometime after binding ‘a’
-      NB: Implicitly-bound variables always come before other ones.
-    • In the type signature:
+BadTelescope2.hs:13:70: error:
+    • Expected kind ‘k0’, but ‘d’ has kind ‘Proxy a’
+    • In the second argument of ‘SameKind’, namely ‘d’
+      In the type signature:
         bar :: forall a (c :: Proxy b) (d :: Proxy a).
                Proxy c -> SameKind b d
index 4ea7458..1137f28 100644 (file)
@@ -1,6 +1,6 @@
 
 BadTelescope3.hs:9:1: error:
-    • These kind and type variables: (a :: k) k (b :: k)
+    • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
     • In the type synonym declaration for ‘S’
index 2394f89..f7c281e 100644 (file)
@@ -1,6 +1,6 @@
 
 BadTelescope4.hs:9:1: error:
-    • These kind and type variables: (a :: k)
+    • These kind and type variables: a
                                      (c :: Proxy b)
                                      (d :: Proxy a)
                                      (x :: SameKind b d)
@@ -11,5 +11,5 @@ BadTelescope4.hs:9:1: error:
         (c :: Proxy b)
         (d :: Proxy a)
         (x :: SameKind b d)
-      NB: Implicitly declared kind variables are put first.
+      NB: Implicitly declared variables come before others.
     • In the data type declaration for ‘Bad’
index 7fa900a..cc852ee 100644 (file)
@@ -1,8 +1,10 @@
 
-InferDependency.hs:6:1: error:
-    • Invalid declaration for ‘Proxy2’; you must explicitly
-      declare which variables are dependent on which others.
-      Inferred variable kinds:
+InferDependency.hs:6:13: error:
+    • Type constructor argument ‘k’ is used dependently.
+      Any dependent arguments must be obviously so, not inferred
+      by the type-checker.
+      Inferred argument kinds:
         k :: *
         a :: k
+      Suggestion: use ‘k’ in a kind to make the dependency clearer.
     • In the data type declaration for ‘Proxy2’
index c1c9803..bc2877c 100644 (file)
@@ -1,6 +1,5 @@
 
 T13601.hs:18:16: error:
-    • Expected kind ‘TYPE (Rep 'LiftedRep)’,
-        but ‘Logic a’ has kind ‘TYPE (Rep rep)’
+    • Expected a type, but ‘Logic a’ has kind ‘TYPE (Rep rep)’
     • In the first argument of ‘Boolean’, namely ‘(Logic a)’
       In the class declaration for ‘Eq’
index f91d7a3..065c700 100644 (file)
@@ -2,7 +2,7 @@
 [2 of 2] Compiling T13780c          ( T13780c.hs, T13780c.o )
 
 T13780c.hs:11:16: error:
-    • Expected kind ‘Sing _’, but ‘SFalse’ has kind ‘Sing 'False’
+    • Expected kind ‘Sing _1’, but ‘SFalse’ has kind ‘Sing 'False’
     • In the third argument of ‘ElimBool’, namely ‘SFalse’
       In the type family declaration for ‘ElimBool’
 
diff --git a/testsuite/tests/dependent/should_fail/T14066.hs b/testsuite/tests/dependent/should_fail/T14066.hs
new file mode 100644 (file)
index 0000000..58396df
--- /dev/null
@@ -0,0 +1,17 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE KindSignatures #-}
+
+module T14066 where
+
+import Data.Kind ( Type )
+import Data.Type.Equality
+import Data.Proxy
+import GHC.Exts
+
+data SameKind :: k -> k -> Type
+
+f (x :: Proxy a) = let g :: forall k (b :: k). SameKind a b
+                       g = undefined
+                   in ()
diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr
new file mode 100644 (file)
index 0000000..cd0142f
--- /dev/null
@@ -0,0 +1,11 @@
+
+T14066.hs:15:59: error:
+    • Expected kind ‘k0’, but ‘b’ has kind ‘k’
+    • In the second argument of ‘SameKind’, namely ‘b’
+      In the type signature: g :: forall k (b :: k). SameKind a b
+      In the expression:
+        let
+          g :: forall k (b :: k). SameKind a b
+          g = undefined
+        in ()
+    • Relevant bindings include x :: Proxy a (bound at T14066.hs:15:4)
diff --git a/testsuite/tests/dependent/should_fail/T14066c.hs b/testsuite/tests/dependent/should_fail/T14066c.hs
new file mode 100644 (file)
index 0000000..b4597d2
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, TypeInType, UndecidableInstances #-}
+
+module T14066c where
+
+type family H a b where
+  H a b = H b a
+
+type X = H True Nothing  -- this should fail to kind-check.
+                         -- if it's accepted, then we've inferred polymorphic recursion for H
diff --git a/testsuite/tests/dependent/should_fail/T14066c.stderr b/testsuite/tests/dependent/should_fail/T14066c.stderr
new file mode 100644 (file)
index 0000000..dc5ba30
--- /dev/null
@@ -0,0 +1,6 @@
+
+T14066c.hs:8:17: error:
+    • Expected kind ‘Bool’, but ‘Nothing’ has kind ‘Maybe a0’
+    • In the second argument of ‘H’, namely ‘Nothing’
+      In the type ‘H True Nothing’
+      In the type declaration for ‘X’
diff --git a/testsuite/tests/dependent/should_fail/T14066d.hs b/testsuite/tests/dependent/should_fail/T14066d.hs
new file mode 100644 (file)
index 0000000..ea47644
--- /dev/null
@@ -0,0 +1,17 @@
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeInType #-}
+
+module T14066d where
+
+import Data.Proxy
+
+g :: (forall c b (a :: c). (Proxy a, Proxy c, b)) -> ()
+g _ = ()
+
+f :: forall b. b -> (Proxy Maybe, ())
+f x = (fstOf3 y :: Proxy Maybe, g y)
+  where
+    y :: (Proxy a, Proxy c, b)  -- this should NOT generalize over b
+                                -- meaning the call to g is ill-typed
+    y = (Proxy, Proxy, x)
+
+fstOf3 (x, _, _) = x
diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr
new file mode 100644 (file)
index 0000000..3a8b90e
--- /dev/null
@@ -0,0 +1,21 @@
+
+T14066d.hs:11:35: error:
+    • Couldn't match type ‘b’ with ‘b1’
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall b. b -> (Proxy Maybe, ())
+        at T14066d.hs:10:1-37
+      ‘b1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall c b1 (a :: c). (Proxy a, Proxy c, b1)
+        at T14066d.hs:11:33-35
+      Expected type: (Proxy a, Proxy c, b1)
+        Actual type: (Proxy a, Proxy c, b)
+    • In the first argument of ‘g’, namely ‘y’
+      In the expression: g y
+      In the expression: (fstOf3 y :: Proxy Maybe, g y)
+    • Relevant bindings include
+        y :: forall k1 k2 (a :: k2) (c :: k1). (Proxy a, Proxy c, b)
+          (bound at T14066d.hs:15:5)
+        x :: b (bound at T14066d.hs:11:3)
+        f :: b -> (Proxy Maybe, ()) (bound at T14066d.hs:11:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.hs b/testsuite/tests/dependent/should_fail/T14066e.hs
new file mode 100644 (file)
index 0000000..9b799e5
--- /dev/null
@@ -0,0 +1,13 @@
+{-# LANGUAGE MonoLocalBinds, TypeInType, ScopedTypeVariables #-}
+
+module T14066e where
+
+import Data.Proxy
+
+-- this should fail because the dependency between b and c can't be
+-- determined in the type signature
+h :: forall a. a -> ()
+h x = ()
+  where
+    j :: forall c b. Proxy a -> Proxy b -> Proxy c -> Proxy b
+    j _ (p1 :: Proxy b') (p2 :: Proxy c') = (p1 :: Proxy (b' :: c'))
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
new file mode 100644 (file)
index 0000000..504ca5a
--- /dev/null
@@ -0,0 +1,11 @@
+
+T14066e.hs:13:59: error:
+    • Expected kind ‘c’, but ‘b'’ has kind ‘k0’
+    • In the first argument of ‘Proxy’, namely ‘(b' :: c')’
+      In an expression type signature: Proxy (b' :: c')
+      In the expression: (p1 :: Proxy (b' :: c'))
+    • Relevant bindings include
+        p2 :: Proxy c (bound at T14066e.hs:13:27)
+        p1 :: Proxy b (bound at T14066e.hs:13:10)
+        j :: Proxy a -> Proxy b -> Proxy c -> Proxy b
+          (bound at T14066e.hs:13:5)
diff --git a/testsuite/tests/dependent/should_fail/T14066f.hs b/testsuite/tests/dependent/should_fail/T14066f.hs
new file mode 100644 (file)
index 0000000..ccb7cea
--- /dev/null
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeInType #-}
+
+module T14066f where
+
+import Data.Proxy
+
+-- a can't come before k.
+type P a k = Proxy (a :: k)
diff --git a/testsuite/tests/dependent/should_fail/T14066f.stderr b/testsuite/tests/dependent/should_fail/T14066f.stderr
new file mode 100644 (file)
index 0000000..44c4ed2
--- /dev/null
@@ -0,0 +1,6 @@
+
+T14066f.hs:8:1: error:
+    • These kind and type variables: a k
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k)
+    • In the type synonym declaration for ‘P’
diff --git a/testsuite/tests/dependent/should_fail/T14066g.hs b/testsuite/tests/dependent/should_fail/T14066g.hs
new file mode 100644 (file)
index 0000000..df0e03b
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeInType #-}
+
+module T14066g where
+
+import Data.Kind
+
+data SameKind :: k -> k -> Type
+
+data Q a (b :: a) (d :: SameKind c b)
diff --git a/testsuite/tests/dependent/should_fail/T14066g.stderr b/testsuite/tests/dependent/should_fail/T14066g.stderr
new file mode 100644 (file)
index 0000000..22ca786
--- /dev/null
@@ -0,0 +1,7 @@
+
+T14066g.hs:9:1: error:
+    • These kind and type variables: a (b :: a) (d :: SameKind c b)
+      are out of dependency order. Perhaps try this ordering:
+        a (c :: a) (b :: a) (d :: SameKind c b)
+      NB: Implicitly declared variables come before others.
+    • In the data type declaration for ‘Q’
diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_fail/T14066h.hs
new file mode 100644 (file)
index 0000000..7e7ecd3
--- /dev/null
@@ -0,0 +1,11 @@
+{-# LANGUAGE ScopedTypeVariables, TypeInType, MonoLocalBinds #-}
+
+module T14066h where
+
+import Data.Proxy
+
+f :: forall b. b -> (Proxy Int, Proxy Maybe)
+f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+  where
+    y :: (Proxy a, b)  -- MonoLocalBinds means this won't generalize over the kind of a
+    y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/T14066h.stderr b/testsuite/tests/dependent/should_fail/T14066h.stderr
new file mode 100644 (file)
index 0000000..bfd3369
--- /dev/null
@@ -0,0 +1,16 @@
+
+T14066h.hs:8:28: error:
+    • Couldn't match kind ‘* -> *’ with ‘*’
+      When matching types
+        a0 :: *
+        Maybe :: * -> *
+      Expected type: Proxy Maybe
+        Actual type: Proxy a0
+    • In the expression: fst y :: Proxy Maybe
+      In the expression: (fst y :: Proxy Int, fst y :: Proxy Maybe)
+      In an equation for ‘f’:
+          f x
+            = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+            where
+                y :: (Proxy a, b)
+                y = (Proxy, x)
index bbec037..02b7737 100644 (file)
@@ -1,4 +1,5 @@
 {-# LANGUAGE RankNTypes, PolyKinds, TypeInType #-}
+-- NB: -fprint-explicit-runtime-reps enabled in all.T
 
 module TypeSkolEscape where
 
index 8853985..e2ef266 100644 (file)
@@ -1,7 +1,5 @@
 
-TypeSkolEscape.hs:8:1: error:
-    • Quantified type's kind mentions quantified type variable
-      (skolem escape)
-           type: forall (a1 :: TYPE v1). a1
-        of kind: TYPE v
-    • In the type synonym declaration for ‘Bad’
+TypeSkolEscape.hs:9:52: error:
+    • Expected kind ‘k0’, but ‘a’ has kind ‘TYPE v’
+    • In the type ‘forall (v :: RuntimeRep) (a :: TYPE v). a’
+      In the type declaration for ‘Bad’
index e28b2df..7273445 100644 (file)
@@ -1,6 +1,6 @@
 test('DepFail1', normal, compile_fail, [''])
 test('RAE_T32a', normal, compile_fail, [''])
-test('TypeSkolEscape', normal, compile_fail, [''])
+test('TypeSkolEscape', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
 test('BadTelescope3', normal, compile_fail, [''])
@@ -10,7 +10,6 @@ test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
 test('T11334b', normal, compile_fail, [''])
-test('InferDependency', normal, compile_fail, [''])
 test('KindLevelsB', normal, compile_fail, [''])
 test('T11473', normal, compile_fail, [''])
 test('T11471', normal, compile_fail, [''])
@@ -21,3 +20,11 @@ test('T13601', normal, compile_fail, [''])
 test('T13780a', normal, compile_fail, [''])
 test('T13780c', [extra_files(['T13780b.hs'])],
                 multimod_compile_fail, ['T13780c', ''])
+test('T14066', normal, compile_fail, [''])
+test('T14066c', normal, compile_fail, [''])
+test('T14066d', normal, compile_fail, [''])
+test('T14066e', normal, compile_fail, [''])
+test('T14066f', normal, compile_fail, [''])
+test('T14066g', normal, compile_fail, [''])
+test('T14066h', normal, compile_fail, [''])
+test('InferDependency', normal, compile_fail, [''])
index e013383..a3034ad 100644 (file)
@@ -14,5 +14,10 @@ instance Cat * (->) where
   catId   = id
   catComp = (.)
 
-newtype Fun1 a b = Fun1 (a -> b) deriving (Cat k)
 newtype Fun2 a b = Fun2 (a -> b) deriving (Cat *)
+
+-- The ticket says this should work:
+--   newtype Fun1 a b = Fun1 (a -> b) deriving (Cat k)
+-- But that requires that the kind of (Cat k) to depend on k, where k is local
+-- This is all due for an update, anyway, when #14331 is done, and it's unclear
+-- what the correct behavior here is, anyway. (Richard thinks: reject!)
index 6585f66..3f54093 100644 (file)
@@ -11,8 +11,6 @@ T12468.hs:9:7: error:
         minBound :: forall a. Bounded a => a
           (imported from ‘Prelude’ at T12468.hs:3:8-13
            (and originally defined in ‘GHC.Enum’))
-        undefined :: forall (a :: TYPE r).
-                     GHC.Stack.Types.HasCallStack =>
-                     a
+        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
           (imported from ‘Prelude’ at T12468.hs:3:8-13
            (and originally defined in ‘GHC.Err’))
index 283ccdd..d6428c5 100644 (file)
@@ -10,7 +10,5 @@
     • Relevant bindings include
         it :: f (Maybe a) (bound at <interactive>:2:1)
       Valid substitutions include
-        undefined :: forall (a :: TYPE r).
-                     GHC.Stack.Types.HasCallStack =>
-                     a
+        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
           (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
index 66ce87c..d495994 100644 (file)
@@ -8,7 +8,5 @@
       In an equation for ‘it’: it = _
     • Relevant bindings include it :: t (bound at <interactive>:1:1)
       Valid substitutions include
-        undefined :: forall (a :: TYPE r).
-                     GHC.Stack.Types.HasCallStack =>
-                     a
+        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
           (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
index 15dbdaf..4cac123 100644 (file)
@@ -18,9 +18,7 @@ Defer03.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
         minBound :: forall a. Bounded a => a
           (imported from ‘Prelude’ at Defer03.hs:1:8-11
            (and originally defined in ‘GHC.Enum’))
-        undefined :: forall (a :: TYPE r).
-                     GHC.Stack.Types.HasCallStack =>
-                     a
+        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
           (imported from ‘Prelude’ at Defer03.hs:1:8-11
            (and originally defined in ‘GHC.Err’))
 
@@ -43,9 +41,7 @@ Defer03.hs:7:5: error:
         minBound :: forall a. Bounded a => a
           (imported from ‘Prelude’ at Defer03.hs:1:8-11
            (and originally defined in ‘GHC.Enum’))
-        undefined :: forall (a :: TYPE r).
-                     GHC.Stack.Types.HasCallStack =>
-                     a
+        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
           (imported from ‘Prelude’ at Defer03.hs:1:8-11
            (and originally defined in ‘GHC.Err’))
 
@@ -68,9 +64,7 @@ Defer03.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
         minBound :: forall a. Bounded a => a
           (imported from ‘Prelude’ at Defer03.hs:1:8-11
            (and originally defined in ‘GHC.Enum’))
-        undefined :: forall (a :: TYPE r).
-                     GHC.Stack.Types.HasCallStack =>
-                     a
+        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
           (imported from ‘Prelude’ at Defer03.hs:1:8-11
            (and originally defined in ‘GHC.Err’))
 
@@ -93,9 +87,7 @@ Defer03.hs:7:5: error:
         minBound :: forall a. Bounded a => a
           (imported from ‘Prelude’ at Defer03.hs:1:8-11
            (and originally defined in ‘GHC.Enum’))
-        undefined :: forall (a :: TYPE r).
-                     GHC.Stack.Types.HasCallStack =>
-                     a
+        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
           (imported from ‘Prelude’ at Defer03.hs:1:8-11
            (and originally defined in ‘GHC.Err’))
 
@@ -118,8 +110,6 @@ Defer03.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
         minBound :: forall a. Bounded a => a
           (imported from ‘Prelude’ at Defer03.hs:1:8-11
            (and originally defined in ‘GHC.Enum’))
-        undefined :: forall (a :: TYPE r).
-                     GHC.Stack.Types.HasCallStack =>
-                     a
+        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
           (imported from ‘Prelude’ at Defer03.hs:1:8-11
            (and originally defined in ‘GHC.Err’))
index 2816e2f..d0c199b 100644 (file)
@@ -1,6 +1,6 @@
 
 T7938.hs:12:16: error:
-    • Expected a type, but ‘(KP :: KProxy k2)’ has kind ‘KProxy k2
+    • Expected a type, but ‘(KP :: KProxy k2)’ has kind ‘KProxy k4
     • In the type ‘(KP :: KProxy k2)’
       In the type instance declaration for ‘Bar’
       In the instance declaration for ‘Foo (a :: k1) (b :: k2)’
index 8a0fb29..b23febd 100644 (file)
@@ -1,3 +1,2 @@
     • Could not deduce (C x0 (F x0))
       • Could not deduce (C x0 (F x0))
-        \    \\226\\128\\162 Could not deduce (C x0 (F x0))\n\
index 4d592ce..52d0ae3 100644 (file)
@@ -11,8 +11,6 @@ mod71.hs:4:9: error:
         x :: t1 -> t -> t2 (bound at mod71.hs:4:3)
         f :: (t1 -> t -> t2) -> t2 (bound at mod71.hs:4:1)
       Valid substitutions include
-        undefined :: forall (a :: TYPE r).
-                     GHC.Stack.Types.HasCallStack =>
-                     a
+        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
           (imported from ‘Prelude’ at mod71.hs:3:8
            (and originally defined in ‘GHC.Err’))
index df83c1a..20c44ec 100644 (file)
@@ -8,8 +8,6 @@ T12531.hs:6:11: warning: [-Wtyped-holes (in -Wdefault)]
         x :: Int# (bound at T12531.hs:6:3)
         f :: Int# -> Int (bound at T12531.hs:6:1)
       Valid substitutions include
-        undefined :: forall (a :: TYPE r).
-                     GHC.Stack.Types.HasCallStack =>
-                     a
+        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
           (imported from ‘Prelude’ at T12531.hs:3:8-13
            (and originally defined in ‘GHC.Err’))
index c17759a..0b9bcb8 100644 (file)
@@ -8,7 +8,8 @@ T10615.hs:4:7: error:
 T10615.hs:5:6: error:
     • Couldn't match type ‘f’ with ‘b1 -> a1’
       ‘f’ is a rigid type variable bound by
-        the inferred type of f1 :: a1 -> f at T10615.hs:5:1-10
+        the inferred type of f1 :: a1 -> f
+        at T10615.hs:5:1-10
       Expected type: a1 -> f
         Actual type: a1 -> b1 -> a1
     • In the expression: const
@@ -24,7 +25,8 @@ T10615.hs:7:7: error:
 T10615.hs:8:6: error:
     • Couldn't match type ‘_f’ with ‘b0 -> a0’
       ‘_f’ is a rigid type variable bound by
-        the inferred type of f2 :: a0 -> _f at T10615.hs:8:1-10
+        the inferred type of f2 :: a0 -> _f
+        at T10615.hs:8:1-10
       Expected type: a0 -> _f
         Actual type: a0 -> b0 -> a0
     • In the expression: const
index f0e2784..2810462 100644 (file)
@@ -1,7 +1,17 @@
 
+T11976.hs:7:7: error:
+    • Cannot instantiate unification variable ‘a0’
+      with a type involving foralls: Lens w3 w4 w5
+        GHC doesn't yet support impredicative polymorphism
+    • In the expression: undefined :: Lens _ _ _
+      In an equation for ‘foo’: foo = undefined :: Lens _ _ _
+    • Relevant bindings include
+        foo :: Lens w w1 w2 (bound at T11976.hs:7:1)
+
 T11976.hs:7:20: error:
-    • Illegal polymorphic type: Lens w0 w1
-      GHC doesn't yet support impredicative polymorphism
-     In an expression type signature: Lens _ _ _
+    • Expected kind ‘k0 -> *’, but ‘Lens _ _’ has kind ‘*’
+    • In the type ‘Lens _ _ _’
+      In an expression type signature: Lens _ _ _
       In the expression: undefined :: Lens _ _ _
-      In an equation for ‘foo’: foo = undefined :: Lens _ _ _
+    • Relevant bindings include
+        foo :: Lens w w1 w2 (bound at T11976.hs:7:1)
index ac9ad8a..cc0d0ca 100644 (file)
@@ -1,9 +1,30 @@
 
 T14040a.hs:21:18: error:
-    • The kind of variable ‘wl1’, namely ‘WeirdList a1’,
-      depends on variable ‘a1’ from an inner scope
-      Perhaps bind ‘wl1’ sometime after binding ‘a1’
-    • In the type signature:
+    • Couldn't match type ‘k0’ with ‘a’
+        because type variable ‘a’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        the type signature for:
+          elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x.
+                                                                x -> WeirdList x -> *).
+                           Sing wl
+                           -> (forall y. p k0 w0 'WeirdNil)
+                           -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
+                               Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs))
+                           -> p k3 w3 wl
+        at T14040a.hs:(21,18)-(28,23)
+      Expected type: Sing wl
+                     -> (forall y. p k1 w0 'WeirdNil)
+                     -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
+                         Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs))
+                     -> p k3 w3 wl
+        Actual type: Sing wl
+                     -> (forall y. p k1 w0 'WeirdNil)
+                     -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
+                         Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs))
+                     -> p k3 w3 wl
+    • In the ambiguity check for ‘elimWeirdList’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x -> Type).
@@ -15,13 +36,11 @@ T14040a.hs:21:18: error:
 
 T14040a.hs:34:8: error:
     • Cannot apply expression of type ‘Sing wl
-                                       -> (forall y. p x0 w0 'WeirdNil)
+                                       -> (forall y. p k0 w0 'WeirdNil)
                                        -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
                                            Sing x
-                                           -> Sing xs
-                                           -> p (WeirdList z1) w1 xs
-                                           -> p z1 w2 ('WeirdCons x xs))
-                                       -> p a1 w3 wl’
+                                           -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs))
+                                       -> p k3 w3 wl’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
index db378fe..941adf1 100644 (file)
@@ -10,7 +10,7 @@ test('haddock.base',
             # 2017-02-19                        24286343184 (x64/Windows) - Generalize kind of (->)
             # 2017-12-24                        18733710728 (x64/Windows) - Unknown
 
-          ,(wordsize(64), 19694554424, 5)
+          ,(wordsize(64), 20980255200, 5)
             # 2012-08-14:  5920822352 (amd64/Linux)
             # 2012-09-20:  5829972376 (amd64/Linux)
             # 2012-10-08:  5902601224 (amd64/Linux)
@@ -44,6 +44,9 @@ test('haddock.base',
             # 2017-06-06: 25173968808 (x86_64/Linux) - Don't pass on -dcore-lint in Haddock.mk
             # 2017-07-12: 23677299848 (x86_64/Linux) - Use getNameToInstancesIndex
             # 2017-08-22: 19694554424 (x86_64/Linux) - Various Haddock optimizations
+           # 2018-03-31: 20980255200 (x86_64/Linux) - Track type variable scope more carefully
+               # previous to this last commit, the allocations were right below the top
+               # of the range. This commit adds only ~1.5% allocations.
 
           ,(platform('i386-unknown-mingw32'), 2885173512, 5)
             # 2013-02-10:                     3358693084 (x86/Windows)
diff --git a/testsuite/tests/polykinds/SigTvKinds3.hs b/testsuite/tests/polykinds/SigTvKinds3.hs
new file mode 100644 (file)
index 0000000..b27be2e
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs, ExplicitForAll, TypeInType #-}
+
+module SigTvKinds3 where
+
+import Data.Kind
+
+data SameKind :: k -> k -> Type
+data Bad a where
+  MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)
diff --git a/testsuite/tests/polykinds/SigTvKinds3.stderr b/testsuite/tests/polykinds/SigTvKinds3.stderr
new file mode 100644 (file)
index 0000000..b498c03
--- /dev/null
@@ -0,0 +1,6 @@
+
+SigTvKinds3.hs:9:62: error:
+    • Expected kind ‘k1’, but ‘b’ has kind ‘k2’
+    • In the second argument of ‘SameKind’, namely ‘b’
+      In the first argument of ‘Bad’, namely ‘(SameKind a b)’
+      In the type ‘Bad (SameKind a b)’
index 2cb4e61..ea687c3 100644 (file)
@@ -1,7 +1,6 @@
 
-T11142.hs:9:8: error:
-    • The kind of variable ‘b’, namely ‘k’,
-      depends on variable ‘k’ from an inner scope
-      Perhaps bind ‘b’ sometime after binding ‘k’
-    • In the type signature:
+T11142.hs:9:49: error:
+    • Expected kind ‘k’, but ‘b’ has kind ‘k0’
+    • In the second argument of ‘SameKind’, namely ‘b’
+      In the type signature:
         foo :: forall b. (forall k (a :: k). SameKind a b) -> ()
index 4dda0cd..e30599d 100644 (file)
@@ -10,8 +10,7 @@ T12593.hs:12:31: error:
     • Expecting one more argument to ‘k’
       Expected a type, but
       ‘k’ has kind
-      ‘(((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
-       -> Constraint’
+      ‘(((k0 -> k1 -> TYPE t1) -> Constraint) -> k2 -> *) -> Constraint’
     • In the kind ‘k’
       In the type signature:
         run :: k2 q =>
@@ -22,65 +21,21 @@ T12593.hs:12:40: error:
     • Expecting two more arguments to ‘k1’
       Expected a type, but
       ‘k1’ has kind
-      ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’
+      ‘((k0 -> k1 -> TYPE t1) -> Constraint) -> k2 -> *’
     • In the kind ‘k1’
       In the type signature:
         run :: k2 q =>
                Free k k1 k2 p a b
                -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
 
-T12593.hs:12:47: error:
-    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-                            -> (k2 -> k3 -> *) -> *)
-                           -> Constraint’
+T12593.hs:12:54: error:
+    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint) -> k2 -> *’
                      with ‘*’
       When matching kinds
-        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
-             -> Constraint
-        k2 :: *
-    • In the first argument of ‘p’, namely ‘c’
-      In the type signature:
-        run :: k2 q =>
-               Free k k1 k2 p a b
-               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
-
-T12593.hs:12:49: error:
-    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-                           -> (k2 -> k3 -> *) -> *’
-                     with ‘*’
-      When matching kinds
-        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
-        k3 :: *
-    • In the second argument of ‘p’, namely ‘d’
-      In the type signature:
-        run :: k2 q =>
-               Free k k1 k2 p a b
-               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
-
-T12593.hs:12:56: error:
-    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-                            -> (k2 -> k3 -> *) -> *)
-                           -> Constraint’
-                     with ‘*’
-      When matching kinds
-        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
-             -> Constraint
-        k0 :: *
-    • In the first argument of ‘q’, namely ‘c’
-      In the type signature:
-        run :: k2 q =>
-               Free k k1 k2 p a b
-               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
-
-T12593.hs:12:58: error:
-    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-                           -> (k2 -> k3 -> *) -> *’
-                     with ‘*’
-      When matching kinds
-        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+        k3 :: ((k0 -> k1 -> *) -> Constraint) -> k2 -> *
         k1 :: *
-    • In the second argument of ‘q’, namely ‘d
-      In the type signature:
+      Expected kind ‘k -> k3 -> *’, but ‘q’ has kind ‘k0 -> k1 -> *
+     In the type signature:
         run :: k2 q =>
                Free k k1 k2 p a b
                -> (forall (c :: k) (d :: k1). p c d -> q c d)&