- ghc-tickets - Haskell.org

[GHC] #15974: QuantifiedConstraints: Spurious error involving superclass constraints
by GHC 30 Nov '18

30 Nov '18

#15974: QuantifiedConstraints: Spurious error involving superclass constraints -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# LANGUAGE KindSignatures, QuantifiedConstraints, UndecidableInstances #-} }}} Consider the following datatype and two classes: {{{#!hs data X (f :: * -> *) class A a class A a => B a }}} If I create an instance `A (X f)` involving a quantified constraint {{{#!hs instance (forall a. A a => A (f a)) => A (X f) }}} then curiously, the following instance declaration for `B (X f)` is rejected with the accompanying error message: {{{#!hs instance (forall a. B a => B (f a)) => B (X f) }}} {{{ /tmp/qc.hs:11:10: error: • Could not deduce (B a) arising from the superclasses of an instance declaration from the context: forall a. B a => B (f a) bound by the instance declaration at /tmp/qc.hs:11:10-46 or from: A a bound by a quantified context at /tmp/qc.hs:1:1 Possible fix: add (B a) to the context of a quantified context • In the instance declaration for ‘B (X f)’ | 11 | instance (forall a. B a => B (f a)) => B (X f) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} Notably, if the instance declaration for `A (X f)` is altered to not use a quantified constraint, as in {{{#!hs instance A (f (X f)) => A (X f) }}} or even just {{{#!hs instance A (X f) }}} then the above instance declaration for `B (X f)` is accepted. I see no reason that the `B (X f)` declaration should be rejected, even with the quantified constraint in the instance context for `A (X f)`. The error message complains that the typechecker cannot deduce `B a`, and it even suggests adding `B a` to the context of the quantified constraint, but `B a` is //already// in that context. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15974> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #15961: TH 'Lift' instance for 'NonEmpty'
by GHC 30 Nov '18

30 Nov '18

#15961: TH 'Lift' instance for 'NonEmpty' -------------------------------------+------------------------------------- Reporter: fr33domlover | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.3 Component: Template | Version: 8.6.2 Haskell | Keywords: lift, | Operating System: Unknown/Multiple instance, nonempty | Architecture: | Type of failure: Other Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I was using `deriving Lift` on a data type and the `DeriveLift` extension: {{{#!hs import Data.List.NonEmpty import Language.Haskell.TH data T = T (NonEmpty String) Int }}} and I noticed I couldn't get an automatic instance because `NonEmpty` doesn't have a `Lift` instance. I'm wondering if an instance can be added to the `template-haskell` package (or elsewhere if that isn't the right place? I'm assuming it is because `NonEmpty` is in `base` now) Since `NonEmpty` has a `Data` instance, I suppose the following would be enough? {{{#!hs instance Data a => Lift (NonEmpty a) }}} And without using `Data` it could be: {{{#!hs nonemptyConName :: Name nonemptyConName = mkNameG DataName "base" "Data.List.NonEmpty" ":|" instance Lift a => Lift (NonEmpty a) where lift (x :| xs) = do x' <- lift x xs' <- traverse lift xs return $ ConE nonemptyConName `AppE` x' `AppE` xs' }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15961> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #15966: panic when using RebindableSyntax
by GHC 30 Nov '18

30 Nov '18

#15966: panic when using RebindableSyntax -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 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: -------------------------------------+------------------------------------- https://gist.github.com/mpickering/216ecdd9d8766dce2ff1080a17f77a0e {{{ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE RebindableSyntax #-} {-# OPTIONS_GHC -Wall -Wno-missing-signatures -Wno-unticked-promoted- constructors -Wno-name-shadowing -fwarn-partial-type-signatures -Wno- partial-type-signatures #-} module Repro(main) where import Prelude hiding (Monad(..)) import Control.Applicative data E (a :: * -> *) (n :: *) where VarE :: a n -> E a n instance IMonad E where return :: a n -> E a n return = VarE (>>=) :: E a n -> (forall n . a n -> E b n) -> E b n VarE x >>= f = f x class IMonad (m :: (* -> *) -> (* -> *)) where return :: forall a n . a n -> m a n (>>=) :: m a n -> (forall n . a n -> m b n) -> m b n one :: Const Int n one = (Const 1) example_4 :: E (Const Int) n example_4 = do x <- (return one) return x main = example_4 `seq` () }}} Compiling this file with GHC leads to a StgCmmEnv panic. {{{ ghc: panic! (the 'impossible' happened) (GHC version 8.6.2 for x86_64-unknown-linux): StgCmmEnv: variable not found $dIMonad_a1lY local binds for: return >>= $tc'VarE $tcE $tcIMonad $trModule $tc'VarE1_r1oI $tc'VarE2_r1ps $krep_r1pt $krep1_r1pu $krep2_r1pv $krep3_r1pw $krep4_r1px $tcE1_r1py $tcE2_r1pz $tcIMonad1_r1pA $tcIMonad2_r1pB $krep5_r1pC $krep6_r1pD $krep7_r1pE $trModule1_r1pF $trModule2_r1pG $trModule3_r1pH $trModule4_r1pI $krep8_r1pJ $krep9_r1pK sat_s1rG Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} Loading the file into GHCi succeeds but then when the `main` function is invoked, a `nameModule` panic occurs. {{{ *Repro> main ghc: panic! (the 'impossible' happened) (GHC version 8.6.2 for x86_64-unknown-linux): nameModule system $dIMonad_a1LV Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/basicTypes/Name.hs:240:3 in ghc:Name Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} Reproduced on 8.6.{2,1} 8.4.4 8.2.2 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15966> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 1

[GHC] #15953: GHC always dumps the output of -ddump-hpc to STDOUT
by GHC 30 Nov '18

30 Nov '18

#15953: GHC always dumps the output of -ddump-hpc to STDOUT -------------------------------------+------------------------------------- Reporter: ckoparkar | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 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: -------------------------------------+------------------------------------- Instead, it should write the output to a file if `-ddump-to-file` is enabled. `-ddump-core-stats` also has a similar problem. But given that it always prints just one line, maybe it should continue to print to `STDOUT`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15953> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #15962: Type family & typeclass interaction suppresses errors
by GHC 30 Nov '18

30 Nov '18

#15962: Type family & typeclass interaction suppresses errors -------------------------------------+------------------------------------- Reporter: madgen | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.4.3 (Type checker) | Keywords: type family, | Operating System: Unknown/Multiple typeclass, error message | Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following program despite having a hole and an undefined variable `iDontExist` *quietly* fails to compile on 8.4.3 and 8.4.4. It produces errors as expected on 8.6.1 and 8.6.2. By quietly failing, I mean it fails on CLI but without producing any error messages and in GHCI. It just says "Failed, no modules loaded." {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} module Bug where import Data.Kind (Type) type Exp a = a -> Type type family Eval (e :: Exp a) :: a data OpKind = Conjunction data Dual (k :: OpKind) :: Exp OpKind data Map :: (a -> Exp b) -> [ a ] -> Exp [ b ] type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as) data Big :: [ OpKind ] -> Type where Big :: [ Big ks ] -> Big ('Conjunction ': ks) dualBig :: Big ks -> Big (Eval (Map Dual ks)) dualBig = _ instance Semigroup (Big a) where Big xs <> Big ys = Big (xs <> ys) instance Monoid (Big ('Conjunction ': ks)) where mempty = iDontExist flatten :: Monoid (Big ks) => Big (k ': k ': ks) -> Big ks flatten = undefined }}} Sorry, the example is a bit big but almost any change causes the errors to appear again including the `Monoid` constraint on `flatten`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15962> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #15930: Add @since-annotations to the Foldable methods
by GHC 30 Nov '18

30 Nov '18

#15930: Add @since-annotations to the Foldable methods -------------------------------------+------------------------------------- Reporter: sjakobi | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.3 Component: Core | Version: 8.6.2 Libraries | 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: -------------------------------------+------------------------------------- Methods like `sum` were added some time after `Foldable`'s inception. It would be nice to know when exactly. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15930> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #14937: QuantifiedConstraints: Reify implication constraints from terms lacking them
by GHC 30 Nov '18

30 Nov '18

#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature | Status: new request | 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: #14822 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This is possibly the same question as #14822, asked in more general terms. Would it be viable/sound to have a way of extracting implication constraints out of terms which effectively encode such constraints, such as `(:-)` from `Data.Constraint`? Here's how I think about it. `a :- b` is equivalent to `forall r. a => (b => r) -> r`. This is a type that, as I read it, expresses "if you can show `a`, then I can show `b`". This is very similar to `forall r. ((a => b) => r) -> r`, which expresses "(without obligations) I can show that `a` implies `b`". It seems to me (and I know this is hand-wavy) like expressions of both of these types actually must have the same "knowledge", i.e. that `a` imples `b`. Is this actually correct? I am wondering whether we could have a built-in function like: {{{#!hs reifyImplication :: forall a b. (forall r. a => (b => r) -> r) -> (forall r. ((a => b) => r) -> r) }}} We can already write the function that goes the other direction. There are plenty of ways to represent this conversion. Some more straight- forward, using `a :- b` or `Dict a -> Dict b`. I just went with one that doesn't require any types beyond arrows. I'm curious about the soundness of this. I have tried really hard to implement this function, but I don't think it can be done. I don't know if this proves anything, but replacing `(=>)` with `(->)` and all constraints `c` with `Dict c`, this function can be written: {{{#!hs dictReifyImplication :: forall a b. (forall r. Dict a -> (Dict b -> r) -> r) -> (forall r. ((Dict a -> Dict b) -> r) -> r) dictReifyImplication f g = g (\a -> f a id) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14937> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #15635: Implication introduction for quantified constraints
by GHC 30 Nov '18

