[GHC] #15351: QuantifiedConstraints ignore FunctionalDependencies
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following code fails to compile: {{{#!hs {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE FunctionalDependencies #-} class C a b | a -> b where foo :: a -> b bar :: (forall a. C (f a) Int) => f a -> String bar = show . foo }}} {{{ • Could not deduce (Show a0) arising from a use of ‘show’ ... The type variable ‘a0’ is ambiguous }}} Yet it ought to work, since this is perfectly fine with top-level instances: {{{#!hs instance C [a] Int where ... baz :: [a] -> String baz = show . foo }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Description changed by aaronvargo: Old description:
The following code fails to compile:
{{{#!hs {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE FunctionalDependencies #-}
class C a b | a -> b where foo :: a -> b
bar :: (forall a. C (f a) Int) => f a -> String bar = show . foo }}}
{{{ • Could not deduce (Show a0) arising from a use of ‘show’ ... The type variable ‘a0’ is ambiguous }}}
Yet it ought to work, since this is perfectly fine with top-level instances:
{{{#!hs instance C [a] Int where ...
baz :: [a] -> String baz = show . foo }}}
New description: The following code fails to compile: {{{#!hs {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE FunctionalDependencies #-} class C a b | a -> b where foo :: a -> b bar :: (forall a. C (f a) Int) => f a -> String bar = show . foo }}} {{{ • Could not deduce (Show a0) arising from a use of ‘show’ ... The type variable ‘a0’ is ambiguous • Could not deduce (C (f a) a0) arising from a use of ‘foo’ ... The type variable ‘a0’ is ambiguous }}} Yet it ought to work, since this is perfectly fine with top-level instances: {{{#!hs instance C [a] Int where ... baz :: [a] -> String baz = show . foo }}} -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Comment (by AntC): Your constraint for `bar` doesn't look well-formed to me. I'm surprised GHC accepted the `forall` without an implication `=>`. I guess what you've ended up with is some sort of impredication. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Comment (by goldfire): Quantified constraints do not need a constraint -- just a `forall` is fine. Though I can't swear to it, I do think the original program should be accepted. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:3 goldfire]:
Quantified constraints do not need a constraint -- just a `forall` is fine.
Then the github proposal's [https://github.com/Gertjan423/ghc- proposals/blob/quantified-constraints/proposals/0000-quantified- constraints.rst#id8 syntax changes] are wrongly described. (And the same text has gone into the Users guide.) The `=>` is the defining syntax for the extension; the `forall` is optional (although often needed in practice). @aaron, perhaps you could take out the `QuantifiedConstraints` flag (but put in `ExplicitForAll`) and try re-compiling. Does GHC complain you need to switch on the extension? (Sorry I can't try that from here.)
I do think the original program should be accepted.
Then what does it mean? At a guess: for some `f0` being the type constructor in an argument to `bar`, there's an `instance C (f0 a') Int`? Note that `a'` is quantified within the constraint, so is distinct from the `a1` argument to the constructor `f0`. There is no such instance declared, whereas for the `baz` example there is an `instance C [a] Int`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Comment (by goldfire): I've created #15354 about the documentation oversight -- you're absolutely right. I agree with your analysis in comment:4. By the constraint `forall a. C (f a) Int` (and the fundep), we know that any instance that begins with `C (f a)` ends with `Int`. Let's name different variables differently: {{{#!hs bar :: (forall b. C (f b) Int) => f a -> String bar = show . foo }}} So, since the usage of `foo` induces a `C (f a) alpha` constraint (for some unknown `alpha`) we can conclude that `alpha` must be `Int` by the fundep. Here is a related example, with the same `C`: {{{#!hs blah :: C Int Double => Int -> String blah = show . foo }}} This is accepted (even with no instances for `C`), because GHC can figure out that the result of `foo` must be `Double`. I don't see how quantified constraints should change that. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, you are right. Generally, when solving a constraint, GHC checks it against all in-scope instances in case there's fundep match. The same should happen for in-scope quantified constraints. Would anyone like to fix this? It's intriguing -- I never expected people to explore the outer limits of quantified constraints so rapidly. I hope that means that they are proving useful (when not so close to the limits). Is that so? Experience reports or blog posts (like Ryan Scott's) would be fascinating. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:5 goldfire]:
{{{#!hs bar :: (forall b. C (f b) Int) => f a -> String bar = show . foo }}}
So, since the usage of `foo` induces a `C (f a) alpha` constraint (for
some unknown `alpha`) we can conclude that `alpha` must be `Int` by the fundep.
Hmm (and accepting for the moment this is a legitimate `QuantifiedConstraint`). The OP doesn't include any `C` instance for the `f` in `bar` -- i.e. evidence for `C (f b) alpha`. Is that what the message `Could not deduce (C (f a) a0) arising from a use of ‘foo’` is saying? Is there another message the OP hasn't included `no instance for (C (f a) a0) ...`? The fact of the message saying ''deduce'' suggests it's trying to do apply some sort of implication?? Deduce what from what? (Simon's comment:6 that arrived as I was writing this doesn't explain what specifically GHC "checks it against" in this case.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Comment (by simonpj):
this doesn't explain what specifically GHC "checks it against" in this case
It's worth reading the original paper -- though alas I cannot find PDF online. Given {{{ class C a b | a -> b instance C Int Bool }}} if GHC finds a wanted constraint `[W] C Int t`, it compares it against all the top-level instances to see if the fist argument of `C` matches the one in the instance. It succeeds in this case, and emits a new Derived constraint `[D] t ~ Bool`. Quantified constraints behave very like top-level instances, so they too should be examined in this search. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Comment (by aaronvargo): Replying to [comment:6 simonpj]:
Would anyone like to fix this?
How difficult would it be? I might like to try, but I've never contributed to GHC before. I could see it being pretty simple since most of the logic should already exist for top-level instances, but I wouldn't know. And I might need some hand-holding...
It's intriguing -- I never expected people to explore the outer limits of quantified constraints so rapidly.
I would guess this is partly because we could already (somewhat painfully) manually represent such constraints with `Dict`s, so we already had some idea of what they might be useful for, and want them to be able to do everything we can do with `Dict`s (though that turns out to be unreasonable). I came across this particular issue while trying to work around #15347, but I'll write more about that on that ticket (at some point. Maybe after I can get my stupid example to work). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:6 simonpj]:
Yes, you are right.
Sorry to be dumb, but who is 'you' and which bit are they 'right' about?
It's worth reading the original paper
Yes I've pored over both your 2000 paper with Ralf, and the hs 2017 more detailed logic. (Both linked from the github proposal.) I didn't see any examples without a `=>` implication; I didn't see any examples without any instances declared at all. And the github proposal didn't mention such possibilities either.
It's intriguing -- I never expected people to explore the outer limits of quantified constraints so rapidly. I hope that means that they are proving useful (when not so close to the limits). Is that so?
I think this extension is going to be huge -- and that was assuming the implications are needed. Experiments I will try when I get my hands on it: * subsuming quasi-injective logic {{{ class ( (b1 ~ True, b2 ~ True) => res ~ True, res ~ True => b1 ~ True, res ~ True => b2 ~ True, (res ~ False, b1 ~ True) => b2 ~ False, (res ~ False, b2 ~ True) => b1 ~ False ) => And (b1 :: Bool) (b2 :: Bool) ( res :: Bool) }}} * subsuming FunDeps {{{ class (forall b'. C a b' => b' ~ b) -- replicates GHC's "bogus" FD consistency check ref Trac #10675 => C a b where ... -- don't need | a -> b }}} (Is there any way to get a 'strict' after substitution `b'` equal type `b` consistency check?) * maybe subsuming overlap logic/apartness guards (of course more interesting uses than this example) {{{ class ( e ~ e' => d ~ Z, e /~ e' => d ~ (S d'), FindElem e l' d') => FindElemPosn e '( e' ': l' ) (d :: Nat) where ... }}} * field presence/absence for record extension/projection {{{ class ( (forall l a. HasField r1 l a => HasField r3 l a), (forall l a. HasField r2 l a => HasField r3 l a) ) => Merge r1 r2 r3 class ( (forall l a. HasField r3 l a => HasField r1 l a), (forall l a a'. (HasField r1 l a, HasField r2 l a') => HasField r3 l a), (forall l. Lacks r2 l => Lacks r3 l) ) => Project r1 r2 r3 }}} (Apologies for poaching on @aaron's ticket: you're welcome to try the above ideas.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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: | -------------------------------------+------------------------------------- Comment (by simonpj):
How difficult would it be?
The logic for top-level instances is in `TcInteract.doTopReactDict`: see `try_fundep_improvement`. You want to do something similar for the local quantified constraints. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | 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 Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC