- ghc-devs - Haskell.org

Use of forall as a sigil
by Bryan Richter 04 Dec '20

04 Dec '20

Dear forall ghc-devs. ghc-devs, As I read through the "Visible 'forall' in types of terms" proposal[1], I stumbled over something that isn't relevant to the proposal itself, so I thought I would bring it here. Given f :: forall a. a -> a (1) I intuitively understand the 'forall' in (1) to represent the phrase "for all". I would read (1) as "For all objects a in Hask, f is some relation from a to a." After reading the proposal, I think my intuition may be wrong, since I discovered `forall a ->`. This means something similar to, but practically different from, `forall a.`. Thus it seems like 'forall' is now simply used as a sigil to represent "here is where some special parameter goes". It could as well be an emoji. What's more, the practical difference between the two forms is *only* distinguished by ` ->` versus `.`. That's putting quite a lot of meaning into a rather small number of pixels, and further reduces any original connection to meaning that 'forall' might have had. I won't object to #281 based only on existing syntax, but I *do* object to the existing syntax. :) Is this a hopeless situation, or is there any possibility of bringing back meaning to the syntax of "dependent quantifiers"? -Bryan [1]: https://github.com/ghc-proposals/ghc-proposals/pull/281

9 17

PSA: type checker plugins to be affected by upcoming changes to GHC
by Richard Eisenberg 01 Dec '20

01 Dec '20

Hi all, I'm hard at work on two significant refactorings within GHC's constraint solver. The first is at https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4149. It removes flattening meta-variables and flattening skolems. This is a very nice simplification. Instead, it just reduces type families directly. My other patch (held up by the first) is at https://gitlab.haskell.org/ghc/ghc/-/tree/wip/derived-refactor and will remove Derived constraints, to be replaced by a little bit of cleverness in suppressing certain confusing error messages. My guess is that either or both of these will invalidate the current behavior of type-checker plugins. Sadly, this is not just a case of finding a new function that replicates the old behavior -- enough is changing under the hood that you might actually have to rewrite chunks of your code. I have never written a type-checker plugin, and so I don't currently have advice for you. But if you are a plugin author affected by this change and want help, please reach out -- I would be happy to walk you through the changes, and then hopefully make a little video explaining the process to other plugin authors. Neither patch will make it for 9.0, but I expect both to be in 9.2. There may be more where this came from (https://gitlab.haskell.org/ghc/ghc/-/issues/18965) in the future, but it's all for a good cause. (I have bcc'd plugin authors that I'm aware of. Just adding this in case you're surprised at receiving this email.) Thanks, Richard

5 11

Hadrian: Error "cannot find -lHSrts-1.0_thr_l" when linking ghc executable.
by Roland Senn 25 Nov '20

25 Nov '20