30 Nov '18

#15635: Implication introduction for quantified constraints -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 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: -------------------------------------+------------------------------------- Now that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types: {{{#!hs data Dict a where Dict :: a => Dict a newtype a :- b = Sub (a => Dict b) }}} `QuantifiedConstraints` suggests another version of `:-`: {{{#!hs newtype Imp a b = Imp { unImp :: forall r. ((a => b) => r) -> r} }}} We can write {{{#!hs fromImp :: Imp a b -> a :- b fromImp (Imp f) = Sub (f Dict) }}} But ... there's no way to go the other way! Let's try it: {{{#!hs toImp :: a :- Dict b -> a :- b toImp (Sub ab) = Imp $ \r -> _ }}} We get {{{ * Found hole: _ :: r * Relevant bindings include r :: (a => b) => r ab :: a => Dict b }}} There's no way to put these things together. But there's no terribly obvious reason they ''can't'' be combined. `a => b` is a function from an `a` dictionary to a `b` dictionary. `a => Dict b` is a function from an `a` dictionary to a value that ''contains'' a `b` dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic: {{{#!hs implIntro :: ((a => b) => q) -> (forall r. (b => r) -> (a => r)) -> q }}} In Core (modulo type abstraction and application), we could simply write {{{#!hs implIntro f g = f (g id) }}} Unfortunately, I doubt that `implIntro` is really general enough to do everything people will want in this space. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15635> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #15975: semantics of concurrent program depends on -O level, -f[no-]omit-yields
by GHC 30 Nov '18

30 Nov '18

#15975: semantics of concurrent program depends on -O level, -f[no-]omit-yields -------------------------------------+------------------------------------- Reporter: j.waldmann | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Research needed Component: Runtime | Version: 8.6.2 System | Keywords: | Operating System: Linux Architecture: x86_64 | Type of failure: Incorrect result (amd64) | at runtime Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I am surprised by the behaviour of the program below (the interesting property is whether it will output "foo"). Behaviours (plural) actually: it seems to depend on optimisation level, on omit-yields, and on very small changes in the source code: It does print (mostly), when compiled with -O0. It does not, when compiled with -O2. With -O2 -fno-omit-yields, it will print. With -O0 -fno-omit-yields, and when I remove the two newTVar in the beginning, it will mostly not print. How come? These differences already occur with the last two lines replaced by "forever $ return ()", so the STM stuff may be inessential here. But that's the context where I came across the problem. See also discussion at https://mail.haskell.org/pipermail/haskell- cafe/2018-November/130274.html {{{ import Control.Concurrent.STM import Control.Concurrent ( forkIO ) import Control.Monad ( forever ) import System.IO main = do atomically $ newTVar "bar" atomically $ newTVar False forkIO $ putStrLn "foo" x <- atomically $ newTVar False forever $ atomically $ writeTVar x True }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15975> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 1

[GHC] #14887: Explicitly quantifying a kind variable causes a type family to fail to typecheck
by GHC 29 Nov '18

29 Nov '18

#14887: Explicitly quantifying a kind variable causes a type family to fail to typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 (Type checker) | Keywords: TypeFamilies, | Operating System: Unknown/Multiple TypeInType | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following program: {{{#!hs {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fprint-explicit-kinds #-} module Bug where import Data.Kind import Data.Type.Equality type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where Foo1 (e :: a :~: a) = a :~: a type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where Foo2 k (e :: a :~: a) = a :~: a }}} `Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not! {{{ $ /opt/ghc/8.2.2/bin/ghci Bug.hs -fprint-explicit-kinds GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:13:10: error: • Couldn't match kind ‘k’ with ‘k1’ When matching the kind of ‘a’ Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’ • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’ In the type family declaration for ‘Foo2’ | 13 | Foo2 k (e :: a :~: a) = a :~: a | ^^^^^^^^^^^^^^ }}} (Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14887> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 15