May 2018 - ghc-tickets

[GHC] #14863: QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c'
by GHC 05 Jun '18

05 Jun '18

#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

1 7

[GHC] #15178: Implement DerivingVia
by GHC 04 Jun '18

04 Jun '18

#15178: Implement DerivingVia -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Keywords: deriving | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The `DerivingVia` GHC proposal [https://github.com/ghc-proposals/ghc- proposals/pull/120 has been accepted]. This ticket serves as a reminder to get the corresponding patch into GHC. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15178> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #14734: QuantifiedConstraints conflated with impredicative polymorphism?
by GHC 04 Jun '18

04 Jun '18

#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

1 8

[GHC] #14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints
by GHC 04 Jun '18

04 Jun '18

#14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language QuantifiedConstraints #-} {-# Language GADTs #-} {-# Language ConstraintKinds #-} data D c where D :: c => D c proof :: (forall xx. f xx) => D (f a) proof = D }}} Running this program with [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:28 wip/T2893] gives {{{ GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 174-quantifiedconstraints.hs, interpreted ) 174-quantifiedconstraints.hs:9:9: error: • Could not deduce: f a arising from a use of ‘D’ from the context: forall xx. f xx bound by the type signature for: proof :: forall (f :: * -> Constraint) a. (forall xx. f xx) => D (f a) at 174-quantifiedconstraints.hs:8:1-37 • In the expression: D In an equation for ‘proof’: proof = D • Relevant bindings include proof :: D (f a) (bound at 174-quantifiedconstraints.hs:9:1) | 9 | proof = D | ^ }}} How can I instantiate `xx` to `a`? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14733> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 13

[GHC] #14983: Have custom type errors imply Void
by GHC 04 Jun '18

04 Jun '18

#14983: Have custom type errors imply Void -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: task | Status: new Priority: lowest | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple CustomTypeErrors | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This is a very minor issue, but `TypeError` (CustomTypeErrors) should entail a constraint like {{{#!hs import Data.Void class (forall x. x) => No where no :: Void }}} so users don't have to use `undefined` or `error ..`: {{{#!hs instance TypeError (Text "Can't show functions) => Show (a -> b) where show :: (a -> b) -> String show = no & absurd }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14983> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #14968: QuantifiedConstraints: Can't be RHS of type family instances
by GHC 04 Jun '18

04 Jun '18

#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 (Type checker) | 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: -------------------------------------+------------------------------------- Here's a type family that I tried to write using QuantifiedConstraints. {{{#!hs {-# LANGUAGE TypeOperators #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE QuantifiedConstraints #-} module QCTypeInstance where import GHC.Exts (Constraint) type family Functors (fs :: [(* -> *) -> * -> *]) :: Constraint type instance Functors '[] = (() :: Constraint) type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts) }}} Unfortunately, GHC complains that it's illegal to have polymorphism on the right hand side of a type instance definition. {{{ $ ../ghc-wip/T2893/inplace/bin/ghc-stage2 --interactive QCTypeInstance.hs GHCi, version 8.5.20180322: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling QCTypeInstance ( QCTypeInstance.hs, interpreted ) QCTypeInstance.hs:13:15: error: • Illegal polymorphic type: forall (f :: * -> *). Functor f => Functor (t f) • In the type instance declaration for ‘Functors’ | 13 | type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts) | ^^^^^^^^ }}} Would it be possible to lift this restriction and allow quantified constraints as right hand sides of type family instances? Or are there fundamental difficulties with what I'm trying to do? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14968> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #14958: QuantifiedConstraints: Doesn't apply implication for existential?
by GHC 04 Jun '18

04 Jun '18

#14958: QuantifiedConstraints: Doesn't apply implication for existential? -------------------------------------+------------------------------------- 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: -------------------------------------+------------------------------------- This fails {{{#!hs {-# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes #-} data Foo where Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) -> Foo a :: Foo a = Foo 10 }}} {{{ $ ... -ignore-dot-ghci /tmp/Optic.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/Optic.hs, interpreted ) /tmp/Optic.hs:7:9: error: • Could not deduce (Num x) arising from the literal ‘10’ from the context: (forall y. cls0 y => Num y, cls0 x) bound by a type expected by the context: forall x. (forall y. cls0 y => Num y, cls0 x) => x at /tmp/Optic.hs:7:5-10 Possible fix: add (Num x) to the context of a type expected by the context: forall x. (forall y. cls0 y => Num y, cls0 x) => x • In the first argument of ‘Foo’, namely ‘10’ In the expression: Foo 10 In an equation for ‘a’: a = Foo 10 | 7 | a = Foo 10 | ^^ Failed, no modules loaded. Prelude> }}} GHC knows that `cls ~=> Num` but still GHC cannot deduce `Num x` from `cls x`. ---- The reason for trying this is creating a `newtype` for optics where we still get subsumption {{{#!hs {-# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes, ApplicativeDo, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, FlexibleContexts #-} data Optic cls s a where Optic :: (forall f. cls f => (a -> f a) -> (s -> f s)) -> Optic cls s a class (forall x. f x => g x) => (f ~=> g) instance (forall x. f x => g x) => (f ~=> g) _1 :: cls ~=> Functor => Optic cls (a, b) a _1 = Optic $ \f (a, b) -> do a' <- f a pure (a', b) lens_1 :: Optic Functor (a, b) a lens_1 = _1 trav_1 :: Optic Applicative (a, b) a trav_1 = _1 }}} and I wanted to move `cls ~=> Functor` into the `Optic` type itself. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14958> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #14943: Make (=>) polykinded (:: k -> k -> Constraint)
by GHC 04 Jun '18

04 Jun '18

#14943: Make (=>) polykinded (:: k -> k -> Constraint) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 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: -------------------------------------+------------------------------------- Would it be a good idea to treat `=>` in `-XQuantifiedConstraints` as {{{#!hs type family (=>) :: k -> k -> Constraint where (=>) = Implies0 (=>) = Implies1 (=>) = Implies2 .. }}} {{{#!hs class (a => b) => Implies a b instance (a => b) => Implies a b class (forall x. f x => g x) => Implies1 f g instance (forall x. f x => g x) => Implies1 f g class (forall x y. f x y => g x y) => Implies2 f g instance (forall x y. f x y => g x y) => Implies2 f g .. }}} or will this get too confusing? This means type signatures like the ones from #14942 {{{#!hs oneTwo :: (forall x. semi x => Semigroup x) => Free semi Int nil :: (forall x. mon x => Monoid x) => Free mon Int together :: (forall x. mon x => Monoid x) => [Free mon Int] }}} could equivalently be written {{{#!hs oneTwo :: (semi => Semigroup) => Free semi Int nil :: (mon => Monoid) => Free mon Int together :: (mon => Monoid) => [Free mon Int] }}} I'm not sold on this idea myself. It's quite possible this would screw with the parser. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14943> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #14879: QuantifiedConstraints: Big error message + can't substitute (=>) with a class alias
by GHC 04 Jun '18

04 Jun '18

#14879: QuantifiedConstraints: Big error message + can't substitute (=>) with a 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: -------------------------------------+------------------------------------- This compiles fine {{{#!hs {-# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, UndecidableInstances, GADTs, TypeOperators #-} class (a => b) => Implies a b instance (a => b) => Implies a b data Dict c where Dict :: c => Dict c type a :- b = Dict (Implies a b) class (forall xx. Implies b xx => Implies a xx) => Yo a b instance (forall xx. Implies b xx => Implies a xx) => Yo a b yo :: Yo a b :- Implies a b yo = Dict }}} until you replace `(=>)` with `Implies` (which should be fine?) {{{#!hs class (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b instance (forall xx. Implies b xx `Implies` Implies a xx) => Yo a b }}} and the error message blows up {{{ $ ghci -ignore-dot-ghci SD.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( SD.hs, interpreted ) SD.hs:15:6: error: • Reduction stack overflow; size = 201 When simplifying the following type: Implies b (Implies b (Implies -->8---->8----several-hundred-lines---->8---->8---- b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Use -freduction-depth=0 to disable this check (any upper bound you could choose might fail unpredictably with minor updates to GHC, so disabling the check is recommended if you're sure that type checking should terminate) • In the expression: Dict In an equation for ‘yo’: yo = Dict | 15 | yo = Dict | ^^^^ Failed, no modules loaded. Prelude> }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14879> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #14831: QuantifiedConstraints: Odd superclass constraint
by GHC 04 Jun '18

04 Jun '18

#14831: QuantifiedConstraints: Odd superclass constraint -------------------------------------+------------------------------------- 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: -------------------------------------+------------------------------------- This code works {{{#!hs {-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #-} import Data.Semigroup newtype Free cls a = Free () instance (forall xx. cls xx => Semigroup xx) => Semigroup (Free cls a) where (<>) = undefined stimes = undefined sconcat = undefined -- instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where -- mempty = undefined }}} but uncomment the `Monoid` instance and we get {{{ $ ghci -ignore-dot-ghci /tmp/I.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/I.hs, interpreted ) /tmp/I.hs:12:10: error: • Could not deduce: cls (Free cls a) arising from the superclasses of an instance declaration from the context: forall xx. cls xx => Semigroup xx bound by the instance declaration at /tmp/I.hs:12:10-67 • In the instance declaration for ‘Monoid (Free cls a)’ | 12 | instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Failed, no modules loaded. Prelude> }}} Is this correct behavior? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14831> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8