- Glasgow-haskell-users

Re: Trouble with injective type families
by Anthony Clayden 07 Jul '17

07 Jul '17

> On Wed Jul 5 14:16:10 UTC 2017, Richard Eisenberg wrote: > I'd like to add that the reason we never extended System FC > with support for injectivity is that the proof of soundness > of doing so has remained elusive. Thank you Richard, Simon. IIRC the original FDs through CHRs paper did think it sound to allow given `C a b1` and `C a b2` conclude `b1 ~ b2` under a FunDep `a -> b`. (I think that was also the case in Mark Jones' original paper on FunDeps.) (See Iavor's comments on Trac #10675, for example.) I know GHC's current FunDep inference is lax, because there's good reasons to want 'wiggle room' with FunDep (in)consistency. I'm suggesting we could tighten that consistency check; then we might make make FD inference stronger(?) https://github.com/ghc-proposals/ghc-proposals/pull/56#issuecomment-3129745… AntC >> Am Mittwoch, den 05.07.2017, 06:45 +0000 schrieb Simon Peyton Jones: >> Functional dependencies and type-family dependencies only induce extra >> "improvement" constraints, not evidence. For example >> >> class C a b | a -> b where foo :: a -> b >> instance C Bool Int where ... >> >> f :: C Bool b => b -> Int >> f x = x -- Rejected >> >> Does the fundep on 'b' allow us to deduce (b ~ Int), GADT-like, in the >> body of 'f', and hence accept the definition. No, it does not. Think >> of the translation into System F. We get >> >> f = /\b \(d :: C Bool b). \(x::b). x |> ??? >> >> What evidence can I used to cast 'x' by to get it >> from type 'b' to Int? >> >> Rather, fundeps resolve ambiguity. Consider >> >> g x = foo True + x >> >> The call to 'foo True' gives rise to a "wanted" constraint (C Bool >> beta), where beta is a fresh unification variable. Then by the fundep >> we get an "improvement" constraint (also "wanted") (beta ~ Int). So we >> can infer g :: Int -> Int. >> >> >> In your example we have >> >> x :: forall a b. (T Int ~ b) => a >> x = False >> >> Think of the System F translation: >> >> x = /\a b. \(d :: T Int ~ b). False |> ?? >> >> Again, what evidence can we use to cast False to 'a'. >> >> >> In short, fundeps and type family dependencies only add extra >> unification constraints, which may help to resolve ambiguous >> types. They dont provide evidence. That's not to say that they >> couldn't. But you'd need to extend System FC, GHC's core language, to >> do so. >> >> Simon >> >> >>> >>> -----Original Message----- >>> From: Glasgow-haskell-users [mailto:glasgow-haskell-users- >>> bounces at haskell.org] On Behalf Of Wolfgang Jeltsch >>> Sent: 05 July 2017 01:21 >>> To: glasgow-haskell-users at haskell.org >>> Subject: Trouble with injective type families >>> >>> Hi! >>> >>> Injective type families as supported by GHC 8.0.1 do not behave like >>> I >>> would expect them to behave from my intuitive understanding. >>> >>> Let us consider the following example: >>> >>>> >>>> {-# LANGUAGE RankNTypes, TypeFamilyDependencies #-} >>>> >>>> class C a where >>>> >>>> type T a = b | b -> a >>>> >>>> instance C Bool where >>>> >>>> type T Bool = Int >>>> >>>> type X b = forall a . T a ~ b => a >>>> >>>> x :: X Int >>>> x = False >>> I would expect this code to be accepted. However, I get the >>> following >>> error message: >>> >>>> >>>> A.hs:14:5: error: >>>> Could not deduce: a ~ Bool >>>> from the context: T a ~ Int >>>> bound by the type signature for: >>>> x :: T a ~ Int => a >>>> at A.hs:13:1-10 >>>> a is a rigid type variable bound by >>>> the type signature for: >>>> x :: forall a. T a ~ Int => a >>>> at A.hs:11:19 >>>> In the expression: False >>>> In an equation for x: x = False >>>> Relevant bindings include x :: a (bound at A.hs:14:1) >>> This is strange, since injectivity should exactly make it possible >>> to >>> deduce a ~ Bool from T a ~ Int. >>> >>> Another example is this: >>> >>>> >>>> {-# LANGUAGE GADTs, TypeFamilyDependencies #-} >>>> >>>> class C a where >>>> >>>> type T a = b | b -> a >>>> >>>> instance C Bool where >>>> >>>> type T Bool = Int >>>> >>>> data G b where >>>> >>>> G :: Eq a => a -> G (T a) >>>> >>>> instance Eq (G b) where >>>> >>>> G a1 == G a2 = a1 == a2a >>> I would also expect this code to be accepted. However, I get the >>> following error message: >>> >>>> >>>> B.hs:17:26: error: >>>> Could not deduce: a1 ~ a >>>> from the context: (b ~ T a, Eq a) >>>> bound by a pattern with constructor: >>>> G :: forall a. Eq a => a -> G (T a), >>>> in an equation for == >>>> at B.hs:17:5-8 >>>> or from: (b ~ T a1, Eq a1) >>>> bound by a pattern with constructor: >>>> G :: forall a. Eq a => a -> G (T a), >>>> in an equation for == >>>> at B.hs:17:13-16 >>>> a1 is a rigid type variable bound by >>>> a pattern with constructor: G :: forall a. Eq a => a -> G >>>> (T >>>> a), >>>> in an equation for == >>>> at B.hs:17:13 >>>> a is a rigid type variable bound by >>>> a pattern with constructor: G :: forall a. Eq a => a -> G >>>> (T >>>> a), >>>> in an equation for == >>>> at B.hs:17:5 >>>> In the second argument of (==), namely a2 >>>> In the expression: a1 == a2 >>>> In an equation for ==: (G a1) == (G a2) = a1 == a2 >>>> Relevant bindings include >>>> a2 :: a1 (bound at B.hs:17:15) >>>> a1 :: a (bound at B.hs:17:7) >>> If b ~ T a and b ~ T a1, then T a ~ T a1 and subsequently a ~ a1, >>> because >>> of injectivity. Unfortunately, GHC does not join the two contexts (b >>> ~ T >>> a, Eq a) and (b ~ T a1, Eq a1). >>> >>> Are these behaviors really intended, or are these bugs showing up? >>>

1 0

Contradictions about DeriveDataTypeable in the manual?
by Chris Martin 26 Jun '17

26 Jun '17

Exhibit A: > With -XDeriveDataTypeable, you can derive instances of the class Data, defined in Data.Data. See "Deriving Typeable instances" for deriving Typeable. Exhibit B: > -XDeriveDataTypeable > Enable automatic deriving of instances for the Typeable typeclass Exhibit C: > Derived instances of Typeable are ignored, and may be reported as an error in a later version of the compiler. ---------------- A and B seem contradictory: Is this extension for deriving Data, or for deriving Typeable? B and C seem... not technically contradictory, but why is there an extension that enables the deriving of instances that will just be ignored? Is this extension meant to be deprecated? >From experimentation, it seems like all types automatically get Typeable instances whether you declare it or not. Is that accurate?

2 2

Proposal: Instance apartness guards
by Anthony Clayden 24 Jun '17

24 Jun '17

After years of pondering this idea (in various forms), and several rounds of discussion on several forums, I've written it up. "This proposal tackles the thorny topic of Overlapping instances, for both type classes and Type Families/Associated types, by annotating instance heads with type-level apartness Guards. Type-level disequality predicates appear in Sulzmann & Stuckey 2002; in the type-level case selection in HList 2004; and in various guises in Haskell cafe discussions in following years. This proposal builds on the apartness testing implemented as part of the Closed Type Families work." All feedback welcome. https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/propo… AntC

1 0

Untouchable type variables
by Wolfgang Jeltsch 19 Jun '17

19 Jun '17

Hi! Today I encountered for the first time the notion of an “untouchable” type variable. I have no clue what this is supposed to mean. A minimal example that exposes my problem is the following: > {-# LANGUAGE Rank2Types, TypeFamilies #-} > > import GHC.Exts (Constraint) > > type family F a b :: Constraint > > data T b c = T > > f :: (forall b . F a b => T b c) -> a > f _ = undefined This results in the following error message from GHC 8.0.1: > Untouchable.hs:9:6: error: > • Couldn't match type ‘c0’ with ‘c’ > ‘c0’ is untouchable > inside the constraints: F a b > bound by the type signature for: > f :: F a b => T b c0 > at Untouchable.hs:9:6-37 > ‘c’ is a rigid type variable bound by > the type signature for: > f :: forall a c. (forall b. F a b => T b c) -> a > at Untouchable.hs:9:6 > Expected type: T b c0 > Actual type: T b c > • In the ambiguity check for ‘f’ > To defer the ambiguity check to use sites, enable AllowAmbiguousTypes > In the type signature: > f :: (forall b. F a b => T b c) -> a I have no idea what the problem is. The type of f looks fine to me. The type variable c should be universally quantified at the outermost level. Why does the type checker even introduce a type variable c0? All the best, Wolfgang

4 4

Profiling plugins
by M Farkas-Dyck 12 Jun '17

12 Jun '17

How is this done? I am working on ConCat [https://github.com/conal/concat] and we need a profile of the plugin itself. I tried "stack test --profile" but that does a profile of the test program, not the plugin. Can i do this and not rebuild GHC?

2 1

8.2.1-rc2 upgrade report
by Alberto Valverde 08 Jun '17

08 Jun '17

Hi, I've finally managed to upgrade all the dependencies of the proprietary app I mentioned some days ago in this list and there are good and bad differences I've noticed between 8.0.2 that I'd like to share. The bad ----------- * An optimized cold build (-O2) is about 3 times slower (~53s vs. ~2m55s) and consumes more memory (~2Gb vs. ~7Gb) at it's peak. The good ------------- * An un-optimized cold build (-O0) takes about the same time (~21s, phew! :) It's maybe even slightly faster with 8.2 (too few and badly taken measurements to really know, though) * The optimized executable is slightly faster and allocates less memory. For this app it makes up for the performance regression of the optimized build (which is almost always done by CI), IMHO. I did only a couple of runs and only wrote down [1] the last run results (which were similar to the previous results) so take these observations with a grain of salt (except maybe the optimized build slowdown, which doesn't have much margin for variance to be skewing the results). I also measured the peak memory usage by observing "top". In case gives a clue: The app is a multi-threaded 2D spread simulator which deals with many mmapped Storable mutable vectors and has been pretty optimized for countless hours (I mean by this that it has (too) many INLINE pragmas. Mostly on polymorphic functions to aid in their specialization). I think some of this information can be deduced from the results I'm linking at the footer. I believe the INLINEs are playing a big part of the slowdown since the slowest modules to compile are the "Main" ones which put everything together, along with the typical lens-th-heavy "Types" ones. I'd like to help by producing a reproducible and isolated benchmark or a better analysis or ... so someone more knowledgeable than me on GHC internals can someday hopefully attack the regression. Any pointers on what would help and where can I learn to do it? Thanks! [1] https://gist.github.com/albertov/46fbb13d940f67a569f9a25c1cb8154c

2 2

[ANNOUNCE] GHC 8.2.1 release candidate 2
by Ben Gamari 19 May '17

19 May '17

Hello everyone, The GHC team is very pleased to announce the second candidate of the 8.2.1 release of the Glasgow Haskell Compiler. Source and binary distributions are available at https://downloads.haskell.org/~ghc/8.2.1-rc2/ This is the second of what will likely be either two or three release candidates leading up the final 8.2.1 release. This release will feature, * A new type-indexed Typeable implementation * The long awaited Backpack * Deriving strategies for disambiguating DeriveAnyClass, GeneralizedNewtypeDeriving, and stock mechanisms * Overloaded record fields * Improved compiler performance * Better code generation through more robust tracking of join points * Compact regions for more efficient garbage collection and serialization * Better support for machines with non-uniform memory architectures * More robust support for levity (e.g. RuntimeRep) polymorphism * A simple interface for streaming eventlog data from live processes * Further refinement of DWARF support This candidate fixes most of the issues present in release candidate one including, * #13233: typePrimRep panic while compiling GHC with profiling enabled * #13509: type error involving unboxed tuples * #13426: compile-time memory-usage regression * #13560: Windows binary distributions carry absolute paths to toolchain * #13585: Control.Lens.Wrapped.ala causes compiler panic * #13623: Join points produce bad code for stream fusion As always, please let us know if you have difficulty. Thanks to everyone who has contributed! Happy testing, - Ben

3 5

Re: [ANNOUNCE] GHC 8.2.1 release candidate 2
by Ben Gamari 16 May '17

16 May '17

Markus Trippelsdorf <markus(a)trippelsdorf.de> writes: > On 2017.05.15 at 22:47 -0400, Ben Gamari wrote: >> >> >> The GHC team is very pleased to announce the second candidate of the >> 8.2.1 release of the Glasgow Haskell Compiler. Source and binary >> distributions are available at >> >> https://downloads.haskell.org/~ghc/8.2.1-rc2/ >> >> This is the second of what will likely be either two or three release >> candidates leading up the final 8.2.1 release. This release will >> feature, >> >> As always, please let us know if you have difficulty. Thanks to everyone >> who has contributed! >> >> Happy testing, > > Unfortunately xmobar segfaults from time to time when build with > 8.2.1-rc2, e.g.: > Thanks for your report! Segfaults are certainly no good. Do you know whether these are also reproducible with rc1? What version of xmobar are you using? What does your configuration look like? I've started an xmobar built from upstream's master branch with an empty configuration to see whether this is reproducible locally. I've opened #13707 to track this. Cheers, - Ben

1 0

Unused import warning on re-export
by Yitzchak Gale 15 May '17

15 May '17

I have a module A with no export list, and a function f which from the API point of view should part of the export list of A. But f must be defined in module B, not module A, due an import cycle. I added this line in module A to re-export f from A: import B as A (f) This resulted in an unused import warning. That is a problem for us - we keep our large code base clean of warnings as a policy. Is there a reason GHC considers this case an unused import? It seems that the use of the import is explicitly stated right within the import itself. Should I submit a ticket for this? Thanks, Yitz

3 3

Re: Superclass Equality constraints cp FunDeps
by Anthony Clayden 08 May '17

08 May '17

Now that I've got the bit between my teeth ... Superclass constraints are not subject to the Paterson conditions. IOW I can write superclass constraints that are not permitted as instance constraints. (Superclass constraints are required to be non-cyclic, which ensures they're terminating.) Is that worth adding to the docos? Something like this is OK: > class (F a b ~ b) => C a b ... > -- equivalently > class (D a b b) => C a b ... Can I think of a use for that? Maybe ... Sometimes even though you have a type function, you can use knowledge of the result to 'improve' the parameters. The classic case is adding type-level Naturals. Maybe even type-level Boolean And: - if the result is True, so must be the params. - if the result is False, and you know one param is True, the other must be False. - but that can't be a function, because if the result is False and you know one param is False, that tells nothing about the other param. AntC > > On Sun Apr 30 19:45:34 UTC 2017, Richard Eisenberg > wrote: > > > Documentation is just about always suboptimal -- but the > > best people to suggest concrete improvements are those > > who were confused to begin with. So, by all means, > > submit patches! > > OK. Done. See #13657. >

2 1