[GHC] #16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley | Owner: (none) Yakeley | Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => QuantifiedConstraints, ImpredicativeTypes -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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 is `Constraint`, then use `check_pred_ty` rather than `check_type`. Do you agree? Would you like to try that? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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? {{{#!hs 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 needing `ImpredicativeTypes`) and later try to define `g :: Proxy (F2 Maybe); g = Proxy`. Would //that// count as impredicative? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I tried your suggestion in comment:3, and unfortunately, impredicativity //does// sneak in, as the following is accepted: {{{#!hs {-# 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: {{{#!hs 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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
It's possible that this is just #16059 manifesting in a different way,
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): though. Sounds likely to me. And we have a plan for #16059, in comment:4. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: 16059 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * blockedby: => 16059 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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: {{{#!hs (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: {{{#!hs f :: (Functor f, forall a. Eq (f a)) => Int }}} While simultaneously rejecting this: {{{#!hs 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... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): At the moment we call `check_pred_ty` in exactly two situations: 1. On each element of the context of a type built with `=>`, such as `forall a. (Eq a, Show a) => blah` 2. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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: {{{#!hs {-# 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)` in `check_type`) is no longer reachable from `check_pred_ty`, since it no longer invokes `check_type`. Similarly, it's now possible to sneak impredicativity into constraints, as the following program is now accepted, even though it shouldn't be: {{{#!hs {-# 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, the `T12447` 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) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Certain programs no longer need QuantifiedConstraints to typecheck, even
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
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` (see `TcHsType.tcHsTypeApp`). * `checkValidType` uses `check_type`, not `check_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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:15 simonpj]:
* `checkValidType` uses `check_type`, not `check_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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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_ty`) 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 [https://gitlab.haskell.org/ghc/ghc/blob/a1e9cd6af8b41fa451fd3be806f4aced0040... this code]): {{{#!hs | 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
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
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by osa1): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints, | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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 https://ghc.haskell.org/trac/ghc/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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16140#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC