December 2014 - ghc-tickets

[GHC] #9427: Do finer-grained dependency analysis to infer more general kinds on type/class declarations
by GHC 27 May '18

27 May '18

#9427: Do finer-grained dependency analysis to infer more general kinds on type/class declarations -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- In the resolution to #9200, as detailed [wiki:GhcKinds/KindInference#Apossiblevariation here], we identified an area for improvement. This improvement was not implemented in the fix for #9200. This ticket will track just this improvement. (In brief: we can do better dependency analysis on mutually recursive type/class declarations to allow more kinds to generalize earlier. This would lessen the burden on programmers to put in kind annotations. See the wiki page.) A solid but unfinished attempt is [https://github.com/goldfirere/ghc/tree /re-sort-non-cusk-decls here]. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9427> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks.
by GHC 25 May '18

25 May '18

#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Operating System: Keywords: type family, | Unknown/Multiple ambiguity check | Type of failure: GHC Architecture: Unknown/Multiple | rejects valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Before the type ambiguity check was introduced, I could write the following code {{{ {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} -- {-# LANGUAGE AllowAmbiguousTypes #-} module T where type family Arr (repr :: * -> *) (a :: *) (b :: *) :: * class ESymantics repr where int :: Int -> repr Int add :: repr Int -> repr Int -> repr Int lam :: (repr a -> repr b) -> repr (Arr repr a b) app :: repr (Arr repr a b) -> repr a -> repr b {- te4 :: (Arr repr (Arr repr Int Int) (Arr repr Int Int) ~ Arr repr (Arr repr Int Int) (Arr repr Int b), ESymantics repr) => repr b -} te4 = let c3 = lam (\f -> lam (\x -> f `app` (f `app` (f `app` x)))) in (c3 `app` (lam (\x -> x `add` int 14))) `app` (int 0) -- t = lam (\f -> f `app` int 0) newtype R a = R{unR :: a} type instance Arr R a b = a -> b instance ESymantics R where int = R add (R x) (R y) = R $ x + y lam f = R $ unR . f . R app (R f) (R x) = R $ f x tR = unR te4 }}} (This is a simple code abstracted from a longer code that for sure worked in 2010: I showed it in a SSGIP lecture at Oxford.) The inferred type of te4 is shown in comments. The type is not ideal but the best what can be done under circumstances. In tR, repr is instantiated to R and the type function Arr can finally be applied and the equality constraint resolved. Since then, the type inference has changed and the code no longer type checks: {{{ Could not deduce (Arr repr (Arr repr a0 b0) (Arr repr a2 b0) ~ Arr repr (Arr repr a b) (Arr repr a4 b)) from the context (ESymantics repr, Arr repr a4 a3 ~ Arr repr a b, Arr repr a3 a ~ Arr repr a b) bound by the inferred type for ‘c3’: (ESymantics repr, Arr repr a4 a3 ~ Arr repr a b, Arr repr a3 a ~ Arr repr a b) => repr (Arr repr (Arr repr a b) (Arr repr a4 b)) }}} What is worse, there does not appear to be *any* way to get the code to type check. No amount of type annotations helps. The code has to be dramatically re-written, or just given up. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 13

[GHC] #9607: Type checking regression between GHC 7.6 and 7.8
by GHC 25 May '18

25 May '18

