Commit 8906e7b7 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu Committed by Ben Gamari

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 #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
parent 6c816c56
......@@ -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)
......
......@@ -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)
......
......@@ -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
......
......@@ -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 )
......
{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms, FlexibleContexts #-}
module ShouldCompile where
data X :: (* -> *) -> * -> * where
......
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
module Foo (A(P,Q)) where
data A a = A a
......
{-# LANGUAGE PatternSynonyms, ExistentialQuantification, GADTSyntax #-}
{-# LANGUAGE PatternSynonyms, ExistentialQuantification, GADTSyntax, TypeFamilies #-}
module T11010 where
......
{-# 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
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PatternSynonyms, TypeFamilies #-}
module T11039a where
data A a = A a
......
{-# 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)
T12819.hs:8:1: error:
The type family ‘F’ should have 1 argument, but has been given none
......@@ -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, [''])
{-# LANGUAGE ExplicitForAll, TypeInType, GADTSyntax,
ExistentialQuantification #-}
module T12911 where
import GHC.Exts
data X where
MkX :: forall (a :: TYPE r). (a -> a) -> X
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment