June 2014 - 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] #8405: experiment with using function-sections for linking (for smaller libs and executables)
by GHC 12 Feb '17

12 Feb '17

#8405: experiment with using function-sections for linking (for smaller libs and executables) ------------------------------------+------------------------------------- Reporter: carter | Owner: Type: task | Status: new Priority: normal | Milestone: 7.10.1 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: | ------------------------------------+------------------------------------- currently the only support we have for making small (ish) executables using split objects, which 1. is not on by default, for various good reasons 2. can seriously penalize compile times 3. in tandem, something like strip is often used, but on some platforms/targets (such as the iOS cross compiler), strip will actually break things might be worth seriously experimenting with function-sections / gc- sections in the object files we generate. example slide deck on this http://elinux.org/images/2/2d/ELC2010-gc- sections_Denys_Vlasenko.pdf -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8405> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 21

[GHC] #8155: Defaulting bug or unfortunate error message with closed type families
by GHC 08 Feb '17

08 Feb '17

#8155: Defaulting bug or unfortunate error message with closed type families ------------------------------------+------------------------------------- Reporter: nh2 | 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: | ------------------------------------+------------------------------------- https://github.com/nh2/infinite-type-families/blob/master/Test2.hs Some code extracted from hmatrix: {{{ {-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleInstances #-} module Test where data Vector a = Vector a data Matrix a = Matrix a class Build f where build' :: BoundsOf f -> f -> ContainerOf f #if __GLASGOW_HASKELL__ <= 706 -- Normal type families with GHC 7.6, works well. type family BoundsOf x type instance BoundsOf (a->a) = Int type instance BoundsOf (a->a->a) = (Int,Int) type family ContainerOf x type instance ContainerOf (a->a) = Vector a type instance ContainerOf (a->a->a) = Matrix a #else -- Closed type families for GHC 7.8 type family BoundsOf x where BoundsOf (a->a->a) = (Int,Int) BoundsOf (a->a) = Int type family ContainerOf x where ContainerOf (a->a) = Vector a ContainerOf (a->a->a) = Matrix a #endif instance (Num a) => Build (a->a) where build' = buildV buildV :: (Integral a, Num b) => a -> (b -> c) -> Vector c buildV _ _ = undefined }}} This is probably related to #8154. With GHC 7.7, we get the following error: {{{ Test2.hs:59:14: Could not deduce (BoundsOf (a -> a) ~ Integer) from the context (Num a) bound by the instance declaration at Test2.hs:58:10-32 Expected type: BoundsOf (a -> a) -> (a -> a) -> ContainerOf (a -> a) Actual type: Integer -> (a -> a) -> Vector a Relevant bindings include build' :: BoundsOf (a -> a) -> (a -> a) -> ContainerOf (a -> a) (bound at Test2.hs:59:5) In the expression: buildV In an equation for ‛build'’: build' = buildV }}} 1) Where does this Integer come from? 2) Change {{{ BoundsOf (a->a) = Int }}} into {{{ BoundsOf (a->a) = Integer }}} You get the same error message, although clearly {{{BoundsOf (a -> a) ~ Integer}}} (you just wrote that down).[[BR]] Even if the order matters in closed type families, is this not the wrong error message? 3) If you flip the order so that the (a->a) case comes first, it works (with both it Int or Integer). I don't quite understand why. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8155> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #8901: (very) bad inline heuristics
by GHC 25 Jan '17

25 Jan '17

#8901: (very) bad inline heuristics ------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- I observe a bad case for inlining blowup for the time library. Observed for 7.7, just checked in 7.9. The problem is so bad that the PowerPC32 assembler cannot resolve cross- routine references. (I have no error message at hand, but could try to get one.) Instead here are the stats for x86, with inlining and certain inlining suppressed. The architecture seems irrelevant. {{{ $ file ./libraries/time/dist-install/build/Data/Time/Format.o ./libraries/time/dist-install/build/Data/Time/Format.o: Mach-O object i386 $ ls -l ./libraries/time/dist-install/build/Data/Time/Format.* -rw-r--r-- 1 ggreif staff 61875 Mar 15 16:48 ./libraries/time/dist- install/build/Data/Time/Format.dyn_hi -rw-r--r-- 1 ggreif staff 450864 Mar 15 16:48 ./libraries/time/dist- install/build/Data/Time/Format.dyn_o -rw-r--r-- 1 ggreif staff 61863 Mar 15 16:48 ./libraries/time/dist- install/build/Data/Time/Format.hi -rw-r--r-- 1 ggreif staff 332216 Mar 15 16:48 ./libraries/time/dist- install/build/Data/Time/Format.o }}} With following patch applied: <https://github.com/ggreif/packages- time/commit/83f08b8896b950707a910fed4e30bddb7ee7f52f> I get: {{{ $ ls -l ./libraries/time/dist-install/build/Data/Time/Format.* -rw-r--r-- 1 ggreif staff 10554 Mar 16 00:08 ./libraries/time/dist- install/build/Data/Time/Format.dyn_hi -rw-r--r-- 1 ggreif staff 106832 Mar 16 00:08 ./libraries/time/dist- install/build/Data/Time/Format.dyn_o -rw-r--r-- 1 ggreif staff 10542 Mar 16 00:08 ./libraries/time/dist- install/build/Data/Time/Format.hi -rw-r--r-- 1 ggreif staff 78864 Mar 16 00:08 ./libraries/time/dist- install/build/Data/Time/Format.o }}} The factor is 4.2 for Format.o, Format.dyn_o and 5.8 for the .hi files. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8901> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 12

[GHC] #8156: amd64 + in-tree gmp build broken
by GHC 23 Jan '17

23 Jan '17