#9607: Type checking regression between GHC 7.6 and 7.8 -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Operating System: Keywords: | Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: GHC Difficulty: Unknown | rejects valid program Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Jason McCarty [http://www.haskell.org/pipermail/haskell- cafe/2014-September/116076.html reported on Haskell-cafe] that this code used to work with GHC 7.6 but in GHC 7.8 it requires `AllowAmbiguousTypes`: {{{#!hs -- The code below is simplified from code that computes a tensor product of -- a tensor with an identity matrix whose size is determined from the -- shapes of the input and output tensors. {-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-} --{-# LANGUAGE AllowAmbiguousTypes #-} module Tensors where import GHC.TypeLits type family (as :: [Nat]) ++ (bs :: [Nat]) :: [Nat] type instance '[] ++ bs = bs type instance (a ': as) ++ bs = a ': (as ++ bs) data Tensor (s :: [Nat]) = Tensor -- content elided -- apparently GHC reduces (++) enough to see that n is determined leftUnit :: Tensor s -> Tensor ('[n, n] ++ s) leftUnit Tensor = Tensor -- accepted in 7.6, not accepted in 7.8 without AllowAmbiguousTypes rightUnit :: Tensor s -> Tensor (s ++ '[n, n]) rightUnit Tensor = Tensor -- also accepted without AllowAmbiguousTypes outsideUnit :: Tensor s -> Tensor ('[n] ++ s ++ '[n]) outsideUnit Tensor = Tensor useleftUnit :: Tensor '[1,1,2] useleftUnit = leftUnit Tensor -- type of Tensor is inferred userightUnit :: Tensor '[1,2,2] userightUnit = rightUnit (Tensor :: Tensor '[1]) -- type must be provided }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9607> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family
by GHC 23 May '18

23 May '18

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- We hoped that closed type families could replace overlapping instances. It is not currently the case: GHC can resolve overlapping instances but cannot resolve the similar closed type family. I'm attaching a minimized example of program where it can be observed. This is reproducible on ghc-7.8.3 and HEAD. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9918> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 21

[GHC] #9640: Invalid object in processHeapClosureForDead(): 2130762223
by GHC 19 May '18

19 May '18

#9640: Invalid object in processHeapClosureForDead(): 2130762223 -------------------------------------+------------------------------------- Reporter: Fuuzetsu | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- I just tried using {{{-hb}}} profiling for Yi and hit {{{ yi: internal error: Invalid object in processHeapClosureForDead(): 2130762223 (GHC version 7.8.3 for x86_64_unknown_linux) Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug Aborted }}} Unfortunately I don't have an easy way to replicate. In my case it's to check out HEAD version of Yi, build with profiling and run {{{ [nix-shell:~/programming/yi/yi]$ TERM=xterm yi_datadir=. dist/build/yi/yi -fpango --as=emacs -y /tmp /tmp/long +RTS -p -hb }}} where {{{/tmp/long}}} here is just a file with 1MB of the letter {{{A}}} repeated on a single line. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9640> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #9840: Permit empty closed type families
by GHC 18 May '18

18 May '18

#9840: Permit empty closed type families -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Operating System: Keywords: | Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: Difficulty: Unknown | None/Unknown Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- At the moment, closed type families without any equations fail with a parse error. In addition, they cannot be created by TH (see #8028). Would it be possible to permit these instead? My use case is in my typechecker plugin for units of measure, where I want to add new type-level operators without any equational theory (because it will be supplied by the plugin) and without users having the ability to introduce their own type family instances. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9840> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 13

[GHC] #8089: Implementation of GHC.Event.Poll.poll is broken due to bad coercion
by GHC 16 May '18

16 May '18

#8089: Implementation of GHC.Event.Poll.poll is broken due to bad coercion -------------------------------------------+------------------------------- Reporter: merijn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 7.6.3 Keywords: patch | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Easy (less than 1 hour) | Type of failure: Runtime Blocked By: | crash Related Tickets: | Test Case: | Blocking: -------------------------------------------+------------------------------- Due to an unsafe coercion in GHC.Event.Poll.poll the implementation has a bug that on some platforms (.e.g. linux) results in subtly wrong semantics and on other platforms (e.g. OS X) downright crashes the runtime. The offending line is line 95 in GHC/Event/Poll.hsc: {{{ c_poll ptr (fromIntegral len) (fromIntegral (fromTimeout tout)) }}} `fromTimeout` returns a timeout in seconds as a value of type Int. `c_poll` takes a timeout in seconds as a value of type CInt. If the max value of Int is larger than that of CInt, this coercion results in an overflow, producing a negative value. The faulty semantics are in turn caused by passing this negative value as timeout to `c_poll`. This overflow happens on many 64bit platforms where GHC's Int is 64bit, but CInt is often 32bit. The result of passing a negative value to poll() depends on the platform, but is (on all platforms I checked) different from the desired semantics! On linux any negative timeouts are treated as infinite, this means that a poll() with a timeout that should be finite results in an infinitely blocking poll on linux! On OSX any negative timeout other than -1 (which is treated as infinity) is considered an invalid parameter, returning an error and crashing the runtime. A minimal example reproducing the error (on systems where `fromIntegral (maxBound :: Int) > (fromIntegral (maxBound :: CInt) :: Integer)`): {{{ import Control.Concurrent main = threadDelay maxBound }}} Using 64bit GHC on OSX this produces an immediate runtime crash. The attached patch solves the issue by comparing the Int timeout against the max value of CInt and, if necessary, looping multiple `c_poll` calls (with a timeout equal to `maxBound :: CInt`) if they return `0` (which indicates the timeout has expired with no events occurring). See also: https://github.com/merijn/packages- base/commit/6d8ea02a3f6a2cdb82a9ad786a8c4db780b92091 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8089> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 22

[GHC] #8995: When generalising, use levels rather than global tyvars
by GHC 05 May '18

05 May '18

#8995: When generalising, use levels rather than global tyvars ------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- A long time ago Didier Remy described how to use 'ranks' or 'levels' to make the test "is this type variable free in the environment" when generalising a type. Oleg gives a [http://okmij.org/ftp/ML/generalization.html great explanation here]. GHC still uses the old "find the free type variables in the environment" method. But in fact GHC ''does'' maintain levels, just as Didier explains. The level is called `Untouchables` and is used to make sure we don't infer non-principal types for things involving GADTs. The same level stuff is used to prevent skolem-escape. Details with `Note [Untouchable type variables]` and `Note [Skolem escape prevention]` in `TcType`. So it ought to be straightforward to use the same levels for generalisation. I had a go, and came across the following tricky points: * We need to bump the level (`pushUntouchables`) when starting to typecheck a let RHS. Currently we don't. That will be a bit less efficient, because we'll end up deferring unification constraints that currently get solved immediately. * However the current set up is actually wrong. In particular, we generate a constraint where the implications do not have monotonically increasing level numbers (invariant `(ImplicInv)` in `TcType`). Try this program with `-ddump-tc-trace`. {{{ {-# LANGUAGE GADTs #-} module Bar where data T where MkT :: a -> (a->Int) -> T f x z = case x of MkT _ _ -> let g y = (y, [z,Nothing]) in (g True, g 'c') }}} I don't know how to make this bug cause an actual problem, but it's very unsettling. Bumping the level before doing the RHS would solve this. * Once we have bumped the level, we then have to do some more type- variable promotion, especially of type variables free in the finally- chosen type of the binder. This came out rather awkwardly in the code. * Because we now get more deferred equality constraints, there's a real risk that we'll end up quantifying over them. If we get, say `(gbl ~ Maybe lcl)`, where `gbl` is a type var free in the envt, we '''do not''' want to quantify over it! (It would be sound, but would lead to horrible types.) A long time ago Didier Remy described how to use 'ranks' or 'levels' to make the test "is this type variable free in the environment" when generalising a type. Oleg gives a [http://okmij.org/ftp/ML/generalization.html great explanation here]. GHC still uses the old "find the free type variables in the environment" method. But in fact GHC ''does'' maintain levels, just as Didier explains. The level is called `Untouchables` and is used to make sure we don't infer non-principal types for things involving GADTs. The same level stuff is used to prevent skolem-escape. Details with `Note [Untouchable type variables]` and `Note [Skolem escape prevention]` in `TcType`. So it ought to be straightforward to use the same levels for generalisation. I had a go, and came across the following tricky points: * We need to bump the level (`pushUntouchables`) when starting to typecheck a let RHS. Currently we don't. That will be a bit less efficient, because we'll end up deferring unification constraints that currently get solved immediately. * However the current set up is actually wrong. In particular, we generate a constraint where the implications do not have monotonically increasing level numbers (invariant `(ImplicInv)` in `TcType`). Try this program with `-ddump-tc-trace`. {{{ {-# LANGUAGE ExistentialQuantification #-} module Bar where data T = forall a. MkT a f x z = case x of MkT y -> let g y = [y,Nothing] in g True }}} Look for the `reportUnsolved` trace and you'll nested implications, both with level 1. I don't know how to make this bug cause an actual problem, but it's very unsettling. Bumping the level before doing the RHS would solve this. * Once we have bumped the level, we then have to do some more type- variable promotion, especially of type variables free in the finally- chosen type of the binder. This came out rather awkwardly in the code. * Because we now get more deferred equality constraints, there's a real risk that we'll end up quantifying over them. If we get, say `(gbl ~ Maybe lcl)`, where `gbl` is a type var free in the envt, we '''do not''' want to quantify over it! (It would be sound, but would lead to horrible types.) Rather we want to promote `lcl`, and not quantify. Currently we don't get many deferred equality constraints, becuase they all get done "on the fly". But if we do get one, we do quantify over it, which yields a rather stupid type. Try this: {{{ {-# LANGUAGE ExistentialQuantification #-} module Bar where data T = forall a. MkT a f x z = case x of MkT _ -> let g y = [z,Nothing] in (g True, g 'c') }}} We get this `g :: forall t a2. Maybe a ~ Maybe a2 => t -> [Maybe a2]`, where `x::a` is in the envt. Not very clever! This only shows up with existentials and In general I think we want to find all the type variables reachable by equality constraints from the environment, and not quantify over them. * We also use the type environment `getGlobalTyVars` in ''kind'' generalisation, and kind inference currently does not use the untoucahble story. Adapting it to use levels might be tricky because we currently assume we solve all kind equality constraints on-the-fly, and don't gather any deferreed constraints. Maybe it's easy, but needs thought. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8995> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #9113: Template Haskell should warn about non-exhaustive pattern matches
by GHC 03 May '18

