Commit e6ca9300 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Fix #11355.

Previously, the check for impredicative type applications was
in the wrong spot.

Test case: typecheck/should_fail/T11355
parent 165ae440
......@@ -291,6 +291,7 @@ checkValidType :: UserTypeCtxt -> Type -> TcM ()
checkValidType ctxt ty
= do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
; rankn_flag <- xoptM LangExt.RankNTypes
; impred_flag <- xoptM LangExt.ImpredicativeTypes
; let gen_rank :: Rank -> Rank
gen_rank r | rankn_flag = ArbitraryRank
| otherwise = r
......@@ -310,7 +311,12 @@ checkValidType ctxt ty
TySynCtxt _ -> rank0
ExprSigCtxt -> rank1
TypeAppCtxt -> rank0
TypeAppCtxt | impred_flag -> ArbitraryRank
| otherwise -> tyConArgMonoType
-- Normally, ImpredicativeTypes is handled in check_arg_type,
-- but visible type applications don't go through there.
-- So we do this check here.
FunSigCtxt {} -> rank1
InfSigCtxt _ -> ArbitraryRank -- Inferred type
ConArgCtxt _ -> rank1 -- We are given the type of the entire
......
{-# LANGUAGE TypeApplications, RankNTypes #-}
module T11355 where
foo = const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a))
T11355.hs:5:7: error:
• Illegal polymorphic or qualified type: forall (a1 :: TYPE t0). a1
GHC doesn't yet support impredicative polymorphism
• In the expression:
const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a))
In an equation for ‘foo’:
foo
= const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a))
......@@ -402,3 +402,4 @@ test('T11274', normal, compile_fail, [''])
test('T10619', normal, compile_fail, [''])
test('T11347', normal, compile_fail, [''])
test('T11356', normal, compile_fail, [''])
test('T11355', normal, compile_fail, [''])
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