Reshuffle levity polymorphism checks.
authorRichard Eisenberg <eir@cis.upenn.edu>
Sat, 17 Dec 2016 23:06:34 +0000 (18:06 -0500)
committerBen Gamari <ben@smart-cactus.org>
Sat, 17 Dec 2016 23:09:37 +0000 (18:09 -0500)
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

Test Plan: ./validate

Reviewers: simonpj, austin, bgamari

Reviewed By: bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2783

GHC Trac Issues: #12819, #12911

14 files changed:
compiler/typecheck/TcSigs.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcValidity.hs
compiler/types/Type.hs
testsuite/tests/patsyn/should_compile/T8968-2.hs
testsuite/tests/patsyn/should_compile/poly-export2.hs
testsuite/tests/patsyn/should_fail/T11010.hs
testsuite/tests/patsyn/should_fail/T11039.hs
testsuite/tests/patsyn/should_fail/T11039a.hs
testsuite/tests/patsyn/should_fail/T12819.hs [new file with mode: 0644]
testsuite/tests/patsyn/should_fail/T12819.stderr [new file with mode: 0644]
testsuite/tests/patsyn/should_fail/all.T
testsuite/tests/typecheck/should_compile/T12911.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index 9c4fd2b..3e63493 100644 (file)
@@ -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)
index 24666cf..381aa4d 100644 (file)
@@ -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)
index 6cc40a5..c2f5d4e 100644 (file)
@@ -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
index 926acf7..1e429ef 100644 (file)
@@ -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 )
index 05453ec..0b196a5 100644 (file)
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
+{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms, FlexibleContexts #-}
 module ShouldCompile where
 
 data X :: (* -> *) -> * -> * where
index cfea998..65c5c7c 100644 (file)
@@ -1,5 +1,6 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
 module Foo (A(P,Q)) where
 
 data A a = A a
index c0bdb6e..c2d0fc6 100644 (file)
@@ -1,4 +1,4 @@
-{-# LANGUAGE PatternSynonyms, ExistentialQuantification, GADTSyntax #-}
+{-# LANGUAGE PatternSynonyms, ExistentialQuantification, GADTSyntax, TypeFamilies #-}
 
 module T11010 where
 
index fab5824..daa2bf1 100644 (file)
@@ -1,4 +1,4 @@
-{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PatternSynonyms, TypeFamilies #-}
 module T11039 where
 
 data A a = A a
@@ -6,4 +6,3 @@ data A a = A a
 -- This should fail
 pattern Q :: () => (A ~ f) => a -> f a
 pattern Q a = A a
-
index 527a90f..f09f08c 100644 (file)
@@ -1,4 +1,4 @@
-{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PatternSynonyms, TypeFamilies #-}
 module T11039a where
 
 data A a = A a
diff --git a/testsuite/tests/patsyn/should_fail/T12819.hs b/testsuite/tests/patsyn/should_fail/T12819.hs
new file mode 100644 (file)
index 0000000..41bde9c
--- /dev/null
@@ -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/T12819.stderr b/testsuite/tests/patsyn/should_fail/T12819.stderr
new file mode 100644 (file)
index 0000000..4c71721
--- /dev/null
@@ -0,0 +1,3 @@
+
+T12819.hs:8:1: error:
+    The type family â€˜F’ should have 1 argument, but has been given none
index fe0922c..cb23b3f 100644 (file)
@@ -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 (file)
index 0000000..88c2125
--- /dev/null
@@ -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
index a01b018..999786e 100644 (file)
@@ -557,6 +557,7 @@ test('T12734', normal, compile, [''])
 test('T12734a', normal, compile_fail, [''])
 test('T12763', normal, compile, [''])
 test('T12797', normal, compile, [''])
+test('T12911', normal, compile, [''])
 test('T12925', normal, compile, [''])
 test('T12919', expect_broken(12919), compile, [''])
 test('T12936', normal, compile, [''])