[GHC] #14860: QuantifiedConstraints: Can't quantify constraint involving type family
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints wipT2893 | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This program fails to typecheck using the `wip/T2893` branch, to my surprise: {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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): 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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 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: {{{#!hs instance C (F a) where ... }}} As a top-level instance. However, as a quantified constraint: {{{#!hs 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: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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:3 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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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):
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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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): 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. 2. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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): In response to goldfire's question, let me ask an analogous one. Currently, we allow this: {{{#!hs 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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): Indeed, GHC appears to have no trouble with this: {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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 Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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:10 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 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): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: wontfix | QuantifiedConstraints wipT2893 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): * status: new => closed * resolution: => wontfix -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: wontfix | QuantifiedConstraints wipT2893 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 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` {{{#!hs 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: wontfix | QuantifiedConstraints wipT2893 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 Iceland_jack): Replying to [comment:11 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: {{{#!hs instance Typeable f => Show (ExTyFam f) where show (MkExTyFam x) | Just HRefl <- typeRep @f `eqTypeRep` typeRep @(Proxy :: Type -> Type) = show x | otherwise = .. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: wontfix | QuantifiedConstraints wipT2893 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 Iceland_jack): An example, from [https://www.microsoft.com/en-us/research/wp- content/uploads/2016/02/jfp-outsidein.pdf OutsideIn(X)] (**2.4**), this function {{{#!hs h :: forall a. (forall b. FB a b ~ Bool) => Bar a -> Bool }}} Details in [https://gist.github.com/Icelandjack/aeda8e98214cc52c96230af7b8724d25 gist]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: wontfix | QuantifiedConstraints 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 edsko): This is all rather unfortunate. I'd like to be able to write {{{#!hs 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 {{{#!hs class (Show (T a)) => C a where type family T a :: * data D a = MkD (T a) -- Could not deduce (Show (T a Int)) -- arising from a use of ‘showsPrec’ 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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: wontfix | QuantifiedConstraints 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 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: wontfix | QuantifiedConstraints 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): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints 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 simonpj): * status: closed => new * resolution: wontfix => Comment: Reopening because comment:19 and comment:20 point to a way forward. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #16123 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #16123 Comment: See #16123 for an example of a program which cannot work without the flattener receiving the upgrade described in comment:19. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #16123 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I've discovered a way to work around the issue in comment:18. This is the instance we are trying to write: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #16123 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #16123 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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`: {{{#!hs 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) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #16123 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 `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: {{{#!hs 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: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC