October 2017 - ghc-devs

RE: GHC rewrite rule type-checking failure
by Simon Peyton Jones 17 Oct '17

17 Oct '17

The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS Well this would be something qualitatively new. We don’t that ability in rules; and it’s far from clear to me what it would mean anyway. I suppose that if k was instantiated to a ground type then you might hope to solve it, but what if it was instantiated to some in-scope type variable t, and some variable of type (C t) was in scope. Should that work too? I’m highly dubious. Happily it sounds as if you are making progress with help from Joachim. Simon From: conal.elliott(a)gmail.com [mailto:conal.elliott@gmail.com] On Behalf Of Conal Elliott Sent: 03 October 2017 16:30 To: Simon Peyton Jones <simonpj(a)microsoft.com> Subject: Re: GHC rewrite rule type-checking failure The revised example I gave earlier in the thread: ``` haskell class C k where comp' :: k b c -> k a b -> k a c instance C (->) where comp' = (.) -- Late-inlining version to enable rewriting. comp :: C k => k b c -> k a b -> k a c comp = comp' {-# INLINE [0] comp #-} morph :: (a -> b) -> k a b morph = error "morph: undefined" {-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph f #-} -- • Could not deduce (C k) arising from a use of ‘comp’ -- from the context: C (->) -- bound by the RULE "morph/(.)" ``` A hypothetical generated Core rule (tweaked slightly from Joachim's note): ``` haskell forall (@ k) (@ b) (@ c) (@ a) ($dC :: C (->)) (f :: a -> b) (g :: b -> c). morph @ k @ a @ c (comp @ (->) @ b @ c @ a $dC g f) = comp @ k @ b @ c @ a $dC' (morph @ k @ b @ c g) (morph @ k @ a @ b f) where $dC' :: C k ``` The new bit here is that `$dC'` is not found via matching in the LHS, but rather by instance resolution from `k`, which does appear explicitly in the LHS. If `C k` cannot be solved, the rule fails. The "where" clause here lists the dictionary variables to be instantiated by instance resolution rather than matching. -- Conal On Tue, Oct 3, 2017 at 8:01 AM, Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> wrote: But synthesising from what? And currently no: there is no type-class dictionary synthesis after the type checker. Not impossible I suppose, but one more fragility: a rule does not fire because some synthesis thing didn’t happen. Maybe give an as-simple-as-poss example of what you have in mind, now you understand the situation better? With all the type and dictionary abstractions written explicitly… S From: conal.elliott(a)gmail.com<mailto:conal.elliott@gmail.com> [mailto:conal.elliott@gmail.com<mailto:conal.elliott@gmail.com>] On Behalf Of Conal Elliott Sent: 03 October 2017 15:56 To: Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> Subject: Re: GHC rewrite rule type-checking failure Thanks, Simon. Your explanation make sense to me. Do you think that the rewrite rule mechanism could be enhanced to try synthesizing the needed dictionaries after LHS matching and before RHS instantiation? I'm doing as much now in my compiling-to-categories plugin, but without the convenience of using concrete syntax for the rules. Regard, - Conal On Tue, Oct 3, 2017 at 12:27 AM, Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> wrote: * Is it feasible for GHC to combine the constraints needed LHS and RHS to form an applicability condition? I don’t think so. Remember that a rewrite rule literally rewrites LHS to RHS. It does not conjure up any new dictionaries out of thin air. In your example, (D k b) is needed in the result of the rewrite. Where can it come from? Only from something matched on the left. So GHC treats any dictionaries matched on the left as “givens” and tries to solve the ones matched on the left. If it fails you get the sort of error you see. One way to see this is to write out the rewrite rule you want, complete with all its dictionary arguments. Can you do that? Simon From: Glasgow-haskell-users [mailto:glasgow-haskell-users-bounces@haskell.org<mailto:glasgow-haskell-users-bounces@haskell.org>] On Behalf Of Conal Elliott Sent: 03 October 2017 01:03 To: Joachim Breitner <mail(a)joachim-breitner.de<mailto:mail@joachim-breitner.de>> Cc: glasgow-haskell-users(a)haskell.org<mailto:glasgow-haskell-users@haskell.org> Subject: Re: GHC rewrite rule type-checking failure Thanks very much for the reply, Joachim. Oops! I flubbed the example. I really `morph` to distribute over an application of `comp`. New code below (and attached). You're right that I wouldn't want to restrict the type of `morph`, since each `morph` *rule* imposes its own restrictions. My questions: * Is it feasible for GHC to combine the constraints needed LHS and RHS to form an applicability condition? * Is there any way I can make the needed constraints explicit in my rewrite rules? * Are there any other work-arounds that would enable writing such RHS-constrained rules? Regards, -- Conal ``` haskell {-# OPTIONS_GHC -Wall #-} -- Demonstrate a type checking failure with rewrite rules module RuleFail where class C k where comp' :: k b c -> k a b -> k a c instance C (->) where comp' = (.) -- Late-inlining version to enable rewriting. comp :: C k => k b c -> k a b -> k a c comp = comp' {-# INLINE [0] comp #-} morph :: (a -> b) -> k a b morph = error "morph: undefined" {-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph f #-} -- • Could not deduce (C k) arising from a use of ‘comp’ -- from the context: C (->) -- bound by the RULE "morph/(.)" ``` On Mon, Oct 2, 2017 at 3:52 PM, Joachim Breitner <mail(a)joachim-breitner.de<mailto:mail@joachim-breitner.de>> wrote: Hi Conal, The difference is that the LHS of the first rule is mentions the `C k` constraint (probably unintentionally): *RuleFail> :t morph comp morph comp :: C k => k1 (k b c) (k a b -> k a c) but the LHS of the second rule side does not: *RuleFail> :t morph addC morph addC :: Num b => k (b, b) b A work-around is to add the constraint to `morph`: morph :: D k b => (a -> b) -> k a b morph = error "morph: undefined" but I fear that this work-around is not acceptable to you. Joachim Am Montag, den 02.10.2017, 14:25 -0700 schrieb Conal Elliott: > -- Demonstrate a type checking failure with rewrite rules > > module RuleFail where > > class C k where comp' :: k b c -> k a b -> k a c > > instance C (->) where comp' = (.) > > -- Late-inlining version to enable rewriting. > comp :: C k => k b c -> k a b -> k a c > comp = comp' > {-# INLINE [0] comp #-} > > morph :: (a -> b) -> k a b > morph = error "morph: undefined" > > {-# RULES "morph/(.)" morph comp = comp #-} -- Fine > class D k a where addC' :: k (a,a) a > > instance Num a => D (->) a where addC' = uncurry (+) > > -- Late-inlining version to enable rewriting. > addC :: D k a => k (a,a) a > addC = addC' > {-# INLINE [0] addC #-} > > {-# RULES "morph/addC" morph addC = addC #-} -- Fail > > -- • Could not deduce (D k b) arising from a use of ‘addC’ > -- from the context: D (->) b > > -- Why does GHC infer the (C k) constraint for the first rule but not (D k b) > -- for the second rule? > > _______________________________________________ > Glasgow-haskell-users mailing list > Glasgow-haskell-users(a)haskell.org<mailto:Glasgow-haskell-users@haskell.org> > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskel…> -- Joachim Breitner mail(a)joachim-breitner.de<mailto:mail@joachim-breitner.de> http://www.joachim-breitner.de/<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim…>

2 4

Compiling natively GHC for ARMv7l softabi
by shiftag＠nanotek.info 16 Oct '17

16 Oct '17

Hi List, I would like to install GHC for my CPU which is an ARMv7L Soft-ABI NEON FPU. I read some stuff on ARM and GHC related. So it appears that an installation is possible but with a RPi. The problem is the stack binary which has been compiled for Hard-Float target. So it should not be difficult to make it work for my architecture. I checked for stack sources (stack-1.5.1.tar.gz) but I have any clue about how to compile it. Can you give me an hand ? Cheers, PS: For info, usually I compiled natively that way : "-march=armv7-a -mfpu=neon -mtune=cortex-a9"

2 1

Can I get the internal name of a package at runtime?
by MarLinn 15 Oct '17

15 Oct '17

Hi. I'm experimenting with plug-ins right now. I did manage to dynamically load functions at runtime. The caveat: Something (cabal? ghc?) mangles the package names. For example, to load a function called "theFunction" from a module called "Callee" in a package "Plugin", I had to address it via the name "Pluginzm0zi0zi0zi0zm2QaFQQzzYhnKJSPRXA7VtPe_Callee_theFunction_closure". O…K. Most parts of that are clear, and thanks for making my package cooler by appending a "z", but who is this Ozi guy and why is he rapping about modems? Without knowing Ozi, the only way I found to get at this magic string is to manually look at the actual ELF-header of the compiled module. While that might be a robust way, it seems neither portable nor elegant. The "plugins" library failed too, probably for the same reason. (Or it's under-documented. Probably both.) The "dynamic-loader" library does something via c, therefore no. Which brings me to the question: Is there any way for a module to get at its own internal package name? Or even at the internal name of an external package? If not, can I somehow recreate the magic mangling at runtime? At first I thought the functions in the "Module", "Name" etc modules of GHC might help – but it seems I either need an existing Name (that I have no idea how to get) or I have to create one (with no idea what magic mangler to call). I'm asking this question here rather than on café as I feel that if there is a solution, it's probably buried in the details of GHC. Thanks for any suggestions, MarLinn

4 8

Invariants about UnivCo?
by Nicolas Frisby 11 Oct '17

11 Oct '17

[I summarize with some direct questions at the bottom of this email.] I spent time last night trying to eliminate -dcore-lint errors from my record and variant library using the coxswain row types plugin. I made some progress, but I'm currently stuck, as discussed on this github Issue. https://github.com/nfrisby/coxswain/issues/3#issuecomment-330577609 Here's the relevant bit: The latest unresolved -dcore-lint error is an out-of-scope cobox co var. I'm certainly not creating it *directly* (there are no U(plugin:coxswain,... in the Core Lint warning), but I have to wonder if my somewhat loose use of UnivCo is violating some assumptions somewhere that's causing GHC to drop the co var binding or overlook this occurrence of it on a renaming/subst pass. I checked UnivCo for source comments looking for anything it should *not* be used for, but I didn't find an obvious explanation along those lines. I haven't yet been able to effectively distill the test case. I'm doing this all at -O0. With `-ddump-tc-trace`, I can see the offending cobox (cobox_a67M) is present in an "implication evbinds" listing after a "solveImplication end }" delimiter, but that's the last obvious binding of it. [G] cobox_a67J = CO Sym cobox_a654, [G] cobox_a67M = cobox_a67J `cast` U(plugin:coxswain,...) cobox_a654 is introduced by a GADT pattern match. I'm also not seeing obvious occurrences of cobox_a67M, but I think the reason is that I'm seeing several (Sym cobox) with no uniques printed (even with `-dppr-debug`). Those are probably the cobox in question, but I can't confirm. Questions: 1) Is there a robust way to ensure that covar's uniques are always printed? (Is the pprIface reuse with a free cobox part of the issue here?) 2) Is my plugin asking for this kind of trouble by using UnivCo to cast coboxes? 3) If I spent the effort to create non-UnivCo coercions where possible, would that likely help? This is currently an "eventually" task, but I haven't seen an urgency for it yet. I could bump its priority if it might help. E.G. I'm using UnivCo to cast entire givens when all I'm doing is reducing a type family application somewhere "deep" within the given's predtype. I could, with considerable effort, instead wrap a single, localized UnivCo within a bunch of non-UnivCo "lifting" coercion constructors. Would that likely help? 3) Is there a usual suspect for this kind of situation where a cobox binding is seemingly dropped (by the typechecker) even though there's an occurrence of it? Thank you for your time. -Nick

3 10

Call for features for GHC 8.4
by Ben Gamari 11 Oct '17

11 Oct '17

Hello everyone, The release of GHC 8.4 is quickly approaching, with a release targetted for February 2018. To allow plenty of time for stabilization, we would like to cut the ghc-8.4 branch sometime in November. Currently there are relatively few items on the 8.4 status page [1]. If you have a feature which you would like to see in 8.4 but is not listed there please do add it soon. Also note that if things go according to plan, 8.6 will come a mere six months after 8.4 so if you have a large feature which won't make it for 8.4, do not fret; another release will be just around the corner. Cheers, - Ben [1] https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.4.1

4 5

Deprecating STM invariant mechanism
by Ben Gamari 09 Oct '17

09 Oct '17

tl;dr. Do you use Control.Monad.STM.always? If so say so on this [1] proposal otherwise the interface may be removed. Hello everyone, GHC's STM subsystem has long had the ability to run user-specified invariant checks when committing transactions, embodied by the Control.Monad.STM.always and alwaysSucceeds functions. However, if Hackage is any indication this feature has seen very little use of the past ten years. In fact, it has very likely been quite broken (#14310) for this entire duration. Consequently, I suggest that we begin deprecating the mechanism. See the deprecation Proposal [1] for full details. Please leave a comment if you object. Cheers, - Ben [1] https://github.com/ghc-proposals/ghc-proposals/pull/77

2 1

In C--: should CmmCall and CmmProc agree on their live registers?
by Moritz Angermann 06 Oct '17

06 Oct '17

Hi, apologies for writing so many emails recently. This is a minor spinoff from the "The Curious Case of T6084" email. While digging into it, I keep asking myself if CmmProc’s live registers should match those of the CmmCall that is calling it? Is there any invariant we try to enforce or would want to enforce? - Can the CmmProcs live registers be a strict superset of the corresponding CmmCalls? From the source comments in `compiler/cmm/Cmm.hs`: > Registers live on entry. Note that the set of live > registers will be correct in generated C-- code, but > not in hand-written C-- code. However, > splitAtProcPoints calculates correct liveness > information for CmmProcs. I would assume that this is an invalid case? - Can the CmmProcs live registers be a strict subset of the corresponding CmmCalls? This case however seems to be valid case. However, this makes me wonder if we can, and should(?) propagate the live register info from the CmmProc to the CmmCall so that they match up, and the registers are not kept live at the origin of the CmmCall if they aren’t needed? And as such potentially compute anything to put into the registers the CmmCall considers live, but the CmmProc would ignore anyway? Cheers, Moritz

2 3

Segmentation faults of bootstrap compiler?
by Ben Gamari 06 Oct '17

06 Oct '17

Hello everyone, Earlier this week there was a commit (perhaps ef26182e2014b0a2a029ae466a4b121bf235e4e4) which appears to trigger segmentation faults of the stage 0 compiler (GHC 8.2.1) during validation on Harbormaster (e.g. [1]). Unfortunately I've been unable to reproduce this reliably. Has anyone else observed this in their own environment? Cheers, - Ben [1] https://phabricator.haskell.org/harbormaster/build/35554/

1 1

Determine instance method from class method callsite
by Robin Palotai 06 Oct '17

06 Oct '17

Sorry, I messed up subject and mailing list. Copying to both list now after the mistake (wanted only ghc-devs for specificity). Thanks! 2017-09-19 7:36 GMT+02:00 Robin Palotai <palotai.robin(a)gmail.com>: > Hello GHC devs, > > Before inventing the wheel, want to check if there is a GHC API way to > look up the (fully) resolved instance method from a class method. > > For example, given a code > > data Foo Int deriving Show > > bar = show (Foo 3) > > when inspecting the Typechecked AST for bar's show call, I would like to > get to the Name / Id of 'show' of the 'Show' typeclass. > > I believe I could use splitHsSigmaTy on the HsType of the function call to > get the context, and then evaluate the HsWrapper somehow to find out what > instance dictionary is applied to the class restriction in the context, and > then look up the instance method from the dictionary.. > > Two questions: > > 1) Is there maybe functionality for this? > > 2) If not, is there any guarantee about the constraint order in the > context, at the method call? So I could more easily determine which > constraint's application to look for.. > > Any hints welcome && Thank you! > Robin >

2 5

Windows build broken
by Simon Peyton Jones 04 Oct '17

04 Oct '17

