Commit 8d18a873 authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

Reject nested predicates in impredicativity checking

When GHC attempts to unify a metavariable with a type containing
foralls, it will be rejected as an occurrence of impredicativity.
GHC was /not/ extending the same treatment to predicate types, such
as in the following (erroneous) example from #11514:

```haskell
foo :: forall a. (Show a => a -> a) -> ()
foo = undefined
```

This will attempt to instantiate `undefined` at
`(Show a => a -> a) -> ()`, which is impredicative. This patch
catches impredicativity arising from predicates in this fashion.

Since GHC is pickier about impredicative instantiations, some test
cases needed to be updated to be updated so as not to fall afoul of
the new validity check. (There were a surprising number of
impredicative uses of `undefined`!) Moreover, the `T14828` test case
now has slightly less informative types shown with `:print`. This is
due to a a much deeper issue with the GHCi debugger (see #14828).

Fixes #11514.
parent 646e3dc2
...@@ -16,7 +16,7 @@ import GhcPrelude ...@@ -16,7 +16,7 @@ import GhcPrelude
import TcRnTypes import TcRnTypes
import TcRnMonad import TcRnMonad
import TcMType import TcMType
import TcUnify( occCheckForErrors, OccCheckResult(..) ) import TcUnify( occCheckForErrors, MetaTyVarUpdateResult(..) )
import TcEnv( tcInitTidyEnv ) import TcEnv( tcInitTidyEnv )
import TcType import TcType
import RnUnbound ( unknownNameSuggestions ) import RnUnbound ( unknownNameSuggestions )
...@@ -1632,7 +1632,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 ...@@ -1632,7 +1632,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
, report , report
] ]
| OC_Occurs <- occ_check_expand | MTVU_Occurs <- occ_check_expand
-- We report an "occurs check" even for a ~ F t a, where F is a type -- We report an "occurs check" even for a ~ F t a, where F is a type
-- function; it's not insoluble (because in principle F could reduce) -- function; it's not insoluble (because in principle F could reduce)
-- but we have certainly been unable to solve it -- but we have certainly been unable to solve it
...@@ -1657,10 +1657,10 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 ...@@ -1657,10 +1657,10 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
; mkErrorMsgFromCt ctxt ct $ ; mkErrorMsgFromCt ctxt ct $
mconcat [important main_msg, extra2, extra3, report] } mconcat [important main_msg, extra2, extra3, report] }
| OC_Bad <- occ_check_expand | MTVU_Bad <- occ_check_expand
= do { let msg = vcat [ text "Cannot instantiate unification variable" = do { let msg = vcat [ text "Cannot instantiate unification variable"
<+> quotes (ppr tv1) <+> quotes (ppr tv1)
, hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2) , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2)
, nest 2 (text "GHC doesn't yet support impredicative polymorphism") ] , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ]
-- Unlike the other reports, this discards the old 'report_important' -- Unlike the other reports, this discards the old 'report_important'
-- instead of augmenting it. This is because the details are not likely -- instead of augmenting it. This is because the details are not likely
......
...@@ -31,7 +31,7 @@ module TcUnify ( ...@@ -31,7 +31,7 @@ module TcUnify (
matchActualFunTys, matchActualFunTysPart, matchActualFunTys, matchActualFunTysPart,
matchExpectedFunKind, matchExpectedFunKind,
metaTyVarUpdateOK, occCheckForErrors, OccCheckResult(..) metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..)
) where ) where
...@@ -2115,43 +2115,43 @@ with (forall k. k->*) ...@@ -2115,43 +2115,43 @@ with (forall k. k->*)
-} -}
data OccCheckResult a data MetaTyVarUpdateResult a
= OC_OK a = MTVU_OK a
| OC_Bad -- Forall or type family | MTVU_Bad -- Forall, predicate, or type family
| OC_Occurs | MTVU_Occurs
instance Functor OccCheckResult where instance Functor MetaTyVarUpdateResult where
fmap = liftM fmap = liftM
instance Applicative OccCheckResult where instance Applicative MetaTyVarUpdateResult where
pure = OC_OK pure = MTVU_OK
(<*>) = ap (<*>) = ap
instance Monad OccCheckResult where instance Monad MetaTyVarUpdateResult where
OC_OK x >>= k = k x MTVU_OK x >>= k = k x
OC_Bad >>= _ = OC_Bad MTVU_Bad >>= _ = MTVU_Bad
OC_Occurs >>= _ = OC_Occurs MTVU_Occurs >>= _ = MTVU_Occurs
occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult () occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult ()
-- Just for error-message generation; so we return OccCheckResult -- Just for error-message generation; so we return MetaTyVarUpdateResult
-- so the caller can report the right kind of error -- so the caller can report the right kind of error
-- Check whether -- Check whether
-- a) the given variable occurs in the given type. -- a) the given variable occurs in the given type.
-- b) there is a forall in the type (unless we have -XImpredicativeTypes) -- b) there is a forall in the type (unless we have -XImpredicativeTypes)
occCheckForErrors dflags tv ty occCheckForErrors dflags tv ty
= case preCheck dflags True tv ty of = case preCheck dflags True tv ty of
OC_OK _ -> OC_OK () MTVU_OK _ -> MTVU_OK ()
OC_Bad -> OC_Bad MTVU_Bad -> MTVU_Bad
OC_Occurs -> case occCheckExpand [tv] ty of MTVU_Occurs -> case occCheckExpand [tv] ty of
Nothing -> OC_Occurs Nothing -> MTVU_Occurs
Just _ -> OC_OK () Just _ -> MTVU_OK ()
---------------- ----------------
metaTyVarUpdateOK :: DynFlags metaTyVarUpdateOK :: DynFlags
-> TcTyVar -- tv :: k1 -> TcTyVar -- tv :: k1
-> TcType -- ty :: k2 -> TcType -- ty :: k2
-> Maybe TcType -- possibly-expanded ty -> Maybe TcType -- possibly-expanded ty
-- (metaTyFVarUpdateOK tv ty) -- (metaTyVarUpdateOK tv ty)
-- We are about to update the meta-tyvar tv with ty -- We are about to update the meta-tyvar tv with ty
-- Check (a) that tv doesn't occur in ty (occurs check) -- Check (a) that tv doesn't occur in ty (occurs check)
-- (b) that ty does not have any foralls -- (b) that ty does not have any foralls
...@@ -2178,17 +2178,18 @@ metaTyVarUpdateOK dflags tv ty ...@@ -2178,17 +2178,18 @@ metaTyVarUpdateOK dflags tv ty
= case preCheck dflags False tv ty of = case preCheck dflags False tv ty of
-- False <=> type families not ok -- False <=> type families not ok
-- See Note [Prevent unification with type families] -- See Note [Prevent unification with type families]
OC_OK _ -> Just ty MTVU_OK _ -> Just ty
OC_Bad -> Nothing -- forall or type function MTVU_Bad -> Nothing -- forall, predicate, or type function
OC_Occurs -> occCheckExpand [tv] ty MTVU_Occurs -> occCheckExpand [tv] ty
preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult () preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
-- A quick check for -- A quick check for
-- (a) a forall type (unless -XImpredivativeTypes) -- (a) a forall type (unless -XImpredicativeTypes)
-- (b) a type family -- (b) a predicate type (unless -XImpredicativeTypes)
-- (c) an occurrence of the type variable (occurs check) -- (c) a type family
-- (d) an occurrence of the type variable (occurs check)
-- --
-- For (a) and (b) we check only the top level of the type, NOT -- For (a), (b), and (c) we check only the top level of the type, NOT
-- inside the kinds of variables it mentions. But for (c) we do -- inside the kinds of variables it mentions. But for (c) we do
-- look in the kinds of course. -- look in the kinds of course.
...@@ -2198,25 +2199,28 @@ preCheck dflags ty_fam_ok tv ty ...@@ -2198,25 +2199,28 @@ preCheck dflags ty_fam_ok tv ty
details = tcTyVarDetails tv details = tcTyVarDetails tv
impredicative_ok = canUnifyWithPolyType dflags details impredicative_ok = canUnifyWithPolyType dflags details
ok :: OccCheckResult () ok :: MetaTyVarUpdateResult ()
ok = OC_OK () ok = MTVU_OK ()
fast_check :: TcType -> OccCheckResult () fast_check :: TcType -> MetaTyVarUpdateResult ()
fast_check (TyVarTy tv') fast_check (TyVarTy tv')
| tv == tv' = OC_Occurs | tv == tv' = MTVU_Occurs
| otherwise = fast_check_occ (tyVarKind tv') | otherwise = fast_check_occ (tyVarKind tv')
-- See Note [Occurrence checking: look inside kinds] -- See Note [Occurrence checking: look inside kinds]
fast_check (TyConApp tc tys) fast_check (TyConApp tc tys)
| bad_tc tc = OC_Bad | bad_tc tc = MTVU_Bad
| otherwise = mapM fast_check tys >> ok | otherwise = mapM fast_check tys >> ok
fast_check (LitTy {}) = ok fast_check (LitTy {}) = ok
fast_check (FunTy _ a r) = fast_check a >> fast_check r fast_check (FunTy{ft_af = af, ft_arg = a, ft_res = r})
| InvisArg <- af
, not impredicative_ok = MTVU_Bad
| otherwise = fast_check a >> fast_check r
fast_check (AppTy fun arg) = fast_check fun >> fast_check arg fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
fast_check (CastTy ty co) = fast_check ty >> fast_check_co co fast_check (CastTy ty co) = fast_check ty >> fast_check_co co
fast_check (CoercionTy co) = fast_check_co co fast_check (CoercionTy co) = fast_check_co co
fast_check (ForAllTy (Bndr tv' _) ty) fast_check (ForAllTy (Bndr tv' _) ty)
| not impredicative_ok = OC_Bad | not impredicative_ok = MTVU_Bad
| tv == tv' = ok | tv == tv' = ok
| otherwise = do { fast_check_occ (tyVarKind tv') | otherwise = do { fast_check_occ (tyVarKind tv')
; fast_check_occ ty } ; fast_check_occ ty }
...@@ -2226,13 +2230,13 @@ preCheck dflags ty_fam_ok tv ty ...@@ -2226,13 +2230,13 @@ preCheck dflags ty_fam_ok tv ty
-- For kinds, we only do an occurs check; we do not worry -- For kinds, we only do an occurs check; we do not worry
-- about type families or foralls -- about type families or foralls
-- See Note [Checking for foralls] -- See Note [Checking for foralls]
fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = MTVU_Occurs
| otherwise = ok | otherwise = ok
-- For coercions, we are only doing an occurs check here; -- For coercions, we are only doing an occurs check here;
-- no bother about impredicativity in coercions, as they're -- no bother about impredicativity in coercions, as they're
-- inferred -- inferred
fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs
| otherwise = ok | otherwise = ok
bad_tc :: TyCon -> Bool bad_tc :: TyCon -> Bool
......
...@@ -34,7 +34,7 @@ fromInteger = Prelude.fromInteger ...@@ -34,7 +34,7 @@ fromInteger = Prelude.fromInteger
insertStore = undefined insertStore = undefined
schema = undefined schema = undefined
withTypeable = undefined withTypeable _ _ = undefined
throw# = undefined throw# = undefined
toDynamicST = undefined toDynamicST = undefined
......
...@@ -12,4 +12,4 @@ Simplifier ticks exhausted ...@@ -12,4 +12,4 @@ Simplifier ticks exhausted
simplifier non-termination has been judged acceptable. simplifier non-termination has been judged acceptable.
To see detailed counts use -ddump-simpl-stats To see detailed counts use -ddump-simpl-stats
Total ticks: 140007 Total ticks: 140086
+ = (_t1::Num a => a -> a -> a) + = (_t1::t1)
print = (_t2::Show a1 => a1 -> IO ()) print = (_t2::t1)
log = (_t3::Floating a2 => a2 -> a2) log = (_t3::t1)
head = (_t4::[a4] -> a4) head = (_t4::[a] -> a)
tail = (_t5::[a7] -> [a7]) tail = (_t5::[a1] -> [a1])
fst = (_t6::(a11, b) -> a11) fst = (_t6::(a2, b) -> a2)
...@@ -4,6 +4,6 @@ import Data.Typeable ...@@ -4,6 +4,6 @@ import Data.Typeable
class Deferrable p where deferEither :: proxy p -> (p => r) -> Either String r class Deferrable p where deferEither :: proxy p -> (p => r) -> Either String r
instance (Typeable a, Typeable b) => Deferrable (a ~ b) where deferEither = undefined instance (Typeable a, Typeable b) => Deferrable (a ~ b) where deferEither _ _ = undefined
:t deferEither @(_ ~ _) :t deferEither @(_ ~ _)
...@@ -6,7 +6,7 @@ return :: Monad m => a -> m a ...@@ -6,7 +6,7 @@ return :: Monad m => a -> m a
return = (_t3::t1) return = (_t3::t1)
pure :: Applicative f => a -> f a pure :: Applicative f => a -> f a
pure = (_t4::t1) pure = (_t4::t1)
mempty = (_t5::Monoid a => a) mempty = (_t5::t1)
mappend = (_t6::Monoid a => a -> a -> a) mappend = (_t6::t1)
foldl' = (_t7::t1) foldl' = (_t7::t1)
f = (_t8::t1) f = (_t8::t1)
...@@ -6,6 +6,6 @@ type family T a ...@@ -6,6 +6,6 @@ type family T a
t2 :: forall a. ((T a ~ a) => a) -> a t2 :: forall a. ((T a ~ a) => a) -> a
t2 = t t2 = t
t :: forall a. ((T a ~ a) => a) -> a t :: forall a. ((T a ~ a) => a) -> a
t = undefined t _ = undefined
T5934.hs:12:7: error: T5934.hs:12:7: error:
• Cannot instantiate unification variable ‘a0’ • Cannot instantiate unification variable ‘a0’
with a type involving foralls: (forall s. GenST s) -> Int with a type involving polytypes: (forall s. GenST s) -> Int
GHC doesn't yet support impredicative polymorphism GHC doesn't yet support impredicative polymorphism
• In the expression: 0 • In the expression: 0
In an equation for ‘run’: run = 0 In an equation for ‘run’: run = 0
...@@ -7,7 +7,7 @@ T11142.hs:9:49: error: ...@@ -7,7 +7,7 @@ T11142.hs:9:49: error:
T11142.hs:10:7: error: T11142.hs:10:7: error:
• Cannot instantiate unification variable ‘a0’ • Cannot instantiate unification variable ‘a0’
with a type involving foralls: with a type involving polytypes:
(forall k1 (a :: k1). SameKind a b) -> () (forall k1 (a :: k1). SameKind a b) -> ()
GHC doesn't yet support impredicative polymorphism GHC doesn't yet support impredicative polymorphism
• In the expression: undefined • In the expression: undefined
......
...@@ -76,7 +76,7 @@ splitApp rep@(TrFun _ a b) = Just (IsApp (mkTrApp arr a) b) ...@@ -76,7 +76,7 @@ splitApp rep@(TrFun _ a b) = Just (IsApp (mkTrApp arr a) b)
splitApp (TrTyCon{}) = Nothing splitApp (TrTyCon{}) = Nothing
withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r
withTypeable = undefined withTypeable _ _ = undefined
eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b) TypeRep a -> TypeRep b -> Maybe (a :~~: b)
......
...@@ -11,7 +11,7 @@ class Deferrable (c :: Constraint) where ...@@ -11,7 +11,7 @@ class Deferrable (c :: Constraint) where
deferPair :: (Deferrable c1, Deferrable c2) => deferPair :: (Deferrable c1, Deferrable c2) =>
Proxy (c1,c2) -> ((c1,c2) => a) -> a Proxy (c1,c2) -> ((c1,c2) => a) -> a
deferPair = undefined deferPair _ _ = undefined
instance (Deferrable c1, Deferrable c2) => Deferrable (c1,c2) where instance (Deferrable c1, Deferrable c2) => Deferrable (c1,c2) where
-- defer p f = deferPair p f -- Succeeds -- defer p f = deferPair p f -- Succeeds
......
...@@ -8,7 +8,7 @@ T11452.hs:6:14: error: ...@@ -8,7 +8,7 @@ T11452.hs:6:14: error:
T11452.hs:6:14: error: T11452.hs:6:14: error:
• Cannot instantiate unification variable ‘p0’ • Cannot instantiate unification variable ‘p0’
with a type involving foralls: forall a. a -> a with a type involving polytypes: forall a. a -> a
GHC doesn't yet support impredicative polymorphism GHC doesn't yet support impredicative polymorphism
• In the Template Haskell quotation [|| \ _ -> () ||] • In the Template Haskell quotation [|| \ _ -> () ||]
In the expression: [|| \ _ -> () ||] In the expression: [|| \ _ -> () ||]
......
...@@ -3,7 +3,8 @@ T12427a.hs:17:29: error: ...@@ -3,7 +3,8 @@ T12427a.hs:17:29: error:
• Couldn't match expected type ‘p’ • Couldn't match expected type ‘p’
with actual type ‘(forall b. [b] -> [b]) -> Int’ with actual type ‘(forall b. [b] -> [b]) -> Int’
‘p’ is a rigid type variable bound by ‘p’ is a rigid type variable bound by
the inferred type of h11 :: T -> p at T12427a.hs:17:1-29 the inferred type of h11 :: T -> p
at T12427a.hs:17:1-29
• In the expression: v • In the expression: v
In a case alternative: T1 _ v -> v In a case alternative: T1 _ v -> v
In the expression: case y of { T1 _ v -> v } In the expression: case y of { T1 _ v -> v }
...@@ -12,7 +13,7 @@ T12427a.hs:17:29: error: ...@@ -12,7 +13,7 @@ T12427a.hs:17:29: error:
T12427a.hs:28:6: error: T12427a.hs:28:6: error:
• Cannot instantiate unification variable ‘p0’ • Cannot instantiate unification variable ‘p0’
with a type involving foralls: (forall b. [b] -> [b]) -> Int with a type involving polytypes: (forall b. [b] -> [b]) -> Int
GHC doesn't yet support impredicative polymorphism GHC doesn't yet support impredicative polymorphism
• In the pattern: T1 _ x1 • In the pattern: T1 _ x1
In a pattern binding: T1 _ x1 = undefined In a pattern binding: T1 _ x1 = undefined
T10194.hs:7:8: error: T10194.hs:7:8: error:
Cannot instantiate unification variable ‘b0’ Cannot instantiate unification variable ‘b0’
with a type involving foralls: X with a type involving polytypes: X
GHC doesn't yet support impredicative polymorphism GHC doesn't yet support impredicative polymorphism
In the expression: (.) In the expression: (.)
In an equation for ‘comp’: comp = (.) In an equation for ‘comp’: comp = (.)
{-# LANGUAGE RankNTypes #-}
module T11514 where
foo :: forall a. (Show a => a -> a) -> ()
foo = undefined
T11514.hs:6:7: error:
• Cannot instantiate unification variable ‘a0’
with a type involving polytypes: (Show a => a -> a) -> ()
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In an equation for ‘foo’: foo = undefined
• Relevant bindings include
foo :: (Show a => a -> a) -> () (bound at T11514.hs:6:1)
T12563.hs:7:15: error: T12563.hs:7:15: error:
• Cannot instantiate unification variable ‘p0’ • Cannot instantiate unification variable ‘p0’
with a type involving foralls: (forall a. f0 a) -> f0 r0 with a type involving polytypes: (forall a. f0 a) -> f0 r0
GHC doesn't yet support impredicative polymorphism GHC doesn't yet support impredicative polymorphism
• In the first argument of ‘foo’, namely ‘g’ • In the first argument of ‘foo’, namely ‘g’
In the expression: foo g In the expression: foo g
......
...@@ -3,7 +3,7 @@ T12589.hs:13:3: error: Variable not in scope: (&) :: t1 -> t0 -> t ...@@ -3,7 +3,7 @@ T12589.hs:13:3: error: Variable not in scope: (&) :: t1 -> t0 -> t
T12589.hs:13:5: error: T12589.hs:13:5: error:
• Cannot instantiate unification variable ‘t0’ • Cannot instantiate unification variable ‘t0’
with a type involving foralls: with a type involving polytypes:
(forall a. Bounded a => f0 a) -> h0 f0 xs0 (forall a. Bounded a => f0 a) -> h0 f0 xs0
GHC doesn't yet support impredicative polymorphism GHC doesn't yet support impredicative polymorphism
• In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’ • In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’
......
...@@ -390,6 +390,7 @@ test('T11347', normal, compile_fail, ['']) ...@@ -390,6 +390,7 @@ test('T11347', normal, compile_fail, [''])
test('T11356', normal, compile_fail, ['']) test('T11356', normal, compile_fail, [''])
test('T11355', normal, compile_fail, ['']) test('T11355', normal, compile_fail, [''])
test('T11464', normal, compile_fail, ['']) test('T11464', normal, compile_fail, [''])
test('T11514', normal, compile_fail, [''])
test('T11563', normal, compile_fail, ['']) test('T11563', normal, compile_fail, [''])
test('T11541', normal, compile_fail, ['']) test('T11541', normal, compile_fail, [''])
test('T11313', normal, compile_fail, ['']) test('T11313', 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