Reshuffle levity polymorphism checks.wip/T12819

Previously, GHC checked for bad levity polymorphism to the
left of all arrows in data constructors. This was wrong, as
reported in #12911 (where an example is also shown). The solution
is to check each individual argument for bad levity polymorphism.
Thus the check has been moved from TcValidity to TcTyClsDecls.

A similar situation exists with pattern synonyms, also fixed here.

This patch also nabs #12819 while I was in town.

Test cases: typecheck/should_compile/T12911, patsyn/should_fail/T12819

8 files changed, 48 insertions, 21 deletions

diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 9c4fd2bf8a..3e63493758 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -30,6 +30,8 @@ import TcRnTypes
 import TcRnMonad
 import TcType
 import TcMType
+import TcHsSyn ( checkForRepresentationPolymorphism )
+import TcValidity ( checkValidType )
 import TcUnify( tcSkolemise, unifyType, noThing )
 import Inst( topInstantiate )
 import TcEnv( tcLookupId )
@@ -367,16 +369,12 @@ tcPatSynSig name sig_ty
 
        -- Kind generalisation
        ; kvs <- kindGeneralize $
-                mkSpecForAllTys (implicit_tvs ++ univ_tvs) $
-                mkFunTys req $
-                mkSpecForAllTys ex_tvs $
-                mkFunTys prov $
-                body_ty
+                build_patsyn_type [] implicit_tvs univ_tvs req
+                                  ex_tvs prov body_ty
 
        -- These are /signatures/ so we zonk to squeeze out any kind
        -- unification variables.  Do this after quantifyTyVars which may
        -- default kind variables to *.
-       -- ToDo: checkValidType?
        ; traceTc "about zonk" empty
        ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs
        ; univ_tvs     <- mapM zonkTcTyCoVarBndr univ_tvs
@@ -385,6 +383,15 @@ tcPatSynSig name sig_ty
        ; prov         <- zonkTcTypes prov
        ; body_ty      <- zonkTcType  body_ty
 
+       -- Now do validity checking
+       ; checkValidType ctxt $
+         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
+       ; mapM_ (checkForRepresentationPolymorphism empty) arg_tys
+
        ; traceTc "tcTySig }" $
          vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs
               , text "kvs" <+> ppr_tvs kvs
@@ -402,6 +409,15 @@ tcPatSynSig name sig_ty
                       , patsig_prov           = prov
                       , patsig_body_ty        = body_ty }) }
   where
