[GHC] #14734: QuantifiedConstraints conflated with impredicative polymorphism?
#14734: QuantifiedConstraints conflated with impredicative polymorphism? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This works: {{{#!hs {-# Language QuantifiedConstraints #-} {-# Language GADTs #-} {-# Language ConstraintKinds #-} {-# Language KindSignatures #-} {-# Language RankNTypes #-} {-# Language FlexibleInstances #-} {-# Language UndecidableInstances #-} {-# Language TypeOperators #-} import Data.Kind data D c where D :: c => D c newtype a :- b = Sub (a => D b) class (forall xx. f xx) => Limit f instance (forall xx. f xx) => Limit f proof :: Limit Eq :- Eq (Int -> Float) proof = Sub D }}} If we replace `Limit Eq` with `(forall xx. Eq xx)` it is considered impredicative polymorphism, but is it? {{{ 174-quantifiedconstraints.hs:20:10: error: • Illegal polymorphic type: forall xx. Eq xx GHC doesn't yet support impredicative polymorphism • In the type signature: proof :: (forall xx. Eq xx) :- Eq (Int -> Float) | 20 | proof :: (forall xx. Eq xx) :- Eq (Int -> Float) | ^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14734 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14734: QuantifiedConstraints conflated with impredicative polymorphism? -------------------------------------+------------------------------------- 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: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * keywords: QuantifiedConstraints => QuantifiedConstraints wipT2893 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14734#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14734: QuantifiedConstraints conflated with impredicative polymorphism? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: invalid | 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: => invalid Comment:
it is considered impredicative polymorphism, but is it?
Yes it is. You are instantiating a type variable (the `a` from `newtype a :- b`) with a polymorphic type. I think you need impredicativity here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14734#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14734: QuantifiedConstraints conflated with impredicative polymorphism? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: invalid | 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): It feels different, there is no way to get around regular impredicativity with type synonyms but in this case we can get around it with the `Limit` class synonym. Hypothetically if GHC were to generate an internal class synonym for impredicative constraints what would go wrong? I'm not aware of differences between `forall xx. f xx` and `Limit f`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14734#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14734: QuantifiedConstraints conflated with impredicative polymorphism? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: invalid | 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): It would be nice to directly write `type a :- b = Dict (a => b)` rather than {{{#!hs class (a => b) => Implies a b instance (a => b) => Implies a b type a :- b = Dict (Implies a b) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14734#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14734: QuantifiedConstraints conflated with impredicative polymorphism? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: invalid | 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): The difficulty with impredicativity is that, during inference, a unification variable may be unified with a polytype. Thus {{{ f :: forall a. [a] -> [a] xs :: [forall b. b->b] ...(f xs).. }}} Here f really has a type argument, and that type is polymorphic. We really have {{{ ...(f @(forall b b->b) xs)... }}} The hard bit is infeering the implicit, invisible type arguments. But here we are the level of types. With explicit arguments there should be nothing wrong with allowing polytypes. (It's a different matter for the implicit kind arguments, of course.) So... may it'd be OK. I'm just not sure what a principled story is. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14734#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14734: QuantifiedConstraints conflated with impredicative polymorphism? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: invalid | 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): Ok thanks for the response, I'll keep using aliases -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14734#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14734: QuantifiedConstraints conflated with impredicative polymorphism? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: invalid | 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): Btw, should the following work? {{{#!hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help Prelude> :set -XGADTs -XQuantifiedConstraints -XConstraintKinds Prelude> data Imp a b where Imp :: (a => b) => Imp a b Prelude> :kind forall a b. Imp a (b => a) forall a b. Imp a (b => a) :: * Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14734#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14734: QuantifiedConstraints conflated with impredicative polymorphism? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: invalid | Keywords: | QuantifiedConstraints 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 RyanGlScott): * keywords: QuantifiedConstraints wipT2893 => QuantifiedConstraints -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14734#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC