Opened 19 months ago

Closed 19 months ago

Last modified 16 months ago

#14861 closed bug (invalid)

QuantifiedConstraints: Can't use forall'd variable in context

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.5
Keywords: QuantifiedConstraints 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

This fails to typecheck, to my surprise:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind

data ECC1 :: (Type -> Constraint) -> (Type -> Type) -> Type -> Type where
  ECC1 :: c p => f p -> ECC1 c f p

class Foldable' f where
  foldMap' :: Monoid m => (a -> m) -> f a -> m

instance (forall p. c p => Foldable' f) => Foldable' (ECC1 c f) where
  foldMap' f (ECC1 x) = foldMap' f x

instance Foldable' [] where
  foldMap' = foldMap

test :: ECC1 Show [] Ordering -> Ordering
test = foldMap' id
$ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:18:25: error:
    • Could not deduce: c p0 arising from a use of ‘foldMap'’
      from the context: forall p. c p => Foldable' f
        bound by the instance declaration at Bug.hs:17:10-63
      or from: Monoid m
        bound by the type signature for:
                   foldMap' :: forall m a. Monoid m => (a -> m) -> ECC1 c f a -> m
        at Bug.hs:18:3-10
      or from: c a
        bound by a pattern with constructor:
                   ECC1 :: forall (f :: * -> *) p (c :: * -> Constraint).
                           c p =>
                           f p -> ECC1 c f p,
                 in an equation for ‘foldMap'’
        at Bug.hs:18:15-20
    • In the expression: foldMap' f x
      In an equation for ‘foldMap'’: foldMap' f (ECC1 x) = foldMap' f x
      In the instance declaration for ‘Foldable' (ECC1 c f)’
    • Relevant bindings include
        foldMap' :: (a -> m) -> ECC1 c f a -> m (bound at Bug.hs:18:3)
   |
18 |   foldMap' f (ECC1 x) = foldMap' f x
   |                         ^^^^^^^^^^^^

I would have expected the (forall p. c p => Foldable' f) quantified constraint to kick in there.

Change History (7)

comment:1 Changed 19 months ago by simonpj

I would have expected the (forall p. c p => Foldable' f) quantified constraint to kick in there.

Can you say why? We are trying to solve c beta. How does the quantified constraint help with that? It tells how to solve Foldable constraints.

comment:2 in reply to:  1 Changed 19 months ago by RyanGlScott

Replying to simonpj:

Can you say why?

When we pattern-match on ECC1, we bring into scope the given constraint c p0, where p0 is a fresh type variable. We have as a constraint:

(forall p. c p => Foldable' f)

GHC should be able to use the given c p0 constraint to discharge the obligation and conclude Foldable' f.

comment:3 Changed 19 months ago by simonpj

If I have

instance forall p. Show p => Show T

then when I invoke the instance declaration I get a Show beta constraint with absolutely nothing telling the compiler what beta should be. Yes, it could be solved with beta := Int or a variety of other things. But GHC never guesses.

Same here. You have

instance (forall p. c p => Foldable' f)  -- Yikes: nothing constrains p
       => Foldable' (ECC1 c f) where

When the quantified constraint fires, to solve Foldable' f, it generates c beta with no constraints whatsoever on beta. The fact that we have in scope c p does not help, because it requires quessing that beta := p. Sorry!

comment:4 Changed 19 months ago by RyanGlScott

I don't think we're talking about the same thing here. You're talking about solving beta := Int, but I'm not asking for that! After, if you had:

instance forall p. Show p => Show T

Then that forces GHC to be parametric in p (so trying to solve p := Int would certainly be nonsense).

Similarly, in:

instance (forall p. c p => Foldable' f)  -- Yikes: nothing constrains p
       => Foldable' (ECC1 c f) where

You put "Yikes: nothing constrains p" here, but that is intentional! The whole point is that this constraint must be parametric in p. Therefore, if we have a given constraint of the form c Int, then this certainly couldn't be used to discharge that quantified constraint.

However, the code I wrote should work, since the given constraint we have is c p0—this does not violate the parametricity of p, as p0 is simply a skolem.

comment:5 Changed 19 months ago by simonpj

No, p is not a skolem. Think of the quantified constraint like a local instance decl. It says

 local instance forall p. c p => Foldable' f

That means, if you want to solve Foldable' f (where f really is a skolem coming from the instance for Foldable' (ECC1 c f)), then

  • If you can solve c beta, where you are free to pick beta
  • then you can solve Foldable' f

So we have to guess beta. And we can't.

Try some top level instances with tyars on the left which don't appear on the right

instance C a => C [b]

comment:6 Changed 19 months ago by RyanGlScott

Resolution: invalid
Status: newclosed

Hm. Your point about instance C a => C [b] being wonky is a good one. In practice, such an instance would probably be OK if we could explicitly manipulate dictionaries and specify what exactly a should be whenever we applied it. But alas, we cannot, and GHC is unwilling to do this for us, so I'm forced to agree that this is in the realm of the impossible for the time being.

comment:7 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.