April 2018 - ghc-tickets

[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

[GHC] #14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'
by GHC 04 Jun '18

04 Jun '18

#14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)' -------------------------------------+------------------------------------- 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: -------------------------------------+------------------------------------- This works with the [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:34 latest change to the -XQuantifiedConstraints branch]. {{{#!hs {-# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, AllowAmbiguousTypes, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #-} class (forall xx. (xx => a) => Implies xx b) => F a b instance (forall xx. (xx => a) => Implies xx b) => F a b class (a => b) => Implies a b instance (a => b) => Implies a b }}} but replacing `Implies xx b` with `(xx => b)` causes it to fail. I don't know if the cause of this overlaps with an existing ticket. {{{#!hs class (forall xx. (xx => a) => (xx => b)) => F a b instance (forall xx. (xx => a) => (xx => b)) => F a b -- $ ghci -ignore-dot-ghci /tmp/ASD.hs -- GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help -- [1 of 1] Compiling Main ( /tmp/ASD.hs, interpreted ) -- -- /tmp/ASD.hs:4:10: error: -- • Could not deduce: xx0 -- arising from the superclasses of an instance declaration -- from the context: forall (xx :: Constraint). (xx => a, xx) => b -- bound by the instance declaration at /tmp/ASD.hs:4:10-53 -- or from: (xx => a, xx) -- bound by a quantified context at /tmp/ASD.hs:1:1 -- • In the instance declaration for ‘F a b’ -- | -- 4 | instance (forall xx. (xx => a) => (xx => b)) => F a b -- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- Failed, no modules loaded. -- Prelude> }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14877> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #14832: QuantifiedConstraints: Strengthening context causes failure
by GHC 04 Jun '18

04 Jun '18

#14832: QuantifiedConstraints: Strengthening context causes failure -------------------------------------+------------------------------------- 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: -------------------------------------+------------------------------------- With Simon's latest changes (ticket:14733#comment:9) this works: {{{#!hs {-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #-} import Control.Category import Data.Kind import Data.Coerce data With cls a b where With :: cls a b => With cls a b type Coercion = With Coercible type Refl rel = (forall xx. rel xx xx :: Constraint) type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint) instance Refl rel => Category (With rel) where id = With (.) = undefined }}} But strengthening the context with `Trans rel`: {{{#!hs instance (Refl rel, Trans rel) => Category (With rel) where }}} causes it to fail {{{ GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( J.hs, interpreted ) J.hs:15:10: error: • Could not deduce: rel xx zz from the context: (Refl rel, Trans rel) bound by an instance declaration: forall k (rel :: k -> k -> Constraint). (Refl rel, Trans rel) => Category (With rel) at J.hs:15:10-53 or from: (rel xx yy, rel yy zz) bound by a quantified context at J.hs:15:10-53 • In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for ‘Category (With rel)’ | 15 | instance (Refl rel, Trans rel) => Category (With rel) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ J.hs:15:10: error: • Could not deduce: rel xx xx from the context: (Refl rel, Trans rel) bound by an instance declaration: forall k (rel :: k -> k -> Constraint). (Refl rel, Trans rel) => Category (With rel) at J.hs:15:10-53 • In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for ‘Category (With rel)’ | 15 | instance (Refl rel, Trans rel) => Category (With rel) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Failed, no modules loaded. Prelude> }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14832> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 16