October 2018 - ghc-tickets

[GHC] #15078: base: Customary type class laws (e.g. for Eq) and non-abiding instances (e.g. Float) should be documented
by GHC 26 Oct '18

26 Oct '18

#15078: base: Customary type class laws (e.g. for Eq) and non-abiding instances (e.g. Float) should be documented -------------------------------------+------------------------------------- Reporter: sjakobi | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.1 Component: Core | Version: 8.4.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: -------------------------------------+------------------------------------- As beginning Haskellers regularly ask about these laws and instances I think it would be good to have them documented where they are defined. Here's a first draft of what I have in mind for `Float`'s `Eq` and `Ord` instances: {{{ -- | Note that in the presence of @NaN@, this instance does not satisfy -- reflexivity: -- -- >>> nan = 0/0 :: Float -- >>> nan == nan -- False -- -- Also note that this instance does not encode structural equality: -- -- >>> 0 == (-0 :: Float) -- True -- >>> recip 0 == recip (-0 :: Float) -- False instance Eq Float where (==) = eqFloat }}} {{{ -- | Due to the peculiarities of @NaN@, this instance does not satisfy totality: -- -- >>> nan = 0/0 :: Float -- >>> nan <= nan -- False -- -- Another special case with @NaN@ is: -- -- @ -- 'compare' x y -- | 'isNaN' x || 'isNaN' y = 'GT' -- @ -- -- However -- -- @ -- nan > _ = False -- _ > nan = False -- @ -- -- In consequence we also have: -- -- @ -- 'max' x y | 'isNaN' x || 'isNaN' y = x -- 'min' x y | 'isNaN' x || 'isNaN' y = y -- @ -- -- Ignoring @NaN@, @Infinity@ and @-Infinity@ are the respective greatest -- and least elements of 'Float'. instance Ord Float where (F# x) `compare` (F# y) = if isTrue# (x `ltFloat#` y) then LT else if isTrue# (x `eqFloat#` y) then EQ else GT (F# x) < (F# y) = isTrue# (x `ltFloat#` y) (F# x) <= (F# y) = isTrue# (x `leFloat#` y) (F# x) >= (F# y) = isTrue# (x `geFloat#` y) (F# x) > (F# y) = isTrue# (x `gtFloat#` y) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15078> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 22

[GHC] #13913: Can't apply higher-ranked kind in type family
by GHC 26 Oct '18

26 Oct '18

#13913: Can't apply higher-ranked kind in type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This code doesn't typecheck due to `F2`: {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind f :: (forall (a :: Type). a -> a) -> Bool f g = g True type F1 (g :: forall (a :: Type). a -> a) = g True type family F2 (g :: forall (a :: Type). a -> a) :: Bool where F2 g = g True }}} {{{ $ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:14:6: error: • Expected kind ‘forall a. a -> a’, but ‘g’ has kind ‘Bool -> Bool’ • In the first argument of ‘F2’, namely ‘g’ In the type family declaration for ‘F2’ | 14 | F2 g = g True | ^ }}} This is surprising to me, since `F2` seems like the type family counterpart to `f` and `F1`, both of which typecheck. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13913> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #15765: Make the "extract" functions in RnTypes pure
by GHC 26 Oct '18

26 Oct '18

#15765: Make the "extract" functions in RnTypes pure -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 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: -------------------------------------+------------------------------------- Once upon a time, the `extract` functions at the bottom of RnTypes were pure. Then, along came `-XTypeInType`, which needed to do a check in these functions for users mixing type variables with kind variables. Now, however, with `-XTypeInType` gone again, we no longer do this check. Thus, there is no reason to keep these functions monadic. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15765> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #15802: Inlining of constant fails when both cross-module and recursive
by GHC 25 Oct '18

25 Oct '18

#15802: Inlining of constant fails when both cross-module and recursive -------------------------------------+------------------------------------- Reporter: j6carey | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Linux Architecture: x86_64 | Type of failure: Runtime (amd64) | performance bug Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- When an inline recursive function is applied to a constant, that application may reduce if it is in the same module, but will not reduce when in a different module. (Naturally, this harms the ability to split a program into modules while retaining efficiency.) For example, consider the following files: T1.hs: {{{#!hs module T1 where data IntList = Nil | Cons Int IntList mapIntList :: (Int -> Int) -> IntList -> IntList mapIntList f Nil = Nil mapIntList f (Cons x xs) = Cons (f x) (mapIntList f xs) {-# INLINE mapIntList #-} mappedNil :: IntList mappedNil = mapIntList id Nil }}} T2.hs: {{{#!hs module T2 where data IntList = Nil | Cons Int IntList mapIntList :: (Int -> Int) -> IntList -> IntList mapIntList f Nil = Nil mapIntList f (Cons x xs) = Cons (f x) (mapIntList f xs) {-# INLINE mapIntList #-} }}} T3.hs: {{{#!hs module T3 where import T2 mappedNil :: IntList mappedNil = mapIntList id Nil }}} The program built from T1.hs should be equivalent to the one built from T2.hs and T3.hs; however, the core output from GHC 8.6.1 with -O2 differs significantly. In the single-module case we obtain: {{{#!hs mappedNil = T1.Nil }}} Whereas in the two-module case we see: {{{#!hs mappedNil = mapIntList (id @ Int) T2.Nil }}} Recursion is relevant; the problem disappears if we make this change: {{{#!hs data IntList = Nil | Cons Int Int mapIntList :: (Int -> Int) -> IntList -> IntList mapIntList f Nil = Nil mapIntList f (Cons x xs) = Cons (f x) (f xs) {-# INLINE mapIntList #-} }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15802> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 7

[GHC] #12160: MonadFail instance for (Either String)?
by GHC 25 Oct '18

25 Oct '18

#12160: MonadFail instance for (Either String)? -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: libraries | Version: 8.0.1 (other) | 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: -------------------------------------+------------------------------------- I think one of the cool things about breaking out `MonadFail` would be the opportunity to introduce an instance for `Either String`, which isn’t possible to do with plain `Monad` without overlapping instances. The instance itself would be completely trivial: {{{#!hs instance MonadFail (Either String) where fail = Left }}} The only possible reason to ''not'' do this, as far as I can tell, would be because it requires `FlexibleInstances`. This already seems to be used for a few instances in `base`, and it seems like it would be extremely useful, so I would really appreciate if such an instance was defined. I’d be happy to submit a patch to add it, but I wasn’t sure if this would be an uncontroversial change or not. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12160> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 15

[GHC] #14332: Deriving clauses can have forall types
by GHC 25 Oct '18

25 Oct '18

#14332: Deriving clauses can have forall types -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: deriving | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC accepts Unknown/Multiple | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I made a horrifying discovery today: GHC accepts this code! {{{#!hs {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# OPTIONS_GHC -ddump-deriv #-} module Bug1 where class C a b data D a = D deriving ((forall a. C a)) }}} {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug1 ( Bug.hs, interpreted ) ==================== Derived instances ==================== Derived class instances: instance Bug1.C a1 (Bug1.D a2) where Derived type family instances: Ok, 1 module loaded. }}} It gets even worse with this example: {{{#!hs {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeInType #-} {-# OPTIONS_GHC -ddump-deriv -fprint-explicit-kinds #-} module Bug1 where import Data.Kind import GHC.Generics data Proxy (a :: k) = Proxy deriving ((forall k. (Generic1 :: (k -> Type) -> Constraint))) }}} {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug1 ( Bug.hs, interpreted ) ==================== Derived instances ==================== Derived class instances: instance GHC.Generics.Generic1 k (Bug1.Proxy k) where GHC.Generics.from1 x_a3ip = GHC.Generics.M1 (case x_a3ip of { Bug1.Proxy -> GHC.Generics.M1 GHC.Generics.U1 }) GHC.Generics.to1 (GHC.Generics.M1 x_a3iq) = case x_a3iq of { (GHC.Generics.M1 GHC.Generics.U1) -> Bug1.Proxy } Derived type family instances: type GHC.Generics.Rep1 k_a2mY (Bug1.Proxy k_a2mY) = GHC.Generics.D1 k_a2mY ('GHC.Generics.MetaData "Proxy" "Bug1" "main" 'GHC.Types.False) (GHC.Generics.C1 k_a2mY ('GHC.Generics.MetaCons "Proxy" 'GHC.Generics.PrefixI 'GHC.Types.False) (GHC.Generics.U1 k_a2mY)) Ok, 1 module loaded. }}} In this example, the `forall`'d `k` from the `deriving` clause is discarded and then unified with the `k` from `data Proxy (a :: k)`. All of this is incredibly unsettling. We really shouldn't be allowing `forall` types in `deriving` clauses in the first place. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14332> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 18

[GHC] #15589: Always promoting metavariables during type inference may be wrong
by GHC 25 Oct '18

25 Oct '18

#15589: Always promoting metavariables during type inference may be wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 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: -------------------------------------+------------------------------------- Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes. Consider {{{#!hs {-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies, AllowAmbiguousTypes #-} import Data.Proxy import Data.Type.Equality import Data.Type.Bool import Data.Kind data SameKind :: forall k. k -> k -> Type type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where IfK (_ :: Proxy True) f _ = f IfK (_ :: Proxy False) _ g = g y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True -> () y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d x = undefined in () }}} This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it. * We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j -> m -> n -> If j m n`, where `If :: forall k. Bool -> k -> k -> k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator. * In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2. * If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem. * Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`. * Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late. Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed. An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case -- promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=co… my thesis] -- section 6.5 to be specific.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15589> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 14

[GHC] #15497: Coercion Quantification
by GHC 25 Oct '18

25 Oct '18

#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 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://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2 -------------------------------------+------------------------------------- As described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2] We would like to have coercion quantifications back in Haskell Core language. This means in Core we can define types like {{{#!hs \/ (a: k1) . \/ (co : k1 ~ k2) -- an explicit quantification for the coercion -> (a |> co) -- use the name for an explicit cast -> ... }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #14859: Allow explicit impredicativity
by GHC 25 Oct '18

25 Oct '18

#14859: Allow explicit impredicativity -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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: -------------------------------------+------------------------------------- In [https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html this email] I suggested allowing a simple form of impredicativity. With a suitable extension flag (`-XExplicitImpredicativeTypes` perhaps), you woudl be allowed: * To write a polytype in a visible type argument; eg. `f @(forall a. a->a)` * To write a polytype as an argument of a type in a signature e.g. `f :: [forall a. a->a] -> Int` ''But that’s all''. A unification variable still cannot be unified with a polytype. The only way you can call a polymorphic function at a polytype is to use Visible Type Application (VTA). So using impredicative types might be tiresome. E.g. {{{ type SID = forall a. a->a xs :: [forall a. a->a] xs = (:) @SID id ( (:) @SID id ([] @ SID)) }}} In short, if you call a function at a polytype, you must use VTA. Simple, easy, predictable; and doubtless annoying. But at least it's possible. The main motivation is that we are naughtily doing this anyway in the implementation of `GeneralisedNewtypeDeriving` -- see Trac #14070 comment:23 ff. If we are doing it under the hood, we could just made it available to programmers. This is much less ambitious, and much easier to implement, than the proposed [https://www.microsoft.com/en-us/research/publication/guarded- impredicative-polymorphism/ Guarded impredicative polymorphism] (PLDI'18). This ticket just records the idea, to see what other use-cases people might want to add. Then someone would have to write a GHC proposal. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14859> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

[GHC] #15778: GHC HEAD-only panic (zonkTcTyVarToTyVar)
by GHC 25 Oct '18

25 Oct '18

#15778: GHC HEAD-only panic (zonkTcTyVarToTyVar) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following program typechecks on GHC 8.0.1 through 8.6.1: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind type a ~> b = a -> b -> Type type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data family Sing (a :: k) data Flarble (a :: Type) where MkFlarble :: Flarble Bool data instance Sing (z :: Flarble a) where SMkFlarble :: Sing MkFlarble elimFlarble :: forall a (p :: forall x. Flarble x ~> Type) (f :: Flarble a). Sing f -> Apply p MkFlarble -> Apply p f elimFlarble s@SMkFlarble pMkFlarble = case s of (_ :: Sing (MkFlarble :: Flarble probablyABadIdea)) -> pMkFlarble }}} However, it panics on GHC HEAD: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181015 for x86_64-unknown-linux): zonkTcTyVarToTyVar probablyABadIdea_aWn[tau:2] Bool Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcMType.hs:1627:34 in ghc:TcMType }}} If I replace `probablyABadIdea` with `Bool`, then it typechecks again. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15778> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8