Opened 8 months ago

Last modified 7 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 8 months ago 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.

comment:2 Changed 8 months ago by RyanGlScott

Keywords: QuantifiedConstraints ImpredicativeTypes added

comment:3 Changed 8 months ago 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?

comment:4 in reply to:  3 Changed 8 months ago 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?
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?

comment:5 Changed 8 months ago 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.

comment:6 Changed 8 months ago by RyanGlScott

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 8 months ago by simonpj

It's possible that this is just #16059 manifesting in a different way, though.

Sounds likely to me. And we have a plan for #16059, in comment:4.

comment:8 Changed 8 months ago by RyanGlScott

Blocked By: 16059 added

comment:9 Changed 8 months ago by RyanGlScott

Blocked By: 16059 removed

comment:10 Changed 8 months ago 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.

comment:11 Changed 8 months ago 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:

(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 MonoTypes! 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 8 months ago 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.

comment:13 Changed 8 months ago 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:
{-# 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:

{-# 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)

comment:14 Changed 8 months ago by simonpj

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 Changed 8 months ago 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.

comment:16 in reply to:  15 Changed 8 months ago by RyanGlScott

Replying to 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.)

comment:17 Changed 8 months ago 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.

comment:18 Changed 8 months ago 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_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?

Last edited 8 months ago by RyanGlScott (previous) (diff)

comment:19 Changed 8 months ago 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 <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 7 months ago 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.

comment:21 Changed 7 months ago 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 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.

Last edited 7 months ago by bgamari (previous) (diff)
Note: See TracTickets for help on using tickets.