03 May '18

#9113: Template Haskell should warn about non-exhaustive pattern matches -------------------------+------------------------------------------------- Reporter: tvh | Owner: Type: bug | Status: new Priority: | Milestone: normal | Version: 7.8.2 Component: | Operating System: Unknown/Multiple Template Haskell | Type of failure: Incorrect warning at Keywords: | compile-time Architecture: | Test Case: Unknown/Multiple | Blocking: Difficulty: | Unknown | Blocked By: | Related Tickets: | -------------------------+------------------------------------------------- When using Typed Template Haskell, There are no warings for non-exhaustive patterns inside the quote. {{{ {-# LANGUAGE TemplateHaskell #-} module Foo where import Language.Haskell.TH.Lib foo :: Maybe Int -> TExpQ Bool foo x = [||case x of Nothing -> False||] }}} Instead the warnings appear where the code is spliced. {{{ {-# LANGUAGE TemplateHaskell #-} module Bar where import Foo x = $$(foo (Just 1)) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9113> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 2

[GHC] #8970: Non-exhaustive pattern match warning with DataKinds and TypeFamilies
by GHC 03 May '18

03 May '18

#8970: Non-exhaustive pattern match warning with DataKinds and TypeFamilies ------------------------------------+------------------------------------- Reporter: tensor5 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- The code is: {{{ data K = Foo | Bar data D1 :: K -> * where F1 :: D1 Foo B1 :: D1 Bar class C (a :: K -> *) where data D2 a :: K -> * foo :: a k -> D2 a k -> Bool instance C D1 where data D2 D1 k where F2 :: D2 D1 Foo B2 :: D2 D1 Bar foo F1 F2 = True foo B1 B2 = True }}} With -Wall it gives the warning: {{{ Test.hs:23:5: Warning: Pattern match(es) are non-exhaustive In an equation for `foo': Patterns not matched: F1 B2 B1 F2 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8970> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5