[GHC] #14840: QuantifiedConstraints: Can't define class alias
#14840: QuantifiedConstraints: Can't define class alias -------------------------------------+------------------------------------- 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: -------------------------------------+------------------------------------- {{{#!hs {-# Language TypeInType, MultiParamTypeClasses, TypeFamilies, FlexibleContexts, FunctionalDependencies, AllowAmbiguousTypes, QuantifiedConstraints, GADTs, ConstraintKinds, KindSignatures, RankNTypes, FlexibleInstances, UndecidableInstances, TypeOperators #-} import Data.Kind class Reifies s a | s -> a where reflect :: proxy s -> a newtype Lift :: forall k. (Type -> Constraint) -> Type -> k -> Type where Lift :: a -> Lift cls a s data family Def :: (k -> Constraint) -> (k -> Type) class (forall s a. Reifies s (Def cls a) => cls (Lift cls a s)) => ReifiableConstraint cls instance (forall s a. Reifies s (Def cls a) => cls (Lift cls a s)) => ReifiableConstraint cls }}} gives an error {{{ $ ghci -ignore-dot-ghci Bug.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/Bug.hs, interpreted ) /tmp/Bug.hs:14:10: error: • Could not deduce: cls (Lift cls a s) arising from the superclasses of an instance declaration from the context: forall (s :: k) a. Reifies s (Def cls a) => cls (Lift cls a s) bound by the instance declaration at /tmp/Bug.hs:14:10-93 or from: Reifies s (Def cls a) bound by a quantified context at /tmp/Bug.hs:1:1 • In the instance declaration for ‘ReifiableConstraint cls’ | 14 | instance (forall s a. Reifies s (Def cls a) => cls (Lift cls a s)) => ReifiableConstraint cls | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Failed, no modules loaded. Prelude> }}} This is a rare occasion that the class alias trick fails for me so ~+~yay~+~. But is it intended? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14840 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14840: QuantifiedConstraints: Can't define class alias -------------------------------------+------------------------------------- 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): I have a hunch this will not be allow, but encoding sums and existentials doesn't work {{{#!hs class (forall sum. (a => sum) => (b => sum) => sum) => Sum a b instance (forall sum. (a => sum) => (b => sum) => sum) => Sum a b class (forall exists. (forall xx. f xx => exists) -> exists) => Exists f instance (forall exists. (forall xx. f xx => exists) -> exists) => Exists f }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14840#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14840: QuantifiedConstraints: Can't define class alias -------------------------------------+------------------------------------- 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): I'm not sure that this is a bug. Here's a reduced version of your first program: {{{#!hs {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE UndecidableInstances #-} module Bug where data T a class C1 a class (forall a. cls (T a)) => C2 cls instance (forall a. cls (T a)) => C2 cls }}} Note that this works without `PolyKinds`, which should give you an idea of the underlying issue. If you compile this with `-fprint-explicit-kinds`, the error message is more enlightening: {{{ Bug.hs:12:10: error: • Could not deduce: cls (T k0 a) from the context: forall (a :: k). cls (T k a) bound by an instance declaration: forall k (cls :: * -> Constraint). (forall (a :: k). cls (T k a)) => C2 cls at Bug.hs:12:10-40 • In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for ‘C2 cls’ | 12 | instance (forall a. cls (T a)) => C2 cls | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} You can fix this by explicitly binding the kind of `a`: {{{#!hs {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE UndecidableInstances #-} module Bug where data T a class C1 a class (forall k (a :: k). cls (T a)) => C2 cls instance (forall k (a :: k). cls (T a)) => C2 cls }}} With that in mind, here's the fixed version of your first program: {{{#!hs {-# Language TypeInType, MultiParamTypeClasses, TypeFamilies, FlexibleContexts, FunctionalDependenc ies, AllowAmbiguousTypes, QuantifiedConstraints, GADTs, ConstraintKinds, KindSignatures, RankNTypes , FlexibleInstances, UndecidableInstances, TypeOperators #-} import Data.Kind class Reifies s a | s -> a where reflect :: proxy s -> a newtype Lift :: forall k. (Type -> Constraint) -> Type -> k -> Type where Lift :: a -> Lift cls a s data family Def :: (k -> Constraint) -> (k -> Type) class (forall k (s :: k) a. Reifies s (Def cls a) => cls (Lift cls a s)) => ReifiableConstraint cls instance (forall k (s :: k) a. Reifies s (Def cls a) => cls (Lift cls a s)) => ReifiableConstraint cls }}} The program in comment:1 seems to be of an entirely different nature. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14840#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14840: QuantifiedConstraints: Can't define class alias -------------------------------------+------------------------------------- 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 Iceland_jack): * status: new => closed * resolution: => fixed Comment: Thanks! And comment:1 works with tricks but probably isn't much use once defined {{{#!hs class (a => b) => (a |- b) instance (a => b) => (a |- b) class (forall xx. f xx |- g xx) => f |~ g instance (forall xx. f xx |- g xx) => f |~ g class (forall xx. f xx |- exists) => Exists1 f exists instance (forall xx. f xx |- exists) => Exists1 f exists class exists => Exists2 f exists instance exists => Exists2 f exists class (Exists1 f |~ Exists2 f) => Exists (f::k -> Constraint) where instance (Exists1 f |~ Exists2 f) => Exists (f::k -> Constraint) where }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14840#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14840: QuantifiedConstraints: Can't define class alias -------------------------------------+------------------------------------- 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 simonpj): OK so the Description is not-a-bug. I don't understand comment:1. You seem to be giving a quantified constraint like {{{ forall (sum :: Constraint). blah => sum }}} which asserts that for ANY constraint we can solve with this quantified constraint. That can't be right can it? I'll close this ticket, but do open a new one if you think comment:1 holds water somehow. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14840#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14840: QuantifiedConstraints: Can't define class alias -------------------------------------+------------------------------------- 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): I'm thinking of these as Church encoding, I wanted to see how close I could get to something like a sum or existential constraints {{{#!hs type Sum a b = forall sum. (a -> sum) -> (b -> sum) -> sum }}} and actually, both of these definitions work-for-some-definition-of! (with judicious aliasing.) Here is an example that works today, I can Church encode `(a, b)` {{{#!hs {-# Language TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, ConstraintKinds, RankNTypes, QuantifiedConstraints #-} data Dict c where Dict :: c => Dict c class (a => b) => (a |- b) instance (a => b) => (a |- b) }}} We define a type class constraint of church encoded products (`forall pair. (a -> b -> pair) -> pair`) {{{#!hs class (forall pair. (a |- b |- pair) |- pair) => ChurchPair a b instance (forall pair. (a |- b |- pair) |- pair) => ChurchPair a b }}} And amazingly GHC can conclude `ChurchPair a b` from `(a, b)`! {{{#!hs type a :- b = Dict (a |- b) wit :: (a, b) :- ChurchPair a b wit = Dict }}} the other half of the isomorphism is too much for GHC {{{#!hs reductionStackOverflow :: ChurchPair a b :- (a, b) reductionStackOverflow = Dict }}} which is as expected, from your response to one of the other tickets -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14840#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14840: QuantifiedConstraints: Can't define class alias -------------------------------------+------------------------------------- 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 simonpj): Given this [wiki:QuantifiedConstraints interesting collection of tickets on quantified constraints] it'd be great if someone (Iceland Jack? Ryan?) wanted to write a blog post or even a paper about what you can and cannot do; and why. These examples make my head hurt! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14840#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14840: QuantifiedConstraints: Can't define class alias -------------------------------------+------------------------------------- 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): I will write a blog post, I would love to expand it into a paper but I'd probably require some guidance. I have a good idea what you can/cannot do but not always why. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14840#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC