November 2015 - ghc-tickets

[GHC] #9131: Experiment with a dedicated solver for Coercible
by GHC 01 Mar '17

01 Mar '17

#9131: Experiment with a dedicated solver for Coercible ------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: task | Status: new Priority: low | 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: | ------------------------------------+------------------------------------- This is something that I might want to do some time; it should not distract us from working and improving the current design and implementation. But I think it should be explored. Currently `Coercible` appears as a type class, we have instances to explain it, and use the existing solver to solve them. The last part sometimes causes problems: * the order the instances are tried matters, there might be dead ends (#9117) * recursive newtypes are not handled as good as they could be. It would be worth exploring if a dedicated solver for `Coercible` constraints could solve these issues. It could replace the existing `getCoercibleInst`. Given a constraint `Coercible s t` it would solve it completely, do nothing or (and this is not planned out yet) return some sufficient and in some sense primitive constraint that should appear in inferred type signatures etc. Ideally we could still explain `Coercible` in terms of the instances written in the ICFP’14 paper, and simply state „GHC will find a solution using these instances, if there are any.“ instead of „The usual solver is employed, it might run into dead ends (or not, hard to tell).“ When tackling this task, I should do something that I keep postponing (because I don’t like to admit my lack of knowlege about that) but I think is really important: What are the theoretical properties of solving `Coercible` constraints? Is it even decidable? Semi decidable? Are there existing standard algorithms? How does this relate to SMT solving? And why don’t I know these things... -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9131> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 9

[GHC] #9117: Coercible constraint solver misses one
by GHC 01 Mar '17

01 Mar '17

#9117: Coercible constraint solver misses one ------------------------------------+------------------------------------- Reporter: goldfire | 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: | ------------------------------------+------------------------------------- When I say {{{ import Data.Type.Coercion import Data.Coerce eta :: Coercible f g => Coercion (f a) (g a) eta = Coercion }}} I get {{{ Could not coerce from ‘f a’ to ‘g a’ because ‘f a’ and ‘g a’ are different types. arising from a use of ‘Coercion’ from the context (Coercible f g) bound by the type signature for eta :: Coercible f g => Coercion (f a) (g a) at /Users/rae/temp/Roles.hs:6:8-44 In the expression: Coercion In an equation for ‘eta’: eta = Coercion }}} But, this coercion is easily expressible in Core. If `(co :: f ~R# g)` then `(co <a> :: f a ~R# g a)`, where `<a>` is the notation for a reflexivity coercion for the type `a`. The constraint solver should be able to do this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9117> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 35

[GHC] #8779: Exhaustiveness checks for pattern synonyms
by GHC 28 Feb '17

28 Feb '17

#8779: Exhaustiveness checks for pattern synonyms -------------------------------------------+------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: -------------------------------------------+------------------------------- Pattern synonyms are great, as they decouple interface from implementation. Especially if #8581 is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting! Another missing piece is exhaustiveness checks. Given this pattern {{{ initLast [] = Nothing initLast xs = Just (init xs, last xs) pattern xs ::: x <- (initLast -> Just (xs,x)) }}} we want the compiler to tell the programmer that {{{ f [] = ... f (xs ::: x) = ... }}} is complete, while {{{ g (xs ::: x) = ... }}} is not. With view pattern directly, this is impossible. But the programmer did not write view patterns! So here is what I think might work well, inspired by the new `MINIMAL` pragma: We add a new pragma `COMPLETE_PATTERNS` (any ideas for a shorter name). The syntax is essentially the same as for `MINIMAL`, i.e. a boolean formula, with constructors and pattern synonyms as atoms. In this case. {{{ {-# COMPLETE_PATTERNS [] && (:::) #-} }}} Multiple pragmas are obviously combined with `||`, and there is an implicit `{-# COMPLETE_PATTERNS [] && (:) #-}` listing all real data constructors. When checking for exhaustiveness, this would be done before unfolding view patterns, and for `g` above we get a warning that `[]` is not matched. Again, the implementation is very much analogous to `MINIMAL`. Clearly, a library author can mess up and give wrong `COMPLETE_PATTERNS` pragmas. I think that is ok (like with `MINIMAL`), and generally an improvement. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8779> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 58

[GHC] #10246: Literal Pattern match loses order
by GHC 26 Feb '17

26 Feb '17

#10246: Literal Pattern match loses order -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- I found this long-standing bug while investigating #10245: Consider this code: {{{ f1 :: Int -> String f1 n = case n of 0 -> "bar" 0x10000000000000000 -> "foo" _ -> "c" {-# NOINLINE f1 #-} g1 :: Int -> String g1 n = if n == 0 then "bar" else if n == 0x10000000000000000 then "foo" else "c" {-# NOINLINE g1 #-} f2 :: Int -> String f2 n = case n of 0x10000000000000000 -> "foo" 0 -> "bar" _ -> "c" {-# NOINLINE f2 #-} g2 :: Int -> String g2 n = if n == 0x10000000000000000 then "foo" else if n == 0 then "bar" else "c" {-# NOINLINE g2 #-} main = do let i = read "0" :: Int print (f1 i) print (g1 i) print (f2 i) print (g2 i) }}} According to the report, `f1` should behave like `g1` and `f2` should behave like `g2`. But that is not the case: I get {{{ "foo" "bar" "foo" "foo" }}} The reason is that the branches are sorted, to create fancy code for it, but this does not take into account that `0x10000000000000000 = 0`, at least for `Int`. This bug is present also in 7.8.4, and not (directly) related to my CmmSwitch code: It can also be observed with interpreted code, so the fix must happen earlier. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10246> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 7

[GHC] #9533: Signed/unsigned integer difference between compiled and interpreted code
by GHC 26 Feb '17

26 Feb '17

#9533: Signed/unsigned integer difference between compiled and interpreted code -------------------------------------+------------------------------------- Reporter: MichaelBurge | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Keywords: | Operating System: Windows Architecture: x86_64 (amd64) | Type of failure: Incorrect Difficulty: Unknown | result at runtime Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- The following code outputs "A". {{{#!hs import Data.Word x :: Word x = 10 y :: Word y = 11 test = case x - y of -1 -> "A" _ -> "B" main = putStrLn $ show test }}} However, adding a new case that isn't matched causes the output to change: {{{#!hs import Data.Word x :: Word x = 10 y :: Word y = 11 test = case x - y of 5 -> "C" -1 -> "A" _ -> "B" main = putStrLn $ show test }}} With the extra '5 -> "C"' line in the case, the output is "B". It gets weirder - interpreted code actually continues to match the -1 case. With the second example in a file 'T.hs', here is a GHCi session: {{{ Prelude Main> :l *T.hs [1 of 1] Compiling Main ( T.hs, interpreted ) Ok, modules loaded: Main. *Main> main "A" *Main> :l T.hs Ok, modules loaded: Main. Prelude Main> main "B" Prelude Main> }}} These examples suggest to me at least 3 improvements: * Issue a warning when a negative number is used in a case statement in unsigned context * Interpreted code should give the same result as compiled code * Adding a case that isn't matched shouldn't change which other patterns get matched -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9533> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 7

[GHC] #10940: Random number chosen by openTempFile is always 1804289383846930886
by GHC 26 Feb '17

26 Feb '17

#10940: Random number chosen by openTempFile is always 1804289383846930886 -------------------------------------+------------------------------------- Reporter: andersk | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: | Version: 7.10.2 libraries/base | Keywords: | Operating System: Linux Architecture: | Type of failure: Incorrect result Unknown/Multiple | at runtime Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | -------------------------------------+------------------------------------- {{{#!hs import System.Directory import System.IO main = do (p, _) <- openTempFile "/tmp" "" print p removeFile p }}} {{{#!console $ runghc temp.hs "/tmp/1804289383846930886" $ runghc temp.hs "/tmp/1804289383846930886" $ runghc temp.hs "/tmp/1804289383846930886" $ runghc temp.hs "/tmp/1804289383846930886" }}} This “random” number is the concatenation of the first two numbers 1804289383, 846930886 returned by glibc’s `rand()` when not seeded (or seeded with 1). This is not immediately a library security bug, I think: the file is created with `O_EXCL`, and if it already exists, `openTempFile` will move onto the next value 16816927771714636915, and so on. However, the predictable filenames make a potential application security bug that much more likely. (For your amusement, [https://www.google.com/search?q=1804289383846930886 Google 1804289383846930886].) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10940> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #10343: Make Typeable track kind information better
by GHC 22 Feb '17

22 Feb '17

#10343: Make Typeable track kind information better -------------------------------------+------------------------------------- Reporter: oerjan | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.10.1 Component: Compiler | Operating System: Unknown/Multiple Keywords: | Type of failure: None/Unknown Architecture: | Blocked By: Unknown/Multiple | Related Tickets: 9858 Test Case: typeOf :: | Typeable (a::k) => Proxy a -> | TypeRep | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- With all the apparent exploitable bugs now fixed, #9858 seems to be settling down. Simon P.J. asked me to make a new ticket for some quibbles I still have with limitations of the new design. These started with some examples that I discussed there pre-implementation with Richard Eisenberg, and which he concluded could be supported by a "sufficently smart solver". In the new (current) design, a `TypeRep` ''does'' contain kind information, which as I understand it is a list of `KindRep`s for the explicit kind parameters applied to the type constructor after type inference. This is sufficient to prevent confusing the same type constructor used at different kinds, and also easily supports type application ''provided'' the `TypeRep`s of the parts are known. For this, the internal `Typeable` constraint solver only ever needs to combine `TypeRep`s, never decompose them. Since no one else complained in #9858, I assume this is enough for what people are currently using `Typeable` for. However: I think the current `TypeRep` representation for `Typeable (a :: k)` doesn't contain enough information to generally extract the `KindRep` for `k` itself, much less to decompose it, even if the internal `Typeable` solver were to try. This prevents some polykinded code that is intuitively sound, and which "worked" in the old system, although if only because it didn't try to track kinds at all. For example, the following expression, with `PolyKinds` enabled: {{{#!hs typeOf :: Typeable a => Proxy a -> TypeRep }}} In the old system, this worked simply by combining the `TypeRep` for `Proxy` with the `TypeRep` for `a`. But in the new system, it fails, because the `TypeRep` for `Proxy` needs to know the kind of `a`, which is neither statically known nor available from the `TypeRep` of `a`. You would need to have compile-time information about the type constructor of `a` to even know how to build the `KindRep` from the kind arguments. This problem with constructing `TypeRep`s would arise whenever a polykinded type constructor is applied to a type whose kind is not a known monomorphic one. The second similar one I can think of is {{{#!hs typeRep :: Typeable a => Proxy (Typeable a) -> TypeRep }}} In an ideal system, we can also find use cases that require not just extracting the `KindRep` for a type, but also decomposing it. Here is my very hypothetical kitchen sink example from [comment:46:ticket:9858] (this example was made up as a test case before I knew what the new solver would support): {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE AutoDeriveTypeable #-} import Data.Typeable newtype C a b = C () step :: Proxy (a :: [k] -> *) -> Proxy (C a :: [k -> *] -> *) step Proxy = Proxy nest :: Typeable (a :: [k] -> *) => Int -> Proxy a -> TypeRep nest 0 x = typeRep x nest n x = nest (n-1) (step x) main = print $ nest 10 (Proxy :: Proxy (C () :: [()] -> *)) }}} Here, to make this compile, the solver would need to derive `Typeable (C a :: [k -> *] -> *]` from `Typeable (a :: [k] -> *)`, which at runtime requires first extracting the `KindRep` of `k` from the `TypeRep` of `a`, and then building the `TypeRep` for the correctly kinded `C`. At least the former part seems essentially impossible with the current `TypeRep` representation, even with a more clever solver. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10343> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 38

[GHC] #11011: Type-indexed TypeReps, Static Pointers and Distributed Closures
by GHC 21 Feb '17

21 Feb '17

#11011: Type-indexed TypeReps, Static Pointers and Distributed Closures -------------------------------------+------------------------------------- Reporter: bjmprice | Owner: Type: feature | Status: new request | 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: -------------------------------------+------------------------------------- There is a mock-up of a new API for type indexed type representations, basic Dynamic functionality, static pointers and distributed closures (https://github.com/brprice/typeableT) based on https://ghc.haskell.org/trac/ghc/wiki/TypeableT. We would like to invite comments and discussion from the community using this ticket as a more permenant home that email. One particular point that would benefit from more eyes is the polymorphic static pointers support. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11011> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 52

[GHC] #9432: IncoherentInstances are too restricted
by GHC 16 Feb '17

16 Feb '17

#9432: IncoherentInstances are too restricted -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature request | Status: new Priority: high | Milestone: Component: Compiler (Type | Version: 7.8.2 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: -------------------------------------+------------------------------------- Hello! The reason behind using `IncoherentInstances`is that we want GHC to commit to a specific instance even if after instantiation of some variables, other instance could be more specific (http://www.haskell.org/ghc/docs/7.0.4/html/users_guide/type-class- extensions.html). There is one problem though. Lets consider following example (which could not make much sense, but shows the problem well): {{{#!haskell {-# OPTIONS_GHC -fno-warn-missing-methods #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE IncoherentInstances #-} {-# LANGUAGE ScopedTypeVariables #-} module Main where import Data.Typeable -------------------------------------------------------------------------------- -- Type classes -------------------------------------------------------------------------------- class InferType a where inferType :: Proxy a -> Proxy a inferType = undefined -------------------------------------------------------------------------------- -- Proxy datatypes -------------------------------------------------------------------------------- data Id0 = Id0 deriving (Show, Typeable) data Id1 t1 = Id1 deriving (Show, Typeable) data Id2 t1 t2 = Id2 deriving (Show, Typeable) data Id3 t1 t2 t3 = Id3 deriving (Show, Typeable) data Id4 t1 t2 t3 t4 = Id4 deriving (Show, Typeable) data Id5 t1 t2 t3 t4 t5 = Id5 deriving (Show, Typeable) -------------------------------------------------------------------------------- -- Instances -------------------------------------------------------------------------------- instance InferType Int instance (InferType m, InferType a) => InferType (m a) instance (a~Id0) => InferType (a :: *) instance (a~Id1) => InferType (a :: * -> *) instance (a~Id2) => InferType (a :: * -> * -> *) -------------------------------------------------------------------------------- -- Tests -------------------------------------------------------------------------------- toProxy :: a -> Proxy a toProxy _ = Proxy --inferTypeBase :: a -> Proxy a inferTypeBase a = inferType $ toProxy a instance InferType Foo1 instance InferType Foo2 tm _ = 5 data Foo1 a = Foo1 a deriving (Show, Typeable) data Foo2 a b = Foo2 a b deriving (Show, Typeable) instance Monad Id1 -- dummy instances just for tests instance Num Id0 main = do print $ typeOf $ inferType $ toProxy $ (return (5)) print $ typeOf $ inferType $ toProxy $ (5) print $ typeOf $ inferType $ toProxy $ (Foo1 (return 5)) print $ typeOf $ inferType $ toProxy $ (Foo2 (return 5) (return 5)) print "hello" ---- OUTPUT: -- Proxy (Id1 Id0) -- Proxy Id0 -- Proxy (Foo1 (Id1 Id0)) -- Proxy (Foo2 (Id1 Id0) (Id1 Id0)) -- "hello" }}} The idea is very simple - replace all unknown type variables with known ones. It works great, but the problem appears with the function `inferTypeBase`. It should have type of `a -> Proxy a`, but GHC claims it has got `Id0 -> Proxy Id0`. It is of course caused by enabled `-XIncoherentInstances` flag, but I think GHC should be more liberal here. If it really cannot pick any instance (causing an error using only `OverlappingInstances`), the `IncoherentInstances` should allow it to pick matching one even if more specific could be available after instantianization. But If no error would occur while using `OverlappingInstances`, `IncoherentInstances` should not affect the way it resolves the instances. I think this would make `IncoherentInstances` much more useful than now. Maybe it would be good to just add some options to the flag? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9432> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #11031: Record Pattern Synonym Cleanup
by GHC 14 Feb '17

14 Feb '17

#11031: Record Pattern Synonym Cleanup -------------------------------------+------------------------------------- Reporter: mpickering | Owner: Type: task | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.10.2 Keywords: newcomer | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Ben comments that there are some loose ends with record pattern synonyms. * It's still not clear to me that the free variables produced in rnPatSynBind are correct * Perhaps in the future we want to refactor tc_single to use a function which extends the typechecking environment instead of using setGblEnv * @mpickering's suggested refactoring of RecSelId to RecSelId (Either PatSyn TyCon) Bool described in the comment in TcExpr.hs * There is a TODO in tc_patsyn_finish which should either be clarified so it can be considered actionable, removed, or just fixed The comment from TcExpr was: > I tried to refactor RecSelId to RecSelId [DataCon] Bool but this causes some pain when it comes to the interface files. Next try it is something like RecSelId (Either PatSyn TyCon) Bool with the aim for something better in the future. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11031> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4