[GHC] #16365: Inconsistency in quantified constraint solving
#16365: Inconsistency in quantified constraint solving -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 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: -------------------------------------+------------------------------------- Consider the following program: {{{#!hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind import Data.Proxy class C a where m :: a -> () data Dict c = c => Dict ----- type family F a :: Type -> Type class C (F a b) => CF a b instance C (F a b) => CF a b works1 :: (forall z. CF a z) => Proxy (a, b) -> Dict (CF a b) works1 _ = Dict works2 :: ( CF a b) => Proxy (a, b) -> Dict (C (F a b)) works2 _ = Dict works3, fails :: (forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b)) works3 p | Dict <- works1 p = Dict fails _ = Dict }}} `fails`, as its name suggests, fails to typecheck: {{{ $ /opt/ghc/8.6.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:33:11: error: • Could not deduce (C (F a b)) arising from a use of ‘Dict’ from the context: forall z. CF a z bound by the type signature for: fails :: forall a b. (forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b)) at Bug.hs:31:1-71 • In the expression: Dict In an equation for ‘fails’: fails _ = Dict | 33 | fails _ = Dict | ^^^^ }}} But I see no reason why this shouldn't typecheck. After all, the fact that `works1` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(forall z. CF a z)` implies `(CF a b)`, and the fact that `works2` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(CF a b)` implies that `(C (F a b))`. Why then can GHC's constraint solver not connect the dots and deduce that `(forall z. CF a z)` implies `(C (F a b))` (in the type of `fails`)? Note that something with the type `(forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b))` //can// be made to work if you explicitly guide GHC along with explicit pattern-matching on a `Dict`, as `works3` demonstrates. But I claim that this shouldn't be necessary. Moreover, in this variation of the program above: {{{#!hs -- <as above> ----- data G a :: Type -> Type class C (G a b) => CG a b instance C (G a b) => CG a b works1' :: (forall z. CG a z) => Proxy (a, b) -> Dict (CG a b) works1' _ = Dict works2' :: ( CG a b) => Proxy (a, b) -> Dict (C (G a b)) works2' _ = Dict works3' :: (forall z. CG a z) => Proxy (a, b) -> Dict (C (G a b)) works3' _ = Dict }}} `works3'` needs no explicit `Dict` pattern-matching to typecheck. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16365 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16365: Inconsistency in quantified constraint solving -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | 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 RyanGlScott): Note that this is quite annoying in practice for the `singletons` library, as the existence of this bug prevents it from using `deriving` to generate its `Show` instances, instead forcing it to laboriously generate `Show` instances with Template Haskell. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16365#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16365: Inconsistency in quantified constraint solving -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | 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): It does look to me that GHC should do what Ryan asks... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16365#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16365: Inconsistency in quantified constraint solving -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | 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): In `works3` we get {{{ [G] forall z. CF a z -- From the type signature [W] forall z. CF a z -- from the call of works1 }}} We can solve this no problem. And we also get {{{ [G] CF a b -- From the pattern match on Dict Dict <- works1 p [W] C (F a b) -- From the call of Dict on the RHS of works3 }}} Now `C (F a b)` is a superclass of `CF a b`, so we get {{{ [G] C (F a b) -- Via superclass expansion [W] C (F a b) -- From the call of Dict on the RHS of works3 }}} We can solve this without difficulty. --------------- However, in `fails` we get this: {{{ [G] forall z. CF a z -- From the type signature on fails [W] C (F a b) }}} From superclass expansion we get {{{ [G] forall z. C (F a z) -- From superclass expansion [W] C (F a b) }}} And now we are stuck. What `z` would make `C (F a z)` match `C (F a b)`? Well, yes, `b` would, but maybe also lots of other things. GHC simply doesn't support matching involving type families. So, as it stands, this looks reasonable. And I don't see an easy way to improve matters. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16365#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16365: Inconsistency in quantified constraint solving -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | 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 RyanGlScott): I'm still not convinced. You say: Replying to [comment:3 simonpj]:
From superclass expansion we get {{{ [G] forall z. C (F a z) -- From superclass expansion [W] C (F a b) }}} And now we are stuck. What `z` would make `C (F a z)` match `C (F a b)`? Well, yes, `b` would, but maybe also lots of other things. GHC simply doesn't support matching involving type families.
I don't really see why `F` being a type family has anything to do with this. Recall the definition of `F`: {{{#!hs type family F a :: Type -> Type }}} Note that `F`'s second argument is //matchable//. This means that given an equality between `F`s, we can easily decompose it into their second type arguments, as demonstrated by the fact that this function typechecks: {{{#!hs f :: Proxy a -> F a b :~: F a c -> b :~: c f _ Refl = Refl }}} Now recall what things we are trying to solve: {{{ [G] forall z. C (F a z) -- From superclass expansion [W] C (F a b) }}} These two constraints only differ in their second argument. But as we just established above, `F` is matchable in its second argument. Therefore, GHC should have no trouble concluding that `z` equals `b`. In other words, `b` is the only sensible choice here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16365#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16365: Inconsistency in quantified constraint solving -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | 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): Ah! I had not focused on the fact that `F` only has arity 1. Good point. Avoiding the issues of superclasses for now, this fails: {{{ fails2 :: (forall z. C (F a z)) => Proxy (a, b) -> Dict (C (F a b)) fails2 _ = Dict }}} saying (quite helpfully) {{{ T16365.hs:37:11: error: • Illegal type synonym family application ‘F a’ in instance: C (F a z) • In the quantified constraint ‘forall z. C (F a z)’ In the type signature: fails2 :: (forall z. C (F a z)) => Proxy (a, b) -> Dict (C (F a b)) | 37 | fails2 :: (forall z. C (F a z)) => Proxy (a, b) -> Dict (C (F a b)) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} You sneak around that by hiding it under a superclass. I'm not sure how to stop you doing that :-). But this succeeds: {{{ fails3 :: (F a ~ fa, forall z. C (fa z)) => Proxy (a, b) -> Dict (C (F a b)) fails3 _ = Dict }}} Alas, I don't see how to use the same trick for `CF`, with its superclass. In other tickets we have wondered if this kind of floating could happen automatically. I argued "no" because it's subtle and you can do it manually. But with your superclass thing you can't do it manually (I thihik. So maybe that's an argument in favour. Hmm. Maybe we could elaboarate the matching process. Usually we match {{{ template: forall a b. [a] -> b target: [(Int,Bool)] -> Char }}} and produce a substitution {{{ a :-> (Int,Bool) b :-> Char }}} such that applying the substitution to the template yields the target. But we could instead additionally produce a list of wanted equalities, and treat a type-family application as a wildcard, something like this: {{{ template: forall a. F a -> a -> Int target: Char -> [Bool] -> Int }}} then we succeed in matching, thus: {{{ Substitution: a :-> Int Wanted equalities: F a ~ [Bool] }}} I don't think this would be terribly useful at top level, but in these quantified constraints it really might be. Interesting. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16365#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC