Opened 15 months ago

Last modified 11 months ago

#15351 new bug

QuantifiedConstraints ignore FunctionalDependencies

Reported by: aaronvargo 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: Differential Rev(s):
Wiki Page:

Description (last modified by aaronvargo)

The following code fails to compile:

{-# 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:

instance C [a] Int where ...

baz :: [a] -> String
baz = show . foo

Change History (12)

comment:1 Changed 15 months ago by aaronvargo

Description: modified (diff)

comment:2 Changed 15 months ago 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.

comment:3 Changed 15 months ago 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.

comment:4 in reply to:  3 Changed 15 months ago by AntC

Replying to goldfire:

Quantified constraints do not need a constraint -- just a forall is fine.

Then the github proposal's 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.

comment:5 Changed 15 months ago 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:

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:

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.

comment:6 Changed 15 months ago 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.

comment:7 in reply to:  5 Changed 15 months ago by AntC

Replying to goldfire:

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.)

comment:8 Changed 15 months ago 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.

comment:9 in reply to:  6 Changed 15 months ago by aaronvargo

Replying to 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 Dicts, 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 Dicts (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).

comment:10 in reply to:  6 Changed 15 months ago by AntC

Replying to 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: EDIT: None of these work. See ticket:15409.

  • 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)
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.)

Last edited 14 months ago by AntC (previous) (diff)

comment:11 Changed 14 months ago 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.

comment:12 Changed 11 months ago by Iceland_jack

Cc: Iceland_jack added
Note: See TracTickets for help on using tickets.