Hi there! I have two GHC trees. One is called ghcdebug and is a little bit outdated (16. September 2020). In this tree, I can work normally: Change code, compile and run the resulting GHC compiler. The second tree is up-to-date! Compiling works fine, however the linker steps for the ghc executable fails. When I restart the failing link step, I get the following error: $ hadrian/build --flavour=devel2 --freeze1 -j2 stage2:exe:ghc-bin Up to date | Run Ghc LinkHs Stage1: _build/stage1/ghc/build/c/hschooks.o (and 7 more) => _build/stage1/bin/ghc /usr/bin/ld.gold: error: cannot find -lHSrts-1.0_thr_l _build/stage1/ghc/build/GHCi/Leak.o(.text+0xd5): error: undefined reference to 'stg_upd_frame_info' _build/stage1/ghc/build/GHCi/Leak.o(.text+0x1c2): error: undefined reference to 'stg_upd_frame_info' _build/stage1/ghc/build/GHCi/Leak.o(.text+0x1e6): error: undefined reference to 'stg_ap_ppp_info' ... and many many more lines with "error: undefined reference to ..." I get the same error when I use a freshly cloned ghc tree. I also get the error independently of the GHC version used to compile (8.8.3 or 8.10.2). I didn't modify any settings files. I do: hadrian/build clean hadrian/build --flavour=devel2 -j2 I'm using a normal x68_64 box with plain vanilla Linux Debian 10. No Docker and no Nix. The directory _build/stage/rts/build contains: roland@goms:~/Projekte/ghc$ ls -all _build/stage1/rts/build/ insgesamt 19396 drwxr-xr-x 5 roland roland 4096 Nov 24 17:58 . drwxr-xr-x 3 roland roland 4096 Nov 24 17:56 .. drwxr-xr-x 2 roland roland 4096 Nov 24 17:56 autogen drwxr-xr-x 7 roland roland 12288 Nov 24 17:58 c drwxr-xr-x 2 roland roland 4096 Nov 24 17:58 cmm -rw-r--r-- 1 roland roland 31349 Nov 24 17:58 DerivedConstants.h -rw-r--r-- 1 roland roland 13764 Nov 24 17:57 ffi.h -rw-r--r-- 1 roland roland 4343 Nov 24 17:57 ffitarget.h -rw-r--r-- 1 roland roland 15128 Nov 24 17:58 ghcautoconf.h -rw-r--r-- 1 roland roland 618 Nov 24 17:58 ghcplatform.h -rw-r--r-- 1 roland roland 732 Nov 24 17:58 ghcversion.h -rw-r--r-- 1 roland roland 82486 Nov 24 17:57 libCffi.a lrwxrwxrwx 1 roland roland 9 Nov 24 17:57 libCffi_thr.a -> libCffi.a -rw-r--r-- 1 roland roland 9166966 Nov 24 17:58 libHSrts-1.0.a -rw-r--r-- 1 roland roland 10490730 Nov 24 17:58 libHSrts-1.0_thr.a Any ideas what's wrong or how to fix? Many thanks and Cheers, Roland

2 3

Questions about System F and data types
by Jan van Brügge 25 Nov '20

25 Nov '20

Hi, I know that this is probably not the correct place to ask as my question is not directly related to GHC itself, but I thought here are the people that can most likely answer this. To better understand PL papers, especially those involving System Fc and its extensions, I started to write a formal proof of type safety including alpha-equivalence. Currently I have a complete proof for System F <https://github.com/jvanbruegge/isabelle-lambda-calculus> (without coercions and data types yet). I mainly used the System Fc paper <https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-…> as reference, ignoring all the parts about coercions. 1. In the Fc paper, the rule `AppT` has a judgement delta as assumption, which does not exist. I assumed the `ty` judgement was meant there by looking at the arguments. Is this correct? 2. In the `Abs` rule, the type of the variable is required to be valid and of kind star by the judgement `ty`. In the `Let` rule, this assumption is missing. I tried it like that, but was not able to complete the proofs. Is such an assumption missing there or should I be able to proof it without? 3. In the Fc paper, the types and kinds of datatype declarations are added to the context with a separate judgement that interprets the datatype declarations. In the System Fc pro paper <https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/p53-yor…> (from what I can tell) those types and kinds are assumed to be already part of the initial context. At the moment I prove progress against the empty context, so I guess I would have to relax that to an initial context that only contains types and kinds of type constants and nothing else. Is that correct? What is here the "best practice" in terms of PL research? Thank you all Jan

2 2

HEAD user manual
by Simon Peyton Jones 25 Nov '20

25 Nov '20

Where can I find the GHC user manual for HEAD these days? I tried https://ghc.gitlab.haskell.org/ghc/doc/, but that takes me to 8.11. The user documentation page https://gitlab.haskell.org/ghc/ghc/-/wikis/ghc-users-guide#ghc-users-docume… has the same link. Thanks Simon

2 1

Adding a way to reduce type families in type errors
by Jakob Brünker 23 Nov '20

23 Nov '20

Hi all, While there is a way to expand type synonyms in type errors (-fprint-expanded-synonyms), as far as I know, the same doesn't exist for type families. For example, the following type family Foo a where Foo Int = String type family Bar a :: Maybe (Foo Int) where Bar a = '() results in the error Expected kind `Maybe (Foo Int)', but '() has kind `()' where I'd like to see "Expected kind `Maybe String'". I'd be interested in trying my hand at implementing a way to see this, either by adding it to -fprint-expanded-synonyms, or as a new flag. Three questions: - Is there already a way to do this that I'm missing? - Are there reasons for why this would be a bad idea? - Would a proposal be necessary for this? Thanks, Jakob

2 2

Re: Use of forall as a sigil
by Andrey Mokhov 23 Nov '20

23 Nov '20

Hi Richard, > In the end, I've never loved the forall ... -> syntax, but I've never seen > anything better. What about the forall @a. syntax? For example: sizeOf :: forall @a. Sized a => Int We already use @ to explicitly specify types, so it seems natural mark type parameters that must be explicitly specified with @ too. Here's how one would read it: "for all explicitly specified a, ..." Apologies if this has been discussed and I missed it. It doesn't seem to be mentioned in the Alternatives section of the proposal but perhaps it will just never work for some reason. Cheers, Andrey

3 3

Correct way of extending the context of the typechecker
by Yiyun Liu 20 Nov '20

20 Nov '20

Hi ghc-devs, Recently we've been trying to merge the typeclass branch of Liquid Haskell into the develop branch (link to the PR: https://github.com/ucsd-progsys/liquidhaskell/pull/1778) Since we want GHC to typecheck the refinements, we had to add some predefined logic symbols such as ==> to the global environment of GHC. In our branch, we use execStmt to add those extra symbols to the interactive context. This is no longer possible after LH becomes available as a GHC plugin because the plugin lives in TcRn. It seems that the only way is to directly interact with the typechecker and explicitly add the extra symbols to the context. It is not obvious to me how that can be done without accidentally breaking the invariants of the compiler. I wonder if there are examples or certain files that I can look into to learn how to interact with the typechecker? Adding the extra symbols is probably not that difficult, but I'd also want to acquire some general knowledge of how the typechecker works to further the integration between LH and GHC so we can remove some of the hacks on our end. Thanks, -Yiyun

2 1

Question about HsWrapper for constructors
by Kai-Oliver Prott 19 Nov '20

19 Nov '20

Hi all, I've tried a development snapshot of GHC's master branch from the beginning of this month and I am curious about the reason for a specific change. I noticed that a simple program like idNil :: [a] -> [a] idNil [] = [] is internally represented (after type checking) as: AbsBinds [] [] {Exports: [idNil <= idNil2] Exported types: idNil :: forall a. [a] -> [a] Binds: idNil2 [] = (/\(@a2). [] @a2) @a Can someone point me to a reason why the right side of idNil2 is not represented as [] @ a, like it was in GHC 8.10.1? I have not tried it with GHC 9.0. It is interesting to have a type lambda that is immediately followed by a type application. Thanks, Kai

2 1

Searching on GitLab
by Richard Eisenberg 08 Nov '20

08 Nov '20

Hi all, Some time ago, I set up a keyword bookmark (https://www-archive.mozilla.org/docs/end-user/keywords.html <https://www-archive.mozilla.org/docs/end-user/keywords.html>) to search in tickets and MRs, by using a Google "site:gitlab.haskell.org/ghc/ghc/issues/ <http://gitlab.haskell.org/ghc/ghc/issues/> %s" query. About a year ago, I noticed that the quality of results decreased to the point of uselessness, and I started to use GitLab's built-in search. This works fine, but it's not as good as Google's. Today, I discovered why the quality went down: GitLab changed its URLs. Previously, a ticket lived at e.g. gitlab.haskell.org/ghc/ghc/issues/1234 <http://gitlab.haskell.org/ghc/ghc/issues/1234>. Today, it lives at gitlab.haskell.org/ghc/ghc/-/issues/1234 <http://gitlab.haskell.org/ghc/ghc/-/issues/1234>. GitLab automatically redirects from the former to the latter, so old links/bookmarks still work great. But Google's search doesn't! The solution was easy: just update my keyword bookmarks to include the extra /-. Better search results, cooked up fresh. Perhaps you want some, too -- hence this email. Enjoy, Richard

1 0