[commit: ghc] wip/T12819: Reshuffle levity polymorphism checks. (ed05156)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/T12819
Link       : http://ghc.haskell.org/trac/ghc/changeset/ed0515682851f592e3f949cef26ee6d06f11e88f/ghc

>---------------------------------------------------------------

commit ed0515682851f592e3f949cef26ee6d06f11e88f
Author: Richard Eisenberg <rae at cs.brynmawr.edu>
Date:   Thu Nov 10 13:41:30 2016 -0500

    Reshuffle levity polymorphism checks.
    
    Previously, GHC checked for bad levity polymorphism to the
    left of all arrows in data constructors. This was wrong, as
    reported in #??? (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: ???


>---------------------------------------------------------------

ed0515682851f592e3f949cef26ee6d06f11e88f
 compiler/typecheck/TcSigs.hs       | 28 ++++++++++++++++++++++------
 compiler/typecheck/TcTyClsDecls.hs |  2 ++
 compiler/typecheck/TcValidity.hs   |  3 ---
 compiler/types/Type.hs             |  5 +++--
 4 files changed, 27 insertions(+), 11 deletions(-)

diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 9c4fd2b..3e63493 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 0b471d2..67fd036 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -2295,6 +2295,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 b316fe2..87c742a 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 )
@@ -487,8 +486,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 f615757..81798fb 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1196,12 +1196,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 )