Fix #17021 by checking more return kinds

All the details are in new Note [Datatype return kinds] in
TcTyClsDecls.

Test case: typecheck/should_fail/T17021{,b}
           typecheck/should_compile/T17021a

Updates haddock submodule

6 files changed, 49 insertions, 26 deletions

diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs
index c6861d8590..b2a66033ac 100644
--- a/compiler/GHC/Core/Coercion/Axiom.hs
+++ b/compiler/GHC/Core/Coercion/Axiom.hs
@@ -198,6 +198,17 @@ axiom as a whole, and they are computed only when the final axiom is built.
 
 During serialization, the list is converted into a list of the indices
 of the branches.
+
+Note [CoAxioms are homogeneous]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+All axioms must be *homogeneous*, meaning that the kind of the LHS must
+match the kind of the RHS. In practice, this means:
+
+  Given a CoAxiom { co_ax_tc = ax_tc },
+  for every branch CoAxBranch { cab_lhs = lhs, cab_rhs = rhs }:
+    typeKind (mkTyConApp ax_tc lhs) `eqType` typeKind rhs
+
+This is checked in FamInstEnv.mkCoAxBranch.
 -}
 
 -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
@@ -233,6 +244,7 @@ data CoAxBranch
     , cab_roles    :: [Role]        -- See Note [CoAxBranch roles]
     , cab_lhs      :: [Type]        -- Type patterns to match against
     , cab_rhs      :: Type          -- Right-hand side of the equality
+                                    -- See Note [CoAxioms are homogeneous]
     , cab_incomps  :: [CoAxBranch]  -- The previous incompatible branches
                                     -- See Note [Storing compatibility]
     }
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index c8e5a7a4f9..10dc63eb50 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -638,13 +638,16 @@ that Note.
 mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
              -> [TyVar] -- Extra eta tyvars
              -> [CoVar] -- possibly stale covars
+             -> TyCon   -- family/newtype TyCon (for error-checking only)
              -> [Type]  -- LHS patterns
              -> Type    -- RHS
              -> [Role]
              -> SrcSpan
              -> CoAxBranch
-mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
-  = CoAxBranch { cab_tvs     = tvs'
+mkCoAxBranch tvs eta_tvs cvs ax_tc lhs rhs roles loc
+  = -- See Note [CoAxioms are homogeneous] in Core.Coercion.Axiom
+    ASSERT( typeKind (mkTyConApp ax_tc lhs) `eqType` typeKind rhs )
+    CoAxBranch { cab_tvs     = tvs'
                , cab_eta_tvs = eta_tvs'
                , cab_cvs     = cvs'
                , cab_lhs     = tidyTypes env lhs
@@ -698,7 +701,7 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
             , co_ax_implicit = False
             , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
   where
-    branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
+    branch = mkCoAxBranch tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
                           (map (const Nominal) tvs)
                           (getSrcSpan ax_name)
 
@@ -716,7 +719,7 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty
             , co_ax_tc       = tycon
             , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
   where
-    branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
+    branch = mkCoAxBranch tvs [] [] tycon (mkTyVarTys tvs) rhs_ty
                           roles (getSrcSpan name)
 
 {-
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index b22705eb6f..92e9a25a6f 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -1388,7 +1388,8 @@ lintInTy ty
   = addLoc (InType ty) $
     do  { ty' <- applySubstTy ty
         ; k  <- lintType ty'
-        ; lintKind k  -- The kind returned by lintType is already
+        ; addLoc (InKind ty' k) $
+          lintKind k  -- The kind returned by lintType is already
                       -- a LintedKind but we also want to check that
                       -- k :: *, which lintKind does
         ; return (ty', k) }
@@ -2278,6 +2279,7 @@ data LintLocInfo
   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
   | TopLevelBindings
   | InType Type         -- Inside a type
+  | InKind Type Kind    -- Inside a kind
   | InCo   Coercion     -- Inside a coercion
 
 initL :: DynFlags -> LintFlags -> [Var]
@@ -2533,6 +2535,8 @@ dumpLoc TopLevelBindings
   = (noSrcLoc, Outputable.empty)
 dumpLoc (InType ty)
   = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
+dumpLoc (InKind ty ki)
+  = (noSrcLoc, text "In the kind of" <+> parens (ppr ty <+> dcolon <+> ppr ki))
 dumpLoc (InCo co)
   = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
 
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index fa188fc022..8719746f67 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -355,8 +355,8 @@ types are apart. This has practical consequences for the ability for closed
 type family applications to reduce. See test case
 indexed-types/should_compile/Overlap14.
 
-Note [Unifying with skolems]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Unification with skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we discover that two types unify if and only if a skolem variable is
 substituted, we can't properly unify the types. But, that skolem variable
 may later be instantiated with a unifyable type. So, we return maybeApart
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index b3a327c4c6..d7f37dac86 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -498,8 +498,21 @@ nlHsTyVar x   = noLoc (HsTyVar noExtField NotPromoted (noLoc x))
 nlHsFunTy a b = noLoc (HsFunTy noExtField (parenthesizeHsType funPrec a) b)
 nlHsParTy t   = noLoc (HsParTy noExtField t)
 
-nlHsTyConApp :: IdP (GhcPass p) -> [LHsType (GhcPass p)] -> LHsType (GhcPass p)
-nlHsTyConApp tycon tys  = foldl' nlHsAppTy (nlHsTyVar tycon) tys
+nlHsTyConApp :: LexicalFixity -> IdP (GhcPass p)
+             -> [LHsTypeArg (GhcPass p)] -> LHsType (GhcPass p)
+nlHsTyConApp fixity tycon tys
+  | Infix <- fixity
+  , HsValArg ty1 : HsValArg ty2 : rest <- tys
+  = foldl' mk_app (noLoc $ HsOpTy noExtField ty1 (noLoc tycon) ty2) rest
+  | otherwise
+  = foldl' mk_app (nlHsTyVar tycon) tys
+  where
+    mk_app :: LHsType (GhcPass p) -> LHsTypeArg (GhcPass p) -> LHsType (GhcPass p)
+    mk_app fun@(L _ (HsOpTy {})) arg = mk_app (noLoc $ HsParTy noExtField fun) arg
+      -- parenthesize things like `(A + B) C`
+    mk_app fun (HsValArg ty) = noLoc (HsAppTy noExtField fun (parenthesizeHsType appPrec ty))
+    mk_app fun (HsTypeArg _ ki) = noLoc (HsAppKindTy noSrcSpan fun (parenthesizeHsType appPrec ki))
+    mk_app fun (HsArgPar _) = noLoc (HsParTy noExtField fun)
 
 nlHsAppKindTy ::
   LHsType (GhcPass p) -> LHsKind (GhcPass p) -> LHsType (GhcPass p)
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index 24dbe364b2..1a52bcc966 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -1044,10 +1044,13 @@ mk_fail_msg dflags pat = "Pattern match failure in do expression at " ++
 
 dsHsVar :: Id -> DsM CoreExpr
 dsHsVar var
-               -- See Wrinkle in Note [Detecting forced eta expansion]
-  = ASSERT2(null (badUseOfLevPolyPrimop var ty), ppr var $$ ppr ty)
-    return (varToCoreExpr var)   -- See Note [Desugaring vars]
+  | let bad_tys = badUseOfLevPolyPrimop var ty
+  , not (null bad_tys)
+  = do { levPolyPrimopErr (ppr var) ty bad_tys
+       ; return unitExpr }  -- return something eminently safe
 
+  | otherwise
+  = return (varToCoreExpr var)   -- See Note [Desugaring vars]
   where
     ty = idType var
 
@@ -1134,6 +1137,8 @@ This invariant is checked in dsExpr.
 With that representation invariant, we simply look inside every HsWrap
 to see if its body is an HsVar whose Id hasNoBinding. Then, we look
 at the wrapped type. If it has any levity polymorphic arguments, reject.
+Because we might have an HsVar without a wrapper, we check in dsHsVar
+as well. typecheck/should_fail/T17021 triggers this case.
 
 Interestingly, this approach does not look to see whether the Id in
 question will be eta expanded. The logic is this:
@@ -1144,20 +1149,6 @@ question will be eta expanded. The logic is this:
     argument. If its wrapped type contains levity polymorphic arguments, reject.
 So, either way, we're good to reject.
 
-Wrinkle
-~~~~~~~
-Currently, all levity-polymorphic Ids are wrapped in HsWrap.
-
-However, this is not set in stone, in the future we might make
-instantiation more lazy.  (See "Visible type application", ESOP '16.)
-If we spot a levity-polymorphic hasNoBinding Id without a wrapper,
-then that is surely a problem. In this case, we raise an assertion failure.
-This failure can be changed to a call to `levPolyPrimopErr` in the future,
-if we decide to change instantiation.
-
-We can just check HsVar and HsConLikeOut for RealDataCon, since
-we don't have levity-polymorphic pattern synonyms. (This might change
-in the future.)
 -}
 
 -- | Takes an expression and its instantiated type. If the expression is an