[GHC] #14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c'
#14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- #14833 fixes #14835: we can witness `curryC :: ((a, b) |- c) :- (a |- b |- c)`. Now for the entirely predictable, how about **un**`curryC` {{{#!hs {-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs, LiberalTypeSynonyms, TypeOperators, MultiParamTypeClasses, FlexibleInstances #-} data Dict c where Dict :: c => Dict c infixr |- class (a => b) => (a |- b) instance (a => b) => (a |- b) type a :- b = Dict (a |- b) uncurryC :: forall a b c. (a |- b |- c) :- ((a, b) |- c) uncurryC = Dict }}} {{{ $ ghci -ignore-dot-ghci Z.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( Z.hs, interpreted ) Z.hs:13:12: error: • Could not deduce: c arising from a use of ‘Dict’ from the context: a |- (b |- c) bound by a quantified context at Z.hs:1:1 or from: (a, b) bound by a quantified context at Z.hs:1:1 • In the expression: Dict In an equation for ‘uncurryC’: uncurryC = Dict • Relevant bindings include uncurryC :: (a |- (b |- c)) :- ((a, b) |- c) (bound at Z.hs:13:1) | 13 | uncurryC = Dict | ^^^^ Failed, no modules loaded. Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14863 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Once again, I think this `:-` thing is a red herring. Here's what I believe to be the essence of the bug: {{{#!hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE UndecidableInstances #-} module Bug where data Dict c where Dict :: c => Dict c class (a => b) => Implies a b instance (a => b) => Implies a b uncurryCImpredic1 :: forall a b c. Implies a (b => c) => Dict (Implies (a, b) c) uncurryCImpredic1 = Dict uncurryCImpredic2 :: forall a b c. a => Implies b c => Dict (Implies (a, b) c) uncurryCImpredic2 = Dict uncurryC1 :: forall a b c. (a => b => c) => Dict (Implies (a, b) c) uncurryC1 = Dict uncurryC2 :: forall a b c. Implies a (Implies b c) => Dict (Implies (a, b) c) uncurryC2 = Dict }}} {{{ $ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:27:13: error: • Could not deduce: c arising from a use of ‘Dict’ from the context: Implies a (Implies b c) bound by the type signature for: uncurryC2 :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint). Implies a (Implies b c) => Dict (Implies (a, b) c) at Bug.hs:26:1-77 or from: (a, b) bound by a quantified context at Bug.hs:1:1 • In the expression: Dict In an equation for ‘uncurryC2’: uncurryC2 = Dict • Relevant bindings include uncurryC2 :: Dict (Implies (a, b) c) (bound at Bug.hs:27:1) | 27 | uncurryC2 = Dict | ^^^^ }}} All of these `uncurryC`-functions typecheck except for `uncurryC2`. (Note that the first two require `ImpredicativeTypes`, so I'm not sure if this is intended to be supported or not.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14863#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): In `uncurryC2` we have a given {{{ [G] Implies a (Implies b c) }}} by taking its superclass we also have {{{ [G] forall. a => Implies b c }}} But now we are stuck because I have not yet implemented the superclass story for quantified constraints. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14863#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): With the [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:34 latest changes] `uncurryC2` works. Should this be closed? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14863#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c'
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.5
Resolution: | Keywords:
| QuantifiedConstraints wipT2893
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
Yes; and I've added a test case
{{{
commit 32e8499889d314e9efd0747b4053290a2dc237d5
Author: Simon Peyton Jones
#14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14863#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): This is great work thanks! For those interested these examples came from [https://www.reddit.com/r/haskell/comments/6k86je/constraint_unions_bringing_... Edward Kmett's encoding of sums of Constraints]. This may be a milestone, since `curryC` / `uncurryC` mean that the "category of entailment" `(:-)` is a Cartesian closed `Constraint` category (which means we could get [https://www.reddit.com/r/haskell/comments/73lp4m/higherorder_abstract_syntax... HOAS syntax for constraints]?). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14863#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T14863 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => quantified-constraints/T14863 * milestone: => 8.6.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14863#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC