Opened 2 years ago
Last modified 12 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 2 years ago by
comment:2 Changed 2 years ago by
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 follow-up: 4 Changed 2 years ago by
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 Changed 2 years ago by
Replying to simonpj:
(And BTW it's possible that
Show (Apply f Int)
might reduce toShow 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 2 years ago by
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 2 years ago by
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:
- Use the given and succeed.
- Reduce
Apply f Int
toBool
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 2 years ago by
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:
- Use the given and succeed.
- 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 2 years ago by
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 2 years ago by
Cc: | Iceland_jack added |
---|
comment:10 follow-up: 11 Changed 2 years ago by
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 follow-up: 15 Changed 2 years ago by
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 2 years ago by
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 2 years ago by
Resolution: | → wontfix |
---|---|
Status: | new → closed |
comment:14 Changed 2 years ago by
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 Changed 22 months ago by
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 22 months ago by
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)
comment:17 Changed 20 months ago by
Keywords: | wipT2893 removed |
---|
comment:18 Changed 14 months ago by
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 allowforall 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.)
comment:19 Changed 14 months ago by
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 14 months ago by
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 14 months ago by
Resolution: | wontfix |
---|---|
Status: | closed → new |
Reopening because comment:19 and comment:20 point to a way forward.
comment:22 Changed 13 months ago by
Related Tickets: | → #16123 |
---|
See #16123 for an example of a program which cannot work without the flattener receiving the upgrade described in comment:19.
comment:23 Changed 12 months ago by
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 12 months ago by
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 12 months ago by
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 12 months ago by
Out of all the workarounds documented on this issue, I somehow overlooked the best one: Iceland_jack's solution in comment:16 involving Dict
s. 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 Dict
s is a bit crude, granted, but this appears to be the best that we can do here at the moment.
Remember, a quantified constraint is a bit like a local instance declaration. We don't allow
where
F
is a type function; and no more should we allowas a quantified constraint (
Apply
is a type function).It's a bug that I do not reject it.
This works
It's tiresome to lift the family application out, but it forces you to ensure that the instance head is ok.
Do you agree?