#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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: | -------------------------------------+------------------------------------- Old description:

This may be related to #14860, but I think it's different.

The following code fails to compile:

{{{#!hs {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ConstraintKinds #-}

import Prelude() import Data.Kind

data Dict c = c => Dict

type family F a :: Constraint

foo :: forall a b. (a => F b, a) => Dict (F b) foo = Dict }}}

{{{ • Could not deduce: F b arising from a use of ‘Dict’ from the context: (a => F b, a) }}}

Yet the following all do compile:

{{{#!hs bar :: forall a. F a => Dict (F a) bar = Dict

baz :: forall a b. (a => b, a) => Dict b baz = Dict

qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b) qux = Dict }}}

It seems that a wanted `F b` can be solved with a given `F b`, but not with a given `a => F b`, which is bizarre. The fact that `qux` still works is also strange, as it means that you get a different result if you first simplify by substituting `c = F b`.

As a more practical example, the following similarly fails to compile, due to the `Cod f` type family:

{{{#!hs -- in addition to the above extensions {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-}

class Ob p a

class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where type Dom f type Cod f

liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a)) liftOb = Dict }}}

While a version which uses fundeps instead does compile:

{{{#!hs class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f | f -> dom cod

liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob cod (f a)) liftOb = Dict }}}

New description: This may be related to #14860, but I think it's different. The following code fails to compile: {{{#!hs {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ConstraintKinds #-} import Prelude() import Data.Kind data Dict c = c => Dict type family F a :: Constraint foo :: forall a b. (a => F b, a) => Dict (F b) foo = Dict }}} {{{ • Could not deduce: F b arising from a use of ‘Dict’ from the context: (a => F b, a) }}} Yet the following all do compile: {{{#!hs bar :: forall a. F a => Dict (F a) bar = Dict baz :: forall a b. (a => b, a) => Dict b baz = Dict qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b) qux = Dict }}} It seems that a wanted `F b` can be solved with a given `F b`, but not with a given `a => F b`, which is bizarre. The fact that `qux` still works is also strange, as it means that you get a different result if you first simplify by substituting `c = F b`. As a more practical example, the following similarly fails to compile, due to the `Cod f` type family: {{{#!hs -- in addition to the above extensions {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} class Ob p a class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where type Dom f type Cod f liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a)) liftOb = Dict }}} While a version which uses fundeps instead does compile: {{{#!hs class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f | f -> dom cod liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob cod (f a)) liftOb = Dict }}} -- Comment (by aaronvargo): Actually, the `Functor` example with type families can be fixed by replacing: {{{#!hs forall a. Ob (Dom f) a => Ob (Cod f) (f a) }}} with {{{#!hs forall a cod. (Ob (Dom f) a, cod ~ Cod f) => Ob cod (f a) }}} Perhaps the compiler could do this rewrite automatically? It rightly doesn't in the case of instance declarations, but perhaps it's fine for quantified constraints. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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 don't see how this is different from #14860. It looks the same to me. But I think `(x ~ F b, forall a. a => x)` and `forall a. a => F b` really are different. It's all about shadowing. The first casts a much bigger shadow, one whose shape can be specified. The second's shadow is too oddly shaped to be predictable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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): To clarify, this also compiles: {{{#!hs class Functor (f :: * -> *) where type Dom f type Cod f liftOb :: ( Functor f, cod ~ Cod f , forall a. Ob (Dom f) a => Ob cod (f a) , Ob (Dom f) a ) => Dict (Ob cod (f a)) liftOb = Dict }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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): Not if the variable is a skolem (is that the right terminology?), which is what I intended. I should have been clearer. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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): Or to give the simpler example, this does too: {{{#!hs wibble :: forall a b fb c. (a, fb ~ F b, a => fb, a => c) => Dict (F b, c) wibble = Dict }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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): Yes, that's what I wanted, but after thinking a bit, I think the current behavior may actually be broken anyway! Consider: {{{#!hs type family F a :: Constraint yikes :: forall a b fb. ( a => fb , fb ~ F b ) => Dict (Eq Int) yikes = Dict }}} The above compiles, but with the current behavior, it actually violates the open world assumption! Consider what happens if we now add: {{{#!hs type instance F a = Eq Int }}} {{{ • Could not deduce: a arising from a use of ‘Dict’ from the context: (a => fb, fb ~ F b) bound by the type signature for: yikes :: forall (a :: Constraint) b (fb :: Constraint). (a => fb, fb ~ F b) => Dict (Eq Int) • In the expression: Dict In an equation for ‘yikes’: yikes = Dict }}} The problem is that since `fb ~ F b`, the `a => fb` constraint can overlap if `F b` can be reduced further. A possible solution is to always first reduce the heads of given quantified constraints using given equalities. Then `a => fb` will become `a => F b`, and won't be usable since `F b` isn't a valid instance head. `qux` would then no longer compile, while `yikes` would continue to compile even after the type instance is added. My trick of floating out type families shouldn't even work! I'm not sure that that even completely solves the problem though...Consider: {{{#!hs type family F a :: Constraint type instance F String = () whatAboutThis :: forall a b. ( F String => (b ~ Int) , a => Eq b ) => Dict (Eq Int) whatAboutThis = Dict }}} Currently this compiles. Should it? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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:10 simonpj]: A few things: First, there's probably another way to do this without a free-variable analysis: float type families out when they appear in wanted constraints. E.g. in `foo`, the floating would happen because `F b` appears in the wanted constraint, not because it's independent of the forall'd variables in the given quantified constraint. Would something like that be more feasible? Second,

Consider this: {{{ type family F a type instance F Int = Bool

instance Eq a => Eq (F a) where ... }}} Should we allow this? Obviously not. It's like allowing...

Indeed, but this is an argument for disallowing ambiguity, not for disallowing type families. In your `Eq` example, `a` is ambiguous since `F` may not be injective. (likewise, `xs` and `ys` are ambiguous in the `map` example since `(++)` isn't injective). Not all uses of type families cause such ambiguity, and the compiler already has a perfectly good ambiguity check which can determine whether they do. Some cases where they don't are: 1. The type family is independent of the quantified variables 2. The type family is injective 3. The type family can be reduced to an expression which is unambiguous (this is #13262) 4. The quantified variables appear ambiguously in the type family, but are still made unambiguous by the rest of the instance head (e.g. `forall a. C (F a) a`) For top-level instances there may be coherence issues with allowing type families even when they don't cause ambiguity (though I'm not sure that there are), but such issues don't apply to QCs, which can't introduce incoherence. So why not allow type families in QCs, but require that the quantified variables be unambiguous? Third, working around this by manually floating out type families can be hugely painful, as it requires sacrificing one of the major benefits of type families, namely the ability to avoid passing around extra class parameters which are already determined by other parameters. The basic problem is this: suppose we have a class: {{{#!hs class (forall a. Eq a => Eq (f a)) => C f t | t -> f }}} Currently, the parameter `f` can never be instantiated with a type family without breaking the quantified constraint. This means the extra parameter needs to be repeated throughout the code for the QC to continue to work, despite the fact that `f` is already determined by `t`. Consider the following encoding of categories and functors, which makes use of type families: {{{#!hs type Hom k = k -> k -> Type -- Natural transformations data (==>) (p :: Hom i) (q :: Hom j) (f :: i -> j) (g :: i -> j) class ( Category (Op p) , Op (Op p) ~ p , Ob (Op p) ~ Ob p , FunctorOf' (Op p) (p ==> (->)) p , forall a. Ob p a => FunctorOf' p (->) (p a) ) => Category (p :: Hom k) where type Ob p :: k -> Constraint type Op p :: Hom k -- FunctorOf without superclasses, to work around issues with UndecidableSuperClasses class FunctorOf' p q (f :: i -> j) | f -> p q -- FunctorOf' with proper superclasses class ( FunctorOf' p q f , Category p , Category q , forall a. Ob p a => Ob q (f a) ) => FunctorOf p q f instance ( FunctorOf' p q f , Category p , Category q , forall a. Ob p a => Ob q (f a) ) => FunctorOf p q f }}} Note that `Category p` has a superclass `Category (Op p)`, which has a superclass: {{{#!hs -- noting that Ob (Op p) ~ Ob p forall a. Ob p a => FunctorOf' (Op p) (->) (Op p a) }}} and that the superclasses of `FunctorOf p q f` include: {{{#!hs forall a. Ob p a => Ob q (f a) forall a. Ob p a => FunctorOf' (Op p) (->) (Op p a) forall a. Ob q a => FunctorOf' (Op q) (->) (Op q a) }}} All of these have independent type families in the heads. Floating them out manually requires doubling the number of class parameters for both `Category` and `FunctorOf`: {{{#!hs class (..., op ~ Op p) => Category op p where ... class ( FunctorOf' p q f , Category opP p , Category opQ q , obQ ~ Ob q , forall a. Ob p a => obQ (f a) ) => FunctorOf opP p opQ q obQ f }}} These parameters will spread throughout all of the code. Subclasses will add yet more parameters, and will never be able to use type families for anything which is a functor or a category, without sacrificing some QCs. Types will be lost in a sea of parameters. This ends up being more painful than just using `Dict`s. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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:14 simonpj]: Yes, sorry!

That is, so far I do not understand why floating out type families (a straightforward source-to-source transformation that does not change the number of class parameters) would sacrifice a major benefit.

It requires changing the number of class parameters when the quantified constraint appears as a superclass. Suppose we would like to write: {{{#!hs class (forall a. Eq a => Eq (F t a)) => C t where type F t :: * -> * }}} where the type family `F t` in the quantified constraint is independent of the quantified `a`. In order to float this type family out, we need to add a new parameter to the class, `ft`, and make it equal to `F t`: {{{#!hs class (ft ~ F t, forall a. Eq a => Eq (ft a)) => C ft t where type F t :: * -> * }}} Furthermore, this parameter can never be instantiated with a type family without once again breaking the quantified constraint. E.g. if we write {{{#!hs class C (F t) t => D t }}} then the inherited quantified constraint will contain a type family, and will no longer work. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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:16 simonpj]:

Really? What wrong with this?

{{{ Not in scope: type variable ‘ft’ }}} The superclass isn't allowed to mention variables which don't appear in the head, even if they're already determined by other parameters. The solution to this limitation has been "use type families", which leads us to this issue. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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:16 simonpj]: I thought I'd once seen a ticket for this, and I've managed to find it: see #3490, where you write:

The easiest way forward is to re-express your program using type functions

Also, on second thought, what I said in comment:18 won't work. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- 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:20 simonpj]:

Not allowing functions in the instance head not to do with ambiguity; it's to do with coherence

But is this an issue for QCs, which can't introduce incoherence? Does it matter if two QCs might overlap, as long as locally we can't tell that they do? Suppose we had: {{{#!hs type family F a = r | r -> a type family G a = r | r -> a foo :: forall b. (forall a. Eq (F a), forall a. Eq (G a)) => Dict (Eq (F b)) foo = Dict }}} While `F b` and `G b` might overlap for some particular `b`, locally only one instance can be used to solve `Eq (F b)`, since we don't know whether `G b ~ F b`. Since the two instances are guaranteed to be coherent, wouldn't it be fine to simply pick the one that matches? (If both were to match then the program would still be rejected). Likewise for the case with non-injective independent type families: {{{#!hs foo :: forall b. (forall t. C (F b) [t], forall t. C (G b) [t]) => Dict (C (F b) [Int]) }}} The first instance should just be used, since it's the only one that matches given the knowledge available locally. How does the compiler currently deal with type families in non-quantified constraints? What makes it more difficult to allow them in QCs?

Can you distil a small example that shows the utility of having a function in the head?

For now I have no use case for the injective type family case, and only really care about the independent family case. I'll try and come up with a simpler example than the category one.

So, maybe a quantified constraint with a function in the head is just "parked", but it wakes up if the function can be reduced.

This is much less useful than what I want, though I suppose it might help in some small minority of cases. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler