[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
It's intriguing -- I never expected people to explore the outer limits of quantified constraints so rapidly. I hope that means that they are
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. 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