summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/typecheck/TcSigs.hs28
-rw-r--r--compiler/typecheck/TcTyClsDecls.hs2
-rw-r--r--compiler/typecheck/TcValidity.hs14
-rw-r--r--compiler/types/Type.hs5
-rw-r--r--testsuite/tests/patsyn/should_compile/T8968-2.hs2
-rw-r--r--testsuite/tests/patsyn/should_compile/poly-export2.hs1
-rw-r--r--testsuite/tests/patsyn/should_fail/T11010.hs2
-rw-r--r--testsuite/tests/patsyn/should_fail/T11039.hs3
-rw-r--r--testsuite/tests/patsyn/should_fail/T11039a.hs2
-rw-r--r--testsuite/tests/patsyn/should_fail/T12819.hs9
-rw-r--r--testsuite/tests/patsyn/should_fail/T12819.stderr3
-rw-r--r--testsuite/tests/patsyn/should_fail/all.T1
-rw-r--r--testsuite/tests/typecheck/should_compile/T12911.hs9
-rw-r--r--testsuite/tests/typecheck/should_compile/all.T1
14 files changed, 56 insertions, 26 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 24666cfc87..381aa4dfcd 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_compile/T8968-2.hs b/testsuite/tests/patsyn/should_compile/T8968-2.hs
index 05453ec98e..0b196a5f88 100644
--- a/testsuite/tests/patsyn/should_compile/T8968-2.hs
+++ b/testsuite/tests/patsyn/should_compile/T8968-2.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
+{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms, FlexibleContexts #-}
module ShouldCompile where
data X :: (* -> *) -> * -> * where
diff --git a/testsuite/tests/patsyn/should_compile/poly-export2.hs b/testsuite/tests/patsyn/should_compile/poly-export2.hs
index cfea9985f8..65c5c7cdbc 100644
--- a/testsuite/tests/patsyn/should_compile/poly-export2.hs
+++ b/testsuite/tests/patsyn/should_compile/poly-export2.hs
@@ -1,5 +1,6 @@
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
module Foo (A(P,Q)) where
data A a = A a
diff --git a/testsuite/tests/patsyn/should_fail/T11010.hs b/testsuite/tests/patsyn/should_fail/T11010.hs
index c0bdb6e0d4..c2d0fc6255 100644
--- a/testsuite/tests/patsyn/should_fail/T11010.hs
+++ b/testsuite/tests/patsyn/should_fail/T11010.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE PatternSynonyms, ExistentialQuantification, GADTSyntax #-}
+{-# LANGUAGE PatternSynonyms, ExistentialQuantification, GADTSyntax, TypeFamilies #-}
module T11010 where
diff --git a/testsuite/tests/patsyn/should_fail/T11039.hs b/testsuite/tests/patsyn/should_fail/T11039.hs
index fab58240e5..daa2bf1602 100644
--- a/testsuite/tests/patsyn/should_fail/T11039.hs
+++ b/testsuite/tests/patsyn/should_fail/T11039.hs
@@ -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
-
diff --git a/testsuite/tests/patsyn/should_fail/T11039a.hs b/testsuite/tests/patsyn/should_fail/T11039a.hs
index 527a90f20b..f09f08c559 100644
--- a/testsuite/tests/patsyn/should_fail/T11039a.hs
+++ b/testsuite/tests/patsyn/should_fail/T11039a.hs
@@ -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
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/T12819.stderr b/testsuite/tests/patsyn/should_fail/T12819.stderr
new file mode 100644
index 0000000000..4c717211ba
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T12819.stderr
@@ -0,0 +1,3 @@
+
+T12819.hs:8:1: error:
+ The type family ‘F’ should have 1 argument, but has been given none
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 a01b018bbe..999786e1c1 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -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, [''])