+    ctxt = PatSynCtxt name
+
+    build_patsyn_type kvs imp univ req ex prov body
+      = mkInvForAllTys kvs $
+        mkSpecForAllTys (imp ++ univ) $
+        mkFunTys req $
+        mkSpecForAllTys ex $
+        mkFunTys prov $
+        body
 
 ppr_tvs :: [TyVar] -> SDoc
 ppr_tvs tvs = braces (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index b9bc595189..0cdad3777b 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -2299,6 +2299,8 @@ checkValidDataCon dflags existential_ok tc con
 
           -- Check all argument types for validity
         ; checkValidType ctxt (dataConUserType con)
+        ; mapM_ (checkForRepresentationPolymorphism empty)
+                (dataConOrigArgTys con)
 
           -- Extra checks for newtype data constructors
         ; when (isNewTyCon tc) (checkNewDataCon con)
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 6cc40a5d67..c2f5d4e469 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -39,7 +39,6 @@ import TyCon
 -- others:
 import HsSyn            -- HsType
 import TcRnMonad        -- TcType, amongst others
-import TcHsSyn     ( checkForRepresentationPolymorphism )
 import TcEnv       ( tcGetInstEnvs )
 import FunDeps
 import InstEnv     ( ClsInst, lookupInstEnv, isOverlappable )
@@ -342,6 +341,7 @@ checkValidType ctxt ty
                  InfSigCtxt _   -> ArbitraryRank        -- Inferred type
                  ConArgCtxt _   -> rank1 -- We are given the type of the entire
                                          -- constructor, hence rank 1
+                 PatSynCtxt _   -> rank1
 
                  ForSigCtxt _   -> rank1
                  SpecInstCtxt   -> rank1
@@ -441,16 +441,6 @@ forAllAllowed ArbitraryRank             = True
 forAllAllowed (LimitedRank forall_ok _) = forall_ok
 forAllAllowed _                         = False
 
--- The zonker issues errors if it zonks a representation-polymorphic binder
--- But sometimes it's nice to check a little more eagerly, trying to report
--- errors earlier.
-representationPolymorphismForbidden :: UserTypeCtxt -> Bool
-representationPolymorphismForbidden = go
-  where
-    go (ConArgCtxt _) = True     -- A rep-polymorphic datacon won't be useful
-    go (PatSynCtxt _) = True     -- Similar to previous case
-    go _              = False    -- Other cases are caught by zonker
-
 ----------------------------------------
 check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
 -- The args say what the *type context* requires, independent
@@ -487,8 +477,6 @@ check_type _ _ _ (TyVarTy _) = return ()
 
 check_type env ctxt rank (FunTy arg_ty res_ty)
   = do  { check_type env ctxt arg_rank arg_ty
-        ; when (representationPolymorphismForbidden ctxt) $
-          checkForRepresentationPolymorphism empty arg_ty
         ; check_type env ctxt res_rank res_ty }
   where
     (arg_rank, res_rank) = funArgResRank rank
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 926acf7eb5..1e429effd1 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1198,12 +1198,13 @@ interfaces.  Notably this plays a role in tcTySigs in TcBinds.hs.
                                 ~~~~~~~~
 -}
 
--- | Make a dependent forall.
+-- | Make a dependent forall over an Inferred (as opposed to Specified)
+-- variable
 mkInvForAllTy :: TyVar -> Type -> Type
 mkInvForAllTy tv ty = ASSERT( isTyVar tv )
                       ForAllTy (TvBndr tv Inferred) ty
 
--- | Like mkForAllTys, but assumes all variables are dependent and invisible,
+-- | Like mkForAllTys, but assumes all variables are dependent and Inferred,
 -- a common case
 mkInvForAllTys :: [TyVar] -> Type -> Type
 mkInvForAllTys tvs ty = ASSERT( all isTyVar tvs )
diff --git a/testsuite/tests/patsyn/should_fail/T12819.hs b/testsuite/tests/patsyn/should_fail/T12819.hs
new file mode 100644
index 0000000000..41bde9c61d
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T12819.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PatternSynonyms, ViewPatterns, TypeFamilies, KindSignatures #-}
+
+module T12819 where
+
+type family F a  -- F :: * -> *
+data T :: (* -> *) -> *
+
+pattern Q :: T F -> String
+pattern Q x <- (undefined -> x)
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index fe0922c882..cb23b3fb2a 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -32,3 +32,4 @@ test('T10426', normal, compile_fail, [''])
 test('T11265', normal, compile_fail, [''])
 test('T11667', normal, compile_fail, [''])
 test('T12165', normal, compile_fail, [''])
+test('T12819', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T12911.hs b/testsuite/tests/typecheck/should_compile/T12911.hs
new file mode 100644
index 0000000000..88c2125f2b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12911.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExplicitForAll, TypeInType, GADTSyntax,
+             ExistentialQuantification #-}
+
+module T12911 where
+
+import GHC.Exts
+
+data X where
+  MkX :: forall (a :: TYPE r). (a -> a) -> X
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 98e4ece08c..cd5bb5378f 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -555,3 +555,4 @@ test('T12734', normal, compile, [''])
 test('T12734a', normal, compile_fail, [''])
 test('T12763', normal, compile, [''])
 test('T12797', normal, compile, [''])
+test('T12911', normal, compile, [''])