Opened 19 months ago

Last modified 7 months ago

#14860 new bug

QuantifiedConstraints: Can't quantify constraint involving type family

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.5
Keywords: QuantifiedConstraints Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #16123 Differential Rev(s):
Wiki Page:

Description

This program fails to typecheck using the wip/T2893 branch, to my surprise:

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

import Data.Proxy

type family   Apply (f :: * -> *) a
type instance Apply Proxy a = Proxy a

data ExTyFam f where
  MkExTyFam :: Apply f a -> ExTyFam f

instance (forall a. Show (Apply f a)) => Show (ExTyFam f) where
  show (MkExTyFam x) = show x
  showsPrec = undefined -- Not defining these leads to the oddities observed in
  showList = undefined  -- https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32

test :: ExTyFam Proxy -> String
test = show

This fails with:

$ 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:17:24: error:
    • Could not deduce (Show (Apply f a)) arising from a use of ‘show’
      from the context: forall a. Show (Apply f a)
        bound by the instance declaration at Bug.hs:16:10-57
    • In the expression: show x
      In an equation for ‘show’: show (MkExTyFam x) = show x
      In the instance declaration for ‘Show (ExTyFam f)’
   |
17 |   show (MkExTyFam x) = show x
   |                        ^^^^^^

I would have expected the (forall a. Show (Apply f a)) quantified constraint to kick in, but it didn't.

Change History (26)

comment:1 Changed 19 months ago by simonpj

Remember, a quantified constraint is a bit like a local instance declaration. We don't allow

instance C (F a) where ...

where F is a type function; and no more should we allow

forall a. Show (Apply f a)

as a quantified constraint (Apply is a type function).

It's a bug that I do not reject it.

This works

type family   Apply (f :: * -> *) :: * -> *
type instance Apply Proxy = Proxy

instance (t ~ Apply f, forall a. Show (t a)) => Show (ExTyFam f) where

It's tiresome to lift the family application out, but it forces you to ensure that the instance head is ok.

Do you agree?

comment:2 Changed 19 months ago by RyanGlScott

I mean, that technically works, but you're cheating a little, as you're changing the definition of Apply. In the code that I actually want to write, such a transformation is impossible, since I need to be able to use the last argument of Apply in its definition.

In any case, I don't see why this type-families-in-instance restriction need apply here. I can certainly see why we'd rule out:

instance C (F a) where ...

As a top-level instance. However, as a quantified constraint:

forall a. Show (Apply f a)

This should be acceptable. Whenever you _use_ this constraint, it certainly must be the case that we reduce this to something that is type-family–free. This is why this would work:

test :: ExTyFam Proxy -> String
test = show

Since we would be able to reduce forall a. Show (Apply Proxy a) to forall a. Show (Proxy a), which has no type families. (If that weren't the case, then I'd certainly expect GHC to error.)

Does that make sense? This is exactly along the same vein as previous generalizations brought about due to quantified constraints. After all, we don't allow this as a top-level instance:

instance Show a => c (F a)

But we do allow this to appear as a quantified constraint (when we use it, it must be the case that this turns into something with an actual class for c). This proposed generalization fits into that tradition.

comment:3 Changed 19 months ago by simonpj

But the error is at line 17, where we don't know f and cannot reduce Apply f a. So we really do have a local instance

local instance forall a. Show (Apply f a)

You might argue that we should use it to solve Show (Apply f Int) or any other instantiation, but we don't. Because we don't expect type functions in instance heads.

