Opened 10 months ago
Last modified 8 months ago
#16140 new bug
Cannot create type synonym for quantified constraint without ImpredicativeTypes
Reported by: | Ashley Yakeley | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.6.3 |
Keywords: | QuantifiedConstraints, ImpredicativeTypes | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
{-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints, FlexibleInstances, UndecidableInstances #-} module Bug where type F1 (f :: * -> *) = forall a. Eq (f a) class (Functor f, F1 f) => C f instance (Functor f, F1 f) => C f type F2 f = (Functor f, F1 f)
Bug.hs:7:1: error: • Illegal polymorphic type: F1 f GHC doesn't yet support impredicative polymorphism • In the type synonym declaration for ‘F2’ | 7 | type F2 f = (Functor f, F1 f) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
(GHC accepts the program with ImpredicativeTypes.)
(Functor f, F1 f)
is allowed as a superclass constraint, and as an instance constraint, but a type synonym cannot be made for it.
Not sure if this really counts as a bug ("just switch on ImpredicativeTypes"), but I think it's worth discussing. I prefer to keep ImpredicativeTypes switched off, but if something can be a constraint, shouldn't I be able to create a type synonym of it?
Change History (21)
comment:1 Changed 10 months ago by
comment:2 Changed 10 months ago by
Keywords: | QuantifiedConstraints ImpredicativeTypes added |
---|
comment:3 follow-up: 4 Changed 10 months ago by
Actually it might not be too hard. The error message comes from TcValidity
, by which time we know for sure what is a constraint and what is an ordinary tuple.
Maybe, with QuantifiedConstraints
we should simply accept polytypes at the top level of a constraint tuple. Indeed, in types like forall a. (pred1, pred2) => glah
we already do, when checking pred1
, pred2
:
check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM () -- Check the validity of a predicate in a signature -- See Note [Validity checking for constraints] check_pred_ty env dflags ctxt pred = do { check_type env SigmaCtxt rank pred ; check_pred_help False env dflags ctxt pred } where rank | xopt LangExt.QuantifiedConstraints dflags = ArbitraryRank | otherwise = constraintMonoType
But we currently do not do this for the RHS of type synonyms of kind Constraint
.
Moreover, we you can see, check_pred_ty
also does some extra validity checks on predicates, using check_pred_help
. (These checks are not described in a Note but probably should be.) Example: require TypeFamilies
for t1 ~ t2
.
We should probably do these exact same checks for the RHS of constraint synonyms.
Proposal:
- In
checkValidType
, if the kind of the type isConstraint
, then usecheck_pred_ty
rather thancheck_type
.
Do you agree? Would you like to try that?
comment:4 Changed 10 months ago by
The spirit of this proposal sounds nice, but there's a couple things that I'm worried about:
- This proposal suggests accepting polytypes in all types of kind
Constraint
. Would that mean that the following would be accepted?
f :: (?x :: Proxy (forall a. Eq a => Eq (f a) :: Constraint)) => Int; f = 42
Unlike in the original example,
Proxy (forall a. Eq a => Eq (f a) :: Constraint)
appears to be truly impredicative.
- Let's suppose you define
type F2 f = (Functor f, forall a. Eq (f a))
(which would now be accepted under this proposal without needingImpredicativeTypes
) and later try to defineg :: Proxy (F2 Maybe); g = Proxy
. Would that count as impredicative?
comment:5 Changed 10 months ago by
This proposal suggests accepting polytypes in all types of kind Constraint. Would that mean that the following would be accepted?
No, it would not. Under the Proxy
we switch off the arbitrary-rank thing. Try it today! (The proposals doesn't change the behaviour of type signatures.
Would that count as impredicative?
I think we have decided that behaviour never changes when type synonyms are expanded; and have already gone to some trouble to make this so (in a recent ticket). So yes it would be impredicative, and would (or should) be caught.
comment:6 Changed 10 months ago by
I tried your suggestion in comment:3, and unfortunately, impredicativity does sneak in, as the following is accepted:
{-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints, FlexibleInstances, UndecidableInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} module Bug where import Data.Kind import Data.Proxy type F1 (f :: * -> *) = forall a. Eq (f a) class (Functor f, F1 f) => C f instance (Functor f, F1 f) => C f type F2 f = (Functor f, F1 f) f :: (Proxy (F2 f) ~ Proxy (F2 f)) => Int f = 42
On the other hand, the following variant:
g :: (Proxy (Functor f, forall a. Eq (f a)) ~ Proxy (Functor f, forall a. Eq (f a))) => Int g = 42
Is rejected as impredicative. (It's possible that this is just #16059 manifesting in a different way, though.)
comment:7 Changed 10 months ago by
comment:8 Changed 10 months ago by
Blocked By: | 16059 added |
---|
comment:9 Changed 10 months ago by
Blocked By: | 16059 removed |
---|
comment:10 Changed 10 months ago by
The good news is that #16059 has been fixed. The downside is that I just discovered that the only reason that I managed to get the program in this ticket to work (after implementing the suggestion in comment:3) is because of #16059! That is to say, when I try implementing comment:3 now, GHC's improved type validity-checker now rejects the program in this ticket. Bummer.
It looks like calling check_pred_ty
isn't enough—there must be something deeper that needs to be changed.
comment:11 Changed 10 months ago by
For reference, here is why check_pred_ty
rejects the program in this ticket under the new-and-improved type validity-checker. We start with this type:
(Functor f, F1 f)
check_pred_ty
calls check_ty
, at which point we discover that this type is headed by a constraint tuple type constructor, so we call check_arg_type
on each of its arguments. As a consequence, we switch the ve_rank
in the ValidityEnv
to tyConArgMonoType
. We eventually check F1 f
and, in turn, check forall a. Eq (f a)
using check_type
(if we were using the old type validity-checker, we would have stopped at F1 f
!).
Since forall a. Eq (f a)
is a polytype, we must check it using forAllAllowed ve_rank
. But our ve_rank
is still tyConArgMonoType
, and forAllAllowed
returns False
for MonoType
s! So GHC ultimately decides to reject it.
What can be done about this? One conceivable route is to add a special case to check_type
for applications of constraint tuple type constructors and, if so, don't call check_arg_type
and instead call some other function which ensures that ve_rank
is permissive enough to handle polytypes. There is precedent for this already—see check_ubx_tuple
.
On the other hand, I don't think this would fix the problem entirely. The issue is that we want to accept this:
f :: (Functor f, forall a. Eq (f a)) => Int
While simultaneously rejecting this:
g :: Proxy (Functor f, forall a. Eq (f a)) -> Int
But in both cases, forall a. Eq (f a)
is directly underneath an application of a constraint tuple tycon, so if we always switch ve_rank
to something permissive whenever we detect an application of a constraint tuple tycon, then I believe that GHC would accept both programs, which isn't what we want. I think that we a finer-grained criterion than this, but I'm not sure what that would be...
comment:12 Changed 10 months ago by
At the moment we call check_pred_ty
in exactly two situations:
- On each element of the context of a type built with
=>
, such asforall a. (Eq a, Show a) => blah
- On the RHS of a type synonym whose RHS kind is
Constraint
.
Your example g :: Proxy (Functor f, forall a. Eq f a) -> Int
is neither of these, so none of the check_pred_ty
stuff will happen; and indeed it should not.
Notice the difference between (1) and (2). In (1) we call check_pred_ty
on each element of the context; in (2) we call check_pred_ty
on the entire RHS. If the entire RHS is (c1, c2)
we will not call check_pred_ty
on c1
and c2
. But if we want to treat the two the same, we probably should.
Now, check_pred_ty
currently works like this:
check_pred_ty env dflags ctxt expand pred = do { check_type ve pred ; check_pred_help False env dflags ctxt pred }
First we call ordinary check_type
; then we make extra checks. That's already a bit odd: why look at pred
twice?
Moreover, the firset thing we do in the "extra checks" is to call classifyPredType
which has a case just for constraint tuples.
So the obvious path is this: move the check_type
stuff into check_pred_help
. So checkPred
would look something like this:
check_pred_ty ve dflags ctxt expand pred = go False pred where rank = ..as now.. ve = ..as now.. go under_syn pred | Just pred' <- tcView pred -- As now = go True pred' go under_syn pred = case classifyPredType pred of EqPred rep t1 t2 -> check_eq_pred ve rep t1 t2 ClassPred cls tys | isCTupleClass cls -> check_tuple_pred under_syn ve pred tys | otherwise -> check_class_pred ve pred cls tys ..etc.. -- Notice that check_eq_pred checks the complete predicate -- including the validity of t1 and t2 check_eq_pred ve rep t1 t2 = do { check_arg_type ve t1 ; check_arg_type ve t1 ; checkTcM (rep == ReprEq || xopt LangExt.TypeFamilies dflags || xopt LangExt.GADTs dflags) (eqPredTyErr env pred) } check_tuple_pred under_syn ve pred tys = do { mapM_ check_pred tys -- <------------------- Aha! use check_pred here! ; ..then as now.. }
This will fix another current bug, namely:
f :: (Eq a, (Show a, forall b. Eq (f b), Ord a) => blah
This has a nested constraint tuple, and will currently be rejected. But it should not be.
comment:13 Changed 10 months ago by
Thanks for the very detailed advice. After implementing the plan in comment:12, the original program in this ticket is now accepted. But we're not out of the woods yet, since several test cases now topple over. I'll try to summarize the issues below:
- Certain programs no longer need
QuantifiedConstraints
to typecheck, even though they should. For instance, this typechecks:
{-# LANGUAGE RankNTypes #-} module Bug where f :: (forall a. Eq a) => Int f = 42
Likely reason: the place where we check if
QuantifiedConstraints
is enabled (checkTcM (forAllAllowed rank)
incheck_type
) is no longer reachable fromcheck_pred_ty
, since it no longer invokescheck_type
.
Similarly, it's now possible to sneak impredicativity into constraints, as the following program is now accepted, even though it shouldn't be:
{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE RankNTypes #-} module Bug where f :: Num (forall a. a) => Int f = 42
TypeApplications
now require language extensions that they didn't before. For instance, theT12447
test case used to be work:
ghci> :set -XRankNTypes -XConstraintKinds -XTypeApplications ghci> deferEither @(_ ~ _)
Now, it produces the following error:
+ +<interactive>:1:1: + Illegal equational constraint _0 ~ _1 + (Use GADTs or TypeFamilies to permit this) + In the expression: deferEither @(_ ~ _) *** unexpected failure for T12447(ghci)
Depending on one's perspective, this might be a desirable outcome. But it is a break from convention, so it's worth noting.
Another example from the
TypeRep
test case:
Compile failed (exit code 1) errors were: [1 of 1] Compiling Main ( TypeRep.hs, TypeRep.o ) TypeRep.hs:41:11: error: • Non type-variable argument in the constraint: Eq Int (Use FlexibleContexts to permit this) • In the second argument of ‘($)’, namely ‘rep @((Eq Int, Eq String) :: Constraint)’ In a stmt of a 'do' block: print $ rep @((Eq Int, Eq String) :: Constraint) In the expression: do print $ rep @String print $ rep @Char print $ rep @Int print $ rep @Word .... *** unexpected failure for TypeRep(normal)
comment:14 Changed 10 months ago by
Certain programs no longer need QuantifiedConstraints to typecheck, even though they should
Aha! That is easily dealt with. Now predicates have their own validity checker, check_pred_ty
. So we can put the quantified-constraint check in the ForAllPred
branch of the classifyPredType
case analysis; and nowhere else. We don't need to monkey with the rank anymore!
comment:15 follow-up: 16 Changed 10 months ago by
TypeApplications now require language extensions that they didn't before.
This one is more mysterious to me.
- The arguments to a VTA is checked with
checkValidType
(seeTcHsType.tcHsTypeApp
). checkValidType
usescheck_type
, notcheck_pred_ty
.
So how come we end up in check_pred_ty
? I don't think we want to; e.g. Eq Int
is a perfectly fine instantiation.
comment:16 Changed 10 months ago by
Replying to simonpj:
checkValidType
usescheck_type
, notcheck_pred_ty
.
I'm confused—didn't you say (in comment:3) that checkValidType
should use check_pred_ty
for Constraint
-kinded things? (Now that I think about it, this is exactly why these errors are popping up—VTA simply didn't go down the check_pred_ty
path before.)
comment:17 Changed 10 months ago by
I'm confused—didn't you say (in comment:3) that checkValidType should use check_pred_ty for Constraint-kinded things?
Yes I did, but that's not what has been implemented! Nor should it be, I think.
comment:12 (at the top) says exactly when check_pred_ty
is used.
comment:18 Changed 10 months ago by
My apologies, I didn't realize that you were implying that we should no longer implement the suggestion in comment:3. But calling check_pred_ty
(instead of check_type
) from checkValidType
is the only reason that the original program in this ticket is accepted! If you don't do that, then we're right back where we started:
../Bug.hs:7:1: error: • Illegal polymorphic type: forall a. Eq (f a) GHC doesn't yet support impredicative polymorphism • In the expansion of type synonym ‘F1’ In the type synonym declaration for ‘F2’ | 7 | type F2 f = (Functor f, F1 f) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The problem is that for type synonym RHSes, we call both checkValidType
and checkTySynRHS
on them (in this code):
| Just syn_rhs <- synTyConRhs_maybe tc -> do { checkValidType syn_ctxt syn_rhs ; checkTySynRhs syn_ctxt syn_rhs }
As a result, we end up calling both check_type
and check_pred
on (Functor f, F1 f)
, and check_type
ends up rejecting it for being "impredicative". Do you think we'd be better off not calling checkValidType
here?
comment:19 Changed 10 months ago by
Do you think we'd be better off not calling checkValidType here?
Yes! If we are going to have checkTySynRhs
at all, then we should do all the work there.
This is the commit that added checkTySynRhs
.
commit 35c9de7ca053eda472cb446c53bcd2007bfd8394 Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Sat Jun 11 23:56:42 2016 +0100 Move the constraint-kind validity check For type synonyms, we need to check that if the RHS has kind Constraint, then we have -XConstraintKinds. For some reason this was done in checkValidType, but it makes more sense to do it in checkValidTyCon. I can't remember quite why I made this change; maybe it fixes a Trac ticket, but if so I forget which. But it's a modest improvement anyway.
But calling both makes no sense.
comment:20 Changed 9 months ago by
Sorry if I'm talking about a different bug, but I think this may be a regression. The original reproducer is rejected by GHC 8.6.3 too, but if you build Cabal (the library) with GHC HEAD at some point you get this error:
$ head.hackage.sh init-local $ cabal new-build --enable-benchmarks --enable-tests --allow-newer=base,template-haskell,tagged ... [211 of 220] Compiling Distribution.Simple.PreProcess ( Distribution/Simple/PreProcess.hs, dist/build/Distribution/Simple/PreProcess.o ) Distribution/Simple/PreProcess.hs:697:24: error: • Illegal qualified type: GHC.Stack.Types.HasCallStack => ghc-prim-0.5.3:GHC.Types.IO [FilePath] GHC doesn't yet support impredicative polymorphism • In the expansion of type synonym ‘WithCallStack’ In the expansion of type synonym ‘IO’ In the expansion of type synonym ‘PreProcessorExtras’ | 697 | knownExtrasHandlers :: [ PreProcessorExtras ] | ^^^^^^^^^^^^^^^^^^^^^^ cabal: Failed to build Cabal-2.4.1.0 (which is required by exe:ppsh from pretty-show-1.6.16 and cabal-install-2.5.0.0). See the build log above for details.
This builds fine with GHC 8.6.3.
comment:21 Changed 9 months ago by
This has nothing to do with this ticket, but rather #16059. Moreover, this is expected behavior—the fix for #16059 revealed an illegal use of impredicativity in Cabal-2.4.1.0
that previously went unnoticed (see the discussion starting at ticket:16059#comment:14). The current version of Cabal
that is bundled with GHC HEAD, Cabal-2.5.0.0
, fixes this issue.
tl;dr You want to use Cabal-2.5.0.0
, not Cabal-2.4.1.0
.
This is an interesting question. When written to the left of an
=>
, the parentheses delimit a list that is inlined. However, in a type synonym, you're really building a tuple. So GHC's behavior here is just a manifestation of this internal design... but the design shouldn't leak this way.I would classify it as a bug, yes. It's unclear to me how to solve it, though, especially because GHC struggles to tell constraint tuples apart from normal ones.