#8156: amd64 + in-tree gmp build broken -------------------------------------+------------------------------------- Reporter: errge | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.8.1 Component: Build System | Version: 7.7 Keywords: | Operating System: Unknown/Multiple Architecture: x86_64 (amd64) | Type of failure: Building GHC Difficulty: Easy (less than 1 | failed hour) | Test Case: Blocked By: | Blocking: Related Tickets: #4022 #4366 #4374 | -------------------------------------+------------------------------------- Currently, the GHC build system has an in-tree GMP. This GMP seems to be used only if there is no usable GMP found on the system and the user didn't provide one using configure flags. When we build GHC using an external shared version of GMP, the resulting GHC is dynamically linked against GMP and also the generated programs are linked dynamically against GMP. When the in-tree GMP is used, it is built statically, even if the GHC we are building is shared GHC on GNU/Linux. This feature is currently broken on amd64 (#4366, #4022), but is working currently very well on Linux i686. Apart from the breakage this setting is very flexible and I'd be very happy if it were possible to keep it, in spite of removeal requests like #4374. When there is a system GMP, nothing would change, this is the most typical usage, e.g. distributions are all building this way. On the other hand, if the user removes his GMP (maybe we should provide an option to explicity trigger this in ./configure, instead of having to remove GMP); she can build a GHC that is not linked dynamically against GMP and the resulting programs are not linked either. This makes it possible to generate binaries that link dynamically against libc (no -static) which is quite compatible amongst versions, but doesn't require a libgmp.so to run. For binary deployments this seems to be the best kind of setup nowadays. Now, if we were only able to fix this for amd64. See this: https://www.gentoo.org/proj/en/base/amd64/howtos/index.xml?part=1&chap=3 On amd64 we can continue to compile GMP statically and link into the binary library, we just have to compile GMP with the fPIC. I attached the patch to fix this. Previously a similar patch has been rejected in #4022 because "this shouldn't be platform specific", but this is clearly not the case, this is specific to amd64. Tadaaaam: {{{ errge@sid64:~/ghc/inplace/bin$ cat test.hs main = print (2^100) errge@sid64:~/ghc/inplace/bin$ ./ghc-stage2 test.hs [1 of 1] Compiling Main ( test.hs, test.o ) Linking test ... errge@sid64:~/ghc/inplace/bin$ ./test 1267650600228229401496703205376 errge@sid64:~/ghc/inplace/bin$ ldd ./test linux-vdso.so.1 (0x00007fff79962000) libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fe4b9a83000) librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007fe4b987a000) libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fe4b9676000) libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fe4b92c6000) libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fe4b90a6000) /lib64/ld-linux-x86-64.so.2 (0x00007fe4b9d83000) }}} No GMP! I attach the build file patch to the bugreport. So, can we please apply this patch and just keep the in-tree GMP? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8156> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 11

[GHC] #9223: Type equality makes type variable untouchable
by GHC 21 Jan '17

21 Jan '17

#9223: Type equality makes type variable untouchable -------------------------------------------+------------------------------- Reporter: Feuerbach | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | 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: -------------------------------------------+------------------------------- This doesn't look right: {{{ {-# LANGUAGE RankNTypes, TypeFamilies #-} type family TF (m :: * -> *) run1 :: (forall m . Monad m => m a) -> a run1 = undefined run2 :: (forall m . (Monad m, TF m ~ ()) => m a) -> a run2 = undefined -- this works x1 = run1 (return ()) -- this fails x2 = run2 (return ()) {- Couldn't match expected type ‘a’ with actual type ‘()’ ‘a’ is untouchable inside the constraints (Monad m, TF m ~ ()) bound by a type expected by the context: (Monad m, TF m ~ ()) => m a at untouchable.hs:15:6-21 ‘a’ is a rigid type variable bound by the inferred type of x2 :: a at untouchable.hs:15:1 Relevant bindings include x2 :: a (bound at untouchable.hs:15:1) In the first argument of ‘return’, namely ‘()’ In the first argument of ‘run2’, namely ‘(return ())’ -} }}} I would expect x2 to type check just like x1 does. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9223> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 13

[GHC] #9137: A way to match RULES only for literals
by GHC 17 Jan '17

17 Jan '17

#9137: A way to match RULES only for literals ------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | 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: | ------------------------------------+------------------------------------- In `GHC/Enum` we have {{{ {-# RULES "enumDeltaToInteger1" [0] forall c n x . enumDeltaToIntegerFB c n x 1 = up_fb c n x 1 #-} -- This rule ensures that in the common case (delta = 1), we do not do the check here, -- and also that we have the chance to inline up_fb, which would allow the constructor to be -- inlined and good things to happen. -- We do not do it for Int this way because hand-tuned code already exists, and -- the special case varies more from the general case, due to the issue of overflows. }}} This rule would be useful for all literals, not just for `1`. I remember a discussion that such a rule would be more useful if we had a way to specify that, for example (random syntax). {-# RULES "enumDeltaToInteger1" [0] forall c n x d . isLiteral d => enumDeltaToIntegerFB c n x d = up_fb c n x d #-} I’m reporting this now to be able to link to it from #9136, where this feature might also help. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9137> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #8761: Make pattern synonyms work with Template Haskell
by GHC 10 Jan '17

10 Jan '17

#8761: Make pattern synonyms work with Template Haskell ------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 7.8.1-rc1 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Template Haskell has no support for pattern synonyms. This should be added. Specifically: * Create syntax in `Language.Haskell.TH.Syntax` and corresponding functions in `Language.Haskell.TH.Lib` * Support in !DsMeta for desugaring pattern synonym quotations. See `rep_bind`. * Support in Convert for splicing in pattern synonyms. * Support in !TcSplice for reifying pattern synonyms. See `reifyThing`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8761> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 26