(And BTW it's possible that Show (Apply f Int) might reduce to Show Bool and we'd be stuck.

comment:4 in reply to:  3 Changed 19 months ago by RyanGlScott

Replying to simonpj:

(And BTW it's possible that Show (Apply f Int) might reduce to Show Bool and we'd be stuck.

So? If we ever use this instance an get Show Bool, then reject that use site! Just as you would reject if you tried to use an instance that had a quantified constraint (forall xx. c (Free c xx)) and you tried to instantiate c with, say, Show, and there is no Show (Free Show xx) instance.

You keep muttering about "we don't expect type functions in instance heads". I would qualify that statement to "we don't expect type functions in top-level instance heads"—there shouldn't be anything problematic about allowing them in quantified constraints!

comment:5 Changed 19 months ago by simonpj

there shouldn't be anything problematic about allowing them in quantified constraints!

But I think there absolutely IS something problematic! At least I have no idea how to specify or implement a system that allows them. Maybe I'm just being dense.

comment:6 Changed 19 months ago by goldfire

I'm struggling with this one, worried about order-dependence. Suppose Apply f Int is Bool. Now suppose we are given forall a. Show (Apply f a) and want to prove Show (Apply f Int). In considering the wanted Show (Apply f Int), we have two choices of how to proceed:

  1. Use the given and succeed.
  1. Reduce Apply f Int to Bool and fail.

The problem is that it seems challenging to guarantee that we don't do (2). Simon's answer appears to be to simply disallow the constraint in the first place.

comment:7 Changed 19 months ago by RyanGlScott

In response to goldfire's question, let me ask an analogous one. Currently, we allow this:

instance (forall xx. c (Free c xx)) => Monad (Free c) where
    Free f >>= g = f g

Also, assume there is no Show (Free Show xx) instance. Now suppose we are given (forall xx. c (Free c xx)), and we want to prove Show (Free Show xx). In considering the wanted Show (Free Show xx), we have two choices of how to proceed:

  1. Use the given and succeed.
  2. Attempt to resolve the Show (Free Show xx) instance and fail.

The exact same problem seems to arise here, so why isn't this disallowed?

comment:8 Changed 19 months ago by RyanGlScott

Indeed, GHC appears to have no trouble with this:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Control.Monad

newtype Free cls a = Free (forall xx. cls xx => (a -> xx) -> xx)

instance Functor (Free cls)
instance Applicative (Free cls)

instance (forall xx. cls (Free cls xx)) => Monad (Free cls) where
  Free f >>= g = f g

f :: Free Show (Free Show a) -> Free Show a
f = join
Bug.hs:18:5: error:
    • No instance for (Show (Free Show xx))
        arising from a use of ‘join’
    • In the expression: join
      In an equation for ‘f’: f = join
   |
18 | f = join
   |     ^^^^

Here, we reject the use site, not the instance.

comment:9 Changed 19 months ago by Iceland_jack

Cc: Iceland_jack added

comment:10 Changed 19 months ago by simonpj

Re comment:7 there are no type functions are there. It's the function in the constraint head that is the nub of the problem.

comment:11 in reply to:  10 ; Changed 19 months ago by RyanGlScott

Replying to simonpj:

Re comment:7 there are no type functions are there. It's the function in the constraint head that is the nub of the problem.

Again... so what? I'm trying to demonstrate why hypothetically allowing type families in quantified constraints would be no different than allowing type variables heading instances in quantified constraints. So far, the only rebuttal you've given me is "but we don't allow type families in instances", which is circular reasoning. So I'm still left wondering what exactly the substantive difference between these two scenarios is.

comment:12 Changed 19 months ago by simonpj

A skolem type variable is just like a type constructor. It is equal to itself, nothing else.

A type function application stands for what it reduces to. It's not a rigid thing you can match against when matching in instances or type-family definitions. We don't allow

type instance F (G a) = [a]

Why not? Because the call F (G Int) would match the type instance -- but could also reduce to something that wouldn't match it any more, which would be terrible.

In contrast, skolem type variables have no such difficulty.

comment:13 Changed 19 months ago by RyanGlScott

Resolution: wontfix
Status: newclosed

comment:14 Changed 19 months ago by Iceland_jack

These problems were my original motivation for #14822, if f has a singleton we can witness Show (Apply f a) without changing the definition of Apply

wit :: forall f a. SingI f :- Show (Apply f a)
wit = Sub
  (case sing :: Sing f of
    SingProxy -> Dict)

If we had a way of turning (a :- b) into (a => b) I think this would solve Ryan's problem?

comment:15 in reply to:  11 Changed 18 months ago by Iceland_jack

Replying to RyanGlScott: I don't think you need quantified constraints (the ticket:14822#comment:3 trick does works to solve my previous comment), how about this:

instance Typeable f => Show (ExTyFam f) where
  show (MkExTyFam x)
    | Just HRefl <- typeRep @f `eqTypeRep` typeRep @(Proxy :: Type -> Type)
    = show x
    | otherwise
    = ..

comment:16 Changed 18 months ago by Iceland_jack

Here an actual solution (detailed in gist):

data ExTyFam :: (Type -> Type) -> Type where
  MkExTyFam :: Proxy a -> Apply f a -> ExTyFam f

class    Show (Apply f a) => ShowApply f a
instance Show (Apply f a) => ShowApply f a

instance (forall xx. ShowApply f xx) => Show (ExTyFam f) where
  show (MkExTyFam (Proxy :: Proxy a) fa) = go @a Dict fa where

    go :: forall x. Dict (ShowApply f x) -> Apply f x -> String
    go Dict = show

edit: another solution, wrapping it in a newtype

newtype ApplyNT f a = MkApplyNT (Apply f a)

deriving newtype
  instance Show (Apply f a) => Show (ApplyNT f a)

and then we can quantify over instance (forall xx. ApplyNT f xx) => Show (ExTyFam f)

Last edited 12 months ago by Iceland_jack (previous) (diff)

comment:17 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed

comment:18 Changed 10 months ago by edsko

This is all rather unfortunate. I'd like to be able to write

class (forall b. Show b => Show (T a b)) => C a where
  type family T a :: * -> *

data D a = MkD (T a Int)

deriving instance C a => Show (D a)

but cannot. @simonpj writes:

"Remember, a quantified constraint is a bit like a local instance declaration. We don't allow instance C (F a) where ... where F is a type function; and no more should we allow forall a. Show (Apply f a) as a quantified constraint".

But then why can I write

class (Show (T a)) => C a where
  type family T a :: *

data D a = MkD (T a)

deriving instance C a => Show (D a)

Shouldn't by the same reasoning this fail to work also? (Please don't make it fail though! :-D ) (Yes, it's not quantified, but it's "trivially quantified"; it feels strange to me to allow one but not the other.)

Note that for this kind of use case there is no easy workaround; as https://ghc.haskell.org/trac/ghc/ticket/15347#comment:15 points out, it involves adding new type variables to the class, kind of defeating the purpose of having type families in the first place. (Not to mention that I have a bunch of these type families in my real example.)

Last edited 10 months ago by edsko (previous) (diff)

comment:19 Changed 10 months ago by simonpj

This is tricky in an interesting way.

What is the problem with quantified constraints with a type-function in the head? Consider

f :: (forall a. C a => C (F a)) => ...

where F is a type family. We really, really can't handle this. Suppose we have

type instance F [b] = (b,b)

and we are trying to solve C (t,t) in f's RHS. Well that's the same as C (F [t]) and lo, now the quantified constraint matches.

It would be utterly different if we had

f :: C (F a) => ...
f = ...needs (C (F a))...

where the two constraints are patently equal; and it'd be equally fine if we had an enclosing constraint (from a GADT, say) telling us a ~ [b]. Then we'd rewrite both the "given" and the "wanted" to C (F [b]), and if that in turn rewrites to C (b,b) then both will so rewrite. It's all fine.

The trouble in the earlier example comes because F is applied to a quantified variable. Here's another example it is, by comparison, fine:

type family F2 a :: * -> *
f2 :: (forall b. C b => C (F2 x b)) => blah

Notice that F2 has arity 1. And notice that the saturated application (F2 x) does not mention the quantified variable b. So we could rewrite the signature thus:

f2a :: (y ~ F2 x, forall b. C b => C (y b)) => blah

This is fine, and it is accepted today. By binding F2 x to y outside the quantification we have shown that the problems described above (about F) can't happen.

Alas, f2 is not accepted today. Until today I thought that once could always rewrite in the f2a style, and that it would be positively good to do so. That's what comment:1 says.

But today you have shown me a counter example. I cannot apply that trick to

class (forall b. Show b => Show (T a b)) => C a where
  type family T a :: * -> *

I might try

class (y ~ T a, forall b. Show b => Show (y b)) => C a where
  type family T a :: * -> *

But now y is not bound in the class head, and we just don't allow that. (Why not? Because a class turns into a data type declaration

data C a = MkC (..superclass1..)
               (..superclass2..)  etc
               (..method1..)
               (..method2..)  etc

so the superclass types can't mention variables not bound on the left. No we do not want existentials here.)

So I am driven to the conclusion:

  • Perhaps we should allow type-family applications in the head of a quantified constraint, provided that the saturated application of the family does not mention any of the quantified variables.

The flattener would have to work a bit harder. Richard, what do you think?

Thanks for the example.

comment:20 Changed 10 months ago by goldfire

I agree with comment:19. Depending on how you read it, the rule is this:

  • You cannot mention locally quantified variables in the arguments to a type family.

where "locally quantified" is meant to refer to the quantification in a quantified constraint. My "depending on how you read it" is about the fact that b isn't really an argument to type family T in T a b. Instead, a is the only argument to T, and b is an argument to the reduct of T a. This is pedantic, but I think it's a healthy way to understand what's going on.

I also want to back Simon up in his refusal to allow locally quantified variables in arguments to type families: the problem is all about backtracking. See my comment:6, which spells trouble.

I don't think the more nuanced rule described in comment:19 and here will be hard to implement. The flattener already treats the a and b in T a b quite differently. See the difference between flatten_fam_app and flatten_exact_fam_app_fully. The former takes T a b and decomposes to pass only T a to the latter.

comment:21 Changed 10 months ago by simonpj

Resolution: wontfix
Status: closednew

Reopening because comment:19 and comment:20 point to a way forward.

comment:22 Changed 9 months ago by RyanGlScott

See #16123 for an example of a program which cannot work without the flattener receiving the upgrade described in comment:19.

comment:23 Changed 8 months ago by RyanGlScott

I've discovered a way to work around the issue in comment:18. This is the instance we are trying to write:

class (forall b. Show b => Show (T a b)) => C a where
  type family T a :: * -> *

This doesn't work because the head of that quantified constraint mentions T, which is a type family. The normal trick is to add an extra constraint ta ~ T a and change the head of the quantified constraint to Show (ta b). But where do we quantify ta?

The answer to this question eluded me for the longest time, but it turns out the answer is shockingly simple: just quantify ta in the quantified constraint itself! That is to say, just do this:

class (forall ta b. (ta ~ T a, Show b) => Show (ta b)) => C a where
  type family T a :: * -> *

That's it! Now the instance typechecks, just like we've always dreamed of. I've tried this trick out on a large codebase that makes heavy use of quantified superclasses of this form, and it appears to work remarkably well.

comment:24 Changed 8 months ago by simonpj

Hmm. Well, please note that this quantified constraint will fire on a constraint like Show (Maybe Int) Why? Because we can instantiate Show (ta b) to give (Show (Maybe Int). So the quantified constraint overlaps with the top-level instance; but quantified constraints are tried (currently) before top-level instances, so the quantified constraint will "win". That might lead you to try to solve (Maybe ~ T a) which will probably fail.

Perhaps in the applications you have in mind this will be fine. And if so, that's great. But I just wanted to point out that there might be unintended consequence.

comment:25 Changed 8 months ago by RyanGlScott

Yes, I think I was a bit too bold in declaring comment:23 to be a viable workaround (in fact, I'm now discovering places in the aforementioned large codebase where this technique breaks down).

A much uglier (but likelier to work in the long run) hack is to add another parameter to C:

class (forall b. (ta ~ T a, Show b) => Show (ta b)) => C a ta where
  type family T a :: * -> *

data D a = MkD (T a Int)
deriving instance (ta ~ T a, C a ta) => Show (D a)

comment:26 Changed 7 months ago by RyanGlScott

Out of all the workarounds documented on this issue, I somehow overlooked the best one: Iceland_jack's solution in comment:16 involving Dicts. This offers a general blueprint to how to sneak type families into quantified constraints in the event that the trick in comment:1 doesn't work.

In the particular example of comment:18, we wish to use Show (T a b) in the head of a quantified constraint. While this isn't directly possible, we can define a "class newtype" around Show (T a b) and use that in the head of a quantified constraint:

class    Show (T a b) => ShowT a b
instance Show (T a b) => ShowT a b

class (forall b. Show b => ShowT a b) => C a where
  type family T a :: * -> *

If we try to define a Show instance for D, it first appears as though we are stuck:

data D a = MkD (T a Int)

instance C a => Show (D a) where
  showsPrec p (MkD x)
    = showParen (p > 10) $ showString "MkD " . showsPrec 11 x
Bug.hs:35:48: error:
    • Could not deduce (Show (T a Int))
        arising from a use of ‘showsPrec’
      from the context: C a
        bound by the instance declaration at Bug.hs:33:10-26
    • In the second argument of ‘(.)’, namely ‘showsPrec 11 x’
      In the second argument of ‘($)’, namely
        ‘showString "MkD " . showsPrec 11 x’
      In the expression:
        showParen (p > 10) $ showString "MkD " . showsPrec 11 x
   |
35 |     = showParen (p > 10) $ showString "MkD " . showsPrec 11 x
   |                                                ^^^^^^^^^^^^^^

GHC appears to be unable to conclude Show (T a Int) from ShowT a Int. But we can help guide GHC along manually by taking advantage of the ever-helpful Dict data type:

data Dict c =
  c => Dict

showTDict :: forall a b. Dict (ShowT a b) -> Dict (Show (T a b))
showTDict Dict = Dict

Using showTDict, we can make our Show instance for D compile with a pinch of pattern guards:

instance C a => Show (D a) where
  showsPrec p (MkD x)
    | Dict <- showTDict @a @Int Dict
    = showParen (p > 10) $ showString "MkD " . showsPrec 11 x

That's it! With enough persistence, we were able to finally realize edsko's dream in comment:18. Having to explicitly match on Dicts is a bit crude, granted, but this appears to be the best that we can do here at the moment.

Note: See TracTickets for help on using tickets.