QuantifiedConstraints ignore FunctionalDependencies

changed weight to 5

added Tbug Trac import typechecker labels

changed the description

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.

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.

Replying to [ticket:15351#comment:156455 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.

I've created #15354 (closed) about the documentation oversight -- you're absolutely right.

I agree with your analysis in ticket:15351#comment:156470. 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.

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.

Replying to [ticket:15351#comment:156483 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 ticket:15351#comment:156490 that arrived as I was writing this doesn't explain what specifically GHC "checks it against" in this case.)

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.

Replying to [ticket:15351#comment:156490 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).

Replying to [ticket:15351#comment:156490 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 #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)

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

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.

mentioned in issue #15989

added 1 deleted label

added QuantifiedConstraints label

added Pnormal label

mentioned in issue #17025 (closed)

I bumped into this issue today, but in a different way than what has been mentioned so far. I tried to use a quantified constraint in an instance context, but the lack of fundeps on the constraint caused my instance to (incorrectly) fail the liberal coverage condition. Here’s a minimal example that reproduces the issue:

class M a (m :: * -> *) | m -> a
class T a (t :: (* -> *) -> * -> *) | t -> a
instance (forall m. M a (t m)) => T a t

I believe the above declarations are well-typed, but GHC rejects them with the following error:

error:
    • Illegal instance declaration for ‘T a t’
        The liberal coverage condition fails in class ‘T’
          for functional dependency: ‘t -> a’
        Reason: lhs type ‘t’ does not determine rhs type ‘a’
        Un-determined variable: a
    • In the instance declaration for ‘T a t’

I imagine the root cause is the same as the problem described in this issue.

Ran into this recently but found a workaround: just instantiate the quantified constraint separately from solving the fundeps. In terms of the original post:

{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE QuantifiedConstraints  #-}

class C a b | a -> b where
  foo :: a -> b

bar :: (forall x. C (f x) Int) => f a -> String
bar = show . helper
  where
    helper :: C (f x) Int => f x -> Int
    helper = foo

This compiles with GHC 8.6.3.

EDIT: Well that's silly, the fundep isn't even necessary there with this approach. I have an example where the fundep is necessary, though, and the same workaround helps: https://github.com/timoffex/quantified-constraint-fundeps/blob/master/QuantifiedConstraintFundeps.hs

For @lexi.lambda 's issue, note that forall m. M a (t m) implies M a (t Maybe). Adding this redundant constraint seems to solve the problem:

class M a (m :: * -> *) | m -> a
class T a (t :: (* -> *) -> * -> *) | t -> a
instance ( forall m. M a (t m)
         , M a (t Maybe)
         ) => T a t

This is a bit of a hack, but I've found it to be a useful trick to know when working with quantified constraints.

added FunctionalDependencies label

QuantifiedConstraints ignore FunctionalDependencies

Child items 0

Activity