My Windows build is broken again. With a clean checkout, I get "" Target platform inferred as: x86_64-unknown-mingw32 Unknown OS msys How can I get past this? Full log below. Simon make[1]: Leaving directory '/c/code/HEAD/testsuite' ['libraries/array/', 'libraries/base/', 'libraries/binary/', 'libraries/bytestring/', 'libraries/Cabal/Cabal', 'libraries/Cabal/', 'libraries/compact/', 'libraries/containers/', 'libraries/deepseq/', 'libraries/directory/', 'libraries/doc/', 'libraries/dph/dph-base', 'libraries/dph/dph-prim-interface', 'libraries/dph/dph-prim-seq', 'libraries/dph/dph-prim-par', 'libraries/dph/dph-lifted-base', 'libraries/dph/dph-lifted-boxed', 'libraries/dph/dph-lifted-copy', 'libraries/dph/dph-lifted-vseg', 'libraries/dph/', 'libraries/dph/', 'libraries/filepath/', 'libraries/ghc-boot/', 'libraries/ghc-boot-th/', 'libraries/ghc-compact/', 'libraries/ghc-prim/', 'libraries/ghci/', 'libraries/haskeline/', 'libraries/hoopl/', 'libraries/hpc/', 'libraries/integer-gmp/', 'libraries/integer-simple/', 'libraries/mtl/', 'libraries/parallel/', 'libraries/parsec/', 'libraries/pretty/', 'libraries/primitive/', 'libraries/process/', 'libraries/random/', 'libraries/stm/', 'libraries/template-haskell/', 'libraries/terminfo/', 'libraries/text/', 'libraries/time/', 'libraries/transformers/', 'libraries/unix/', 'libraries/vector/', 'libraries/Win32/', 'libraries/xhtml/'] Creating libraries/array/ghc.mk Creating libraries/base/ghc.mk Creating libraries/binary/ghc.mk Creating libraries/bytestring/ghc.mk Creating libraries/Cabal/Cabal/ghc.mk Creating libraries/containers/ghc.mk Creating libraries/deepseq/ghc.mk Creating libraries/directory/ghc.mk Creating libraries/dph/dph-base/ghc.mk Creating libraries/dph/dph-prim-interface/ghc.mk Creating libraries/dph/dph-prim-seq/ghc.mk Creating libraries/dph/dph-prim-par/ghc.mk Creating libraries/dph/dph-lifted-base/ghc.mk Creating libraries/dph/dph-lifted-boxed/ghc.mk Creating libraries/dph/dph-lifted-copy/ghc.mk Creating libraries/dph/dph-lifted-vseg/ghc.mk Creating libraries/filepath/ghc.mk Creating libraries/ghc-boot/ghc.mk Creating libraries/ghc-boot-th/ghc.mk Creating libraries/ghc-compact/ghc.mk Creating libraries/ghc-prim/ghc.mk Creating libraries/ghci/ghc.mk Creating libraries/haskeline/ghc.mk Creating libraries/hoopl/ghc.mk Creating libraries/hpc/ghc.mk Creating libraries/integer-gmp/ghc.mk Creating libraries/integer-simple/ghc.mk Creating libraries/mtl/ghc.mk Creating libraries/parallel/ghc.mk Creating libraries/parsec/ghc.mk Creating libraries/pretty/ghc.mk Creating libraries/primitive/ghc.mk Creating libraries/process/ghc.mk Creating libraries/random/ghc.mk Creating libraries/stm/ghc.mk Creating libraries/template-haskell/ghc.mk Creating libraries/terminfo/ghc.mk Creating libraries/text/ghc.mk Creating libraries/time/ghc.mk Creating libraries/transformers/ghc.mk Creating libraries/unix/ghc.mk Creating libraries/vector/ghc.mk Creating libraries/Win32/ghc.mk Creating libraries/xhtml/ghc.mk Booting . Booting libraries/base/ Booting libraries/directory/ Booting libraries/integer-gmp/ Booting libraries/process/ Booting libraries/terminfo/ Booting libraries/time/ Booting libraries/unix/ checking for gfind... no checking for find... /usr/bin/find checking for sort... /usr/bin/sort checking for GHC version date... inferred 8.3.20171004 checking for GHC Git commit id... inferred 3030eee24c9d538f7ae2c854fd86129563b6ddf3 checking for ghc... /c/fp/ghc-8.0.2/bin/ghc checking version of ghc... 8.0.2 GHC path canonicalised to: c:/fp/ghc-8.0.2/bin/ghc checking build system type... x86_64-pc-msys checking host system type... x86_64-pc-msys checking target system type... x86_64-pc-msys Build platform inferred as: x86_64-unknown-mingw32 Host platform inferred as: x86_64-unknown-mingw32 Target platform inferred as: x86_64-unknown-mingw32 Unknown OS msys /c/code/HEAD$ git pull Already up-to-date. /c/code/HEAD$ git submodule update /c/code/HEAD$

3 3